From 650770148d218b0f45b16ab8b2fa455ef23cf65a Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 8 Jan 2015 20:31:39 +0100 Subject: [PATCH] Main now compiles again, yay. Former-commit-id: cc1307aea8c9c1fcd9f544eafba551ed6342b726 --- src/adapters/ExplicitModelAdapter.h | 18 +++++++++- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 36 +++++++------------ src/storage/expressions/ExpressionManager.cpp | 16 +++++++-- src/storage/expressions/ExpressionManager.h | 5 +++ src/storage/expressions/SimpleValuation.cpp | 26 ++++++++++++++ src/storage/expressions/SimpleValuation.h | 5 +++ src/storage/prism/Constant.cpp | 2 +- 8 files changed, 82 insertions(+), 28 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 6899f87c0..b0bb7d864 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/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; } @@ -478,6 +478,22 @@ namespace storm { // Initialize a queue and insert the initial state. std::queue 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 addIndexPair = getOrAddStateIndex(initialState, stateInformation); stateInformation.initialStateIndices.push_back(addIndexPair.second); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 9be7e4333..9c5d25808 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -194,7 +194,7 @@ namespace storm { std::unordered_map> resultingMap; for (auto state : stateInformation.relevantStates) { - resultingMap.emplace(state, std::list()); + resultingMap.emplace(state, std::list()); std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { variableNameBuffer.str(""); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 891d73ad2..f0f18b26c 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/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 getUsedLabelSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { boost::container::flat_set 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 const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::Mdp const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set 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 formulae; + std::vector formulae; boost::container::flat_set 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 const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::Mdp const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set 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 formulae; + std::vector formulae; boost::container::flat_set 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; diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index aa7ffc6f8..6738a0502 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/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 { @@ -269,6 +269,18 @@ namespace storm { std::shared_ptr ExpressionManager::getSharedPointer() const { 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 \ No newline at end of file diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index a2461ff02..c0bda2a5c 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -6,6 +6,7 @@ #include #include #include +#include #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" @@ -320,6 +321,8 @@ namespace storm { */ std::shared_ptr 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); } } diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index b634b68c3..f7b4eff52 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/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>()(valuation->booleanValues); boost::hash_combine(seed, valuation->integerValues); diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index a10f5a927..dda66754d 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -3,6 +3,7 @@ #include #include +#include #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 booleanValues; @@ -60,6 +63,8 @@ namespace storm { std::vector 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. diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 1e3d8d1d8..8f95d9e55 100644 --- a/src/storage/prism/Constant.cpp +++ b/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();