From bac0e0183598358e3e242b7c8a813c714fed3279 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 14 Apr 2015 21:29:08 +0200 Subject: [PATCH] added time measurement, support for stateelimination Former-commit-id: 14dfcb603af5afdfd8ee4c3236c5901068dc04f5 --- .../SparseDtmcEliminationModelChecker.cpp | 292 +++++++----------- .../SparseDtmcEliminationModelChecker.h | 7 + src/utility/cli.h | 8 +- 3 files changed, 125 insertions(+), 182 deletions(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 60a56f07b..0025c82a5 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -10,15 +10,13 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/solver/SmtSolver.h" -#include "src/solver/Smt2SmtSolver.h" - #include "src/utility/graph.h" #include "src/utility/vector.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidStateException.h" +#include "exceptions/UnexpectedException.h" namespace storm { namespace modelchecker { @@ -1049,11 +1047,67 @@ namespace storm { return flexibleMatrix; } #ifdef STORM_HAVE_CARL + + template + void SparseDtmcEliminationModelChecker::eliminateStates(storm::storage::BitVector& subsystem, FlexibleSparseMatrix& flexibleMatrix, std::vector& oneStepProbabilities, FlexibleSparseMatrix& flexibleBackwardTransitions, storm::storage::BitVector const& initialstates){ + //.. simple strategy for now... do not eliminate anything + /* + boost::optional> missingStateRewards; + storm::storage::BitVector statesToEliminate = ~initialstates; + + std::vector states(statesToEliminate.begin(), statesToEliminate.end()); + + STORM_LOG_DEBUG("Eliminating " << states.size() << " states." << std::endl); + for (auto const& state : states) { + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards); + subsystem.set(state,false); + } + STORM_LOG_DEBUG("Eliminated " << states.size() << " states." << std::endl); + //Note: we could also "eliminate" the initial state to get rid of its selfloop + */ + } + + template<> + void SparseDtmcEliminationModelChecker::formulateModelWithSMT(storm::solver::Smt2SmtSolver& solver, std::vector& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleSparseMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities){ + carl::VariablePool& varPool = carl::VariablePool::getInstance(); + + //first add a state variable for every state in the subsystem, providing that such a variable does not already exist. + for (storm::storage::sparse::state_type state : subsystem){ + if(stateProbVars[state].isZero()){ //variable does not exist yet + 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[state] = stateVarAsPoly; + } + } + + //now lets add the actual transitions + for (storm::storage::sparse::state_type state : subsystem){ + storm::RationalFunction reachProbability(oneStepProbabilities[state]); + 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); + } + } + + template + void SparseDtmcEliminationModelChecker::formulateModelWithSMT(storm::solver::Smt2SmtSolver& solver, std::vector& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleSparseMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities){ + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "SMT formulation is not supported for this type"); + } + 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...) + std::chrono::high_resolution_clock::time_point timeStart = std::chrono::high_resolution_clock::now(); + + //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"); @@ -1062,20 +1116,16 @@ namespace storm { 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; 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."); @@ -1093,76 +1143,55 @@ namespace storm { 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); + std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); + + // Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated. + storm::storage::BitVector subsystem = storm::storage::BitVector(submatrix.getRowCount(), true); + eliminateStates(subsystem, flexibleMatrix, oneStepProbabilities, flexibleBackwardTransitions, newInitialStates); + + std::chrono::high_resolution_clock::time_point timeStateElemEnd = std::chrono::high_resolution_clock::now(); - //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]); - 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); - } + std::vector stateProbVars(subsystem.size(), storm::RationalFunction::PolyType(0)); + // todo maybe introduce the parameters already at this point? + formulateModelWithSMT(solver, stateProbVars, subsystem, flexibleMatrix, oneStepProbabilities); - //the property should be satisfied in the initial state + //the property should be satisfied in the initial state for all parameters. + //this is equivalent to: + //the negation of the property should not be satisfied for some parameter valuation. + //Hence, we flip the comparison relation and later check whether all the constraints are unsat. storm::CompareRelation propertyCompRel; switch (probOpForm.getComparisonType()){ case storm::logic::ComparisonType::Greater: - propertyCompRel=storm::CompareRelation::GT; + propertyCompRel=storm::CompareRelation::LEQ; break; case storm::logic::ComparisonType::GreaterEqual: - propertyCompRel=storm::CompareRelation::GEQ; + propertyCompRel=storm::CompareRelation::LT; break; case storm::logic::ComparisonType::Less: - propertyCompRel=storm::CompareRelation::LT; + propertyCompRel=storm::CompareRelation::GEQ; break; case storm::logic::ComparisonType::LessEqual: - propertyCompRel=storm::CompareRelation::LEQ; + propertyCompRel=storm::CompareRelation::GT; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); @@ -1184,155 +1213,62 @@ namespace storm { solver.add(carl::Constraint(uB,storm::CompareRelation::LEQ)); } - switch (solver.check()){ + std::chrono::high_resolution_clock::time_point timeSmtFormulationEnd = std::chrono::high_resolution_clock::now(); + + // TODO find further restriction on probabilities + + std::chrono::high_resolution_clock::time_point timeRestrictingEnd = std::chrono::high_resolution_clock::now(); + + std::cout << "start solving ..." << std::endl; + bool result; + switch (solver.check()){ case storm::solver::SmtSolver::CheckResult::Sat: std::cout << "sat!" << std::endl; + result=false; break; case storm::solver::SmtSolver::CheckResult::Unsat: std::cout << "unsat!" << std::endl; + result=true; break; case storm::solver::SmtSolver::CheckResult::Unknown: std::cout << "unknown!" << std::endl; + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not solve the SMT-Problem (Check-result: Unknown)") + result=false; break; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not solve the SMT-Problem (Check-result: Unknown)") + result=false; } - /* - //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. + std::chrono::high_resolution_clock::time_point timeSolvingEnd = std::chrono::high_resolution_clock::now(); - // 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; + std::chrono::high_resolution_clock::duration timePreprocessing = timePreprocessingEnd - timeStart; + std::chrono::high_resolution_clock::duration timeStateElem = timeStateElemEnd - timePreprocessingEnd; + std::chrono::high_resolution_clock::duration timeSmtFormulation = timeSmtFormulationEnd - timeStateElemEnd; + std::chrono::high_resolution_clock::duration timeRestricting = timeRestrictingEnd - timeSmtFormulationEnd; + std::chrono::high_resolution_clock::duration timeSolving = timeSolvingEnd- timeRestrictingEnd; + std::chrono::high_resolution_clock::duration timeOverall = timeSolvingEnd - timeStart; + std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast(timePreprocessing); + std::chrono::milliseconds timeStateElemInMilliseconds = std::chrono::duration_cast(timeStateElem); + std::chrono::milliseconds timeSmtFormulationInMilliseconds = std::chrono::duration_cast(timeSmtFormulation); + std::chrono::milliseconds timeRestrictingInMilliseconds = std::chrono::duration_cast(timeRestricting); + std::chrono::milliseconds timeSolvingInMilliseconds = std::chrono::duration_cast(timeSolving); + std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(timeOverall); + STORM_PRINT_AND_LOG(std::endl << "required time: " << timeOverallInMilliseconds.count() << "ms. Time Breakdown:" << std::endl); + STORM_PRINT_AND_LOG(" * " << timePreprocessingInMilliseconds.count() << "ms for Preprocessing" << std::endl); + STORM_PRINT_AND_LOG(" * " << timeStateElemInMilliseconds.count() << "ms for StateElemination" << std::endl); + STORM_PRINT_AND_LOG(" * " << timeSmtFormulationInMilliseconds.count() << "ms for SmtFormulation" << std::endl); + STORM_PRINT_AND_LOG(" * " << timeRestrictingInMilliseconds.count() << "ms for Restricting" << std::endl); + STORM_PRINT_AND_LOG(" * " << timeSolvingInMilliseconds.count() << "ms for Solving" << std::endl); + + return result; } 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"); } - + #endif template class SparseDtmcEliminationModelChecker; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 15aff7f86..ab595dcea 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -5,6 +5,8 @@ #include "src/models/sparse/Dtmc.h" #include "src/modelchecker/AbstractModelChecker.h" #include "src/utility/constants.h" +#include "src/solver/SmtSolver.h" +#include "src/solver/Smt2SmtSolver.h" namespace storm { namespace modelchecker { @@ -93,6 +95,11 @@ namespace storm { std::vector getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities); + //eliminates some of the states according to different strategies. + void eliminateStates(storm::storage::BitVector& subsystem, FlexibleSparseMatrix& flexibleMatrix, std::vector& oneStepProbabilities, FlexibleSparseMatrix& flexibleBackwardTransitions, storm::storage::BitVector const& initialStates); + + void formulateModelWithSMT(storm::solver::Smt2SmtSolver& solver, std::vector& stateProbVars, storm::storage::BitVector const& subsystem, FlexibleSparseMatrix const& flexibleMatrix, std::vector const& oneStepProbabilities); + // The model this model checker is supposed to analyze. storm::models::sparse::Dtmc const& model; diff --git a/src/utility/cli.h b/src/utility/cli.h index 25b24be1d..80c71925b 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -479,13 +479,13 @@ namespace storm { storm::RationalFunction::CoeffType zeroPointOne(1); zeroPointOne = zeroPointOne/10; storm::modelchecker::SparseDtmcEliminationModelChecker::ParameterRegion param1; - param1.lowerBound= zeroPointOne*2; - param1.upperBound= zeroPointOne*4; + param1.lowerBound= zeroPointOne*6; + param1.upperBound= zeroPointOne*9; 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.lowerBound= zeroPointOne*7; + param2.upperBound= zeroPointOne*8; param2.variable=carl::VariablePool::getInstance().findVariableWithName("pK"); regions.push_back(param2);