diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 8e40891f4..f2d880db0 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -64,6 +64,12 @@ namespace storm { template std::unique_ptr AbstractModelChecker::computeProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); + + //TODO if this is not checked first, computeStateFormulaProbabilities(...) is called (hasQualitativeResult true) + if (formula.isHOAPathFormula()) { + return this->computeHOAPathProbabilities(env, checkTask.substituteFormula(formula.asHOAPathFormula())); + } + if (formula.isStateFormula() || formula.hasQualitativeResult()) { return this->computeStateFormulaProbabilities(env, checkTask.substituteFormula(formula)); } @@ -83,6 +89,7 @@ namespace storm { } else if (formula.isUntilFormula()) { return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula())); } else if (formula.isHOAPathFormula()) { + // TODO checked earlier? return this->computeHOAPathProbabilities(env, checkTask.substituteFormula(formula.asHOAPathFormula())); } else if (formula.isNextFormula()) { return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula())); diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index b1a895ebc..f564c8221 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -26,6 +26,23 @@ namespace storm { // Intentionally left empty. } + template + std::map SparseLTLHelper::computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ + std::map apSets; + for (auto& p: extracted) { + STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); + + std::unique_ptr subResultPointer = formulaChecker(p.second); + + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto sat = subResult.getTruthValuesVector(); + + apSets[p.first] = std::move(sat); + STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); + } + return apSets; + } + template storm::storage::BitVector SparseLTLHelper::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { @@ -308,22 +325,6 @@ namespace storm { return numericResult; } - template - std::map SparseLTLHelper::computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ - std::map apSets; - for (auto& p: extracted) { - STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); - - std::unique_ptr subResultPointer = formulaChecker(p.second); - - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto sat = subResult.getTruthValuesVector(); - - apSets[p.first] = std::move(sat); - STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); - } - return apSets; - } template class SparseLTLHelper; template class SparseLTLHelper; diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 71760e717..c5e2a9c33 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -34,25 +34,14 @@ namespace storm { */ SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfSates); - - /*! - * Computes the LTL probabilities - * @param the LTL formula - * @param the atomic propositions and satisfaction sets - * @return a value for each state - */ - std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); - /*! * todo computes Sat sets of AP * @param * @param * @return */ - std::map computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); - + static std::map computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); - private: /*! * Computes the (maximizing) probabilities for the constructed DA product * @param the DA to build the product with @@ -62,6 +51,15 @@ namespace storm { */ std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets); + /*! + * Computes the LTL probabilities + * @param the LTL formula + * @param the atomic propositions and satisfaction sets + * @return a value for each state + */ + std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); + + private: /*! * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 7aa519bc6..ade41c728 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -125,39 +125,22 @@ namespace storm { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_INFO("Obtaining HOA automaton..."); storm::automata::DeterministicAutomaton::ptr da = pathFormula.readAutomaton(); - const storm::automata::APSet& apSet = da->getAPSet(); STORM_LOG_INFO("Deterministic automaton from HOA file has " << da->getNumberOfStates() << " states, " << da->getAPSet().size() << " atomic propositions and " << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); - // TODO move computation of apSets to SparseLTLHelper (extracted: AP to formula - std::map>) - std::map apSets; - for (std::string const& ap : apSet.getAPs()) { - std::shared_ptr expression = pathFormula.getAPMapping().at(ap); - STORM_LOG_INFO("Computing satisfaction set for atomic proposition \"" << ap << "\" <=> " << *expression << "..."); - std::unique_ptr resultPointer = this->check(*expression); - ExplicitQualitativeCheckResult const& result = resultPointer->asExplicitQualitativeCheckResult(); - storm::storage::BitVector bitVector = result.getTruthValuesVector(); - STORM_LOG_INFO("Atomic proposition \"" << ap << "\" is satisfied by " << bitVector.getNumberOfSetBits() << " states."); - apSets[ap] = std::move(bitVector); - } - const SparseDtmcModelType& dtmc = this->getModel(); - storm::solver::SolveGoal goal(dtmc, checkTask); - - // TODO HOA call LTL helper - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); - // storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); - // storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); - - // Compute Satisfaction sets for APs (see above) - // auto formulaChecker = [&] (std::shared_ptr const& formula) {return this->check(*formula); }; - // std::map apSets = helper.computeApSets(extracted, formulaChecker); + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), dtmc.getNumberOfStates()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); - // std::vector numericResult = helper.computeDAProductProbabilities(env, *da, apSatSets); + // Compute Satisfaction sets for APs + storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted = pathFormula.getAPMapping(); + auto formulaChecker = [&] (std::shared_ptr const& formula) {return this->check(*formula); }; + std::map apSets = helper.computeApSets(extracted, formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *da, apSets); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -180,7 +163,7 @@ namespace storm { dtmc.writeDotToStream(modelDot); modelDot.close(); } - + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); @@ -189,7 +172,6 @@ namespace storm { std::map apSets = helper.computeApSets(extracted, formulaChecker); std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index 419f744cc..1fa6f4159 100755 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -821,6 +821,8 @@ namespace { formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> !\"done\" }]"; // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]" formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]"; + // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]" + formulasString += "; P>0.3[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString); auto model = std::move(modelFormulas.first); @@ -850,6 +852,9 @@ namespace { result = checker->check(tasks[5]); EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[6]); + EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result)); } else { EXPECT_FALSE(checker->canHandle(tasks[0])); }