added correct insertion of probabilities into BDD and reachability analysis

Former-commit-id: 51e91d4d64

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -274,6 +274,16 @@ namespace storm {
                 return cachedDd;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType> AbstractCommand<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
+                storm::dd::Add<DdType> result = ddInformation.manager->getAddZero();
+                for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
+                    result += ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex).toAdd() * ddInformation.manager->getConstant(command.get().getUpdate(updateIndex).getLikelihoodExpression().evaluateAsDouble());
+                }
+                result *= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()).toAdd();
+                return result;
+            }
+            
             template class AbstractCommand<storm::dd::DdType::CUDD, double>;
         }
     }

src/storage/prism/menu_games/AbstractCommand.h

@@ -54,6 +54,13 @@ namespace storm {
                  */
                 std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> getAbstractBdd();
                 
+                /*!
+                 * Retrieves an ADD that maps the encoding of the command and its updates to their probabilities.
+                 *
+                 * @return The command-update probability ADD.
+                 */
+                storm::dd::Add<DdType> getCommandUpdateProbabilitiesAdd() const;
+                
             private:
                 /*!
                  * Determines the relevant predicates for source as well as successor states wrt. to the given assignments

src/storage/prism/menu_games/AbstractModule.cpp

@@ -47,6 +47,15 @@ namespace storm {
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType> AbstractModule<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
+                storm::dd::Add<DdType> result = ddInformation.manager->getAddZero();
+                for (auto const& command : commands) {
+                    result += command.getCommandUpdateProbabilitiesAdd();
+                }
+                return result;
+            }
+            
             template class AbstractModule<storm::dd::DdType::CUDD, double>;
         }
     }

src/storage/prism/menu_games/AbstractModule.h

@@ -47,6 +47,13 @@ namespace storm {
                  */
                 storm::dd::Bdd<DdType> getAbstractBdd();
                 
+                /*!
+                 * Retrieves an ADD that maps the encodings of commands and their updates to their probabilities.
+                 *
+                 * @return The command-update probability ADD.
+                 */
+                storm::dd::Add<DdType> getCommandUpdateProbabilitiesAdd() const;
+                
             private:
                 // A factory that can be used to create new SMT solvers.
                 storm::utility::solver::SmtSolverFactory const& smtSolverFactory;

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -58,15 +58,28 @@ namespace storm {
                 for (auto const& module : program.getModules()) {
                     modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory);
                 }
+                
+                // Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
+                commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Add<DdType> AbstractProgram<DdType, ValueType>::getAbstractAdd() {
                 // As long as there is only one module, we build its game representation and return it.
+                return modules.front().getAbstractBdd().toAdd() * commandUpdateProbabilitiesAdd;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation) {
+                storm::dd::Bdd<storm::dd::DdType::CUDD> frontier = initialStates;
+
+                storm::dd::Bdd<storm::dd::DdType::CUDD> reachableStates = initialStates;
+                while (!frontier.isZero()) {
+                    frontier = frontier.andExists(transitionRelation, ddInformation.successorVariables);
+                    reachableStates |= frontier;
+                }
                 
-                
-                // FIXME: multiply with probabilities for updates.
-                return modules.front().getAbstractBdd().toAdd();
+                return reachableStates;
             }
             
             // Explicitly instantiate the class.

src/storage/prism/menu_games/AbstractProgram.h

@@ -44,6 +44,16 @@ namespace storm {
                 storm::dd::Add<DdType> getAbstractAdd();
                 
             private:
+                /*!
+                 * Computes the reachable states of the transition relation.
+                 *
+                 * @param initialStates The BDD representing the initial states of the model.
+                 * @param transitionRelation The BDD representing the transition relation that does only contain state
+                 * and successor variables.
+                 * @return The BDD representing the reachable states.
+                 */
+                storm::dd::Bdd<DdType> getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation);
+                
                 // A factory that can be used to create new SMT solvers.
                 std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 
@@ -58,6 +68,9 @@ namespace storm {
                 
                 // The concrete program this abstract program refers to.
                 std::reference_wrapper<Program const> program;
+                
+                // An ADD characterizing the probabilities of commands and their updates.
+                storm::dd::Add<DdType> commandUpdateProbabilitiesAdd;
             };
         }
     }

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -39,6 +39,8 @@ namespace storm {
                 predicateDdVariables.push_back(newMetaVariable);
                 predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
                 predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd());
+                sourceVariables.insert(newMetaVariable.first);
+                successorVariables.insert(newMetaVariable.second);
             }
          
             template <storm::dd::DdType DdType, typename ValueType>

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -3,6 +3,7 @@
 
 #include <memory>
 #include <vector>
+#include <set>
 
 #include "src/storage/dd/DdType.h"
 #include "src/storage/expressions/Variable.h"
@@ -64,6 +65,12 @@ namespace storm {
                 
                 // The DD variables corresponding to the predicates.
                 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;
+                
+                // The set of all source variables.
+                std::set<storm::expressions::Variable> sourceVariables;
+
+                // The set of all source variables.
+                std::set<storm::expressions::Variable> successorVariables;
 
                 // The BDDs corresponding to the predicates.
                 std::vector<std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>>> predicateBdds;