From b395b1292e9040bb31934d77472475e20606c850 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 8 Apr 2015 22:57:42 +0200 Subject: [PATCH] started Smtlib Solver interface and some 'prototypy' method to check parameter regions Former-commit-id: e3cf6528d915b59a2dff093c8178d070827133dc --- src/adapters/Smt2ExpressionAdapter.h | 165 ++++++++++ .../SparseDtmcEliminationModelChecker.cpp | 311 ++++++++++++++++++ .../SparseDtmcEliminationModelChecker.h | 24 ++ src/settings/modules/GeneralSettings.cpp | 5 + src/settings/modules/GeneralSettings.h | 8 + src/solver/Smt2SmtSolver.cpp | 136 ++++++++ src/solver/Smt2SmtSolver.h | 112 +++++++ src/utility/cli.h | 59 +++- 8 files changed, 806 insertions(+), 14 deletions(-) create mode 100644 src/adapters/Smt2ExpressionAdapter.h create mode 100644 src/solver/Smt2SmtSolver.cpp create mode 100644 src/solver/Smt2SmtSolver.h diff --git a/src/adapters/Smt2ExpressionAdapter.h b/src/adapters/Smt2ExpressionAdapter.h new file mode 100644 index 000000000..1d42b103c --- /dev/null +++ b/src/adapters/Smt2ExpressionAdapter.h @@ -0,0 +1,165 @@ +#ifndef STORM_ADAPTERS_SMT2EXPRESSIONADAPTER_H_ +#define STORM_ADAPTERS_SMT2EXPRESSIONADAPTER_H_ + +#include + +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" +#include "src/storage/expressions/Expressions.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/utility/macros.h" +#include "src/exceptions/ExpressionEvaluationException.h" +#include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace adapters { + + class Smt2ExpressionAdapter{ + public: + /*! + * Creates an expression adapter that can translate expressions to the format of Smt2. + * + * @param manager The manager that can be used to build expressions. + * @param useReadableVarNames sets whether the expressions should use human readable names for the variables or the internal representation + */ + Smt2ExpressionAdapter(storm::expressions::ExpressionManager& manager, bool useReadableVarNames) : manager(manager), useReadableVarNames(useReadableVarNames) { + declaredVariables.emplace_back(std::set()); + } + + /*! + * Translates the given expression to an equivalent expression for Smt2. + * + * @param expression The expression to translate. + * @return An equivalent expression for Smt2. + */ + std::string translateExpression(storm::expressions::Expression const& expression) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + +#ifdef STORM_HAVE_CARL + /*! + * Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2. + + * @param leftHandSide + * @param relation + * @param RightHandSide + * @return An equivalent expression for Smt2. + */ + std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) { + + return "(" + carl::toString(relation) + + " (/ " + + leftHandSide.nominator().toString(false, useReadableVarNames) + " " + + leftHandSide.denominator().toString(false, useReadableVarNames) + + ") (/ " + + rightHandSide.nominator().toString(false, useReadableVarNames) + " " + + rightHandSide.denominator().toString(false, useReadableVarNames) + + ") " + + ")"; + } + + /*! + * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2. + + * @param constraint + * @return An equivalent expression for Smt2. + */ + std::string translateExpression(carl::Constraint const& constraint) { + + return "(" + carl::toString(constraint.rel()) + " " + + constraint.lhs().toString(false, useReadableVarNames) + " " + + "0 " + + ")"; + } +#endif + /*! + * Translates the given variable to an equivalent expression for Smt2. + * + * @param variable The variable to translate. + * @return An equivalent expression for smt2. + */ + std::string translateExpression(storm::expressions::Variable const& variable) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + /*! + * Finds the counterpart to the given smt2 variable declaration. + * + * @param smt2Declaration The declaration for which to find the equivalent. + * @return The equivalent counterpart. + */ + storm::expressions::Variable const& getVariable(std::string smt2Declaration) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + void increaseScope(uint_fast64_t n=1){ + for(uint_fast64_t i=0; i()); + } + } + + void decreaseScope(uint_fast64_t n=1){ + STORM_LOG_THROW(declaredVariables.size()>=n, storm::exceptions::InvalidArgumentException, "Scope increased too much. Too many calls of pop()?"); + for(uint_fast64_t i=0; i const checkForUndeclaredVariables(std::set const& variables){ + std::vector result; + carl::VariablePool& vPool = carl::VariablePool::getInstance(); + for (storm::Variable const& variableToCheck : variables){ + std::string const& variableString = vPool.getName(variableToCheck, useReadableVarNames); + // first check if this variable is already declared + bool alreadyDeclared=false; + for(std::set const& variables : declaredVariables){ + if(variables.find(variableString)!=variables.end()){ + alreadyDeclared=true; + break; + } + } + // secondly, declare the variable if necessary + if(!alreadyDeclared){ + STORM_LOG_DEBUG("Declaring the variable " + variableString); + declaredVariables.back().insert(variableString); + std::string varDeclaration = "( declare-fun " + variableString + " () "; + switch (variableToCheck.getType()){ + case carl::VariableType::VT_BOOL: + varDeclaration += "Bool"; + break; + case carl::VariableType::VT_REAL: + varDeclaration += "Real"; + break; + case carl::VariableType::VT_INT: + varDeclaration += "Int"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "The type of the variable is not supported"); + } + varDeclaration += " )"; + result.push_back(varDeclaration); + } + } + return result; + } +#endif + + private: + // The manager that can be used to build expressions. + storm::expressions::ExpressionManager& manager; + // A flag to decide whether readable var names should be used instead of intern representation + bool useReadableVarNames; + // the declared variables for the different scopes + std::vector> declaredVariables; + }; + } // namespace adapters +} // namespace storm + +#endif /* STORM_ADAPTERS_SMT2EXPRESSIONADAPTER_H_ */ diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 2d377564d..ef6c9282e 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -10,6 +10,8 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/solver/Smt2SmtSolver.h" + #include "src/utility/graph.h" #include "src/utility/vector.h" #include "src/utility/macros.h" @@ -986,6 +988,36 @@ namespace storm { } } + template<> + storm::storage::SparseMatrix SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::instantiateAsDouble(std::map substitutions){ + + //Check if the CoeffType is as expected + STORM_LOG_THROW((std::is_same::value), storm::exceptions::IllegalArgumentException, "Unexpected Type of Coefficients"); + + //get a Matrix builder + index_type numElements=0; + for(row_type const& row : this->data){ + numElements += row.size(); + } + storm::storage::SparseMatrixBuilder matrixBuilder(this->getNumberOfRows(), this->getNumberOfRows(), numElements); + + //fill in the data... + for(index_type rowIndex=0; rowIndex < this->getNumberOfRows(); ++rowIndex){ + for(auto const& entry : this->getRow(rowIndex)){ + double value = cln::double_approx(entry.getValue().evaluate(substitutions)); + matrixBuilder.addNextValue(rowIndex, entry.getColumn(), value); + } + } + + return matrixBuilder.build(); + } + + template + storm::storage::SparseMatrix SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::instantiateAsDouble(std::map substitutions){ + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Instantiation of flexible matrix is not supported for this type"); + } + + template typename SparseDtmcEliminationModelChecker::FlexibleSparseMatrix SparseDtmcEliminationModelChecker::getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) { FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); @@ -1014,6 +1046,285 @@ namespace storm { return flexibleMatrix; } + template<> + bool SparseDtmcEliminationModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector::ParameterRegion> parameterRegions){ + //Note: this is an 'experimental' implementation + //Start with some preprocessing (inspired by computeUntilProbabilities...) + + //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) + //get the (sub)formulae and the vector of target states + STORM_LOG_THROW(formula.isStateFormula(), storm::exceptions::IllegalArgumentException, "expected a stateFormula"); + STORM_LOG_THROW(formula.asStateFormula().isProbabilityOperatorFormula(), storm::exceptions::IllegalArgumentException, "expected a probabilityOperatorFormula"); + storm::logic::ProbabilityOperatorFormula const& probOpForm=formula.asStateFormula().asProbabilityOperatorFormula(); + STORM_LOG_THROW(probOpForm.hasBound(), storm::exceptions::IllegalArgumentException, "The formula has no bound"); + STORM_LOG_THROW(probOpForm.getSubformula().asPathFormula().isEventuallyFormula(), storm::exceptions::IllegalArgumentException, "expected an eventually subformula"); + storm::logic::EventuallyFormula const& eventFormula = probOpForm.getSubformula().asPathFormula().asEventuallyFormula(); + + std::unique_ptr targetStatesResultPtr = this->check(eventFormula.getSubformula()); + storm::storage::BitVector const& targetStates = targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + // Do some sanity checks to establish some required properties. + STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); + + // Then, compute the subset of states that has a probability of 0 or 1, respectively. + std::pair statesWithProbability01 = storm::utility::graph::performProb01(model, storm::storage::BitVector(model.getNumberOfStates(),true), targetStates); + storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; + std::cout << "states with prob 0" << statesWithProbability0 << std::endl; + storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); + + // If the initial state is known to have either probability 0 or 1, we can directly return the result. + if (model.getInitialStates().isDisjointFrom(maybeStates)) { + STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); + double res= statesWithProbability0.get(*model.getInitialStates().begin()) ? 0.0 : 1.0; + switch (probOpForm.getComparisonType()){ + case storm::logic::ComparisonType::Greater: + return (res > probOpForm.getBound()); + case storm::logic::ComparisonType::GreaterEqual: + return (res >= probOpForm.getBound()); + case storm::logic::ComparisonType::Less: + return (res < probOpForm.getBound()); + case storm::logic::ComparisonType::LessEqual: + return (res <= probOpForm.getBound()); + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); + } + } + + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + + // Create a vector for the probabilities to go to a state with probability 1 in one step. + std::vector oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); + + // Determine the set of initial states of the sub-model. + storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. + FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); + FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); + + + //TODO... + // eliminate some states.. update the one step probabilities! + + // SMT formulation of resulting pdtmc + storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions + carl::VariablePool& varPool = carl::VariablePool::getInstance(); + storm::solver::Smt2SmtSolver solver(manager, true); + + // todo maybe introduce the parameters already at this point? + + // we will introduce a variable for every state which encodes the probability to reach a target state from this state. + // we will store them as polynomials to easily use operations with rational functions + std::vector stateProbVars; + for (storm::storage::sparse::state_type state = 0; state < flexibleMatrix.getNumberOfRows(); ++state){ + storm::Variable stateVar = varPool.getFreshVariable("p_" + std::to_string(state)); + std::shared_ptr>> cache(new carl::Cache>()); + storm::RationalFunction::PolyType stateVarAsPoly(storm::RationalFunction::PolyType::PolyType(stateVar), cache); + + //each variable is in the interval [0,1] + solver.add(storm::RationalFunction(stateVarAsPoly), storm::CompareRelation::GEQ, storm::RationalFunction(0)); + solver.add(storm::RationalFunction(stateVarAsPoly), storm::CompareRelation::LEQ, storm::RationalFunction(1)); + stateProbVars.push_back(stateVarAsPoly); + } + + //now lets add the actual transitions + for (storm::storage::sparse::state_type state = 0; state < flexibleMatrix.getNumberOfRows(); ++state){ + storm::RationalFunction reachProbability(oneStepProbabilities[state]); + if(!reachProbability.isZero()){ + std::cout << "non zero " << state << ": " << reachProbability << std::endl; + } + for(auto const& transition : flexibleMatrix.getRow(state)){ + reachProbability += transition.getValue() * stateProbVars[transition.getColumn()]; + } + //Todo: depending on the objective (i.e. the formlua) it suffices to use LEQ or GEQ here... maybe this is faster? + solver.add(storm::RationalFunction(stateProbVars[state]), storm::CompareRelation::EQ, reachProbability); + } + + //the property should be satisfied in the initial state + storm::CompareRelation propertyCompRel; + switch (probOpForm.getComparisonType()){ + case storm::logic::ComparisonType::Greater: + propertyCompRel=storm::CompareRelation::GT; + break; + case storm::logic::ComparisonType::GreaterEqual: + propertyCompRel=storm::CompareRelation::GEQ; + break; + case storm::logic::ComparisonType::Less: + propertyCompRel=storm::CompareRelation::LT; + break; + case storm::logic::ComparisonType::LessEqual: + propertyCompRel=storm::CompareRelation::LEQ; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); + } + uint_fast64_t thresholdDenominator = 1.0/storm::settings::generalSettings().getPrecision(); + uint_fast64_t thresholdNumerator = probOpForm.getBound()*thresholdDenominator; + storm::RationalFunction threshold(thresholdNumerator); + threshold = threshold / thresholdDenominator; + solver.add(storm::RationalFunction(stateProbVars[*newInitialStates.begin()]), propertyCompRel, threshold); + + //the bounds for the parameters + solver.push(); + for(auto param : parameterRegions){ + storm::RawPolynomial lB(param.variable); + lB -= param.lowerBound; + solver.add(carl::Constraint(lB,storm::CompareRelation::GEQ)); + storm::RawPolynomial uB(param.variable); + uB -= param.upperBound; + solver.add(carl::Constraint(uB,storm::CompareRelation::LEQ)); + } + + flexibleMatrix.print(); + + + /* + //testing stuff... + auto varx=varPool.getFreshVariable("x"); + storm::RawPolynomial px(varx); + carl::Constraint cx(px,storm::CompareRelation::GEQ); + carl::Constraint cx1(px-storm::RawPolynomial(1),storm::CompareRelation::LEQ); + storm::RationalFunction zero(0); + storm::RationalFunction one(1); + storm::RationalFunction two(2); + storm::RationalFunction funcWithpK = flexibleMatrix.getRow(1).begin()->getValue(); + storm::RationalFunction funcWithpL = flexibleMatrix.getRow(11).begin()->getValue(); + carl::Constraint cpLzero(funcWithpL,storm::CompareRelation::GEQ); + + solver.add(one,storm::CompareRelation::LEQ, two); + solver.add(funcWithpL,storm::CompareRelation::LEQ, one); + solver.push(); + solver.add(funcWithpL,storm::CompareRelation::GEQ, zero); + solver.add(funcWithpK,storm::CompareRelation::GEQ, zero); + solver.pop(); + solver.add(funcWithpK,storm::CompareRelation::GEQ, zero); + solver.add(cpLzero); + solver.add(cx); + solver.add(cx1); + + */ + /* + solver.add(p,storm::CompareRelation::LEQ, two); + solver.add(q,storm::CompareRelation::LT, p); + solver.add(q-p,storm::CompareRelation::LT); + + */ + + // find further restriction on probabilities + //start solving ... + + /* maybe useful stuff... + // Create a bit vector that represents the subsystem of states we still have to eliminate. + storm::storage::BitVector subsystem = storm::storage::BitVector(submatrix.getRowCount(), true); + + std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); + + + //from compute reachability + uint_fast64_t maximalDepth = 0; + if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { + // If we are required to do pure state elimination, we simply create a vector of all states to + // eliminate and sort it according to the given priorities. + + // Remove the initial state from the states which we need to eliminate. + subsystem &= ~initialStates; + std::vector states(subsystem.begin(), subsystem.end()); + + if (statePriorities) { + std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); + } + + STORM_LOG_DEBUG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); + for (auto const& state : states) { + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); + } + STORM_LOG_DEBUG("Eliminated " << states.size() << " states." << std::endl); + } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { + // When using the hybrid technique, we recursively treat the SCCs up to some size. + std::vector entryStateQueue; + STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); + maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, stateRewards, statePriorities); + + // If the entry states were to be eliminated last, we need to do so now. + STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); + if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) { + for (auto const& state : entryStateQueue) { + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); + } + } + STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl); + } + + // Finally eliminate initial state. + if (!stateRewards) { + // If we are computing probabilities, then we can simply call the state elimination procedure. It + // will scale the transition row of the initial state with 1/(1-loopProbability). + STORM_LOG_INFO("Eliminating initial state " << *initialStates.begin() << "." << std::endl); + eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards); + } else { + // If we are computing rewards, we cannot call the state elimination procedure for technical reasons. + // Instead, we need to get rid of a potential loop in this state explicitly. + + // Start by finding the self-loop element. Since it can only be the only remaining outgoing transition + // of the initial state, this amounts to checking whether the outgoing transitions of the initial + // state are non-empty. + if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) { + STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more."); + STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not."); + ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue(); + loopProbability = storm::utility::one() / (storm::utility::one() - loopProbability); + STORM_LOG_DEBUG("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability); + stateRewards.get()[(*initialStates.begin())] *= loopProbability; + flexibleMatrix.getRow(*initialStates.begin()).clear(); + } + } + */ + std::cout << std::endl << "-----------------------" << std::endl << "testing stuff..." << std::endl; + std::map testmap; + + storm::Variable pK = varPool.findVariableWithName("pK"); + storm::Variable pL = varPool.findVariableWithName("pL"); + storm::Variable bs = varPool.findVariableWithName("bs"); + std::cout << "pk id is " << pK.getId() << std::endl; + std::cout << "pL id is " << pL.getId() << std::endl; + std::cout << "bs id is " << bs.getId() << std::endl; + if(bs == storm::Variable::NO_VARIABLE){ + std::cout << "bs is not a variable" << std::endl; + } + storm::RationalFunction::CoeffType pKSub=4; + pKSub= pKSub/10; + storm::RationalFunction::CoeffType pLSub=8; + pLSub= pLSub/10; + testmap[pK]=pKSub; + testmap[pL]=pLSub; + storm::storage::SparseMatrix resultingMatr = flexibleMatrix.instantiateAsDouble(testmap); + std::cout << "Old matrix: column: " << flexibleMatrix.getRow(1).begin()->getColumn() << " value:" << flexibleMatrix.getRow(1).begin()->getValue() << std::endl; + std::cout << "New matrix: column: " << resultingMatr.getRow(1).begin()->getColumn() << " value:" << resultingMatr.getRow(1).begin()->getValue() << std::endl; + //END OF TESTING STUFF + //*/ + //from until method + //boost::optional> missingStateRewards; + //return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities))); + + return false; + } + + template + bool SparseDtmcEliminationModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector::ParameterRegion> parameterRegions){ + + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type"); + } + template class SparseDtmcEliminationModelChecker; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 4ae3d7a9e..ee08ddad6 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -22,6 +22,20 @@ namespace storm { virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; + struct ParameterRegion{ + storm::Variable variable; + storm::RationalFunction::CoeffType lowerBound; + storm::RationalFunction::CoeffType upperBound; + }; + + /*! + * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions + * ParameterRegions should contain all parameters (not mentioned parameters are assumed to be arbitrary reals) + */ + bool checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions); + + + private: class FlexibleSparseMatrix { public: @@ -52,6 +66,16 @@ namespace storm { */ bool hasSelfLoop(storm::storage::sparse::state_type state); + /*! + * Instantiates the matrix, i.e., evaluate the occurring functions according to the given substitution of the variables + * + * @param substitutions A mapping that assigns a constant value to every variable + * + * @return A matrix with constant (double) entries + */ + storm::storage::SparseMatrix instantiateAsDouble(std::map substitutions); + + private: std::vector data; }; diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index e8f64ac9f..4f7377612 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -45,6 +45,7 @@ namespace storm { #ifdef STORM_HAVE_CARL const std::string GeneralSettings::parametricOptionName = "parametric"; + const std::string GeneralSettings::parametricRegionOptionName = "parametricRegion"; #endif GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { @@ -93,6 +94,7 @@ namespace storm { #ifdef STORM_HAVE_CARL this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, parametricRegionOptionName, false, "Sets whether to use the parametric Region engine.").build()); #endif } @@ -257,6 +259,9 @@ namespace storm { bool GeneralSettings::isParametricSet() const { return this->getOption(parametricOptionName).getHasOptionBeenSet(); } + bool GeneralSettings::isParametricRegionSet() const { + return this->getOption(parametricRegionOptionName).getHasOptionBeenSet(); + } #endif bool GeneralSettings::check() const { diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 6b1d23857..632a037bb 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -301,6 +301,13 @@ namespace storm { * @return True iff the option was set. */ bool isParametricSet() const; + + /*! + * Retrieves whether the option enabling parametric region model checking is set. + * + * @return True iff the option was set. + */ + bool isParametricRegionSet() const; #endif bool check() const override; @@ -346,6 +353,7 @@ namespace storm { #ifdef STORM_HAVE_CARL static const std::string parametricOptionName; + static const std::string parametricRegionOptionName; #endif }; diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp new file mode 100644 index 000000000..d9201c09f --- /dev/null +++ b/src/solver/Smt2SmtSolver.cpp @@ -0,0 +1,136 @@ +#include "src/solver/Smt2SmtSolver.h" + +#include "src/exceptions/NotSupportedException.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/NotImplementedException.h" +#include "utility/macros.h" +#include "adapters/CarlAdapter.h" +#include "exceptions/IllegalArgumentException.h" +#include "exceptions/IllegalFunctionCallException.h" + +namespace storm { + namespace solver { + + Smt2SmtSolver::Smt2ModelReference::Smt2ModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager), expressionAdapter(expressionAdapter){ + // Intentionally left empty. + } + + bool Smt2SmtSolver::Smt2ModelReference::getBooleanValue(storm::expressions::Variable const& variable) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + int_fast64_t Smt2SmtSolver::Smt2ModelReference::getIntegerValue(storm::expressions::Variable const& variable) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + double Smt2SmtSolver::Smt2ModelReference::getRationalValue(storm::expressions::Variable const& variable) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) { +#ifndef STORM_HAVE_CARL + STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException, "Tried to use carl expressions but storm is not linked with CARL"); +#endif + expressionAdapter = std::unique_ptr(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), true)); + init(); + } + + Smt2SmtSolver::~Smt2SmtSolver() { + writeCommand("( exit )"); + //todo make sure that the process exits + } + + void Smt2SmtSolver::push() { + expressionAdapter->increaseScope(); + writeCommand("( push 1 ) "); + } + + void Smt2SmtSolver::pop() { + expressionAdapter->decreaseScope(); + writeCommand("( pop 1 ) "); + } + + void Smt2SmtSolver::pop(uint_fast64_t n) { + expressionAdapter->decreaseScope(n); + writeCommand("( pop " + std::to_string(n) + " ) "); + } + + void Smt2SmtSolver::reset() { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + void Smt2SmtSolver::add(storm::expressions::Expression const& assertion) { + STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + +#ifdef STORM_HAVE_CARL + void Smt2SmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) { + STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions"); + //if some of the occurring variables are not declared yet, we will have to. + std::set variables; + leftHandSide.gatherVariables(variables); + rightHandSide.gatherVariables(variables); + std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); + for (auto declaration : varDeclarations){ + writeCommand(declaration); + } + writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )"); + } + + template<> + void Smt2SmtSolver::add(carl::Constraint const& constraint) { + add(constraint.lhs(), constraint.rel()); + } + + template<> + void Smt2SmtSolver::add(carl::Constraint const& constraint) { + //if some of the occurring variables are not declared yet, we will have to. + std::set variables = constraint.lhs().gatherVariables(); + std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); + for (auto declaration : varDeclarations){ + writeCommand(declaration); + } + writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )"); + } + + +#endif + + SmtSolver::CheckResult Smt2SmtSolver::check() { + writeCommand("( check-sat )"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + + SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set const& assumptions) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + +#ifndef WINDOWS + + SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } +#endif + + void Smt2SmtSolver::init() { + //hard coded output file.. for now + commandFile.open("/home/tim/Desktop/smtlibcommand.txt", std::ios::trunc); + STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); + + //some initial commands + writeCommand("( set-logic QF_NRA )"); + + } + + void Smt2SmtSolver::writeCommand(std::string smt2Command) { + if (commandFile.is_open()) { + commandFile << smt2Command << std::endl; + } else{ + std::cout << "COMMAND FILE IS CLOSED" < +#include + +#include "storm-config.h" +#include "src/solver/SmtSolver.h" +#include "src/adapters/Smt2ExpressionAdapter.h" +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace solver { + + class Smt2SmtSolver : public SmtSolver { + public: + + class Smt2ModelReference : public SmtSolver::ModelReference { + public: + Smt2ModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter); + virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override; + virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override; + virtual double getRationalValue(storm::expressions::Variable const& variable) const override; + + private: + + // The expression adapter that is used to translate the variable names. + storm::adapters::Smt2ExpressionAdapter& expressionAdapter; + }; + + public: + /*! + * Creates a new solver with the given manager. + * In addition to storm expressions, this solver also allows carl expressions (but not both). + * Hence, there is a flag to chose between the two + */ + Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false); + virtual ~Smt2SmtSolver(); + + virtual void push() override; + + virtual void pop() override; + + virtual void pop(uint_fast64_t n) override; + + virtual void reset() override; + + virtual void add(storm::expressions::Expression const& assertion) override; +#ifdef STORM_HAVE_CARL + //adds the constraint "leftHandSide relation rightHandSide" + virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0)); + + //adds the given carl constraint + template + void add(typename carl::Constraint const& constraint); +#endif + + virtual CheckResult check() override; + + virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; + +#ifndef WINDOWS + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif + //Todo: some of these might be added in the future + //virtual storm::expressions::SimpleValuation getModelAsValuation() override; + + //virtual std::shared_ptr getModel() override; + + // virtual std::vector allSat(std::vector const& important) override; + + // virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; + + // virtual uint_fast64_t allSat(std::vector const& important, std::function const& callback) override; + + // virtual std::vector getUnsatAssumptions() override; + + private: + + + /*! + * Initializes the solver + */ + void init(); + + + /*! Writes the given command to the solver + * @param smt2Command the command that the solver will receive + */ + void writeCommand(std::string smt2Command); + + + + // a filestream where the commands that we send to the solver will be stored (can be used for debugging purposes) + std::ofstream commandFile; + + // An expression adapter that is used for translating the expression into Smt2's format. + std::unique_ptr expressionAdapter; + + // A flag storing whether the last call to a check method provided aussumptions. + bool lastCheckAssumptions; + + // The last result that was returned by any of the check methods. + CheckResult lastResult; + + // A flag that states whether we want to use carl expressions. + bool useCarlExpressions; + + }; + } +} +#endif // STORM_SOLVER_SMT2SMTSOLVER \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 3e0c31b5a..e8e06ac5c 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -445,22 +445,53 @@ namespace storm { std::shared_ptr> dtmc = model->template as>(); std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; + //do we want to check for a parameter region? + if(settings.isParametricRegionSet()){ + std::cout << std::endl; + //experimental implementation! check some hardcoded region + std::vector::ParameterRegion> regions; + storm::RationalFunction::CoeffType zeroPointOne(1); + zeroPointOne = zeroPointOne/10; + storm::modelchecker::SparseDtmcEliminationModelChecker::ParameterRegion param1; + param1.lowerBound= zeroPointOne*2; + param1.upperBound= zeroPointOne*4; + param1.variable=carl::VariablePool::getInstance().findVariableWithName("pL"); + regions.push_back(param1); + storm::modelchecker::SparseDtmcEliminationModelChecker::ParameterRegion param2; + param2.lowerBound= zeroPointOne*3; + param2.upperBound= zeroPointOne*5; + param2.variable=carl::VariablePool::getInstance().findVariableWithName("pK"); + regions.push_back(param2); + + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + bool result = modelchecker.checkRegion(*formula.get(), regions); + std::cout << "... done." << std::endl; + if (result){ + std::cout << "the property holds for all parameters in the given region" << std::endl; + }else{ + std::cout << "the property does NOT hold for all parameters in the given region" << std::endl; + } + + + }else{ + //just obtain the resulting rational function + std::unique_ptr result; - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula.get())) { - result = modelchecker.check(*formula.get()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); - } + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula.get())) { + result = modelchecker.check(*formula.get()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); + } - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->writeToStream(std::cout, model->getInitialStates()); - std::cout << std::endl << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->writeToStream(std::cout, model->getInitialStates()); + std::cout << std::endl << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } } } #endif