From 8a26af29f911c8b04ae68132ced01a686c49800b Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 11 Aug 2021 21:01:29 +0200 Subject: [PATCH] allow HOA formulas for cslstar and pctlstar Conflicts: src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp --- src/storm/logic/FragmentSpecification.cpp | 2 ++ .../SparseMarkovAutomatonCslModelChecker.cpp | 4 +-- .../prctl/SparseMdpPrctlModelChecker.cpp | 4 +-- .../csl/CtmcCslModelCheckerTest.cpp | 28 +++++++++++++++++++ .../MarkovAutomatonCslModelCheckerTest.cpp | 28 +++++++++++++++++++ .../prctl/mdp/MdpPrctlModelCheckerTest.cpp | 28 +++++++++++++++++++ 6 files changed, 90 insertions(+), 4 deletions(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 9e28eec3e..2272ef61f 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -52,6 +52,7 @@ namespace storm { pctlstar.setUnaryBooleanPathFormulasAllowed(true); pctlstar.setNestedOperatorsAllowed(true); pctlstar.setNestedPathFormulasAllowed(true); + pctlstar.setHOAPathFormulasAllowed(true); return pctlstar; } @@ -128,6 +129,7 @@ namespace storm { cslstar.setUnaryBooleanPathFormulasAllowed(true); cslstar.setNestedOperatorsAllowed(true); cslstar.setNestedPathFormulasAllowed(true); + cslstar.setHOAPathFormulasAllowed(true); return cslstar; } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 1874a1384..7afb03f38 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -132,8 +132,8 @@ namespace storm { std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 7ce739537..6551b61fe 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -160,8 +160,8 @@ namespace storm { std::unique_ptr SparseMdpPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index d61224024..e13d0ebb1 100755 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -525,4 +525,32 @@ namespace { #endif } + + TYPED_TEST(CtmcCslModelCheckerTest, HOAProbabilitiesPolling) { + // "P=? [ F "target" & (X s=1)]" + std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"target\", \"p1\" -> (s=1) }]"; + // "P=? [!(s=1) U (s=1)]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s=1) , \"p1\" -> \"target\" }]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // Not supported in all engines (Hybrid, PrismDd, JaniDd) + if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse || TypeParam::engine == CtmcEngine::JitSparse) { + result = checker->check(tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[1]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } else { + EXPECT_FALSE(checker->canHandle(tasks[0])); + } + + } } diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 58359c41a..3d02af1c2 100755 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -387,4 +387,32 @@ namespace { GTEST_SKIP(); #endif } + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, HOASimple) { + // "P=? [ F (s=3) & (X s=1)]" + std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s>1), \"p1\" -> !(s=1) }]"; + // "P=? [ (s=2) U (s=1)]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s=2), \"p1\" -> (s=1) }]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // Not supported in all engines (Hybrid, PrismDd, JaniDd) + if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse || TypeParam::engine == MaEngine::JitSparse) { + result = checker->check(tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[1]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } else { + EXPECT_FALSE(checker->canHandle(tasks[0])); + } + + } } diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp index 271c59321..82f25b7c0 100755 --- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -787,5 +787,33 @@ namespace { } + TYPED_TEST(MdpPrctlModelCheckerTest, HOADice) { + // "P=? [ F "three" & (X s=1)]" + std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"three\", \"p1\" -> s2=1 }]"; + // "P=? [!(s2=6) U "done"]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s2=6), \"p1\" -> \"done\" }]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(169ul, model->getNumberOfStates()); + EXPECT_EQ(436ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // Not supported in all engines (Hybrid, PrismDd, JaniDd) + if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse || TypeParam::engine == MdpEngine::JitSparse) { + result = checker->check(tasks[0]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[1]); + EXPECT_NEAR(this->parseNumber("3/4"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } else { + EXPECT_FALSE(checker->canHandle(tasks[0])); + } + + } + }