Main now compiles again, yay.

Former-commit-id: cc1307aea8

src/adapters/ExplicitModelAdapter.h

@@ -174,7 +174,6 @@ namespace storm {
             static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::prism::Update const& update) {
                 StateType* newState = new StateType(*state);
                 
-                // This variable needs to be declared prior to the switch, because of C++ rules.
                 int_fast64_t newValue = 0;
                 for (auto const& assignment : update.getAssignments()) {
                     if (assignment.getExpression().hasBooleanType()) {
@@ -188,6 +187,7 @@ namespace storm {
                         STORM_LOG_ASSERT(false, "Invalid type '" << assignment.getExpression().getType() << "' of assignment.");
                     }
                 }
+                
                 return newState;
             }
                                     
@@ -479,6 +479,22 @@ namespace storm {
                 std::queue<uint_fast64_t> stateQueue;
                 StateType* initialState = new StateType(program.getManager().getSharedPointer());
                 
+                // We need to initialize the values of the variables to their initial value.
+                for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
+                    initialState->setBooleanValue(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool());
+                }
+                for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
+                    initialState->setIntegerValue(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt());
+                }
+                for (auto const& module : program.getModules()) {
+                    for (auto const& booleanVariable : module.getBooleanVariables()) {
+                        initialState->setBooleanValue(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool());
+                    }
+                    for (auto const& integerVariable : module.getIntegerVariables()) {
+                        initialState->setIntegerValue(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt());
+                    }
+                }
+        
                 std::pair<bool, uint_fast64_t> addIndexPair = getOrAddStateIndex(initialState, stateInformation);
                 stateInformation.initialStateIndices.push_back(addIndexPair.second);
                 stateQueue.push(stateInformation.stateToIndexMap[initialState]);

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -194,7 +194,7 @@ namespace storm {
                 std::unordered_map<uint_fast64_t, std::list<storm::expressions::Variable>> resultingMap;
                 
                 for (auto state : stateInformation.relevantStates) {
-                    resultingMap.emplace(state, std::list<std::string>());
+                    resultingMap.emplace(state, std::list<storm::expressions::Variable>());
                     std::list<uint_fast64_t> const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state);
                     for (uint_fast64_t row : relevantChoicesForState) {
                         variableNameBuffer.str("");

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -977,7 +977,7 @@ namespace storm {
                     solver.add(labelExpression);
 
                     // Assert constraint for (2).
-                    storm::expressions::Expression orderExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second) || variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(sourceState)) < variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(targetState));
+                    storm::expressions::Expression orderExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second) || variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(sourceState)).getExpression() < variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(targetState)).getExpression();
                     solver.add(orderExpression);
                 }
             }
@@ -1286,17 +1286,10 @@ namespace storm {
             static boost::container::flat_set<uint_fast64_t> getUsedLabelSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) {
                 boost::container::flat_set<uint_fast64_t> result;
                 for (auto const& labelIndexPair : variableInformation.labelToIndexMap) {
-                    z3::expr auxValue = model.eval(variableInformation.labelVariables.at(labelIndexPair.second));
+                    bool commandIncluded = model.getBooleanValue(variableInformation.labelVariables.at(labelIndexPair.second));
                     
-                    // Check whether the auxiliary variable was set or not.
-                    if (eq(auxValue, context.bool_val(true))) {
+                    if (commandIncluded) {
                         result.insert(labelIndexPair.first);
-                    } else if (eq(auxValue, context.bool_val(false))) {
-                        // Nothing to do in this case.
-                    } else if (eq(auxValue, variableInformation.labelVariables.at(labelIndexPair.second))) {
-                        // If the auxiliary variable is a don't care, then we don't take the corresponding command.
-                    } else {
-                        throw storm::exceptions::InvalidStateException() << "Could not retrieve value of boolean variable from illegal value.";
                     }
                 }
                 return result;
@@ -1340,7 +1333,7 @@ namespace storm {
 
                 // As long as the constraints are unsatisfiable, we need to relax the last at-most-k constraint and
                 // try with an increased bound.
-                while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::) {
+                while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::Unsat) {
                     LOG4CPLUS_DEBUG(logger, "Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound.");
                     solver.add(variableInformation.auxiliaryVariables.back());
                     variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound));
@@ -1355,7 +1348,6 @@ namespace storm {
             /*!
              * Analyzes the given sub-MDP that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable.
              *
-             * @param context The Z3 context in which to build the expressions.
              * @param solver The solver to use for the satisfiability evaluation.
              * @param subMdp The sub-MDP resulting from restricting the original MDP to the given command set.
              * @param originalMdp The original MDP.
@@ -1364,7 +1356,7 @@ namespace storm {
              * @param commandSet The currently chosen set of commands.
              * @param variableInformation A structure with information about the variables of the solver.
              */
-            static void analyzeZeroProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
+            static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
                 storm::storage::BitVector reachableStates(subMdp.getNumberOfStates());
                 
                 LOG4CPLUS_DEBUG(logger, "Analyzing solution with zero probability.");
@@ -1459,14 +1451,14 @@ namespace storm {
                 }
                 
                 // Given the results of the previous analysis, we construct the implications.
-                std::vector<z3::expr> formulae;
+                std::vector<storm::expressions::Expression> formulae;
                 boost::container::flat_set<uint_fast64_t> unknownReachableLabels;
                 std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end()));
                 for (auto label : unknownReachableLabels) {
                     formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
                 }
                 for (auto const& cutLabelSet : cutLabels) {
-                    z3::expr cube = context.bool_val(true);
+                    storm::expressions::Expression cube = variableInformation.manager->boolean(true);
                     for (auto cutLabel : cutLabelSet) {
                         cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel));
                     }
@@ -1476,14 +1468,12 @@ namespace storm {
                 
                 LOG4CPLUS_DEBUG(logger, "Asserting reachability implications.");
                 assertDisjunction(solver, formulae, *variableInformation.manager);
-                
             }
             
             /*!
              * Analyzes the given sub-MDP that has a non-zero maximal reachability and tries to construct assertions that aim to guide the solver to solutions
              * with an improved probability value.
              *
-             * @param context The Z3 context in which to build the expressions.
              * @param solver The solver to use for the satisfiability evaluation.
              * @param subMdp The sub-MDP resulting from restricting the original MDP to the given command set.
              * @param originalMdp The original MDP.
@@ -1492,7 +1482,7 @@ namespace storm {
              * @param commandSet The currently chosen set of commands.
              * @param variableInformation A structure with information about the variables of the solver.
              */
-            static void analyzeInsufficientProbabilitySolution(z3::context& context, z3::solver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
+            static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::Mdp<T> const& subMdp, storm::models::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
 
                 LOG4CPLUS_DEBUG(logger, "Analyzing solution with insufficient probability.");
 
@@ -1569,14 +1559,14 @@ namespace storm {
                 }
                 
                 // Given the results of the previous analysis, we construct the implications
-                std::vector<z3::expr> formulae;
+                std::vector<storm::expressions::Expression> formulae;
                 boost::container::flat_set<uint_fast64_t> unknownReachableLabels;
                 std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end()));
                 for (auto label : unknownReachableLabels) {
                     formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
                 }
                 for (auto const& cutLabelSet : cutLabels) {
-                    z3::expr cube = context.bool_val(true);
+                    storm::expressions::Expression cube = variableInformation.manager->boolean(true);
                     for (auto cutLabel : cutLabelSet) {
                         cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel));
                     }
@@ -1694,7 +1684,7 @@ namespace storm {
                 do {
                     LOG4CPLUS_DEBUG(logger, "Computing minimal command set.");
                     solverClock = std::chrono::high_resolution_clock::now();
-                    commandSet = findSmallestCommandSet(solver, variableInformation, currentBound);
+                    commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound);
                     totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock;
                     LOG4CPLUS_DEBUG(logger, "Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << ".");
                     
@@ -1721,11 +1711,11 @@ namespace storm {
                             ++zeroProbabilityCount;
                             
                             // If there was no target state reachable, analyze the solution and guide the solver into the right direction.
-                            analyzeZeroProbabilitySolution(context, solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation);
+                            analyzeZeroProbabilitySolution(*solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation);
                         } else {
                             // If the reachability probability was greater than zero (i.e. there is a reachable target state), but the probability was insufficient to exceed
                             // the given threshold, we analyze the solution and try to guide the solver into the right direction.
-                            analyzeInsufficientProbabilitySolution(context, solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation);
+                            analyzeInsufficientProbabilitySolution(*solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation);
                         }
                     } else {
                         done = true;

src/storage/expressions/ExpressionManager.cpp

@@ -255,7 +255,7 @@ namespace storm {
         }
         
         ExpressionManager::const_iterator ExpressionManager::begin() const {
-            return ExpressionManager::const_iterator(*this, this->nameToIndexMapping.end(), this->nameToIndexMapping.begin(), const_iterator::VariableSelection::OnlyRegularVariables);
+            return ExpressionManager::const_iterator(*this, this->nameToIndexMapping.begin(), this->nameToIndexMapping.end(), const_iterator::VariableSelection::OnlyRegularVariables);
         }
         
         ExpressionManager::const_iterator ExpressionManager::end() const {
@@ -270,5 +270,17 @@ namespace storm {
             return this->shared_from_this();
         }
         
+        std::ostream& operator<<(std::ostream& out, ExpressionManager const& manager) {
+            out << "manager {" << std::endl;
+            
+            for (auto const& variableTypePair : manager) {
+                std::cout << "\t" << variableTypePair.second << " " << variableTypePair.first.getName() << " [offset " << variableTypePair.first.getOffset() << "]" << std::endl;
+            }
+            
+            out << "}" << std::endl;
+            
+            return out;
+        }
+        
     } // namespace expressions
 } // namespace storm

src/storage/expressions/ExpressionManager.h

@@ -6,6 +6,7 @@
 #include <vector>
 #include <unordered_map>
 #include <unordered_set>
+#include <iostream>
 
 #include "src/storage/expressions/Variable.h"
 #include "src/storage/expressions/Expression.h"
@@ -320,6 +321,8 @@ namespace storm {
              */
             std::shared_ptr<ExpressionManager const> getSharedPointer() const;
 
+            friend std::ostream& operator<<(std::ostream& out, ExpressionManager const& manager);
+            
         private:
             /*!
              * Checks whether the given variable name is valid.
@@ -404,6 +407,8 @@ namespace storm {
             // A mask that can be used to project a variable index to its offset (with the group of equally typed variables).
             static const uint64_t offsetMask = (1ull << 50) - 1;
         };
+        
+        std::ostream& operator<<(std::ostream& out, ExpressionManager const& manager);
     }
 }
 

src/storage/expressions/SimpleValuation.cpp

@@ -87,6 +87,32 @@ namespace storm {
             rationalValues[rationalVariable.getOffset()] = value;
         }
         
+        std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) {
+            out << "valuation {" << std::endl;
+            out << valuation.getManager() << std::endl;
+            if (!valuation.booleanValues.empty()) {
+                for (auto const& element : valuation.booleanValues) {
+                    out << element << " ";
+                }
+                out << std::endl;
+            }
+            if (!valuation.integerValues.empty()) {
+                for (auto const& element : valuation.integerValues) {
+                    out << element << " ";
+                }
+                out << std::endl;
+            }
+            if (!valuation.rationalValues.empty()) {
+                for (auto const& element : valuation.rationalValues) {
+                    out << element << " ";
+                }
+                out << std::endl;
+            }
+            out << "}" << std::endl;
+            
+            return out;
+        }
+        
         std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* valuation) const {
             size_t seed = std::hash<std::vector<bool>>()(valuation->booleanValues);
             boost::hash_combine(seed, valuation->integerValues);

src/storage/expressions/SimpleValuation.h

@@ -3,6 +3,7 @@
 
 #include <cstdint>
 #include <vector>
+#include <iostream>
 
 #include "src/storage/expressions/Valuation.h"
 
@@ -53,6 +54,8 @@ namespace storm {
             virtual double getRationalValue(Variable const& rationalVariable) const override;
             virtual void setRationalValue(Variable const& rationalVariable, double value) override;
             
+            friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation);
+            
         private:
             // Containers that store the values of the variables of the appropriate type.
             std::vector<bool> booleanValues;
@@ -60,6 +63,8 @@ namespace storm {
             std::vector<double> rationalValues;
         };
         
+        std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation);
+        
         /*!
          * A helper class that can pe used as the hash functor for data structures that need to hash valuations given
          * via pointers.

src/storage/prism/Constant.cpp

@@ -38,7 +38,7 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
-            stream << "const " << constant.getExpressionVariable().getType();
+            stream << "const " << constant.getExpressionVariable().getType() << " ";
             stream << constant.getName();
             if (constant.isDefined()) {
                 stream << " = " << constant.getExpression();