From 87843e084eb0b220acebd4fb9766ad2c7467a616 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 May 2018 15:53:35 +0200 Subject: [PATCH] several fixes related to game-based abstraction --- src/storm/abstraction/MenuGameRefiner.cpp | 17 +++++--- src/storm/abstraction/StateSetAbstractor.cpp | 2 +- .../abstraction/ValidBlockAbstractor.cpp | 10 +++-- src/storm/abstraction/ValidBlockAbstractor.h | 2 + .../jani/JaniMenuGameAbstractor.cpp | 4 ++ .../abstraction/prism/ModuleAbstractor.cpp | 5 ++- .../prism/PrismMenuGameAbstractor.cpp | 4 ++ src/storm/adapters/MathsatExpressionAdapter.h | 42 ++++++++++++++++++- .../abstraction/GameBasedMdpModelChecker.cpp | 7 ++-- src/storm/solver/MathsatSmtSolver.cpp | 8 +++- .../expressions/EquivalenceChecker.cpp | 1 + src/storm/storage/jani/Automaton.cpp | 21 ++++++++++ src/storm/storage/jani/Automaton.h | 6 +++ src/storm/storage/jani/Model.cpp | 15 +++++++ src/storm/storage/jani/Model.h | 6 +++ src/storm/storage/prism/InitialConstruct.cpp | 4 +- src/storm/storage/prism/Program.cpp | 1 + src/storm/utility/constants.h | 2 + 18 files changed, 139 insertions(+), 18 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index a821dc8e5..b75a6380a 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -1362,18 +1362,21 @@ namespace storm { } // Now clean the classes in the sense that redundant predicates are cleaned. + uint64_t checkCounter = 0; for (auto& predicateClass : predicateClasses) { std::vector cleanedAtomsOfClass; for (auto const& predicate : predicateClass.second) { bool addPredicate = true; for (auto const& atom : cleanedAtomsOfClass) { + ++checkCounter; if (predicate.areSame(atom)) { addPredicate = false; break; } - if (addPredicate && equivalenceChecker.areEquivalentModuloNegation(predicate, atom)) { + ++checkCounter; + if (equivalenceChecker.areEquivalentModuloNegation(predicate, atom)) { addPredicate = false; break; } @@ -1397,19 +1400,21 @@ namespace storm { auto oldPredicateClassIt = oldPredicateClasses.find(predicateClass.first); if (oldPredicateClassIt != oldPredicateClasses.end()) { for (auto const& newAtom : predicateClass.second) { + bool addAtom = true; for (auto const& oldPredicate : oldPredicateClassIt->second) { - bool addAtom = true; + ++checkCounter; if (newAtom.areSame(oldPredicate)) { addAtom = false; break; } + ++checkCounter; if (equivalenceChecker.areEquivalentModuloNegation(newAtom, oldPredicate)) { addAtom = false; break; } - if (addAtom) { - cleanedAtoms.push_back(newAtom); - } + } + if (addAtom) { + cleanedAtoms.push_back(newAtom); } } } else { @@ -1417,7 +1422,7 @@ namespace storm { } } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Preprocessing predicates took " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_TRACE("Preprocessing predicates took " << std::chrono::duration_cast(end - start).count() << "ms (" << checkCounter << " checks)."); return cleanedAtoms; } else { diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp index 48e2042a9..86a3b8412 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm/abstraction/StateSetAbstractor.cpp @@ -23,8 +23,8 @@ namespace storm { // Extract the variables of the predicate, so we know which variables were used when abstracting. std::set usedVariables = predicate.getVariables(); concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end()); - localExpressionInformation.relate(usedVariables); } + localExpressionInformation.relate(concretePredicateVariables); } template diff --git a/src/storm/abstraction/ValidBlockAbstractor.cpp b/src/storm/abstraction/ValidBlockAbstractor.cpp index dcfdcf20c..16364b156 100644 --- a/src/storm/abstraction/ValidBlockAbstractor.cpp +++ b/src/storm/abstraction/ValidBlockAbstractor.cpp @@ -34,6 +34,13 @@ namespace storm { return validBlocks; } + template + void ValidBlockAbstractor::constrain(storm::expressions::Expression const& constraint) { + for (uint64_t i = 0; i < smtSolvers.size(); ++i) { + smtSolvers[i]->add(constraint); + } + } + template void ValidBlockAbstractor::refine(std::vector const& predicates) { for (auto const& predicate : predicates) { @@ -114,13 +121,10 @@ namespace storm { template storm::dd::Bdd ValidBlockAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); -// std::cout << "new model ----------------" << std::endl; for (auto const& variableIndexPair : relevantVariablesAndPredicates[blockIndex]) { if (model.getBooleanValue(variableIndexPair.first)) { -// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is true" << std::endl; result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } else { -// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is false" << std::endl; result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } } diff --git a/src/storm/abstraction/ValidBlockAbstractor.h b/src/storm/abstraction/ValidBlockAbstractor.h index 6e0b28ab4..33f7fb590 100644 --- a/src/storm/abstraction/ValidBlockAbstractor.h +++ b/src/storm/abstraction/ValidBlockAbstractor.h @@ -33,6 +33,8 @@ namespace storm { void refine(std::vector const& predicates); + void constrain(storm::expressions::Expression const& constraint); + private: /*! * Checks which parts of the valid blocks need to be recomputed. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 35c61caeb..b32df498a 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -48,6 +48,7 @@ namespace storm { for (auto const& range : this->model.get().getAllRangeExpressions()) { abstractionInformation.addConstraint(range); initialStateAbstractor.constrain(range); + validBlockAbstractor.constrain(range); } uint_fast64_t totalNumberOfCommands = 0; @@ -181,6 +182,9 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates(); + if (!model.get().hasTrivialInitialStatesExpression()) { + initialStates &= validBlockAbstractor.getValidBlocks(); + } initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index 84c6d9523..e8dc2795e 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -26,8 +26,10 @@ namespace storm { ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. + uint64_t counter = 0; for (auto const& command : module.getCommands()) { commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition); + ++counter; } } @@ -83,7 +85,8 @@ namespace storm { BottomStateResult ModuleAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); - for (auto& command : commands) { + for (uint64_t index = 0; index < commands.size(); ++index) { + auto& command = commands[index]; BottomStateResult commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); result.states |= commandBottomStateResult.states; result.transitions |= commandBottomStateResult.transitions; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 3490c5a45..b9b6b8ab9 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -45,6 +45,7 @@ namespace storm { for (auto const& range : this->program.get().getAllRangeExpressions()) { abstractionInformation.addConstraint(range); initialStateAbstractor.constrain(range); + validBlockAbstractor.constrain(range); } uint_fast64_t totalNumberOfCommands = 0; @@ -174,6 +175,9 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); + if (program.get().hasInitialConstruct()) { + initialStates &= validBlockAbstractor.getValidBlocks(); + } initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index 0b111a10f..e99c7d0c5 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -58,11 +58,13 @@ namespace storm { * @return An equivalent term for MathSAT. */ msat_term translateExpression(storm::expressions::Expression const& expression) { + additionalConstraints.clear(); msat_term result = boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); if (MSAT_ERROR_TERM(result)) { std::string errorMessage(msat_last_error_message(env)); STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format. (Message: " << errorMessage << ")"); } + return result; } @@ -82,6 +84,17 @@ namespace storm { return msat_make_constant(env, variableExpressionPair->second); } + bool hasAdditionalConstraints() const { + return !additionalConstraints.empty(); + } + + /*! + * Retrieves additional constraints that were created because of encodings using auxiliary variables. + */ + std::vector const& getAdditionalConstraints() const { + return additionalConstraints; + } + /*! * Retrieves the variable that is associated with the given MathSAT variable declaration. * @@ -118,6 +131,12 @@ namespace storm { msat_term result = leftResult; int_fast64_t exponent; + int_fast64_t modulus; + storm::expressions::Variable freshAuxiliaryVariable; + msat_term modVariable; + msat_term lower; + msat_term upper; + typename storm::NumberTraits::IntegerType gmpModulus; switch (expression.getOperatorType()) { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: return msat_make_plus(env, leftResult, rightResult); @@ -141,6 +160,23 @@ namespace storm { } } return result; + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Modulo: + modulus = expression.getSecondOperand()->evaluateAsInt(); + STORM_LOG_THROW(modulus > 0, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression with negative modulus."); + + freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true); + modVariable = msat_make_constant(env, createVariable(freshAuxiliaryVariable)); + + gmpModulus = typename storm::NumberTraits::IntegerType(static_cast(modulus)); + + // Create the constraint that fixes the value of the fresh variable. + additionalConstraints.push_back(msat_make_int_modular_congruence(env, gmpModulus.get_mpz_t(), modVariable, leftResult)); + + // Create the constraint that limits the value of the modulo operation to 0 <= val <= modulus-1. + lower = msat_make_number(env, "-1"); + upper = msat_make_number(env, std::to_string(modulus - 1).c_str()); + additionalConstraints.push_back(msat_make_and(env, msat_make_not(env, msat_make_leq(env, modVariable, lower)), msat_make_leq(env, modVariable, upper))); + return modVariable; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast(expression.getOperatorType()) << "' in expression " << expression << "."); } @@ -313,11 +349,15 @@ namespace storm { // The MathSAT environment used. msat_env& env; + + // A vector of constraints that need to be kept separate, because they were only implicitly part of an + // assertion that was added. + std::vector additionalConstraints; // A mapping of variable names to their declaration in the MathSAT environment. std::unordered_map variableToDeclarationMapping; - // A mapping from MathSAT variable declaration to our variables. + // A mapping from MathSAT variable declarations to our variables. std::unordered_map declarationToVariableMapping; }; #endif diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 7657c0ceb..e6eab03dc 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -574,9 +574,10 @@ namespace storm { } // #ifdef LOCAL_DEBUG - // targetStates.template toAdd().exportToDot("target.dot"); - // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); - // game.getReachableStates().template toAdd().exportToDot("reach.dot"); +// initialStates.template toAdd().exportToDot("init.dot"); +// targetStates.template toAdd().exportToDot("target.dot"); +// abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); +// game.getReachableStates().template toAdd().exportToDot("reach.dot"); // #endif std::unique_ptr result; diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp index 9b6f7da2b..219efe530 100644 --- a/src/storm/solver/MathsatSmtSolver.cpp +++ b/src/storm/solver/MathsatSmtSolver.cpp @@ -139,7 +139,13 @@ namespace storm { void MathsatSmtSolver::add(storm::expressions::Expression const& e) { #ifdef STORM_HAVE_MSAT - msat_assert_formula(env, expressionAdapter->translateExpression(e)); + msat_term expression = expressionAdapter->translateExpression(e); + msat_assert_formula(env, expression); + if (expressionAdapter->hasAdditionalConstraints()) { + for (auto const& constraint : expressionAdapter->getAdditionalConstraints()) { + msat_assert_formula(env, constraint); + } + } #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif diff --git a/src/storm/storage/expressions/EquivalenceChecker.cpp b/src/storm/storage/expressions/EquivalenceChecker.cpp index 5d1ffad56..ba286dd63 100644 --- a/src/storm/storage/expressions/EquivalenceChecker.cpp +++ b/src/storm/storage/expressions/EquivalenceChecker.cpp @@ -39,6 +39,7 @@ namespace storm { this->smtSolver->push(); this->smtSolver->add(!storm::expressions::iff(first, !second)); equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat; + this->smtSolver->pop(); return equivalent; } diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 7d856e56c..88f5f0489 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -351,6 +351,27 @@ namespace storm { return result; } + bool Automaton::hasTrivialInitialStatesExpression() const { + if (this->hasInitialStatesRestriction()) { + return false; + } + + bool result = true; + for (auto const& variable : this->getVariables()) { + if (variable.isTransient()) { + continue; + } + + result &= variable.hasInitExpression(); + + if (!result) { + break; + } + } + + return result; + } + bool Automaton::hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const { return actionIndices.find(actionIndex) != actionIndices.end(); } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index c549ecca8..92c5374bb 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -252,6 +252,12 @@ namespace storm { */ storm::expressions::Expression getInitialStatesExpression() const; + /*! + * Retrieves whether the initial states expression is trivial in the sense that the automaton has no initial + * states restriction and all non-transient variables have initial values. + */ + bool hasTrivialInitialStatesExpression() const; + /*! * Retrieves whether there is an edge labeled with the action with the given index in this automaton. */ diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index a6491a884..8da333cb7 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -928,6 +928,21 @@ namespace storm { return getInitialStatesExpression(allAutomata); } + bool Model::hasTrivialInitialStatesExpression() const { + if (this->hasInitialStatesRestriction()) { + return false; + } + + bool result = true; + for (auto const& automaton : this->getAutomata()) { + result &= automaton.hasTrivialInitialStatesExpression(); + if (!result) { + break; + } + } + return result; + } + storm::expressions::Expression Model::getInitialStatesExpression(std::vector> const& automata) const { // Start with the restriction of variables. storm::expressions::Expression result = initialStatesRestriction; diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 2dc69d147..262ec1288 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -349,6 +349,12 @@ namespace storm { */ storm::expressions::Expression getInitialStatesExpression() const; + /*! + * Retrieves whether the initial states expression is trivial in the sense that no automaton has an initial + * states restriction and all variables have initial values. + */ + bool hasTrivialInitialStatesExpression() const; + /*! * Retrieves the expression defining the legal initial values of the variables. * diff --git a/src/storm/storage/prism/InitialConstruct.cpp b/src/storm/storage/prism/InitialConstruct.cpp index a2bce30e9..715b76752 100644 --- a/src/storm/storage/prism/InitialConstruct.cpp +++ b/src/storm/storage/prism/InitialConstruct.cpp @@ -16,9 +16,9 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct) { - stream << "initial " << std::endl; + stream << "init " << std::endl; stream << "\t" << initialConstruct.getInitialStatesExpression() << std::endl; - stream << "endinitial" << std::endl; + stream << "endinit" << std::endl; return stream; } } // namespace prism diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index cda98bc09..ad1713a9a 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1554,6 +1554,7 @@ namespace storm { // Finally, we can create the module and the program and return it. storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); + return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true); } diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index 360128f00..c74592575 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -16,6 +16,8 @@ #include #include +#include "storm/utility/NumberTraits.h" + namespace storm { // Forward-declare MatrixEntry class.