diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 8d8a91302..b3fc509cf 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1113,25 +1113,56 @@ namespace storm { } #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 - /* ... or all? - boost::optional> missingStateRewards; + template<> + void SparseDtmcEliminationModelChecker::eliminateStates(storm::storage::BitVector& subsystem, FlexibleSparseMatrix& flexibleMatrix, std::vector& oneStepProbabilities, FlexibleSparseMatrix& flexibleBackwardTransitions, storm::storage::BitVector const& initialstates){ + //.. Todo: chose between different strategies for elimination of states + + //only eliminate states with constant outgoing transitions and non-initial states. + /* this does not work since the transitions change while processing + storm::storage::BitVector constantOutgoing(subsystem.size(), true); + storm::storage::BitVector constantIncoming(subsystem.size(), true); + for(FlexibleSparseMatrix::index_type row=0; row states(statesToEliminate.begin(), statesToEliminate.end()); - + //todo some special ordering? STORM_LOG_DEBUG("Eliminating " << states.size() << " states." << std::endl); + boost::optional> missingStateRewards; for (auto const& state : states) { - eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards); - subsystem.set(state,false); + bool onlyConstantOutgoingTransitions=true; + for(auto const& entry : flexibleMatrix.getRow(state)){ + if(!entry.getValue().isConstant()){ + onlyConstantOutgoingTransitions=false; + break; + } + } + if(onlyConstantOutgoingTransitions){ + 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::eliminateStates(storm::storage::BitVector& subsystem, FlexibleSparseMatrix& flexibleMatrix, std::vector& oneStepProbabilities, FlexibleSparseMatrix& flexibleBackwardTransitions, storm::storage::BitVector const& initialstates){ + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "elimination of states not suported for this type"); + } + + 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(); @@ -1342,7 +1373,7 @@ namespace storm { std::chrono::high_resolution_clock::time_point timeSmtFormulationEnd = std::chrono::high_resolution_clock::now(); // find further restriction on probabilities - restrictProbabilityVariables(solver,stateProbVars,subsystem,flexibleMatrix,oneStepProbabilities, parameterRegions, probOpForm.getComparisonType()); + //restrictProbabilityVariables(solver,stateProbVars,subsystem,flexibleMatrix,oneStepProbabilities, parameterRegions, probOpForm.getComparisonType()); std::chrono::high_resolution_clock::time_point timeRestrictingEnd = std::chrono::high_resolution_clock::now(); diff --git a/src/utility/cli.h b/src/utility/cli.h index 80c71925b..7a2dda7ce 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*6; + param1.lowerBound= zeroPointOne*8; param1.upperBound= zeroPointOne*9; param1.variable=carl::VariablePool::getInstance().findVariableWithName("pL"); regions.push_back(param1); storm::modelchecker::SparseDtmcEliminationModelChecker::ParameterRegion param2; param2.lowerBound= zeroPointOne*7; - param2.upperBound= zeroPointOne*8; + param2.upperBound= zeroPointOne*9; param2.variable=carl::VariablePool::getInstance().findVariableWithName("pK"); regions.push_back(param2);