diff --git a/src/modelchecker/reachability/DirectEncoding.h b/src/modelchecker/reachability/DirectEncoding.h index 46ea6fe92..6bc2506e7 100644 --- a/src/modelchecker/reachability/DirectEncoding.h +++ b/src/modelchecker/reachability/DirectEncoding.h @@ -28,7 +28,7 @@ namespace storm std::vector stateVars; for(carl::Variable p : parameters) { - smt2 << carl::io::smt2flag::ASSERT; + smt2 << ("parameter_bound_" + vpool.getName(p)); smt2 << carl::io::smt2node::AND; smt2 << carl::Constraint(Polynomial(p), carl::CompareRelation::GT); smt2 << carl::Constraint(Polynomial(p) - Polynomial(1), carl::CompareRelation::LT); @@ -41,16 +41,15 @@ namespace storm stateVars.push_back(stateVar); if(!finalStates[state]) { - smt2 << carl::io::smt2flag::ASSERT; + smt2 << ("state_bound_" + std::to_string(state)); smt2 << carl::io::smt2node::AND; - smt2 << carl::Constraint(Polynomial(stateVar), carl::CompareRelation::GE); - smt2 << carl::Constraint(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LE); + smt2 << carl::Constraint(Polynomial(stateVar), carl::CompareRelation::GT); + smt2 << carl::Constraint(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LT); smt2 << carl::io::smt2node::CLOSENODE; } } - smt2 << carl::io::smt2flag::ASSERT; - smt2 << carl::io::smt2node::AND; + smt2.setAutomaticLineBreaks(true); Polynomial initStateReachSum; for(uint_fast64_t state = 0; state < nrStates-1; ++state) @@ -82,16 +81,20 @@ namespace storm } } + smt2 << ("transition_" + std::to_string(state)); smt2 << carl::Constraint(reachpropPol - stateVars[state], carl::CompareRelation::EQ); } } //smt2 << carl::Constraint(Polynomial(stateVars[nrStates-1]), carl::CompareRelation::EQ); - smt2 << carl::io::smt2node::CLOSENODE; - smt2 << carl::io::smt2flag::ASSERT; + + + smt2 << ("reachability"); carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LE : carl::CompareRelation::GE; smt2 << carl::Constraint(initStateReachSum - threshold, thresholdRelation); smt2 << carl::io::smt2flag::CHECKSAT; + smt2 << carl::io::smt2flag::MODEL; + smt2 << carl::io::smt2flag::UNSAT_CORE; std::stringstream strm; strm << smt2; return strm.str(); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 301c806d3..4f4f099d1 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -303,6 +303,10 @@ class AbstractModel: public std::enable_shared_from_this> { storm::models::AtomicPropositionsLabeling const& getStateLabeling() const { return stateLabeling; } + + storm::models::AtomicPropositionsLabeling & getStateLabeling() { + return stateLabeling; + } /*! * Retrieves whether this model has a state reward model. diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index e86c85923..4dfefdcc9 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -272,7 +272,7 @@ public: // Get the choice label sets and move the needed values to the front. std::vector> newChoice(this->getChoiceLabeling()); - storm::utility::vector::selectVectorValues(newChoice, subSysStates, newChoice); + storm::utility::vector::selectVectorValues(newChoice, subSysStates, this->getChoiceLabeling()); // Throw away all values after the last state and set the choice label set for s_b as empty. newChoice.resize(newStateCount); diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 6e9f08386..8e1db232a 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -1,5 +1,6 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/AbstractModel.h" +#include "src/storage/parameters.h" namespace storm { namespace storage { @@ -204,5 +205,11 @@ namespace storm { // Explicitly instantiate the SCC decomposition. template class StronglyConnectedComponentDecomposition; + #ifdef PARAMETRIC_SYSTEMS + template class StronglyConnectedComponentDecomposition; + template class StronglyConnectedComponentDecomposition; + #endif + + } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 641336c76..4959dccc7 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -25,7 +25,8 @@ namespace storm { } storm::expressions::Expression const& Constant::getExpression() const { - LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant."); + assert(this->isDefined()); + LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant: " + this->getName()); return this->expression; } diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 585695d4e..816f9edca 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -272,7 +272,7 @@ namespace storm { constantSubstitution.emplace(constant.getName(), constant.getExpression()); - // If there is at least one more constant to come, we substitute the costants we have so far. + // If there is at least one more constant to come, we substitute the constants we have so far. if (constantIndex + 1 < newConstants.size()) { newConstants[constantIndex + 1] = newConstants[constantIndex + 1].substitute(constantSubstitution); } diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 81de7704c..93643dd8a 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -32,31 +32,33 @@ std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& lab dtmc->makeAbsorbing(targetStates); // 2. throw away anything which does not add to the reachability probability. // 2a. remove non productive states - storm::storage::BitVector productive = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates); - // 2b. throw away non reachable states - storm::storage::BitVector reachable = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates); - storm::storage::BitVector bv = productive & reachable; + storm::storage::BitVector productiveStates = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates); + // 2b. calculate set of states wich + storm::storage::BitVector almostSurelyReachingTargetStates = ~utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, ~productiveStates); + // 2c. Make such states also target states. + dtmc->makeAbsorbing(almostSurelyReachingTargetStates); + // 2d. throw away non reachable states + storm::storage::BitVector reachableStates = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates); + storm::storage::BitVector bv = productiveStates & reachableStates; + dtmc->getStateLabeling().addAtomicProposition("__targets__", targetStates | almostSurelyReachingTargetStates); models::Dtmc subdtmc = dtmc->getSubDtmc(bv); phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true); initStates = subdtmc.getInitialStates(); - targetStates = subdtmc.getLabeledStates(label); + targetStates = subdtmc.getLabeledStates("__targets__"); storm::storage::BitVector deadlockStates(phiStates); deadlockStates.set(subdtmc.getNumberOfStates()-1,false); - // Calculate whether there are states which surely lead into the target. - storm::storage::BitVector potentialIntoDeadlock = utility::graph::performProbGreater0(subdtmc, subdtmc.getBackwardTransitions(), phiStates, deadlockStates); - storm::storage::BitVector extraTargets = ~potentialIntoDeadlock & ~targetStates; - if(extraTargets.empty()) - { - // TODO implement this if necessary. - std::cout << "Extra targets exist. Please implement!" << std::endl; - } + // Search for states with only one non-deadlock successor. std::map> chainedStates; StateId nrStates = subdtmc.getNumberOfStates(); StateId deadlockState = nrStates - 1; - for(StateId source = 0; source < nrStates; ++source) + for(StateId source = 0; source < nrStates - 1; ++source) { + if(targetStates[source]) + { + continue; + } storage::DeterministicTransition productiveTransition(nrStates); for(auto const& transition : subdtmc.getRows(source)) { @@ -79,16 +81,37 @@ std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& lab { chainedStates.emplace(source, productiveTransition); } - for(auto chainedState : chainedStates) + } + storage::BitVector eliminatedStates(nrStates, false); + for(auto & chainedState : chainedStates) + { + assert(chainedState.first != chainedState.second.targetState()); + auto it = chainedStates.find(chainedState.second.targetState()); + if(it != chainedStates.end()) { - auto it = chainedStates.find(chainedState.second.targetState()); - if(it != chainedStates.end()) - { - chainedState.second.targetState() = it->second.targetState(); - chainedState.second.probability() *= it->second.probability(); - } + //std::cout << "----------------------------" << std::endl; + //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; + //std::cout << it->first << " -- " << it->second.probability() << " --> " << it->second.targetState() << std::endl; + chainedState.second.targetState() = it->second.targetState(); + chainedState.second.probability() *= it->second.probability(); + //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; + //std::cout << "----------------------------" << std::endl; + chainedStates.erase(it); + eliminatedStates.set(it->first, true); + } + } + + + for(auto chainedState : chainedStates) + { + if(!eliminatedStates[chainedState.first]) + { + std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; } } + + storage::StronglyConnectedComponentDecomposition sccs(subdtmc); + std::cout << sccs << std::endl; modelchecker::reachability::DirectEncoding dec; std::vector parameters; @@ -102,7 +125,7 @@ std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& lab parameters.push_back(p); } } - return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates(label), mpq_class(1,2)); + return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2)); }