From 71f72d84b223e6f1f8f4111cbd72ca09f40a500c Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 18 Jun 2021 12:29:24 +0200 Subject: [PATCH] Ma ltl-MC and tests --- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../MarkovAutomatonCslModelCheckerTest.cpp | 35 +++++++++++++++++++ 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index c35c05b43..35239a154 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -40,7 +40,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { - auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(true).setNextFormulasAllowed(true).setNestedPathFormulasAllowed(true).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); + auto singleObjectiveFragment = storm::logic::csl().setUnaryBooleanPathFormulasAllowed(true).setBinaryBooleanPathFormulasAllowed(true).setNestedPathFormulasAllowed(true).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setRewardAccumulationAllowed(true); if (!storm::NumberTraits::SupportsExponential) { singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 745c32f55..07475ce7a 100755 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -349,4 +349,39 @@ namespace { } #endif } + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, LtlSimple) { + std::string formulasString = "Pmax=? [X X s=3]"; + formulasString += "; Pmax=? [X X G s>2]"; + formulasString += "; Pmin=? [X X G s>2]"; + formulasString += "; Pmax=? [F ((s=0) U X(s=0) & X(s=2))]"; + + 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; + + // LTL not supported in all engines (Hybrid, PrismDd, JaniDd) + if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse || TypeParam::engine == MaEngine::JitSparse) { + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1/10"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("1/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1/10"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("9/10"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } else { + EXPECT_FALSE(checker->canHandle(tasks[0])); + } + + } }