From 9a0be7e9ca21d7c8d741c202b7651721413ad60d Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 15:15:25 +0200 Subject: [PATCH 01/59] added first rpatl fragment checker tests Conflicts: src/test/storm/logic/FragmentCheckerTest.cpp --- src/test/storm/logic/FragmentCheckerTest.cpp | 89 +++++++++++++------- 1 file changed, 57 insertions(+), 32 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index c0f10a5ed..9f2df5ccd 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -12,16 +12,16 @@ TEST(FragmentCheckerTest, Propositional) { storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); @@ -42,10 +42,10 @@ TEST(FragmentCheckerTest, Pctl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification pctl = storm::logic::pctl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); @@ -63,19 +63,19 @@ TEST(FragmentCheckerTest, Prctl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification prctl = storm::logic::prctl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); @@ -90,19 +90,19 @@ TEST(FragmentCheckerTest, Csl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csl = storm::logic::csl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, csl)); @@ -114,25 +114,25 @@ TEST(FragmentCheckerTest, Csrl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csrl = storm::logic::csrl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); } @@ -140,32 +140,57 @@ TEST(FragmentCheckerTest, Csrl) { TEST(FragmentCheckerTest, MultiObjective) { storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective(); - + storm::parser::FormulaParser formulaParser; std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"label\" & R<=4[F \"label\"]])]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - +} + +TEST(FragmentCheckerTest, Rpatl) { + auto expManager = std::make_shared(); + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification rpatl = storm::logic::rpatl(); + + storm::parser::FormulaParser formulaParser(expManager); + std::shared_ptr formula; + + ASSERT_ANY_THROW(formula = formulaParser.parseSingleFormulaFromString("<> \"label\"")); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1>> P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2>> Pmin=? [ \"label1\" U \"label2\" ]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> Rmax=? [ LRA ]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> R=? [C<=3]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); } From 8d11ed9f42b08bf7d5a216a9661faa698d7fb291 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 15:16:09 +0200 Subject: [PATCH 02/59] added first rpatl fragment checker tests Conflicts: src/test/storm/logic/FragmentCheckerTest.cpp --- src/test/storm/logic/FragmentCheckerTest.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 9f2df5ccd..440adffce 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -169,6 +169,7 @@ TEST(FragmentCheckerTest, MultiObjective) { EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); } + TEST(FragmentCheckerTest, Rpatl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; From 3d73e71162afaac599b3f911188f12fe2117636d Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 16:08:07 +0200 Subject: [PATCH 03/59] introduced test-modelchecker-rpatl-smg --- src/test/storm/CMakeLists.txt | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index 4fc60ab16..9adda6440 100755 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -13,6 +13,7 @@ include_directories(${GTEST_INCLUDE_DIR}) set(NON_SPLIT_TESTS abstraction adapter automata builder logic model parser permissiveschedulers simulator solver storage transformer utility) set(MODELCHECKER_TEST_SPLITS abstraction csl exploration multiobjective reachability) set(MODELCHECKER_PRCTL_TEST_SPLITS dtmc mdp) +set(MODELCHECKER_RPATL_TEST_SPLITS smg) function(configure_testsuite_target testsuite) #message(CONFIGURING TESTSUITE '${testsuite}') #DEBUG @@ -43,3 +44,10 @@ foreach(prctl_split ${MODELCHECKER_PRCTL_TEST_SPLITS}) add_executable(test-modelchecker-prctl-${prctl_split} ${TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) configure_testsuite_target(modelchecker-prctl-${prctl_split}) endforeach() + +# Modelchecker-Rpatl testsuite split +foreach(rpatl_split ${MODELCHECKER_RPATL_TEST_SPLITS}) + file(GLOB_RECURSE TEST_MODELCHECKER_RPATL_${rpatl_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/rpatl/${rpatl_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/rpatl/${rpatl_split}/*.cpp) + add_executable(test-modelchecker-rpatl-${rpatl_split} ${TEST_MODELCHECKER_RPATL_${rpatl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) + configure_testsuite_target(modelchecker-rpatl-${rpatl_split}) +endforeach() \ No newline at end of file From a7919a651c603c14d4b098fbd2e4fa04c3e4e205 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 16:09:14 +0200 Subject: [PATCH 04/59] added a smg example for checking test-modelchecker-rpatl-smg --- resources/examples/testfiles/smg/walker.nm | 29 ++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 resources/examples/testfiles/smg/walker.nm diff --git a/resources/examples/testfiles/smg/walker.nm b/resources/examples/testfiles/smg/walker.nm new file mode 100644 index 000000000..e50b3aa5b --- /dev/null +++ b/resources/examples/testfiles/smg/walker.nm @@ -0,0 +1,29 @@ +smg + +player walker + [a0], [a00], [a1], [a2], [a3] +endplayer + +player blocker + [a40], [a41] +endplayer + +label "s0" = c=0 & b=0 & a=0; +label "s1" = c=0 & b=0 & a=1; +label "s2" = c=0 & b=1 & a=0; +label "s3" = c=0 & b=1 & a=1; +label "s4" = c=1 & b=0 & a=0; + +module transitions + a : [0..1] init 0; + b : [0..1] init 0; + c : [0..1] init 0; + + [a0] a=0 & b=0 & c=0 -> 4/10 : (a'=1) + 6/10 : (b'=1); + [a00] a=0 & b=0 & c=0 -> true; + [a1] a=1 & b=0 & c=0 -> 3/10 : (a'=0) + 3/10 : (a'=0) & (b'=1) + 4/10 : (b'=1); + [a2] a=0 & b=1 & c=0 -> 2/10 : (a'=1) + 8/10 : (b'=0) & (c'=1); + [a3] a=1 & b=1 & c=0 -> true; + [a40] a=0 & b=0 & c=1 -> 3/10 : (c'=0) + 7/10 : (a'=1) & (b'=1) & (c'=0); + [a41] a=0 & b=0 & c=1 -> true; +endmodule \ No newline at end of file From 7565bc5d6aef3b1f9aa76fc1f6f8dd9f01d08880 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 16:10:19 +0200 Subject: [PATCH 05/59] created SmgRpatlModelCheckerTest.cpp as test suite for rpatl smg models --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 208 ++++++++++++++++++ 1 file changed, 208 insertions(+) create mode 100644 src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp new file mode 100644 index 000000000..79b635845 --- /dev/null +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -0,0 +1,208 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + +#include "storm/models/sparse/Smg.h" +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + + enum class SmgEngine {PrismSparse}; + + class SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel); + env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx); + return env; + } + }; + + class SparseDoubleValueIterationGmmxxRegularMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular); + env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx); + return env; + } + }; + + class SparseDoubleValueIterationNativeGaussSeidelMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel); + env.solver().multiplier().setType(storm::solver::MultiplierType::Native); + return env; + } + }; + + class SparseDoubleValueIterationNativeRegularMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular); + env.solver().multiplier().setType(storm::solver::MultiplierType::Native); + return env; + } + }; + + template + class SmgRpatlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Smg SparseModelType; + + SmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + if (TestType::engine == SmgEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == SmgEngine::PrismSparse) { + return std::make_shared>(*model); + } else { + STORM_LOG_ERROR("TestType::engine must be PrismSparse!"); + return nullptr; + } + } + +/* bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQualitativeCheckResult().forallTrue(); + }*/ + + ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); + } + + private: + storm::Environment _environment; + + std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { + if (isSparseModel()) { + return std::make_unique(model->template as()->getInitialStates()); + } else { + STORM_LOG_ERROR("Smg Rpatl Model must be a Sparse Model!"); + return nullptr; + } + } + }; + + typedef ::testing::Types< + SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment, + SparseDoubleValueIterationGmmxxRegularMultEnvironment, + SparseDoubleValueIterationNativeGaussSeidelMultEnvironment, + SparseDoubleValueIterationNativeRegularMultEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(SmgRpatlModelCheckerTest, TestingTypes,); + + TYPED_TEST(SmgRpatlModelCheckerTest, Walker) { + std::string formulasString = "<> Pmax=? [X \"s2\"]"; + formulasString += "; <> Pmin=? [X \"s2\"]"; + + // TODO: bounded eventually causes wrong compuations for native multipliers + // TODO: do some more checks for comutation +/* formulasString += "; <> Pmax=? [F \"s3\"]"; + formulasString += "; <> Pmin=? [F \"s3\"]"; + + formulasString += "; <> Pmax=? [F [3,4] \"s4\"]"; + formulasString += "; <> Pmax=? [F [3,5] \"s4\"]";*/ + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/walker.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(12ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + +/* result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.345454"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("0.576"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision());*/ + } + + // TODO: create more test cases +} From fdb84fdee5f5b3f6b6b216a31bd1e02423a84069 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 11 Aug 2021 09:50:06 +0200 Subject: [PATCH 06/59] changed the info about statesOfCoalition to STORM_LOG_INFO --- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index bf04dc000..f44a7cef7 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -63,7 +63,7 @@ namespace storm { storm::logic::Formula const& subFormula = gameFormula.getSubformula(); statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition()); - std::cout << "Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition." << std::endl; + STORM_LOG_INFO("Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition."); statesOfCoalition.complement(); if (subFormula.isRewardOperatorFormula()) { From d0f85313f3209c6bf91bc3e90d34bb8923694847 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 11 Aug 2021 11:33:46 +0200 Subject: [PATCH 07/59] added probabalisticFormula.rpatl in testfolder for rpatl for future purposes --- resources/examples/testfiles/rpatl/probabalisticFormula.rpatl | 1 + 1 file changed, 1 insertion(+) create mode 100644 resources/examples/testfiles/rpatl/probabalisticFormula.rpatl diff --git a/resources/examples/testfiles/rpatl/probabalisticFormula.rpatl b/resources/examples/testfiles/rpatl/probabalisticFormula.rpatl new file mode 100644 index 000000000..1b0eed235 --- /dev/null +++ b/resources/examples/testfiles/rpatl/probabalisticFormula.rpatl @@ -0,0 +1 @@ +<> Pmax=? [ F "goal" ] \ No newline at end of file From b49dd5910119fac84a1573a79a3c571ae708155e Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 11 Aug 2021 11:35:33 +0200 Subject: [PATCH 08/59] WIP added testcases for globally probabilities for SmgRpatlModelCheckerTest "Walker" --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 79b635845..24267e80d 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -167,9 +167,12 @@ namespace { TYPED_TEST(SmgRpatlModelCheckerTest, Walker) { std::string formulasString = "<> Pmax=? [X \"s2\"]"; formulasString += "; <> Pmin=? [X \"s2\"]"; + formulasString += "; <> Pmax=? [G !\"s3\"]"; + formulasString += "; <> Pmin=? [G !\"s3\"]"; + formulasString += "; <> Pmax=? [G a=0 ]"; + formulasString += "; <> Pmin=? [G a=0 ]"; - // TODO: bounded eventually causes wrong compuations for native multipliers - // TODO: do some more checks for comutation + // TODO: check why computation with nativeMultiplier does not work /* formulasString += "; <> Pmax=? [F \"s3\"]"; formulasString += "; <> Pmin=? [F \"s3\"]"; @@ -191,6 +194,18 @@ namespace { result = checker->check(this->env(), tasks[1]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0.65454565"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.48"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + /* result = checker->check(this->env(), tasks[2]); EXPECT_NEAR(this->parseNumber("0.345454"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); From 3a91b266d4eeedf0523a0c96559a3e9061a56fe4 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 11 Aug 2021 15:07:32 +0200 Subject: [PATCH 09/59] WIP expanded tests, now tests run for X, U, G, F --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 65 ++++++++++++------- 1 file changed, 41 insertions(+), 24 deletions(-) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 24267e80d..67fd4336a 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -165,19 +165,26 @@ namespace { TYPED_TEST_SUITE(SmgRpatlModelCheckerTest, TestingTypes,); TYPED_TEST(SmgRpatlModelCheckerTest, Walker) { + // NEXT tests std::string formulasString = "<> Pmax=? [X \"s2\"]"; formulasString += "; <> Pmin=? [X \"s2\"]"; + formulasString += "; <> Pmax=? [X !\"s1\"]"; + formulasString += "; <> Pmin=? [X !\"s1\"]"; + // UNTIL tests + formulasString += "; <> Pmax=? [ a=0 U a=1 ]"; + formulasString += "; <> Pmin=? [ a=0 U a=1 ]"; + formulasString += "; <> Pmax=? [ b=0 U b=1 ]"; + formulasString += "; <> Pmin=? [ b=0 U b=1 ]"; + // GLOBALLY tests formulasString += "; <> Pmax=? [G !\"s3\"]"; formulasString += "; <> Pmin=? [G !\"s3\"]"; formulasString += "; <> Pmax=? [G a=0 ]"; formulasString += "; <> Pmin=? [G a=0 ]"; - - // TODO: check why computation with nativeMultiplier does not work -/* formulasString += "; <> Pmax=? [F \"s3\"]"; + // EVENTUALLY tests + formulasString += "; <> Pmax=? [F \"s3\"]"; formulasString += "; <> Pmin=? [F \"s3\"]"; - formulasString += "; <> Pmax=? [F [3,4] \"s4\"]"; - formulasString += "; <> Pmax=? [F [3,5] \"s4\"]";*/ + formulasString += "; <> Pmax=? [F [3,5] \"s4\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/walker.nm", formulasString); auto model = std::move(modelFormulas.first); @@ -188,36 +195,46 @@ namespace { auto checker = this->createModelChecker(model); std::unique_ptr result; - result = checker->check(this->env(), tasks[0]); + // NEXT results + result = checker->check(this->env(), tasks[0]); //OK + EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[1]); //OK + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); //OK + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); //OK EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[1]); + // UNTIL results + result = checker->check(this->env(), tasks[4]); //FAIL -> 0.99999922964892118 this may happen if the walker does not get caught in s4 + EXPECT_NEAR(this->parseNumber("0.52"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[5]); //OK + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[6]); //OK + EXPECT_NEAR(this->parseNumber("0.9999996417"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[7]); //OK EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); + // GLOBALLY tests + result = checker->check(this->env(), tasks[8]); //FAIL -> 2.686012256170045e-06 this may happen if the walker does not stay in s0 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); + result = checker->check(this->env(), tasks[9]); //FAIL -> 1 this is maybe exactly the other way round (by minimizing leaving) EXPECT_NEAR(this->parseNumber("0.65454565"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); + result = checker->check(this->env(), tasks[10]); //FAIL -> 7.7035107881595621e-07 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[5]); + result = checker->check(this->env(), tasks[11]); //FAIL -> 1 EXPECT_NEAR(this->parseNumber("0.48"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); -/* result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("0.345454"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); + // EVENTUALLY tests + result = checker->check(this->env(), tasks[12]); //FAIL -> 0.99999731398774383 + EXPECT_NEAR(this->parseNumber("0.34545435"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[13]); //OK EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); + result = checker->check(this->env(), tasks[14]); //FAIL -> 0.63359999999999994 here is maybe an offset of 1 step EXPECT_NEAR(this->parseNumber("0.576"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision());*/ + result = checker->check(this->env(), tasks[15]); //FAIL -> 0.64511999999999992 + EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } - // TODO: create more test cases + // TODO: create more test cases (files) } From d14b04fe724806ad75b9b9b5b3e30b363a3fcea1 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 11 Aug 2021 15:29:08 +0200 Subject: [PATCH 10/59] WIP DEBUG message for multiplier type --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 85a08ea96..60af5b2d0 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -18,6 +18,15 @@ namespace storm { // TODO add Kwiatkowska original reference auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); + //solverEnv.solver().multiplier().setType(storm::solver::MultiplierType::Native); + + if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Native) { + STORM_LOG_DEBUG("Multiplier type = Native"); + } else if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Gmmxx) { + STORM_LOG_DEBUG("Multiplier type = Gmmxx"); + } else { + STORM_LOG_DEBUG("Multiplier type unknown"); + } // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; @@ -52,6 +61,15 @@ namespace storm { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } } + + if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Native) { + STORM_LOG_DEBUG("Multiplier type = Native"); + } else if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Gmmxx) { + STORM_LOG_DEBUG("Multiplier type = Gmmxx"); + } else { + STORM_LOG_DEBUG("Multiplier type unknown"); + } + // Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default) storm::utility::vector::setVectorValues(result, relevantStates, x); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); From 04dd2b2e926bb1460a037749cabb73b226080b4c Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 15:19:04 +0200 Subject: [PATCH 11/59] added a smg to PrismParserTest.cpp Conflicts: src/test/storm/parser/PrismParserTest.cpp --- src/test/storm/parser/PrismParserTest.cpp | 143 ++++++++++++++-------- 1 file changed, 91 insertions(+), 52 deletions(-) diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index b9ed393b4..51945865d 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -14,6 +14,7 @@ TEST(PrismParser, StandardModelTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader3_5.pm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/smg/walker.nm")); } TEST(PrismParser, SimpleTest) { @@ -23,16 +24,16 @@ TEST(PrismParser, SimpleTest) { b : bool; [a] true -> 1: (b'=true != false = b => false); endmodule)"; - + storm::prism::Program result; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); EXPECT_FALSE(result.hasUnboundedVariables()); - + testInput = R"(mdp - + module main x : [1..5] init 1; [] x=1 -> 1:(x'=2); @@ -51,21 +52,21 @@ TEST(PrismParser, SimpleTest) { TEST(PrismParser, ComplexTest) { std::string testInput = R"(ma - + const int a; const int b = 10; const bool c; const bool d = true | false; const double e; const double f = 9; - + formula test = a >= 10 & (max(a,b) > floor(e)); formula test2 = a+b; formula test3 = (a + b > 10 ? floor(e) : h) + a; - + global g : bool init false; global h : [0 .. b]; - + module mod1 i : bool; j : bool init c; @@ -74,25 +75,25 @@ TEST(PrismParser, ComplexTest) { [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(e) + max(k, b) - 1 + k); [b] true -> (i'=i); endmodule - + module mod2 [] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (g'=(1-a) * 2 + floor(f) > 2); endmodule - + module mod3 = mod1 [ i = i1, j = j1, k = k1 ] endmodule - + label "mal" = max(a, 10) > 0; - + rewards "testrewards" [a] true : a + 7; max(f, a) <= 8 : 2*b; endrewards - + rewards "testrewards2" [b] true : a + 7; max(f, a) <= 8 : 2*b; endrewards)"; - + storm::prism::Program result; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType()); @@ -100,6 +101,44 @@ TEST(PrismParser, ComplexTest) { EXPECT_EQ(2ul, result.getNumberOfRewardModels()); EXPECT_EQ(1ul, result.getNumberOfLabels()); EXPECT_FALSE(result.hasUnboundedVariables()); + + testInput = + R"(smg + + player walker + [a0], [a00], [a1], [a2], [a3] + endplayer + + player blocker + [a40], [a41] + endplayer + + label "s0" = c=0 & b=0 & a=0; + label "s1" = c=0 & b=0 & a=1; + label "s2" = c=0 & b=1 & a=0; + label "s3" = c=0 & b=1 & a=1; + label "s4" = c=1 & b=0 & a=0; + + module transitions + a : [0..1] init 0; + b : [0..1] init 0; + c : [0..1] init 0; + + [a0] a=0 & b=0 & c=0 -> 4/10 : (a'=1) + 6/10 : (b'=1); + [a00] a=0 & b=0 & c=0 -> true; + [a1] a=1 & b=0 & c=0 -> 3/10 : (a'=0) + 3/10 : (a'=0) & (b'=1) + 4/10 : (b'=1); + [a2] a=0 & b=1 & c=0 -> 2/10 : (a'=1) + 8/10 : (b'=0) & (c'=1); + [a3] a=1 & b=1 & c=0 -> true; + [a40] a=0 & b=0 & c=1 -> 3/10 : (c'=0) + 7/10 : (a'=1) & (b'=1) & (c'=0); + [a41] a=0 & b=0 & c=1 -> true; + endmodule)"; + + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); + EXPECT_EQ(storm::prism::Program::ModelType::SMG, result.getModelType()); + EXPECT_EQ(1ul, result.getNumberOfModules()); + EXPECT_EQ(2ul, result.getNumberOfPlayers()); + EXPECT_EQ(5ul, result.getNumberOfLabels()); +>>>>>>> d7e3f7ed6 (added a smg to PrismParserTest.cpp) } TEST(PrismParser, UnboundedTest) { @@ -109,7 +148,7 @@ TEST(PrismParser, UnboundedTest) { b : int; [a] true -> 1: (b'=b+1); endmodule)"; - + storm::prism::Program result; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); @@ -186,119 +225,119 @@ TEST(PrismParser, IllegalInputTest) { const int a; const bool a = true; - + module mod1 c : [0 .. 8] init 1; - [] c < 3 -> 2: (c' = c+1); + [] c < 3 -> 2: (c' = c+1); endmodule )"; - + storm::prism::Program result; STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + const int a; - + module mod1 a : [0 .. 8] init 1; - [] a < 3 -> 1: (a' = a+1); + [] a < 3 -> 1: (a' = a+1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + const int a = 2; formula a = 41; - + module mod1 c : [0 .. 8] init 1; - [] c < 3 -> 1: (c' = c+1); + [] c < 3 -> 1: (c' = c+1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + const int a = 2; - + init c > 3 endinit - + module mod1 c : [0 .. 8] init 1; - [] c < 3 -> 1: (c' = c+1); + [] c < 3 -> 1: (c' = c+1); endmodule - + init c > 3 endinit )"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c < 3 -> 1: (c' = c+1); endmodule - + module mod2 [] c < 3 -> 1: (c' = c+1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c < 3 -> 1: (c' = c+1)&(c'=c-1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c < 3 -> 1: (c' = true || false); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c + 3 -> 1: (c' = 1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c + 3 -> 1: (c' = 1); endmodule - + label "test" = c + 1; - + )"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); } From 1b81c009c107f965ae798538ba29f36196c44c9a Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 08:22:38 +0200 Subject: [PATCH 12/59] WIP added GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 62 +++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 src/test/storm/parser/GameFormulaParserTest.cpp diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp new file mode 100644 index 000000000..2f867a494 --- /dev/null +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -0,0 +1,62 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/FragmentSpecification.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/storage/expressions/ExpressionManager.h" + +// TODO: write this to <> inputs (games)! + +TEST(GameFormulaParserTest, LabelTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> \"label\""; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(formula->isAtomicLabelFormula()); +} + +TEST(GameFormulaParserTest, ComplexLabelTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\""; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); + EXPECT_TRUE(formula->isBinaryBooleanStateFormula()); +} + +TEST(GameFormulaParserTest, ExpressionTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("y"); + + storm::parser::FormulaParser formulaParser(manager); + + std::string input = "!(x | y > 3)"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); + EXPECT_TRUE(formula->isUnaryBooleanStateFormula()); +} + +TEST(GameFormulaParserTest, LabelAndExpressionTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("y"); + + storm::parser::FormulaParser formulaParser(manager); + + std::string input = "!\"a\" | x | y > 3"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); + + input = "x | y > 3 | !\"a\""; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); +} \ No newline at end of file From e1b00dae7aaa18756055f35a1b20438491d9861f Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 09:42:51 +0200 Subject: [PATCH 13/59] small change in FragmentCheckerTest Rpatl --- src/test/storm/logic/FragmentCheckerTest.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 440adffce..53993b677 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -178,9 +178,10 @@ TEST(FragmentCheckerTest, Rpatl) { storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - ASSERT_ANY_THROW(formula = formulaParser.parseSingleFormulaFromString("<> \"label\"")); + // this may be a parsing issue + //ASSERT_ANY_THROW(formula = formulaParser.parseSingleFormulaFromString("<> \"label\"")); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1>> P=? [F \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2>> Pmin=? [ \"label1\" U \"label2\" ]")); From 868f42b38b6a8188aacc08962c07e5ceadd2d5bb Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 09:43:22 +0200 Subject: [PATCH 14/59] Bounded LTL formula check for FragmentCheckerTest Rpatl --- src/test/storm/logic/FragmentCheckerTest.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 53993b677..866e63fb0 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -193,6 +193,6 @@ TEST(FragmentCheckerTest, Rpatl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> R=? [C<=3]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); } From d8592bffa2fbb5c3c613a5f67688953002f94909 Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 09:56:33 +0200 Subject: [PATCH 15/59] shielding check for FragmentCheckerTest Rpatl --- src/test/storm/logic/FragmentCheckerTest.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 866e63fb0..056c84a88 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -195,4 +195,14 @@ TEST(FragmentCheckerTest, Rpatl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G <=5 \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G [0,1] \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + } From f1aa210b5a548fea67094a09338f6302c3292ebe Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 10:00:44 +0200 Subject: [PATCH 16/59] shielding check for FragmentCheckerTest Prctl --- src/test/storm/logic/FragmentCheckerTest.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 056c84a88..762f26f73 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -84,6 +84,15 @@ TEST(FragmentCheckerTest, Prctl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [\"label1\" U [5,7] \"label2\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G <=10 \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); } TEST(FragmentCheckerTest, Csl) { From 45319ca2da06177e199918dd3c207712e077da14 Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 16:18:33 +0200 Subject: [PATCH 17/59] WIP GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 148 +++++++++++++++--- 1 file changed, 125 insertions(+), 23 deletions(-) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 2f867a494..c2d3291a5 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -1,31 +1,32 @@ #include "test/storm_gtest.h" -#include "storm-config.h" #include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" -// TODO: write this to <> inputs (games)! - TEST(GameFormulaParserTest, LabelTest) { storm::parser::FormulaParser formulaParser; - std::string input = "<> \"label\""; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + std::string input = "<> Pmax=? [F \"label\"]"; + + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isAtomicLabelFormula()); + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); } TEST(GameFormulaParserTest, ComplexLabelTest) { storm::parser::FormulaParser formulaParser; - std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\""; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + std::string input = "<> Pmin=? [X !(\"a\" & \"b\") | \"a\" & !\"c\"]"; + + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); - EXPECT_TRUE(formula->isBinaryBooleanStateFormula()); + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); } TEST(GameFormulaParserTest, ExpressionTest) { @@ -35,12 +36,14 @@ TEST(GameFormulaParserTest, ExpressionTest) { storm::parser::FormulaParser formulaParser(manager); - std::string input = "!(x | y > 3)"; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + std::string input = "<> Pmin=? [G !(x | y > 3)]"; + + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); - EXPECT_TRUE(formula->isUnaryBooleanStateFormula()); + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); } TEST(GameFormulaParserTest, LabelAndExpressionTest) { @@ -50,13 +53,112 @@ TEST(GameFormulaParserTest, LabelAndExpressionTest) { storm::parser::FormulaParser formulaParser(manager); - std::string input = "!\"a\" | x | y > 3"; + std::string input = "<> Pmax=? [\"b\" U !\"a\" | x | y > 3]"; + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); + + input = "<> Pmax=? [x | y > 3 | !\"a\" U \"b\"]"; + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); +} + +TEST(GameFormulaParserTest, OnePlayerCoalitionTest) { + storm::parser::FormulaParser formulaParser; + + std::string player = "p1"; + std::string input = "<<" + player + ">>" + " Pmax=? [F \"label\"]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + + auto const& gameFormula = formula->asGameFormula(); + auto const& playerCoalition = gameFormula.getCoalition(); + //ASSERT_NO_THROW(auto const& players = playerCoalition.getPlayers()); + + std::ostringstream stream; + stream << playerCoalition; + std::string playerCoalitionString = stream.str(); + + EXPECT_EQ(player, playerCoalitionString); +} + +TEST(GameFormulaParserTest, PlayersCoalitionTest) { + storm::parser::FormulaParser formulaParser; + + std::string player = "p1, p2, p3, p4, p5"; + std::string input = "<<" + player + ">>" + " Pmin=? [X \"label\"]"; + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); + auto const& gameFormula = formula->asGameFormula(); + auto const& playerCoalition = gameFormula.getCoalition(); + EXPECT_EQ(5ul, playerCoalition.getPlayers().size()); + + std::ostringstream stream; + stream << playerCoalition; + std::string playerCoalitionString = stream.str(); + + std::string playerWithoutWhiteSpace = "p1,p2,p3,p4,p5"; + + EXPECT_EQ(playerWithoutWhiteSpace, playerCoalitionString); +} - input = "x | y > 3 | !\"a\""; +TEST(GameFormulaParserTest, ProbabilityOperatorTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> Pmax=? [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); -} \ No newline at end of file + + auto const& gameFormula = formula->asGameFormula(); + auto const& probFormula = gameFormula.getSubformula(); + + EXPECT_TRUE(probFormula.isProbabilityOperatorFormula()); + EXPECT_FALSE(probFormula.asProbabilityOperatorFormula().hasBound()); + EXPECT_TRUE(probFormula.asProbabilityOperatorFormula().hasOptimalityType()); +} + +// TODO: NextOperatorTest + +TEST(GameFormulaParserTest, UntilOperatorTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<

> Pmax=? [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& gameFormula1 = formula->asGameFormula(); + auto const& probFormula1 = gameFormula1.getSubformula(); + auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula1.isUntilFormula()); + EXPECT_FALSE(rawFormula1.isBoundedUntilFormula()); + + input = "<

> Pmax=? [\"a\" U <= 4 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& gameFormula2 = formula->asGameFormula(); + auto const& probFormula2 = gameFormula2.getSubformula(); + auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula2.isBoundedUntilFormula()); + EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(0, rawFormula2.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_EQ(4, rawFormula2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "<> Pmin=? [ (a&b) U [5,9] (b|c) ]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& gameFormula3 = formula->asGameFormula(); + auto const& probFormula3 = gameFormula3.getSubformula(); + auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula3.isBoundedUntilFormula()); + EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(5, rawFormula3.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); +} + + From bc6dabb088fe4a7fb0bf835961eead41b569f43c Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:03:37 +0200 Subject: [PATCH 18/59] fixed UntilOperatorTest in GameFormulaParserTest.cpp --- src/test/storm/parser/GameFormulaParserTest.cpp | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index c2d3291a5..d6b6bff3b 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -105,9 +105,7 @@ TEST(GameFormulaParserTest, PlayersCoalitionTest) { std::ostringstream stream; stream << playerCoalition; std::string playerCoalitionString = stream.str(); - std::string playerWithoutWhiteSpace = "p1,p2,p3,p4,p5"; - EXPECT_EQ(playerWithoutWhiteSpace, playerCoalitionString); } @@ -134,30 +132,39 @@ TEST(GameFormulaParserTest, UntilOperatorTest) { std::string input = "<

> Pmax=? [\"a\" U \"b\"]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); auto const& gameFormula1 = formula->asGameFormula(); auto const& probFormula1 = gameFormula1.getSubformula(); + EXPECT_TRUE(probFormula1.isProbabilityOperatorFormula()); auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(rawFormula1.isUntilFormula()); EXPECT_FALSE(rawFormula1.isBoundedUntilFormula()); - input = "<

> Pmax=? [\"a\" U <= 4 \"b\"]"; + input = "<

> Pmax=? [ \"a\" U <= 4 \"b\" ]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); auto const& gameFormula2 = formula->asGameFormula(); auto const& probFormula2 = gameFormula2.getSubformula(); + EXPECT_TRUE(probFormula2.isProbabilityOperatorFormula()); auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(rawFormula2.isBoundedUntilFormula()); EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); - EXPECT_EQ(0, rawFormula2.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_FALSE(rawFormula2.asBoundedUntilFormula().hasLowerBound()); + EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().hasUpperBound()); EXPECT_EQ(4, rawFormula2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); - input = "<> Pmin=? [ (a&b) U [5,9] (b|c) ]"; + input = "<> Pmin=? [ \"a\" & \"b\" U [5,9] \"c\" ] "; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); auto const& gameFormula3 = formula->asGameFormula(); auto const& probFormula3 = gameFormula3.getSubformula(); + EXPECT_TRUE(probFormula3.isProbabilityOperatorFormula()); auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); EXPECT_TRUE(rawFormula3.isBoundedUntilFormula()); EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().hasLowerBound()); EXPECT_EQ(5, rawFormula3.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().hasUpperBound()); EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); } From 442ffecd137aec900d2e44142c51792ee1d4b2b1 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:04:04 +0200 Subject: [PATCH 19/59] created NextOperatorTest in GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 35 ++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index d6b6bff3b..72ae61070 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -124,7 +124,40 @@ TEST(GameFormulaParserTest, ProbabilityOperatorTest) { EXPECT_TRUE(probFormula.asProbabilityOperatorFormula().hasOptimalityType()); } -// TODO: NextOperatorTest +TEST(GameFormulaParserTest, NextOperatorTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("a"); + storm::parser::FormulaParser formulaParser(manager); + + std::string input = "<

> Pmax=? [X \"a\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + auto const& gameFormula1 = formula->asGameFormula(); + auto const& probFormula1 = gameFormula1.getSubformula(); + EXPECT_TRUE(probFormula1.isProbabilityOperatorFormula()); + auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula1.isNextFormula()); + + input = "<> Pmin=? [X !x ]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + auto const& gameFormula2 = formula->asGameFormula(); + auto const& probFormula2 = gameFormula2.getSubformula(); + EXPECT_TRUE(probFormula2.isProbabilityOperatorFormula()); + auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula2.isNextFormula()); + + input = "<> Pmax=? [ X a>5 ]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + auto const& gameFormula3 = formula->asGameFormula(); + auto const& probFormula3 = gameFormula3.getSubformula(); + EXPECT_TRUE(probFormula3.isProbabilityOperatorFormula()); + auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula3.isNextFormula()); +} TEST(GameFormulaParserTest, UntilOperatorTest) { storm::parser::FormulaParser formulaParser; From 90568c54a2e0c26df415190c4126baa1053e5dc8 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:15:11 +0200 Subject: [PATCH 20/59] added RewardOperatorTest to GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 72ae61070..ef4deaf22 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -201,4 +201,22 @@ TEST(GameFormulaParserTest, UntilOperatorTest) { EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); } +TEST(GameFormulaParserTest, RewardOperatorTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> Rmin<0.9 [F \"a\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType()); + input = "<> R=? [I=10]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula()); +} From 4d84b84230fe68a792605f9ffa934010d47fc518 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:18:04 +0200 Subject: [PATCH 21/59] added ConditionalProbabilityTest to GameFormulaParserTest.cpp --- src/test/storm/parser/GameFormulaParserTest.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index ef4deaf22..a5fa7036a 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -220,3 +220,15 @@ TEST(GameFormulaParserTest, RewardOperatorTest) { EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType()); EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula()); } + +TEST(GameFormulaParserTest, ConditionalProbabilityTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> P<0.9 [F \"a\" || F \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asGameFormula().getSubformula().asProbabilityOperatorFormula(); + EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula()); +} From a3816184036f3dd2d5fd84aca22cfac6383d650d Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:20:16 +0200 Subject: [PATCH 22/59] added NestedPathFormulaTest to GameFormulaParserTest.cpp --- src/test/storm/parser/GameFormulaParserTest.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index a5fa7036a..ede75a6ad 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -232,3 +232,15 @@ TEST(GameFormulaParserTest, ConditionalProbabilityTest) { storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asGameFormula().getSubformula().asProbabilityOperatorFormula(); EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula()); } + +TEST(GameFormulaParserTest, NestedPathFormulaTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> P<0.9 [F X \"a\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula()); +} \ No newline at end of file From 3f2e636e34a6988793ee94768d457c42069965b6 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:25:04 +0200 Subject: [PATCH 23/59] added CommentTest to GameFormulaParserTest.cpp --- src/test/storm/parser/GameFormulaParserTest.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index ede75a6ad..82979d17f 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -243,4 +243,16 @@ TEST(GameFormulaParserTest, NestedPathFormulaTest) { EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula()); +} + +TEST(GameFormulaParserTest, CommentTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "// This is a comment. And this is a commented out formula: <

> P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n<

> P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment."; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula()); + ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula()); } \ No newline at end of file From 284a944f63bc89000d410a47bc7a73c532f3b387 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:28:17 +0200 Subject: [PATCH 24/59] added WrongFormatTest to GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 82979d17f..4d7f1ea08 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -255,4 +255,27 @@ TEST(GameFormulaParserTest, CommentTest) { EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula()); +} + +TEST(GameFormulaParserTest, WrongFormatTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("y"); + + storm::parser::FormulaParser formulaParser(manager); + std::string input = "<> P>0.5 [ a ]"; + std::shared_ptr formula(nullptr); + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<

> P=0.5 [F \"a\"]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<> P>0.5 [F !(x = 0)]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<< p1, p2 >> P>0.5 [F !y]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<< 1,2,3 >> P>0.5 [F y!=0)]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); } \ No newline at end of file From 567584e285c43336ef79642e259d99c29151a4bc Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:33:34 +0200 Subject: [PATCH 25/59] added MultiObjectiveFormulaTest to GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 4d7f1ea08..cc8c7014a 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -278,4 +278,34 @@ TEST(GameFormulaParserTest, WrongFormatTest) { input = "<< 1,2,3 >> P>0.5 [F y!=0)]"; STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); +} + +TEST(GameFormulaParserTest, MultiObjectiveFormulaTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "multi(<> P<0.9 [ F \"a\" ], <> R<42 [ F \"b\" ], <> Pmin=? [ F\"c\" ])"; + std::shared_ptr formula; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + ASSERT_TRUE(formula->isMultiObjectiveFormula()); + storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula(); + ASSERT_EQ(3ull, mof.getNumberOfSubformulas()); + + ASSERT_TRUE(mof.getSubformula(0).isGameFormula()); + ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().isProbabilityOperatorFormula()); + ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); + ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasBound()); + + ASSERT_TRUE(mof.getSubformula(1).isGameFormula()); + ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().isRewardOperatorFormula()); + ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); + ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); + + ASSERT_TRUE(mof.getSubformula(2).isGameFormula()); + ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().isProbabilityOperatorFormula()); + ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); + ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasOptimalityType()); + ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getOptimalityType())); } \ No newline at end of file From 54522409446e22cdc986f14716bdad3a4e7466fc Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:53:04 +0200 Subject: [PATCH 26/59] removed unnecessary testcases (e.g. there are no atomic label formulas in game formulas since they must have a coalition of players and an operator) --- .../storm/parser/GameFormulaParserTest.cpp | 66 ------------------- 1 file changed, 66 deletions(-) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index cc8c7014a..f07807dae 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -3,72 +3,6 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/storage/expressions/ExpressionManager.h" -TEST(GameFormulaParserTest, LabelTest) { - storm::parser::FormulaParser formulaParser; - - std::string input = "<> Pmax=? [F \"label\"]"; - - std::shared_ptr gameFormula(nullptr); - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); -} - -TEST(GameFormulaParserTest, ComplexLabelTest) { - storm::parser::FormulaParser formulaParser; - - std::string input = "<> Pmin=? [X !(\"a\" & \"b\") | \"a\" & !\"c\"]"; - - std::shared_ptr gameFormula(nullptr); - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); -} - -TEST(GameFormulaParserTest, ExpressionTest) { - std::shared_ptr manager(new storm::expressions::ExpressionManager()); - manager->declareBooleanVariable("x"); - manager->declareIntegerVariable("y"); - - storm::parser::FormulaParser formulaParser(manager); - - std::string input = "<> Pmin=? [G !(x | y > 3)]"; - - std::shared_ptr gameFormula(nullptr); - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); -} - -TEST(GameFormulaParserTest, LabelAndExpressionTest) { - std::shared_ptr manager(new storm::expressions::ExpressionManager()); - manager->declareBooleanVariable("x"); - manager->declareIntegerVariable("y"); - - storm::parser::FormulaParser formulaParser(manager); - - std::string input = "<> Pmax=? [\"b\" U !\"a\" | x | y > 3]"; - std::shared_ptr gameFormula(nullptr); - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); - - input = "<> Pmax=? [x | y > 3 | !\"a\" U \"b\"]"; - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); -} - TEST(GameFormulaParserTest, OnePlayerCoalitionTest) { storm::parser::FormulaParser formulaParser; From d86dbcd4e39be858799ac1f9601415d065e934bc Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 10:09:11 +0200 Subject: [PATCH 27/59] removed partial results for formula parsing, added fragment checks for rpatl --- .../storm/parser/GameFormulaParserTest.cpp | 94 +++++++++---------- 1 file changed, 42 insertions(+), 52 deletions(-) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index f07807dae..34ebc724c 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -12,10 +12,8 @@ TEST(GameFormulaParserTest, OnePlayerCoalitionTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - auto const& gameFormula = formula->asGameFormula(); - auto const& playerCoalition = gameFormula.getCoalition(); - //ASSERT_NO_THROW(auto const& players = playerCoalition.getPlayers()); - + EXPECT_TRUE(formula->isGameFormula()); + auto const& playerCoalition = formula->asGameFormula().getCoalition(); std::ostringstream stream; stream << playerCoalition; std::string playerCoalitionString = stream.str(); @@ -32,8 +30,8 @@ TEST(GameFormulaParserTest, PlayersCoalitionTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - auto const& gameFormula = formula->asGameFormula(); - auto const& playerCoalition = gameFormula.getCoalition(); + EXPECT_TRUE(formula->isGameFormula()); + auto const& playerCoalition = formula->asGameFormula().getCoalition(); EXPECT_EQ(5ul, playerCoalition.getPlayers().size()); std::ostringstream stream; @@ -50,12 +48,11 @@ TEST(GameFormulaParserTest, ProbabilityOperatorTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - auto const& gameFormula = formula->asGameFormula(); - auto const& probFormula = gameFormula.getSubformula(); - - EXPECT_TRUE(probFormula.isProbabilityOperatorFormula()); - EXPECT_FALSE(probFormula.asProbabilityOperatorFormula().hasBound()); - EXPECT_TRUE(probFormula.asProbabilityOperatorFormula().hasOptimalityType()); + EXPECT_TRUE(formula->isGameFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().hasBound()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().hasOptimalityType()); } TEST(GameFormulaParserTest, NextOperatorTest) { @@ -68,29 +65,23 @@ TEST(GameFormulaParserTest, NextOperatorTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isGameFormula()); - auto const& gameFormula1 = formula->asGameFormula(); - auto const& probFormula1 = gameFormula1.getSubformula(); - EXPECT_TRUE(probFormula1.isProbabilityOperatorFormula()); - auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); - EXPECT_TRUE(rawFormula1.isNextFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula()); input = "<> Pmin=? [X !x ]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isGameFormula()); - auto const& gameFormula2 = formula->asGameFormula(); - auto const& probFormula2 = gameFormula2.getSubformula(); - EXPECT_TRUE(probFormula2.isProbabilityOperatorFormula()); - auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); - EXPECT_TRUE(rawFormula2.isNextFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula()); input = "<> Pmax=? [ X a>5 ]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isGameFormula()); - auto const& gameFormula3 = formula->asGameFormula(); - auto const& probFormula3 = gameFormula3.getSubformula(); - EXPECT_TRUE(probFormula3.isProbabilityOperatorFormula()); - auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); - EXPECT_TRUE(rawFormula3.isNextFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula()); } TEST(GameFormulaParserTest, UntilOperatorTest) { @@ -100,39 +91,33 @@ TEST(GameFormulaParserTest, UntilOperatorTest) { std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isGameFormula()); - auto const& gameFormula1 = formula->asGameFormula(); - auto const& probFormula1 = gameFormula1.getSubformula(); - EXPECT_TRUE(probFormula1.isProbabilityOperatorFormula()); - auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); - EXPECT_TRUE(rawFormula1.isUntilFormula()); - EXPECT_FALSE(rawFormula1.isBoundedUntilFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isUntilFormula()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula()); input = "<

> Pmax=? [ \"a\" U <= 4 \"b\" ]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isGameFormula()); - auto const& gameFormula2 = formula->asGameFormula(); - auto const& probFormula2 = gameFormula2.getSubformula(); - EXPECT_TRUE(probFormula2.isProbabilityOperatorFormula()); - auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); - EXPECT_TRUE(rawFormula2.isBoundedUntilFormula()); - EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); - EXPECT_FALSE(rawFormula2.asBoundedUntilFormula().hasLowerBound()); - EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().hasUpperBound()); - EXPECT_EQ(4, rawFormula2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasLowerBound()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasUpperBound()); + EXPECT_EQ(4, formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt()); input = "<> Pmin=? [ \"a\" & \"b\" U [5,9] \"c\" ] "; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isGameFormula()); - auto const& gameFormula3 = formula->asGameFormula(); - auto const& probFormula3 = gameFormula3.getSubformula(); - EXPECT_TRUE(probFormula3.isProbabilityOperatorFormula()); - auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); - EXPECT_TRUE(rawFormula3.isBoundedUntilFormula()); - EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); - EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().hasLowerBound()); - EXPECT_EQ(5, rawFormula3.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); - EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().hasUpperBound()); - EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); + EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasLowerBound()); + EXPECT_EQ(5, formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasUpperBound()); + EXPECT_EQ(9, formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt()); } TEST(GameFormulaParserTest, RewardOperatorTest) { @@ -145,6 +130,7 @@ TEST(GameFormulaParserTest, RewardOperatorTest) { EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula()); EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); input = "<> R=? [I=10]"; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -153,6 +139,7 @@ TEST(GameFormulaParserTest, RewardOperatorTest) { EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType()); EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); } TEST(GameFormulaParserTest, ConditionalProbabilityTest) { @@ -165,6 +152,7 @@ TEST(GameFormulaParserTest, ConditionalProbabilityTest) { EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asGameFormula().getSubformula().asProbabilityOperatorFormula(); EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); } TEST(GameFormulaParserTest, NestedPathFormulaTest) { @@ -177,6 +165,7 @@ TEST(GameFormulaParserTest, NestedPathFormulaTest) { EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula()); + EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl())); } TEST(GameFormulaParserTest, CommentTest) { @@ -222,6 +211,7 @@ TEST(GameFormulaParserTest, MultiObjectiveFormulaTest) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); ASSERT_TRUE(formula->isMultiObjectiveFormula()); storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula(); + EXPECT_FALSE(formula->isInFragment(storm::logic::rpatl())); ASSERT_EQ(3ull, mof.getNumberOfSubformulas()); ASSERT_TRUE(mof.getSubformula(0).isGameFormula()); From 45e660fe9b40e053f2b851981c3eb4c5793a3f44 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 11:08:08 +0200 Subject: [PATCH 28/59] added parser tests for game shields GameShieldingParserTest.cpp --- .../storm/parser/GameShieldingParserTest.cpp | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 src/test/storm/parser/GameShieldingParserTest.cpp diff --git a/src/test/storm/parser/GameShieldingParserTest.cpp b/src/test/storm/parser/GameShieldingParserTest.cpp new file mode 100644 index 000000000..53ae456a7 --- /dev/null +++ b/src/test/storm/parser/GameShieldingParserTest.cpp @@ -0,0 +1,81 @@ +#include "test/storm_gtest.h" +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/FragmentSpecification.h" +#include "storm/storage/expressions/ExpressionManager.h" + +TEST(GameShieldingParserTest, PreSafetyShieldTest) { + storm::parser::FormulaParser formulaParser; + + std::string filename = "preSafetyShieldFileName"; + std::string value = "0.9"; + std::string input = "<" + filename + ", PreSafety, lambda=" + value + "> <> Pmax=? [F \"label\"]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr shieldExpression(nullptr); + ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); + EXPECT_TRUE(shieldExpression->isPreSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isOptimalShield()); + EXPECT_TRUE(shieldExpression->isRelative()); + EXPECT_EQ(std::stod(value), shieldExpression->getValue()); + EXPECT_EQ(filename, shieldExpression->getFilename()); +} + +TEST(GameShieldingParserTest, PostSafetyShieldTest) { + storm::parser::FormulaParser formulaParser; + + std::string filename = "postSafetyShieldFileName"; + std::string value = "0.7569"; + std::string input = "<" + filename + ", PostSafety, gamma=" + value + "> <> Pmin=? [X !\"label\"]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr shieldExpression(nullptr); + ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); + EXPECT_FALSE(shieldExpression->isPreSafetyShield()); + EXPECT_TRUE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isOptimalShield()); + EXPECT_FALSE(shieldExpression->isRelative()); + EXPECT_EQ(std::stod(value), shieldExpression->getValue()); + EXPECT_EQ(filename, shieldExpression->getFilename()); +} + +TEST(GameShieldingParserTest, OptimalShieldTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareIntegerVariable("x"); + manager->declareIntegerVariable("y"); + + storm::parser::FormulaParser formulaParser(manager); + + std::string filename = "optimalShieldFileName"; + std::string input = "<" + filename + ", Optimal> <> Pmax=? [G x>y]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr shieldExpression(nullptr); + ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); + EXPECT_FALSE(shieldExpression->isPreSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_TRUE(shieldExpression->isOptimalShield()); + EXPECT_FALSE(shieldExpression->isRelative()); + EXPECT_EQ(filename, shieldExpression->getFilename()); +} \ No newline at end of file From cdc0fd2873ad8ff74b6ad5d78fe91fc6b309b770 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 11:16:06 +0200 Subject: [PATCH 29/59] added parser tests for mdp shields MdpShieldingParserTest.cpp --- .../storm/parser/MdpShieldingParserTest.cpp | 72 +++++++++++++++++++ 1 file changed, 72 insertions(+) create mode 100644 src/test/storm/parser/MdpShieldingParserTest.cpp diff --git a/src/test/storm/parser/MdpShieldingParserTest.cpp b/src/test/storm/parser/MdpShieldingParserTest.cpp new file mode 100644 index 000000000..2baf68f30 --- /dev/null +++ b/src/test/storm/parser/MdpShieldingParserTest.cpp @@ -0,0 +1,72 @@ +#include "test/storm_gtest.h" +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/FragmentSpecification.h" +#include "storm/storage/expressions/ExpressionManager.h" + +TEST(MdpShieldingParserTest, PreSafetyShieldTest) { + storm::parser::FormulaParser formulaParser; + + std::string filename = "preSafetyShieldFileName"; + std::string value = "0.6667"; + std::string input = "<" + filename + ", PreSafety, gamma=" + value + "> Pmax=? [F \"label\"]"; + + std::shared_ptr formula(nullptr); + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr shieldExpression(nullptr); + ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); + EXPECT_TRUE(shieldExpression->isPreSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isOptimalShield()); + EXPECT_FALSE(shieldExpression->isRelative()); + EXPECT_EQ(std::stod(value), shieldExpression->getValue()); + EXPECT_EQ(filename, shieldExpression->getFilename()); +} + +TEST(MdpShieldingParserTest, PostSafetyShieldTest) { + storm::parser::FormulaParser formulaParser; + + std::string filename = "postSafetyShieldFileName"; + std::string value = "0.95"; + std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]"; + + std::shared_ptr formula(nullptr); + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr shieldExpression(nullptr); + ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); + EXPECT_FALSE(shieldExpression->isPreSafetyShield()); + EXPECT_TRUE(shieldExpression->isPostSafetyShield()); + EXPECT_FALSE(shieldExpression->isOptimalShield()); + EXPECT_TRUE(shieldExpression->isRelative()); + EXPECT_EQ(std::stod(value), shieldExpression->getValue()); + EXPECT_EQ(filename, shieldExpression->getFilename()); +} + +TEST(MdpShieldingParserTest, OptimalShieldTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("a"); + manager->declareIntegerVariable("x"); + + storm::parser::FormulaParser formulaParser(manager); + + std::string filename = "optimalShieldFileName"; + std::string input = "<" + filename + ", Optimal> Pmax=? [G (a|x>3)]"; + + std::shared_ptr formula(nullptr); + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr shieldExpression(nullptr); + ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression()); + EXPECT_FALSE(shieldExpression->isPreSafetyShield()); + EXPECT_FALSE(shieldExpression->isPostSafetyShield()); + EXPECT_TRUE(shieldExpression->isOptimalShield()); + EXPECT_FALSE(shieldExpression->isRelative()); + EXPECT_EQ(filename, shieldExpression->getFilename()); +} \ No newline at end of file From 2064cbb0a9e49060c0991818dfc5e98f9c507d1c Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 15:41:26 +0200 Subject: [PATCH 30/59] fix for the NativeMultiplier in case of having coalitionStates (games) --- src/storm/storage/SparseMatrix.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 228fb4604..365535951 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1754,6 +1754,7 @@ namespace storm { template void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { + std::cout << *dirOverride << std::endl; if(dirOverride && !dirOverride->empty()) { if (dir == OptimizationDirection::Minimize) { multiplyAndReduceForward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); @@ -1848,11 +1849,11 @@ namespace storm { // Finally write value to target vector. *resultIt = currentValue; if(dirOverridden) { - if (choices && dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) { + if (choices && (dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue))) { *choiceIt = selectedChoice; } } else { - if (choices && compare(currentValue, oldSelectedChoiceValue)) { + if (choices && (compare(currentValue, oldSelectedChoiceValue))) { *choiceIt = selectedChoice; } } @@ -2129,8 +2130,7 @@ namespace storm { } else { target = &result; } - - this->multiplyAndReduceForward(dir, rowGroupIndices, vector, summand, *target, choices); + this->multiplyAndReduceForward(dir, rowGroupIndices, vector, summand, *target, choices, dirOverride); if (target == &temporary) { std::swap(temporary, result); From 229097d8487c8e6211a8c259f6b5f31884c7b9f9 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 15:46:36 +0200 Subject: [PATCH 31/59] removed debug output --- src/storm/storage/SparseMatrix.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 365535951..08161b04e 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1754,7 +1754,6 @@ namespace storm { template void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { - std::cout << *dirOverride << std::endl; if(dirOverride && !dirOverride->empty()) { if (dir == OptimizationDirection::Minimize) { multiplyAndReduceForward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); From d70c73370977b6fa78f4334a4aefd86316cfd3b3 Mon Sep 17 00:00:00 2001 From: lukpo Date: Mon, 23 Aug 2021 15:26:34 +0200 Subject: [PATCH 32/59] removed comments for results in SmgRpatlModelCheckerTest.cpp --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 67fd4336a..b3c4bbcb7 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -196,43 +196,43 @@ namespace { std::unique_ptr result; // NEXT results - result = checker->check(this->env(), tasks[0]); //OK + result = checker->check(this->env(), tasks[0]); EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[1]); //OK + result = checker->check(this->env(), tasks[1]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); //OK + result = checker->check(this->env(), tasks[2]); EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[3]); //OK + result = checker->check(this->env(), tasks[3]); EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); // UNTIL results - result = checker->check(this->env(), tasks[4]); //FAIL -> 0.99999922964892118 this may happen if the walker does not get caught in s4 + result = checker->check(this->env(), tasks[4]); EXPECT_NEAR(this->parseNumber("0.52"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[5]); //OK + result = checker->check(this->env(), tasks[5]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[6]); //OK + result = checker->check(this->env(), tasks[6]); EXPECT_NEAR(this->parseNumber("0.9999996417"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[7]); //OK + result = checker->check(this->env(), tasks[7]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); // GLOBALLY tests - result = checker->check(this->env(), tasks[8]); //FAIL -> 2.686012256170045e-06 this may happen if the walker does not stay in s0 + result = checker->check(this->env(), tasks[8]); EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[9]); //FAIL -> 1 this is maybe exactly the other way round (by minimizing leaving) + result = checker->check(this->env(), tasks[9]); EXPECT_NEAR(this->parseNumber("0.65454565"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[10]); //FAIL -> 7.7035107881595621e-07 + result = checker->check(this->env(), tasks[10]); EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[11]); //FAIL -> 1 + result = checker->check(this->env(), tasks[11]); EXPECT_NEAR(this->parseNumber("0.48"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); // EVENTUALLY tests - result = checker->check(this->env(), tasks[12]); //FAIL -> 0.99999731398774383 + result = checker->check(this->env(), tasks[12]); EXPECT_NEAR(this->parseNumber("0.34545435"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[13]); //OK + result = checker->check(this->env(), tasks[13]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[14]); //FAIL -> 0.63359999999999994 here is maybe an offset of 1 step + result = checker->check(this->env(), tasks[14]); EXPECT_NEAR(this->parseNumber("0.576"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[15]); //FAIL -> 0.64511999999999992 + result = checker->check(this->env(), tasks[15]); EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } From 28f1c9d368b40b424a0d7df8a3c3e8706f39fab4 Mon Sep 17 00:00:00 2001 From: lukpo Date: Mon, 23 Aug 2021 15:27:08 +0200 Subject: [PATCH 33/59] removed DEBUG for multiplier type in SparseSmgRpatlHelper.cpp --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 60af5b2d0..2a352c381 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -18,15 +18,6 @@ namespace storm { // TODO add Kwiatkowska original reference auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - //solverEnv.solver().multiplier().setType(storm::solver::MultiplierType::Native); - - if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Native) { - STORM_LOG_DEBUG("Multiplier type = Native"); - } else if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Gmmxx) { - STORM_LOG_DEBUG("Multiplier type = Gmmxx"); - } else { - STORM_LOG_DEBUG("Multiplier type unknown"); - } // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; @@ -62,14 +53,6 @@ namespace storm { } } - if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Native) { - STORM_LOG_DEBUG("Multiplier type = Native"); - } else if(solverEnv.solver().multiplier().getType() == storm::solver::MultiplierType::Gmmxx) { - STORM_LOG_DEBUG("Multiplier type = Gmmxx"); - } else { - STORM_LOG_DEBUG("Multiplier type unknown"); - } - // Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default) storm::utility::vector::setVectorValues(result, relevantStates, x); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); From 4f4abf2342aff15e3e23e67dad54747907e1de13 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 24 Aug 2021 10:34:16 +0200 Subject: [PATCH 34/59] added testcase messageHack (messageHack.nm) to SmgRpatlModelCheckerTest.cpp --- .../examples/testfiles/smg/messageHack.nm | 52 +++++++++++++++ .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 65 +++++++++++++++++++ 2 files changed, 117 insertions(+) create mode 100644 resources/examples/testfiles/smg/messageHack.nm diff --git a/resources/examples/testfiles/smg/messageHack.nm b/resources/examples/testfiles/smg/messageHack.nm new file mode 100644 index 000000000..e67352bef --- /dev/null +++ b/resources/examples/testfiles/smg/messageHack.nm @@ -0,0 +1,52 @@ +// PRISM Model of hacking a communication +// - Bob and Alice are chatting. +// - Eve wants to hack the messages from Bob. +// - The propability of successfull hacking is 0.05. + +smg + +player bob + [receiveB], [readWriteB], [sendB], [waitB] +endplayer + +player alice + [receiveA], [readWriteA], [sendA], [waitA] +endplayer + +player eve + [hackE], [waitE] +endplayer + +// 0 bob, 1 eve, 2 alice +global move : [0..2] init 0; +// +global bobSent : [0..1] init 0; +global hacked : [0..1] init 0; + +label "hacked" = hacked=1; + +module communication + bobReceived : [0..1] init 0; + bobWroteMessage : [0..1] init 1; + aliceReceived : [0..1] init 0; + aliceWroteMessage : [0..1] init 0; + aliceSent : [0..1] init 0; + + // bob's communication part + [receiveB] move=0 & aliceSent=1 -> (bobReceived'=1) & (aliceSent'=0) & (move'=1); + [readWriteB] move=0 & bobReceived=1 -> (bobWroteMessage'=1) & (bobReceived'=0) & (move'=1); + [sendB] move=0 & bobWroteMessage=1 -> (bobSent'=1) & (bobWroteMessage'=0) & (move'=1); + [waitB] move=0 & !(aliceSent=1 | bobReceived=1 | bobWroteMessage=1) -> (move'=1); + + // alice's communication part + [receiveA] move=2 & bobSent=1 -> (aliceReceived'=1) & (bobSent'=0) & (move'=0); + [readWriteA] move=2 & aliceReceived=1 -> (aliceWroteMessage'=1) & (aliceReceived'=0) & (move'=0); + [sendA] move=2 & aliceWroteMessage=1 -> (aliceSent'=1) & (aliceWroteMessage'=0) & (move'=0); + [waitA] move=2 & !(bobSent=1 | aliceReceived=1 | aliceWroteMessage=1) -> (move'=0); + +endmodule + +module hacking + [hackE] move=1 & bobSent=1 -> 0.05: (hacked'=1) & (move'=2) + 0.95: (move'=2); + [waitE] move=1 & !(bobSent=1) -> (move'=2); +endmodule diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index b3c4bbcb7..63fc4e1b4 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -235,6 +235,71 @@ namespace { result = checker->check(this->env(), tasks[15]); EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) { + // This test is for borders of bounded U with conversations from G and F + // bounded G + std::string formulasString = "<> Pmax=? [ G !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=1 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=2 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=10 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=17 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=32 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=47 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=61 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=62 !\"hacked\" ]"; + + // bounded F + formulasString += "; <> Pmin=? [ F \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [1,2] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [3,16] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [0,17] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [17,31] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [17,32] \"hacked\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/messageHack.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(30ul, model->getNumberOfStates()); + EXPECT_EQ(31ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // bounded G results + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1.99379598e-05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("0.9025"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.857375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[6]); + EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[7]); + EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[8]); + EXPECT_NEAR(this->parseNumber("0.7737809375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + // bounded F results + result = checker->check(this->env(), tasks[9]); + EXPECT_NEAR(this->parseNumber("0.999980062"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[10]); + EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[11]); + EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[12]); + EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[13]); + EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[14]); + EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + // TODO: create more test cases (files) } From bec28d55c602b71c93a6f289b02821054cdcf355 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 24 Aug 2021 15:02:33 +0200 Subject: [PATCH 35/59] added testcase rightDecision (rightDecision.nm) to SmgRpatlModelCheckerTest.cpp --- .../examples/testfiles/smg/rightDecision.nm | 42 ++++++++++++++++ .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 49 +++++++++++++++++++ 2 files changed, 91 insertions(+) create mode 100644 resources/examples/testfiles/smg/rightDecision.nm diff --git a/resources/examples/testfiles/smg/rightDecision.nm b/resources/examples/testfiles/smg/rightDecision.nm new file mode 100644 index 000000000..a47222e10 --- /dev/null +++ b/resources/examples/testfiles/smg/rightDecision.nm @@ -0,0 +1,42 @@ +// PRISM Model of a decision for a shortcut +// - A hiker has to make a decision of taking a shortcut. +// - On the shortcut a native can be asked for getting to the target waypoint. +// - The native can lead the hiker to the goal or can give a proposal for getting to 0.9 to the target. + +smg + +player hiker + [startShortcut], [startWay], [waypoint1], [waypoint2target], [waypoint2start], [target], [lost] +endplayer + +player native + [wait], [shortcutBad], [shortcutGood] +endplayer + +// 0 bob, 1 native, +global move : [0..1] init 0; + +global shortcut : [0..1] init 0; +global target : [0..1] init 0; +global lost : [0..1] init 0; + +label "target" = target=1; + +module hikerModule + startpoint : [0..1] init 1; + waypoints : [0..2] init 0; + + [startShortcut] move=0 & startpoint=1 -> (shortcut'=1) & (startpoint'=0) & (move'=1); + [startWay] move=0 & startpoint=1 -> (waypoints'=1) & (startpoint'=0) & (move'=1); + [waypoint1] move=0 & waypoints=1 -> (waypoints'=2) & (move'=1); + [waypoint2target] move=0 & waypoints=2 -> (waypoints'=0) & (target'=1) & (move'=1); + [waypoint2start] move=0 & waypoints=2 -> (waypoints'=0) & (startpoint'=1) & (move'=1); + [target] move=0 & target=1 -> (move'=1); + [lost] move=0 & lost=1 -> (move'=1); +endmodule + +module nativeModule + [wait] move=1 & !(shortcut=1) -> (move'=0); + [shortcutBad] move=1 & shortcut=1 -> 0.9: (shortcut'=0) & (target'=1) & (move'=0) + 0.1: (shortcut'=0) & (lost'=1) & (move'=0); + [shortcutGood] move=1 & shortcut=1 -> (shortcut'=0) & (target'=1) & (move'=0); +endmodule diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 63fc4e1b4..34a805537 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -300,6 +300,55 @@ namespace { EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, RightDecision) { + // This test is for making decisions and creating shields + // testing probabilities for decisions + std::string formulasString = "<> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + + // testing create shielding expressions + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(11ul, model->getNumberOfStates()); + EXPECT_EQ(15ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // probability results + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.9"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + // shielding results + result = checker->check(this->env(), tasks[4]); + result = checker->check(this->env(), tasks[5]); + result = checker->check(this->env(), tasks[6]); + result = checker->check(this->env(), tasks[7]); + result = checker->check(this->env(), tasks[8]); + result = checker->check(this->env(), tasks[9]); + result = checker->check(this->env(), tasks[10]); + result = checker->check(this->env(), tasks[11]); + + //TODO: check the shields + } // TODO: create more test cases (files) } From 02464909a455289e643a773ff6462ce79b81ee12 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 24 Aug 2021 15:03:16 +0200 Subject: [PATCH 36/59] removed unused method getQualitativeResultAtInitialState --- .../modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 34a805537..a55413e98 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -130,12 +130,6 @@ namespace { } } -/* bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { - auto filter = getInitialStateFilter(model); - result->filter(*filter); - return result->asQualitativeCheckResult().forallTrue(); - }*/ - ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { auto filter = getInitialStateFilter(model); result->filter(*filter); From 4cfbaa3a3367b4f49732a041b419d3f741929ce9 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 10:26:51 +0200 Subject: [PATCH 37/59] removed shielding tests from SmgRpatlModelCheckerTest.cpp --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 24 +------------------ 1 file changed, 1 insertion(+), 23 deletions(-) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index a55413e98..f46106a91 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -295,23 +295,13 @@ namespace { } TYPED_TEST(SmgRpatlModelCheckerTest, RightDecision) { - // This test is for making decisions and creating shields + // This test is for making decisions // testing probabilities for decisions std::string formulasString = "<> Pmax=? [ F <=3 \"target\" ]"; formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; formulasString += "; <> Pmin=? [ F \"target\" ]"; - // testing create shielding expressions - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmin=? [ F \"target\" ]"; - formulasString += "; <> Pmin=? [ F \"target\" ]"; - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); auto model = std::move(modelFormulas.first); auto tasks = this->getTasks(modelFormulas.second); @@ -330,18 +320,6 @@ namespace { EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); result = checker->check(this->env(), tasks[3]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - // shielding results - result = checker->check(this->env(), tasks[4]); - result = checker->check(this->env(), tasks[5]); - result = checker->check(this->env(), tasks[6]); - result = checker->check(this->env(), tasks[7]); - result = checker->check(this->env(), tasks[8]); - result = checker->check(this->env(), tasks[9]); - result = checker->check(this->env(), tasks[10]); - result = checker->check(this->env(), tasks[11]); - - //TODO: check the shields } // TODO: create more test cases (files) From c55e4920b268eb99939f2fe35227b342378fbfa8 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 10:28:05 +0200 Subject: [PATCH 38/59] WIP created ShieldGenerationSmgRpatlModelCheckerTest.cpp for testing the generation of shielding files for SMGs --- ...ieldGenerationSmgRpatlModelCheckerTest.cpp | 137 ++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp new file mode 100644 index 000000000..037af55d7 --- /dev/null +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -0,0 +1,137 @@ +#include +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + +#include "storm/models/sparse/Smg.h" +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + class DoubleViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + template + class ShieldGenerationSmgRpatlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + ShieldGenerationSmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + + std::pair>, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair>, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as>(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + DoubleViEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(ShieldGenerationSmgRpatlModelCheckerTest, TestingTypes,); + + TYPED_TEST(ShieldGenerationSmgRpatlModelCheckerTest, RightDecision) { + typedef typename TestFixture::ValueType ValueType; + + // testing that no shield is created + std::string formulasString = "<> Pmax=? [ F <=3 \"target\" ]"; + + // testing create shielding expressions + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); + auto smg = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(11ul, smg->getNumberOfStates()); + EXPECT_EQ(15ul, smg->getNumberOfTransitions()); + ASSERT_EQ(smg->getType(), storm::models::ModelType::Smg); + EXPECT_EQ(14ull, smg->getNumberOfChoices()); + + //std::unique_ptr result; + storm::modelchecker::SparseSmgRpatlModelChecker> checker(*smg); + + // first result must not be a shielding result + auto result = checker.check(this->env(), tasks[0]); + EXPECT_FALSE( tasks[1].isShieldingTask()); + + // shielding results + storm::logic::ShieldingType type = storm::logic::ShieldingType::PreSafety; + std::string filename = "preSafetyShieldLambda1"; + storm::logic::ShieldComparison comparison = storm::logic::ShieldComparison::Relative; + double value = 0.9; + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(type, filename, comparison, value)); + tasks[1].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[1].isShieldingTask()); + + result = checker.check(this->env(), tasks[1]); + + filename += ".shield"; + std::ifstream resultFile(filename); + std::stringstream resultBuffer; + resultBuffer << resultFile.rdbuf(); + std::string resultString = resultBuffer.str(); + std::cout << resultString << std::endl; + std::remove(filename.c_str()); + // THIS WORKS!! + + //TODO: EXPECT_EQUAL: string from solution and string from comparison-file + + // TODO: build back the values, e.g. we do not need a method for computing string-shields + // - testfiles for comparison, make an folder for that and name it like the test case names + // - this also would work fine fith mdps, so finish this example, add it to mdp folder + // - then we can go to solve examples, we have to integrate a lot of examples... + + result = checker.check(this->env(), tasks[2]); + result = checker.check(this->env(), tasks[3]); + result = checker.check(this->env(), tasks[4]); + result = checker.check(this->env(), tasks[5]); + result = checker.check(this->env(), tasks[6]); + result = checker.check(this->env(), tasks[7]); + result = checker.check(this->env(), tasks[8]); + } + + // TODO: create more test cases (files) +} From 2ecf7ff1380db553235e700febf50be22c3863e9 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 15:06:22 +0200 Subject: [PATCH 39/59] Added Shield Test to ShieldGenerationSmgRpatlModelCheckerTest.cpp with files to compare --- ...ightDecisionPostSafetyGamma05PmaxF5.shield | 7 + ...ightDecisionPostSafetyGamma05PminF5.shield | 6 + ...ightDecisionPostSafetyGamma09PmaxF3.shield | 7 + ...ightDecisionPostSafetyGamma09PminF3.shield | 6 + ...ghtDecisionPostSafetyLambda05PmaxF5.shield | 8 + ...ghtDecisionPostSafetyLambda05PminF5.shield | 8 + ...ghtDecisionPostSafetyLambda09PmaxF3.shield | 8 + ...ghtDecisionPostSafetyLambda09PminF3.shield | 8 + ...rightDecisionPreSafetyGamma05PmaxF5.shield | 7 + ...rightDecisionPreSafetyGamma05PminF5.shield | 6 + ...rightDecisionPreSafetyGamma09PmaxF3.shield | 7 + ...rightDecisionPreSafetyGamma09PminF3.shield | 6 + ...ightDecisionPreSafetyLambda05PmaxF5.shield | 8 + ...ightDecisionPreSafetyLambda05PminF5.shield | 8 + ...ightDecisionPreSafetyLambda09PmaxF3.shield | 8 + ...ightDecisionPreSafetyLambda09PminF3.shield | 8 + ...ieldGenerationSmgRpatlModelCheckerTest.cpp | 195 ++++++++++++++---- 17 files changed, 276 insertions(+), 35 deletions(-) create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield create mode 100644 resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield new file mode 100644 index 000000000..73f8c1342 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.500000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield new file mode 100644 index 000000000..c5e6ddce1 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.500000): +model state: correction [: ()}: + 4 0: 0 + 5 0: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield new file mode 100644 index 000000000..b8cf860c2 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.900000): +model state: correction [: ()}: + 0 0: 0; 1: 0 + 5 0: 0 + 9 0: 0; 1: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield new file mode 100644 index 000000000..dbdb1771a --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.900000): +model state: correction [: ()}: + 4 0: 0 + 5 0: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield new file mode 100644 index 000000000..6385fca02 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.500000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield new file mode 100644 index 000000000..6385fca02 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.500000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield new file mode 100644 index 000000000..c115a997a --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.900000): +model state: correction [: ()}: + 0 0: 0; 1: 0 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield new file mode 100644 index 000000000..24a913b11 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.900000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield new file mode 100644 index 000000000..083d98dc2 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Pre-Safety-Shield with absolute comparison (gamma = 0.500000): +model state: choice(s) [: ()}: + 0 0.9: (0); 1: (1) + 5 1: (0) + 9 1: (0); 0.9: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield new file mode 100644 index 000000000..854110128 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Pre-Safety-Shield with absolute comparison (gamma = 0.500000): +model state: choice(s) [: ()}: + 4 0: (0) + 5 0: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield new file mode 100644 index 000000000..5cc5423f1 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Pre-Safety-Shield with absolute comparison (gamma = 0.900000): +model state: choice(s) [: ()}: + 0 0.9: (0) + 5 1: (0) + 9 1: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield new file mode 100644 index 000000000..5afcb6598 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Pre-Safety-Shield with absolute comparison (gamma = 0.900000): +model state: choice(s) [: ()}: + 4 0: (0) + 5 0: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield new file mode 100644 index 000000000..f38157e63 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Pre-Safety-Shield with relative comparison (lambda = 0.500000): +model state: choice(s) [: ()}: + 0 0.9: (0); 1: (1) + 4 0: (0) + 5 1: (0) + 9 1: (0); 0.9: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield new file mode 100644 index 000000000..363275926 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Pre-Safety-Shield with relative comparison (lambda = 0.500000): +model state: choice(s) [: ()}: + 0 0: (1) + 4 0: (0) + 5 0: (0) + 9 0: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield new file mode 100644 index 000000000..0f9beb691 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Pre-Safety-Shield with relative comparison (lambda = 0.900000): +model state: choice(s) [: ()}: + 0 0.9: (0) + 4 0: (0) + 5 1: (0) + 9 1: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield new file mode 100644 index 000000000..eb3d29cd3 --- /dev/null +++ b/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Pre-Safety-Shield with relative comparison (lambda = 0.900000): +model state: choice(s) [: ()}: + 0 0: (1) + 4 0: (0) + 5 0: (0) + 9 0: (1) +___________________________________________________________________ diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index 037af55d7..0410c671f 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -69,18 +69,43 @@ namespace { TYPED_TEST(ShieldGenerationSmgRpatlModelCheckerTest, RightDecision) { typedef typename TestFixture::ValueType ValueType; - // testing that no shield is created - std::string formulasString = "<> Pmax=? [ F <=3 \"target\" ]"; + // definition of shield file names + std::vector fileNames; + fileNames.push_back("rightDecisionPreSafetyLambda09PmaxF3"); + fileNames.push_back("rightDecisionPreSafetyLambda09PminF3"); + fileNames.push_back("rightDecisionPreSafetyGamma09PmaxF3"); + fileNames.push_back("rightDecisionPreSafetyGamma09PminF3"); + fileNames.push_back("rightDecisionPostSafetyLambda09PmaxF3"); + fileNames.push_back("rightDecisionPostSafetyLambda09PminF3"); + fileNames.push_back("rightDecisionPostSafetyGamma09PmaxF3"); + fileNames.push_back("rightDecisionPostSafetyGamma09PminF3"); + fileNames.push_back("rightDecisionPreSafetyLambda05PmaxF5"); + fileNames.push_back("rightDecisionPreSafetyLambda05PminF5"); + fileNames.push_back("rightDecisionPreSafetyGamma05PmaxF5"); + fileNames.push_back("rightDecisionPreSafetyGamma05PminF5"); + fileNames.push_back("rightDecisionPostSafetyLambda05PmaxF5"); + fileNames.push_back("rightDecisionPostSafetyLambda05PminF5"); + fileNames.push_back("rightDecisionPostSafetyGamma05PmaxF5"); + fileNames.push_back("rightDecisionPostSafetyGamma05PminF5"); // testing create shielding expressions - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <> Pmin=? [ F \"target\" ]"; - formulasString += "; <> Pmin=? [ F \"target\" ]"; + std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[2] + ", PreSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[6] + ", PostSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + + formulasString += "; <" + fileNames[8] + ", PreSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[10] + ", PreSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[12] + ", PostSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[14] + ", PostSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); auto smg = std::move(modelFormulas.first); @@ -93,44 +118,144 @@ namespace { //std::unique_ptr result; storm::modelchecker::SparseSmgRpatlModelChecker> checker(*smg); - // first result must not be a shielding result - auto result = checker.check(this->env(), tasks[0]); - EXPECT_FALSE( tasks[1].isShieldingTask()); + // definitions + storm::logic::ShieldingType typePreSafety = storm::logic::ShieldingType::PreSafety; + storm::logic::ShieldingType typePostSafety = storm::logic::ShieldingType::PostSafety; + storm::logic::ShieldComparison comparisonRelative = storm::logic::ShieldComparison::Relative; + storm::logic::ShieldComparison comparisonAbsolute = storm::logic::ShieldComparison::Absolute; + double value09 = 0.9; + double value05 = 0.5; + std::string filename, shieldingString, compareFileString; // shielding results - storm::logic::ShieldingType type = storm::logic::ShieldingType::PreSafety; - std::string filename = "preSafetyShieldLambda1"; - storm::logic::ShieldComparison comparison = storm::logic::ShieldComparison::Relative; - double value = 0.9; - auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(type, filename, comparison, value)); + filename = fileNames[0]; + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09)); + tasks[0].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[0].isShieldingTask()); + auto result = checker.check(this->env(), tasks[0]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[1]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09)); tasks[1].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[1].isShieldingTask()); - result = checker.check(this->env(), tasks[1]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); - filename += ".shield"; - std::ifstream resultFile(filename); - std::stringstream resultBuffer; - resultBuffer << resultFile.rdbuf(); - std::string resultString = resultBuffer.str(); - std::cout << resultString << std::endl; - std::remove(filename.c_str()); - // THIS WORKS!! - - //TODO: EXPECT_EQUAL: string from solution and string from comparison-file - - // TODO: build back the values, e.g. we do not need a method for computing string-shields - // - testfiles for comparison, make an folder for that and name it like the test case names - // - this also would work fine fith mdps, so finish this example, add it to mdp folder - // - then we can go to solve examples, we have to integrate a lot of examples... - + filename = fileNames[2]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09)); + tasks[2].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[2].isShieldingTask()); result = checker.check(this->env(), tasks[2]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[3]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09)); + tasks[3].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[3].isShieldingTask()); result = checker.check(this->env(), tasks[3]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[4]; + auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09)); + tasks[4].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[4].isShieldingTask()); result = checker.check(this->env(), tasks[4]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[5]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09)); + tasks[5].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[5].isShieldingTask()); result = checker.check(this->env(), tasks[5]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[6]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09)); + tasks[6].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[6].isShieldingTask()); result = checker.check(this->env(), tasks[6]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[7]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09)); + tasks[7].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[7].isShieldingTask()); result = checker.check(this->env(), tasks[7]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + + filename = fileNames[8]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05)); + tasks[8].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[8].isShieldingTask()); result = checker.check(this->env(), tasks[8]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[9]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05)); + tasks[9].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[9].isShieldingTask()); + result = checker.check(this->env(), tasks[9]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[10]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05)); + tasks[10].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[10].isShieldingTask()); + result = checker.check(this->env(), tasks[10]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[11]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05)); + tasks[11].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[11].isShieldingTask()); + result = checker.check(this->env(), tasks[11]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[12]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05)); + tasks[12].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[12].isShieldingTask()); + result = checker.check(this->env(), tasks[12]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[13]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05)); + tasks[13].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[13].isShieldingTask()); + result = checker.check(this->env(), tasks[13]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[14]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05)); + tasks[14].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[14].isShieldingTask()); + result = checker.check(this->env(), tasks[14]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[15]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05)); + tasks[15].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[15].isShieldingTask()); + result = checker.check(this->env(), tasks[15]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); } // TODO: create more test cases (files) From 4925135f8781cec002be5e30b117c5f87c4c6e12 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 15:07:28 +0200 Subject: [PATCH 40/59] added conversion methods for ShieldGenerationSmgRpatlModelCheckerTest.cpp --- ...hieldGenerationSmgRpatlModelCheckerTest.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index 0410c671f..f9b75c7dd 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -56,8 +56,26 @@ namespace { ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + void convertShieldingFileToString(std::string filename, std::string &shieldingString) { + filename += shieldEnding; + std::ifstream resultFile(filename); + std::stringstream resultBuffer; + resultBuffer << resultFile.rdbuf(); + shieldingString = resultBuffer.str(); + } + + void getStringsToCompare(std::string filename, std::string &shieldingString, std::string &compareFileString) { + this->convertShieldingFileToString(filename, shieldingString); + std::string compareFileName = STORM_TEST_RESOURCES_DIR "/smg-shields/" + filename; + this->convertShieldingFileToString(compareFileName, compareFileString); + filename += shieldEnding; + std::remove(filename.c_str()); + } + + private: storm::Environment _environment; + std::string shieldEnding = ".shield"; }; typedef ::testing::Types< From 18497b30b040747354d7b6764447bc9ee880e269 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 15:09:12 +0200 Subject: [PATCH 41/59] added line below for postShield files (analogue to preShield files) --- src/storm/storage/PostScheduler.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 2e4392891..92a81b434 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/src/storm/storage/PostScheduler.cpp @@ -135,6 +135,7 @@ namespace storm { // jump to label if we find one undefined choice. skipStatesWithUndefinedChoices:; } + out << "___________________________________________________________________" << std::endl; } template class PostScheduler; From 70c689ff1eae68c9342c8cedccc131f5133b9774 Mon Sep 17 00:00:00 2001 From: lukpo Date: Mon, 30 Aug 2021 10:44:30 +0200 Subject: [PATCH 42/59] fixed bug in SparseNondeterministicStepBoundedHorizonHelper.cpp (use of uint choiceValuesCounter without initialization) --- .../SparseNondeterministicStepBoundedHorizonHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp index 0d88c456e..ea1948d54 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -87,7 +87,7 @@ namespace storm { std::vector rowGroupIndices = transitionMatrix.getRowGroupIndices(); std::vector maybeStatesRowGroupSizes; - uint choiceValuesCounter; + uint choiceValuesCounter = 0; getMaybeStatesRowGroupSizes(transitionMatrix, maybeStates, maybeStatesRowGroupSizes, choiceValuesCounter); choiceValues = std::vector(choiceValuesCounter, storm::utility::zero()); From d3b0046fa05661be551b938c36c2c2c104125508 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 31 Aug 2021 08:34:45 +0200 Subject: [PATCH 43/59] fixed bug in reduce method in Multiplier.cpp for SMGs and MDPs --- .../SparseNondeterministicStepBoundedHorizonHelper.cpp | 3 ++- .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 4 +++- src/storm/solver/Multiplier.cpp | 9 +++++++-- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp index ea1948d54..8e3da6930 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -20,10 +20,11 @@ namespace storm { template void SparseNondeterministicStepBoundedHorizonHelper::getMaybeStatesRowGroupSizes(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, std::vector& maybeStatesRowGroupSizes, uint& choiceValuesCounter) { std::vector rowGroupIndices = transitionMatrix.getRowGroupIndices(); + choiceValuesCounter = 0; for(uint counter = 0; counter < maybeStates.size(); counter++) { if(maybeStates.get(counter)) { - maybeStatesRowGroupSizes.push_back(rowGroupIndices.at(counter)); choiceValuesCounter += transitionMatrix.getRowGroupSize(counter); + maybeStatesRowGroupSizes.push_back(choiceValuesCounter); } } } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 2a352c381..139165ee3 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -110,7 +110,9 @@ namespace storm { } // Create a multiplier for reduction. auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition); + auto rowGroupIndices = transitionMatrix.getRowGroupIndices(); + rowGroupIndices.erase(rowGroupIndices.begin()); + multiplier->reduce(env, goal.direction(), b, rowGroupIndices, result, &statesOfCoalition); if (goal.isShieldingTask()) { choiceValues = b; } diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 2324b7833..e5df00b05 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -92,8 +92,13 @@ namespace storm { template void Multiplier::reduce(Environment const& env, OptimizationDirection const& dir, std::vector const& choiceValues, std::vector::index_type> rowGroupIndices, std::vector& result, storm::storage::BitVector const* dirOverride) const { auto choice_it = choiceValues.begin(); - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + for(uint state = 0; state < rowGroupIndices.size(); state++) { + uint rowGroupSize; + if(state == 0) { + rowGroupSize = rowGroupIndices[state]; + } else { + rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state-1]; + } if(dirOverride != nullptr) { if((dir == storm::OptimizationDirection::Minimize && !dirOverride->get(state)) || (dir == storm::OptimizationDirection::Maximize && dirOverride->get(state))) { result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize); From 412a74069e49a6d3237b0927a8c6ed74647d43c0 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 31 Aug 2021 09:11:57 +0200 Subject: [PATCH 44/59] Added shield generation test for MDPs ShieldGenerationMdpPrctlModelCheckerTest.cpp and shielding files for comparison of the results --- .../dieSelectionPostSafetygamma07Pmax.shield | 5 + .../dieSelectionPostSafetygamma07Pmin.shield | 8 + .../dieSelectionPostSafetylambda07Pmax.shield | 8 + .../dieSelectionPostSafetylambda07Pmin.shield | 8 + .../dieSelectionPreSafetygamma08Pmax.shield | 8 + .../dieSelectionPreSafetygamma08Pmin.shield | 7 + .../dieSelectionPreSafetylambda08Pmax.shield | 10 + .../dieSelectionPreSafetylambda08Pmin.shield | 6 + ...ieldGenerationMdpPrctlModelCheckerTest.cpp | 198 ++++++++++++++++++ 9 files changed, 258 insertions(+) create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield create mode 100644 resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield create mode 100644 src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield new file mode 100644 index 000000000..f14bbb1ba --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield @@ -0,0 +1,5 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.700000): +model state: correction [: ()}: + 4 0: 2; 1: 2; 2: 2 +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield new file mode 100644 index 000000000..26c138cc2 --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.700000): +model state: correction [: ()}: + 0 0: 0; 1: 1; 2: 2 + 1 0: 0; 1: 1; 2: 2 + 3 0: 0; 1: 1; 2: 2 + 4 0: 0; 1: 1; 2: 2 +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield new file mode 100644 index 000000000..89cc541ed --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.700000): +model state: correction [: ()}: + 0 0: 0; 1: 1; 2: 2 + 1 0: 0; 1: 1; 2: 2 + 3 0: 0; 1: 1; 2: 2 + 4 0: 0; 1: 1; 2: 2 +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield new file mode 100644 index 000000000..5cbf8cc99 --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.700000): +model state: correction [: ()}: + 0 0: 2; 1: 2; 2: 2 + 1 0: 0; 1: 0; 2: 0 + 3 0: 2; 1: 2; 2: 2 + 4 0: 2; 1: 2; 2: 2 +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield new file mode 100644 index 000000000..ac02291df --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Pre-Safety-Shield with absolute comparison (gamma = 0.800000): +model state: choice(s) [: ()}: + 1 0.9375: (0); 0.925: (1); 0.9125: (2) + 3 0.875: (0); 0.85: (1); 0.825: (2) + 4 1: (0); 1: (1); 1: (2) + 5 1: (0); 0.82: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield new file mode 100644 index 000000000..2834984eb --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Pre-Safety-Shield with absolute comparison (gamma = 0.800000): +model state: choice(s) [: ()}: + 0 0.33: (0); 0.366: (1); 0.402: (2) + 2 0.2025: (0); 0.243: (1); 0.2835: (2) + 3 0.755: (0); 0.706: (1); 0.657: (2) +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield new file mode 100644 index 000000000..8924f65da --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield @@ -0,0 +1,10 @@ +___________________________________________________________________ +Pre-Safety-Shield with relative comparison (lambda = 0.800000): +model state: choice(s) [: ()}: + 0 0.725: (0); 0.73: (1); 0.735: (2) + 1 0.9375: (0); 0.925: (1); 0.9125: (2) + 2 0.6: (1); 0.7: (2) + 3 0.875: (0); 0.85: (1); 0.825: (2) + 4 1: (0); 1: (1); 1: (2) + 5 1: (0); 0.82: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield new file mode 100644 index 000000000..5e126c2fc --- /dev/null +++ b/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Pre-Safety-Shield with relative comparison (lambda = 0.800000): +model state: choice(s) [: ()}: + 2 0.2025: (0) + 5 0.49: (1); 0.405: (2) +___________________________________________________________________ diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..02dc012c6 --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,198 @@ +#include +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + +#include "storm/models/sparse/Smg.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + class DoubleViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + template + class ShieldGenerationMdpPrctlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + ShieldGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + + std::pair>, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair>, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as>(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + + void convertShieldingFileToString(std::string filename, std::string &shieldingString) { + filename += shieldEnding; + std::ifstream resultFile(filename); + std::stringstream resultBuffer; + resultBuffer << resultFile.rdbuf(); + shieldingString = resultBuffer.str(); + } + + void getStringsToCompare(std::string filename, std::string &shieldingString, std::string &compareFileString) { + this->convertShieldingFileToString(filename, shieldingString); + std::string compareFileName = STORM_TEST_RESOURCES_DIR "/mdp-shields/" + filename; + this->convertShieldingFileToString(compareFileName, compareFileString); + filename += shieldEnding; + std::remove(filename.c_str()); + } + + private: + storm::Environment _environment; + std::string shieldEnding = ".shield"; + }; + + typedef ::testing::Types< + DoubleViEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(ShieldGenerationMdpPrctlModelCheckerTest, TestingTypes,); + + TYPED_TEST(ShieldGenerationMdpPrctlModelCheckerTest, DieSelection) { + typedef typename TestFixture::ValueType ValueType; + + // definition of shield file names + std::vector fileNames; + fileNames.push_back("dieSelectionPreSafetylambda08Pmax"); + fileNames.push_back("dieSelectionPreSafetygamma08Pmax"); + fileNames.push_back("dieSelectionPreSafetylambda08Pmin"); + fileNames.push_back("dieSelectionPreSafetygamma08Pmin"); + + fileNames.push_back("dieSelectionPostSafetylambda07Pmax"); + fileNames.push_back("dieSelectionPostSafetygamma07Pmax"); + fileNames.push_back("dieSelectionPostSafetylambda07Pmin"); + fileNames.push_back("dieSelectionPostSafetygamma07Pmin"); + + // testing create shielding expressions + std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.8> Pmax=? [ F <5 \"done\" ]"; + formulasString += "; <" + fileNames[1] + ", PreSafety, gamma=0.8> Pmax=? [ F <5 \"done\" ]"; + formulasString += "; <" + fileNames[2] + ", PreSafety, lambda=0.8> Pmin=? [ F <5 \"done\" ]"; + formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.8> Pmin=? [ F <5 \"done\" ]"; + + formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.7> Pmax=? [ F <6 \"two\" ]"; + formulasString += "; <" + fileNames[5] + ", PostSafety, gamma=0.7> Pmax=? [ F <6 \"two\" ]"; + formulasString += "; <" + fileNames[6] + ", PostSafety, lambda=0.7> Pmin=? [ F <6 \"two\" ]"; + formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.7> Pmin=? [ F <6 \"two\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/die_selection.nm", formulasString); + auto mdp = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(13ul, mdp->getNumberOfStates()); + EXPECT_EQ(43ul, mdp->getNumberOfTransitions()); + ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); + EXPECT_EQ(25ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + // definitions + storm::logic::ShieldingType typePreSafety = storm::logic::ShieldingType::PreSafety; + storm::logic::ShieldingType typePostSafety = storm::logic::ShieldingType::PostSafety; + storm::logic::ShieldComparison comparisonRelative = storm::logic::ShieldComparison::Relative; + storm::logic::ShieldComparison comparisonAbsolute = storm::logic::ShieldComparison::Absolute; + double value08 = 0.8; + double value07 = 0.7; + std::string filename, shieldingString, compareFileString; + + // shielding results + filename = fileNames[0]; + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08)); + tasks[0].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[0].isShieldingTask()); + auto result = checker.check(this->env(), tasks[0]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[1]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08)); + tasks[1].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[1].isShieldingTask()); + result = checker.check(this->env(), tasks[1]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[2]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08)); + tasks[2].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[2].isShieldingTask()); + result = checker.check(this->env(), tasks[2]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[3]; + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08)); + tasks[3].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[3].isShieldingTask()); + result = checker.check(this->env(), tasks[3]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[4]; + auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07)); + tasks[4].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[4].isShieldingTask()); + result = checker.check(this->env(), tasks[4]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[5]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07)); + tasks[5].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[5].isShieldingTask()); + result = checker.check(this->env(), tasks[5]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[6]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07)); + tasks[6].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[6].isShieldingTask()); + result = checker.check(this->env(), tasks[6]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); + + filename = fileNames[7]; + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07)); + tasks[7].setShieldingExpression(postSafetyShieldingExpression); + EXPECT_TRUE(tasks[7].isShieldingTask()); + result = checker.check(this->env(), tasks[7]); + this->getStringsToCompare(filename, shieldingString, compareFileString); + EXPECT_EQ(shieldingString, compareFileString); +} + +// TODO: create more test cases (files) +} From c74dd841a5d2d7fca218b6b5b43c23ff2313ce9e Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 2 Sep 2021 14:18:26 +0200 Subject: [PATCH 45/59] changed GameViHelper::performValueIteration for computing also value iteration with upper bounds --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 20 ++++-- .../rpatl/helper/internal/GameViHelper.cpp | 63 +++++-------------- .../rpatl/helper/internal/GameViHelper.h | 12 +--- 3 files changed, 29 insertions(+), 66 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 139165ee3..cffe35987 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -1,4 +1,5 @@ #include +#include #include "SparseSmgRpatlHelper.h" #include "storm/environment/Environment.h" @@ -15,7 +16,6 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - // TODO add Kwiatkowska original reference auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); @@ -40,7 +40,7 @@ namespace storm { if (produceScheduler) { viHelper.setProduceScheduler(true); } - viHelper.performValueIteration(env, x, b, goal.direction()); + viHelper.performValueIteration(env, x, b, goal.direction(), constrainedChoiceValues); if(goal.isShieldingTask()) { viHelper.getChoiceValues(env, x, constrainedChoiceValues); } @@ -172,10 +172,12 @@ namespace storm { } // If the lowerBound = 0, value iteration is done until the upperBound. if(lowerBound == 0) { - viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues); + solverEnv.solver().game().setMaximalNumberOfIterations(upperBound); + viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues); } else { // The lowerBound != 0, the first computation between the given bound steps is done. - viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound, constrainedChoiceValues); + solverEnv.solver().game().setMaximalNumberOfIterations(upperBound - lowerBound); + viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues); // Initialization of subResult, fill it with the result of the first computation and 1s for the psiStates in full range. std::vector subResult = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -199,7 +201,9 @@ namespace storm { b = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero()); // The second computation is done between step 0 and the lowerBound - viHelper.performValueIterationUpperBound(env, subResult, b, goal.direction(), lowerBound, constrainedChoiceValues); + solverEnv.solver().game().setMaximalNumberOfIterations(lowerBound); + viHelper.performValueIteration(solverEnv, subResult, b, goal.direction(), constrainedChoiceValues); + x = subResult; } viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); @@ -208,7 +212,11 @@ namespace storm { } storm::utility::vector::setVectorValues(result, relevantStates, x); } - // In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds. + // In bounded until and bounded eventually formula the psiStates have probability 1 to satisfy the formula, + // because once reaching a state where psi holds those formulas are satisfied. + // In bounded globally formulas we cannot set those states to 1 because it is possible to leave a set of safe states after reaching a psiState + // and in globally the formula has to hold in every time step (between the bounds). + // e.g. phiState -> phiState -> psiState -> unsafeState if(!computeBoundedGlobally){ storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 4ddadc247..5b644e23d 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -25,13 +25,14 @@ namespace storm { } template - void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { prepareSolversAndMultipliers(env); // Get precision for convergence check. ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x1 = x; _x2 = _x1; if (this->isProduceSchedulerSet()) { @@ -42,17 +43,25 @@ namespace storm { } uint64_t iter = 0; - std::vector result = x; + constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); + while (iter < maxIter) { - ++iter; + if(iter == maxIter - 1) { + _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); + auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); + rowGroupIndices.erase(rowGroupIndices.begin()); + _multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew()); + break; + } performIterationStep(env, dir); - if (checkConvergence(precision)) { + _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); break; } if (storm::utility::resources::isTerminate()) { break; } + ++iter; } x = xNew(); @@ -74,18 +83,11 @@ namespace storm { } else { _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); } - - // compare applyPointwise - storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { - if(a > b) return a; - else return b; - }); } template bool GameViHelper::checkConvergence(ValueType threshold) const { STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); - // Now check whether the currently produced results are precise enough STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); auto x1It = xOld().begin(); @@ -113,43 +115,6 @@ namespace storm { return true; } - template - void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { - prepareSolversAndMultipliers(env); - _x = x; - _b = b; - - if (this->isProduceSchedulerSet()) { - if (!this->_producedOptimalChoices.is_initialized()) { - this->_producedOptimalChoices.emplace(); - } - this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); - } - for (uint64_t iter = 0; iter < upperBound; iter++) { - if(iter == upperBound - 1) { - _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); - } - performIterationStepUpperBound(env, dir); - } - - x = _x; - } - - template - void GameViHelper::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { - if (!_multiplier) { - prepareSolversAndMultipliers(env); - } - // multiplyandreducegaussseidel - // Ax = x' - if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition); - } else { - // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition); - } - } - template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 393f8a79a..db4b2939f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -26,12 +26,7 @@ namespace storm { /*! * Perform value iteration until convergence */ - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); - - /*! - * Perform value iteration until upper bound - */ - void performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues); /*! * Sets whether an optimal scheduler shall be constructed during the computation @@ -68,11 +63,6 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - /*! - * Performs one iteration step for value iteration with upper bound - */ - void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - /*! * Checks whether the curently computed value achieves the desired precision */ From cde5b353cf28a80d2b299a6e387831f438cbc2c2 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 08:41:28 +0200 Subject: [PATCH 46/59] moved shielding folders testfiles to new directory 'shields' --- .../mdp-shields/dieSelectionPostSafetygamma07Pmax.shield | 0 .../mdp-shields/dieSelectionPostSafetygamma07Pmin.shield | 0 .../mdp-shields/dieSelectionPostSafetylambda07Pmax.shield | 0 .../mdp-shields/dieSelectionPostSafetylambda07Pmin.shield | 0 .../mdp-shields/dieSelectionPreSafetygamma08Pmax.shield | 0 .../mdp-shields/dieSelectionPreSafetygamma08Pmin.shield | 0 .../mdp-shields/dieSelectionPreSafetylambda08Pmax.shield | 0 .../mdp-shields/dieSelectionPreSafetylambda08Pmin.shield | 0 .../smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield | 0 .../smg-shields/rightDecisionPostSafetyGamma05PminF5.shield | 0 .../smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield | 0 .../smg-shields/rightDecisionPostSafetyGamma09PminF3.shield | 0 .../smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield | 0 .../smg-shields/rightDecisionPostSafetyLambda05PminF5.shield | 0 .../smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield | 0 .../smg-shields/rightDecisionPostSafetyLambda09PminF3.shield | 0 .../smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield | 0 .../smg-shields/rightDecisionPreSafetyGamma05PminF5.shield | 0 .../smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield | 0 .../smg-shields/rightDecisionPreSafetyGamma09PminF3.shield | 0 .../smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield | 0 .../smg-shields/rightDecisionPreSafetyLambda05PminF5.shield | 0 .../smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield | 0 .../smg-shields/rightDecisionPreSafetyLambda09PminF3.shield | 0 24 files changed, 0 insertions(+), 0 deletions(-) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield (100%) rename resources/examples/testfiles/{ => shields}/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield (100%) rename resources/examples/testfiles/{ => shields}/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield (100%) diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield diff --git a/resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield similarity index 100% rename from resources/examples/testfiles/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield rename to resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield diff --git a/resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield similarity index 100% rename from resources/examples/testfiles/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield rename to resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield From 3c78b0b064e4b9396b77f38f8213b7289855a1c8 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 08:42:35 +0200 Subject: [PATCH 47/59] renamed file to probabilisticFormula.rpatl - typo --- .../{probabalisticFormula.rpatl => probabilisticFormula.rpatl} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename resources/examples/testfiles/rpatl/{probabalisticFormula.rpatl => probabilisticFormula.rpatl} (100%) diff --git a/resources/examples/testfiles/rpatl/probabalisticFormula.rpatl b/resources/examples/testfiles/rpatl/probabilisticFormula.rpatl similarity index 100% rename from resources/examples/testfiles/rpatl/probabalisticFormula.rpatl rename to resources/examples/testfiles/rpatl/probabilisticFormula.rpatl From 189ff1aae1ac0e72c6bd9c2f8c34a6f24d839aff Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 08:45:12 +0200 Subject: [PATCH 48/59] removed check - parsing issue --- src/test/storm/logic/FragmentCheckerTest.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 762f26f73..25a1714ae 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -187,9 +187,6 @@ TEST(FragmentCheckerTest, Rpatl) { storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - // this may be a parsing issue - //ASSERT_ANY_THROW(formula = formulaParser.parseSingleFormulaFromString("<> \"label\"")); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); From 09f0cc36a39e4e1f85ee57cf67402f6f7037f678 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 08:52:10 +0200 Subject: [PATCH 49/59] renamed shieldEnding to shieldFiletype --- .../prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp | 6 +++--- .../rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp index 02dc012c6..af99ac910 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -57,7 +57,7 @@ namespace { ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} void convertShieldingFileToString(std::string filename, std::string &shieldingString) { - filename += shieldEnding; + filename += shieldFiletype; std::ifstream resultFile(filename); std::stringstream resultBuffer; resultBuffer << resultFile.rdbuf(); @@ -68,13 +68,13 @@ namespace { this->convertShieldingFileToString(filename, shieldingString); std::string compareFileName = STORM_TEST_RESOURCES_DIR "/mdp-shields/" + filename; this->convertShieldingFileToString(compareFileName, compareFileString); - filename += shieldEnding; + filename += shieldFiletype; std::remove(filename.c_str()); } private: storm::Environment _environment; - std::string shieldEnding = ".shield"; + std::string shieldFiletype = ".shield"; }; typedef ::testing::Types< diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index f9b75c7dd..72e89d49e 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -57,7 +57,7 @@ namespace { ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} void convertShieldingFileToString(std::string filename, std::string &shieldingString) { - filename += shieldEnding; + filename += shieldFiletype; std::ifstream resultFile(filename); std::stringstream resultBuffer; resultBuffer << resultFile.rdbuf(); @@ -68,14 +68,14 @@ namespace { this->convertShieldingFileToString(filename, shieldingString); std::string compareFileName = STORM_TEST_RESOURCES_DIR "/smg-shields/" + filename; this->convertShieldingFileToString(compareFileName, compareFileString); - filename += shieldEnding; + filename += shieldFiletype; std::remove(filename.c_str()); } private: storm::Environment _environment; - std::string shieldEnding = ".shield"; + std::string shieldFiletype = ".shield"; }; typedef ::testing::Types< From 43b58a65c71a21636363874e1d0b31e2e35a9139 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 09:14:19 +0200 Subject: [PATCH 50/59] changed path of shielding testfiles --- .../prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp | 2 +- .../rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp index af99ac910..a9e41a304 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -66,7 +66,7 @@ namespace { void getStringsToCompare(std::string filename, std::string &shieldingString, std::string &compareFileString) { this->convertShieldingFileToString(filename, shieldingString); - std::string compareFileName = STORM_TEST_RESOURCES_DIR "/mdp-shields/" + filename; + std::string compareFileName = STORM_TEST_RESOURCES_DIR "/shields/mdp-shields/" + filename; this->convertShieldingFileToString(compareFileName, compareFileString); filename += shieldFiletype; std::remove(filename.c_str()); diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index 72e89d49e..b0f26f02b 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -66,7 +66,7 @@ namespace { void getStringsToCompare(std::string filename, std::string &shieldingString, std::string &compareFileString) { this->convertShieldingFileToString(filename, shieldingString); - std::string compareFileName = STORM_TEST_RESOURCES_DIR "/smg-shields/" + filename; + std::string compareFileName = STORM_TEST_RESOURCES_DIR "/shields/smg-shields/" + filename; this->convertShieldingFileToString(compareFileName, compareFileString); filename += shieldFiletype; std::remove(filename.c_str()); From 70947ebee4c48eadef9dee95a3cb52a423da30f1 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 09:52:43 +0200 Subject: [PATCH 51/59] changes from default changelist --- .../modelchecker/results/ExplicitQuantitativeCheckResult.cpp | 2 +- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 19b1f627e..ee7c2d91d 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -221,7 +221,7 @@ namespace storm { STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); return *scheduler.get(); } - + template void print(std::ostream& out, ValueType const& value) { if (value == storm::utility::infinity()) { diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index f44a7cef7..3e8cd7569 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -216,7 +216,7 @@ namespace storm { auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); } return result; } From 27bf04ac5bb38ba24096deaf5503c9539836c67f Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 13:35:18 +0200 Subject: [PATCH 52/59] added testcase RobotCircle to SmgRpatlModelCheckerTest.cpp and the test file robotCircle.nm --- .../examples/testfiles/smg/robotCircle.nm | 61 +++++++++++++++++++ .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 47 ++++++++++++++ 2 files changed, 108 insertions(+) create mode 100644 resources/examples/testfiles/smg/robotCircle.nm diff --git a/resources/examples/testfiles/smg/robotCircle.nm b/resources/examples/testfiles/smg/robotCircle.nm new file mode 100644 index 000000000..92170a97a --- /dev/null +++ b/resources/examples/testfiles/smg/robotCircle.nm @@ -0,0 +1,61 @@ +// PRISM Model of a simple robot game +// - A player - friendlyRobot - moves around and tries not to "crash" with another player - adversary Robot. +// - friendlyRobot can choose the direction of movement. +// - adversaryRobot should move in a circle counterclockwise on the grid, but has a probabilty to fail and move into the wrong direction. +// - The movement of adversaryRobot is defined as a pseudo random movement with probabilty = 1/4 into one of the 4 possible directions. + +smg + +player friendlyRobot + [e1], [w1], [n1], [s1] +endplayer + +player adversaryRobot + [e2], [w2], [n2], [s2], [middle] +endplayer + +// 3x3 grid +const int width = 2; +const int height = 2; + +const int xmin = 0; +const int xmax = width; +const int ymin = 0; +const int ymax = height; + +// probabilty to fail +const double failProb = 1/10; +const double notFailProb = 1-failProb; + +// definition of randomProb, this has to be 0.25 since it is the prob of go into one direction from the middle for the adverseryRobot +const double randomProb = 1/4; + +global move : [0..1] init 0; + +//F__ +//___ +//__R + +label "crash" = x1=x2 & y1=y2; + +module robot1 + x1 : [0..width] init 0; + y1 : [0..height] init 0; + + [e1] move=0 & x1 (x1'=x1+1) & (move'=1); + [w1] move=0 & x1>0 -> (x1'=x1-1) & (move'=1); + [n1] move=0 & y1>0 -> (y1'=y1-1) & (move'=1); + [s1] move=0 & y1 (y1'=y1+1) & (move'=1); +endmodule + +module robot2 + x2 : [0..width] init width; + y2 : [0..height] init height; + + [e2] move=1 & x2 notFailProb : (x2'=x2+1) & (move'=0) + failProb : (y2'=y2-1) & (move'=0); + [w2] move=1 & x2>0 & y2=0 -> notFailProb : (x2'=x2-1) & (move'=0) + failProb : (y2'=y2+1) & (move'=0); + [n2] move=1 & x2=xmax & y2>0 -> notFailProb : (y2'=y2-1) & (move'=0) + failProb : (x2'=x2-1) & (move'=0); + [s2] move=1 & x2=0 & y2 notFailProb : (y2'=y2+1) & (move'=0) + failProb : (x2'=x2+1) & (move'=0); + + [middle] move=1 & x2=1 & y2=1 -> randomProb : (x2'=x2+1) & (move'=0) + randomProb : (x2'=x2-1) & (move'=0) + randomProb : (y2'=y2-1) & (move'=0) + randomProb : (y2'=y2+1) & (move'=0); +endmodule diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index f46106a91..0f0a63ca6 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -229,6 +229,7 @@ namespace { result = checker->check(this->env(), tasks[15]); EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) { // This test is for borders of bounded U with conversations from G and F // bounded G @@ -322,5 +323,51 @@ namespace { EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) { + // This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound) + std::string formulasString = " <> Pmax=? [ G<1 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=1 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=5 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=6 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=7 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=8 !\"crash\" ]"; + + formulasString += "; <> Pmax=? [ G[1,5] !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G[5,6] !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G[7,8] !\"crash\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/robotCircle.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(81ul, model->getNumberOfStates()); + EXPECT_EQ(196ul, model->getNumberOfTransitions()); + EXPECT_EQ(148ul, model->getNumberOfChoices()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // results for bounded globally with upper bound + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + // results for bounded globally with upper and lower bound + result = checker->check(this->env(), tasks[6]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[7]); + EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[8]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + // TODO: create more test cases (files) } From 82ffb9b7c017d9817279217921c65590c445146f Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 14:46:06 +0200 Subject: [PATCH 53/59] fixed typo - updateStatesOfCoalition --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp | 4 ++-- src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index cffe35987..bc18f35ff 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -194,7 +194,7 @@ namespace storm { // Update the viHelper for the (full-size) submatrix and statesOfCoalition. viHelper.updateTransitionMatrix(submatrix); - viHelper.updateStatesOfCoaltion(statesOfCoalition); + viHelper.updateStatesOfCoalition(statesOfCoalition); // Reset constrainedChoiceValues and b to 0-vector in the correct dimension. constrainedChoiceValues = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero()); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 5b644e23d..54efd3c7c 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -131,8 +131,8 @@ namespace storm { } template - void GameViHelper::updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion) { - _statesOfCoalition = newStatesOfCoaltion; + void GameViHelper::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) { + _statesOfCoalition = newStatesOfCoalition; } template diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index db4b2939f..507eb60b7 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -46,7 +46,7 @@ namespace storm { /*! * Changes the statesOfCoalition to the given one. */ - void updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion); + void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition); storm::storage::Scheduler extractScheduler() const; From 3732cef1acb5c4d71e854a7b84333d5531dfbb28 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 13:58:08 +0200 Subject: [PATCH 54/59] reintroduced shields to formula parser --- .../parser/FormulaParserGrammar.cpp | 127 ++++++++++++------ .../parser/FormulaParserGrammar.h | 11 ++ 2 files changed, 98 insertions(+), 40 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 13b56d8a9..ea96f31a2 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -179,11 +179,29 @@ namespace storm { constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)]; constantDefinition.name("constant definition"); + // Shielding properties + shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + + shieldExpression.name("shield expression"); + + shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] | + qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] | + qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield"); + shieldingType.name("shielding type"); + + probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; + probability.name("double between 0 and 1"); + + shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | + qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; + shieldComparison.name("shield comparison type"); + #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > topLevelFormula > qi::lit(",") > formula(FormulaKind::State, storm::logic::FormulaContext::Undefined)> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | - (-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; + (-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | + (-formulaName >> shieldExpression >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -195,45 +213,45 @@ namespace storm { start.name("start"); // Enable the following lines to print debug output for most the rules. -// debug(rewardModelName) -// debug(rewardMeasureType) -// debug(operatorFormula) -// debug(labelFormula) -// debug(expressionFormula) -// debug(booleanLiteralFormula) -// debug(atomicPropositionFormula) -// debug(basicPropositionalFormula) -// debug(negationPropositionalFormula) -// debug(andLevelPropositionalFormula) -// debug(orLevelPropositionalFormula) -// debug(propositionalFormula) -// debug(timeBoundReference) -// debug(timeBound) -// debug(timeBounds) -// debug(eventuallyFormula) -// debug(nextFormula) -// debug(globallyFormula) -// debug(hoaPathFormula) -// debug(multiBoundedPathFormula) -// debug(prefixOperatorPathFormula) -// debug(basicPathFormula) -// debug(untilLevelPathFormula) -// debug(pathFormula) -// debug(longRunAverageRewardFormula) -// debug(instantaneousRewardFormula) -// debug(cumulativeRewardFormula) -// debug(totalRewardFormula) -// debug(playerCoalition) -// debug(gameFormula) -// debug(multiOperatorFormula) -// debug(quantileBoundVariable) -// debug(quantileFormula) -// debug(formula) -// debug(topLevelFormula) -// debug(formulaName) -// debug(filterProperty) -// debug(constantDefinition ) -// debug(start) + //debug(rewardModelName); + //debug(rewardMeasureType); + //debug(operatorFormula); + //debug(labelFormula); + //debug(expressionFormula); + //debug(booleanLiteralFormula); + //debug(atomicPropositionFormula); + //debug(basicPropositionalFormula); + //debug(negationPropositionalFormula); + //debug(andLevelPropositionalFormula); + //debug(orLevelPropositionalFormula); + //debug(propositionalFormula); + //debug(timeBoundReference); + //debug(timeBound); + //debug(timeBounds); + //debug(eventuallyFormula); + //debug(nextFormula); + //debug(globallyFormula); + //debug(hoaPathFormula); + //debug(multiBoundedPathFormula); + //debug(prefixOperatorPathFormula); + //debug(basicPathFormula); + //debug(untilLevelPathFormula); + //debug(pathFormula); + //debug(longRunAverageRewardFormula); + //debug(instantaneousRewardFormula); + //debug(cumulativeRewardFormula); + //debug(totalRewardFormula); + ////debug(playerCoalition); + //debug(gameFormula); + //debug(multiOperatorFormula); + //debug(quantileBoundVariable); + //debug(quantileFormula); + //debug(formula); + //debug(topLevelFormula); + //debug(formulaName); + //debug(filterProperty); + ////debug(constantDefinition); + //debug(start); // Enable error reporting. qi::on_error(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -386,6 +404,11 @@ namespace storm { } } + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + } + + /* std::shared_ptr FormulaParserGrammar::createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -401,6 +424,7 @@ namespace storm { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } } + */ std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::NextFormula(subformula)); @@ -619,6 +643,29 @@ namespace storm { } } + std::pair FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) { + return std::make_pair(comparisonType, value); + } + + std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { + if(comparisonStruct.is_initialized()) { + STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored."); + return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); + } else { + STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)"); + return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); + } + } + + storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldExpression) { + ++propertyCount; + if (propertyName) { + return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula), shieldExpression); + } else { + return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula), shieldExpression); + } + } + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { return storm::logic::PlayerCoalition(playerIds); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index fca3b3a1c..9f0953577 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -234,6 +234,12 @@ namespace storm { }; qi::rule, Skipper> constantDefinition; + // Shielding properties + qi::rule(), Skipper> shieldExpression; + qi::rule shieldingType; + qi::rule probability; + qi::rule, qi::locals, Skipper> shieldComparison; + // Start symbol qi::rule(), Skipper> start; @@ -242,6 +248,9 @@ namespace storm { storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; + std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); + std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); @@ -259,6 +268,7 @@ namespace storm { std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + //std::shared_ptr createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula); @@ -285,6 +295,7 @@ namespace storm { std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); + storm::jani::Property createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldingExpression); bool isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage = false); bool raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op); From d1f81a7c9361c05f85c7fa93712920698763bf1e Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 13:58:26 +0200 Subject: [PATCH 55/59] adapted reference shields after change in model cf. https://github.com/moves-rwth/storm/commit/76bf1049eef7deaa1dae4398916133b434d9915a#diff-dc46d467dffbe6500791e92e7daf53e87d0905cad845a393b0d4e1182fae24af --- .../mdp-shields/dieSelectionPreSafetygamma08Pmax.shield | 5 ++++- .../mdp-shields/dieSelectionPreSafetygamma08Pmin.shield | 3 +-- .../mdp-shields/dieSelectionPreSafetylambda08Pmax.shield | 7 ++++--- .../mdp-shields/dieSelectionPreSafetylambda08Pmin.shield | 2 -- .../prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp | 4 ++-- 5 files changed, 11 insertions(+), 10 deletions(-) diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield index ac02291df..3014f95c4 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield @@ -1,8 +1,11 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.800000): model state: choice(s) [: ()}: + 0 0.8: (0) 1 0.9375: (0); 0.925: (1); 0.9125: (2) + 2 0.9625: (0); 0.97: (1); 0.9775: (2) 3 0.875: (0); 0.85: (1); 0.825: (2) 4 1: (0); 1: (1); 1: (2) - 5 1: (0); 0.82: (1) + 5 1: (0); 1: (1); 1: (2) + 6 0.925: (0); 0.91: (1); 0.895: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield index 2834984eb..6b32fa01a 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield @@ -1,7 +1,6 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.800000): model state: choice(s) [: ()}: - 0 0.33: (0); 0.366: (1); 0.402: (2) - 2 0.2025: (0); 0.243: (1); 0.2835: (2) + 0 0.58: (0); 0.566: (1); 0.552: (2) 3 0.755: (0); 0.706: (1); 0.657: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield index 8924f65da..7d91ac6f8 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield @@ -1,10 +1,11 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.800000): model state: choice(s) [: ()}: - 0 0.725: (0); 0.73: (1); 0.735: (2) + 0 0.8: (0); 0.79: (1); 0.78: (2) 1 0.9375: (0); 0.925: (1); 0.9125: (2) - 2 0.6: (1); 0.7: (2) + 2 0.9625: (0); 0.97: (1); 0.9775: (2) 3 0.875: (0); 0.85: (1); 0.825: (2) 4 1: (0); 1: (1); 1: (2) - 5 1: (0); 0.82: (1) + 5 1: (0); 1: (1); 1: (2) + 6 0.925: (0); 0.91: (1); 0.895: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield index 5e126c2fc..dcd83f02c 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield @@ -1,6 +1,4 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.800000): model state: choice(s) [: ()}: - 2 0.2025: (0) - 5 0.49: (1); 0.405: (2) ___________________________________________________________________ diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp index a9e41a304..7fda8f70c 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -113,9 +113,9 @@ namespace { auto mdp = std::move(modelFormulas.first); auto tasks = this->getTasks(modelFormulas.second); EXPECT_EQ(13ul, mdp->getNumberOfStates()); - EXPECT_EQ(43ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(48ul, mdp->getNumberOfTransitions()); ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); - EXPECT_EQ(25ull, mdp->getNumberOfChoices()); + EXPECT_EQ(27ul, mdp->getNumberOfChoices()); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); From 776dd502acc079f5784da7104d1b7d4edd19e062 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 14:00:55 +0200 Subject: [PATCH 56/59] Prism NSG correctly sets player indices of unsynced actions --- src/storm/generator/PrismNextStateGenerator.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index a9c845d32..600615c64 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -548,7 +548,6 @@ namespace storm { // Iterate over all commands. for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { storm::prism::Command const& command = module.getCommand(j); - // Only consider commands that are not possibly synchronizing. if (isCommandPotentiallySynchronizing(command)) continue; @@ -615,9 +614,15 @@ namespace storm { } if (program.getModelType() == storm::prism::Program::ModelType::SMG) { - storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i); - STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command."); - choice.setPlayerIndex(playerOfModule); + if(command.getActionName() != "") { + storm::storage::PlayerIndex const& playerOfAction = actionIndexToPlayerIndexMap.at(command.getActionIndex()); + STORM_LOG_THROW(playerOfAction != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Command " << command.getActionName() << " is not owned by any player."); + choice.setPlayerIndex(playerOfAction); + } else { + storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i); + STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command."); + choice.setPlayerIndex(playerOfModule); + } } if (this->options.isExplorationChecksSet()) { From 564cb6b9b17dcacfde7cf2652f0a8ada91f04ab7 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 14:02:24 +0200 Subject: [PATCH 57/59] removed some test cases for now we do not support bounded globally formulas explicitely, as well as `multi()`-formulae for SMGs --- src/test/storm/logic/FragmentCheckerTest.cpp | 6 +-- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 42 +++++-------------- .../storm/parser/GameFormulaParserTest.cpp | 31 -------------- 3 files changed, 13 insertions(+), 66 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 25a1714ae..3583ac019 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -88,7 +88,7 @@ TEST(FragmentCheckerTest, Prctl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [\"label1\" U [5,7] \"label2\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G <=10 \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); @@ -205,10 +205,10 @@ TEST(FragmentCheckerTest, Rpatl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G <=5 \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G [0,1] \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); } diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 0f0a63ca6..d8e9217dc 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -232,16 +232,8 @@ namespace { TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) { // This test is for borders of bounded U with conversations from G and F - // bounded G + // G std::string formulasString = "<> Pmax=? [ G !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=1 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=2 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=10 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=17 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=32 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=47 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=61 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=62 !\"hacked\" ]"; // bounded F formulasString += "; <> Pmin=? [ F \"hacked\" ]"; @@ -260,38 +252,22 @@ namespace { auto checker = this->createModelChecker(model); std::unique_ptr result; - // bounded G results + // G results result = checker->check(this->env(), tasks[0]); EXPECT_NEAR(this->parseNumber("1.99379598e-05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[3]); - EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[4]); - EXPECT_NEAR(this->parseNumber("0.9025"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("0.857375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[6]); - EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[7]); - EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[8]); - EXPECT_NEAR(this->parseNumber("0.7737809375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); // bounded F results - result = checker->check(this->env(), tasks[9]); + result = checker->check(this->env(), tasks[1]); EXPECT_NEAR(this->parseNumber("0.999980062"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[10]); + result = checker->check(this->env(), tasks[2]); EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[11]); + result = checker->check(this->env(), tasks[3]); EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[12]); + result = checker->check(this->env(), tasks[4]); EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[13]); + result = checker->check(this->env(), tasks[5]); EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[14]); + result = checker->check(this->env(), tasks[6]); EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } @@ -323,6 +299,7 @@ namespace { EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + /* TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) { // This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound) std::string formulasString = " <> Pmax=? [ G<1 !\"crash\" ]"; @@ -368,6 +345,7 @@ namespace { result = checker->check(this->env(), tasks[8]); EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + */ // TODO: create more test cases (files) } diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 34ebc724c..bdb551e53 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -202,34 +202,3 @@ TEST(GameFormulaParserTest, WrongFormatTest) { input = "<< 1,2,3 >> P>0.5 [F y!=0)]"; STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); } - -TEST(GameFormulaParserTest, MultiObjectiveFormulaTest) { - storm::parser::FormulaParser formulaParser; - - std::string input = "multi(<> P<0.9 [ F \"a\" ], <> R<42 [ F \"b\" ], <> Pmin=? [ F\"c\" ])"; - std::shared_ptr formula; - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - ASSERT_TRUE(formula->isMultiObjectiveFormula()); - storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula(); - EXPECT_FALSE(formula->isInFragment(storm::logic::rpatl())); - ASSERT_EQ(3ull, mof.getNumberOfSubformulas()); - - ASSERT_TRUE(mof.getSubformula(0).isGameFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().isProbabilityOperatorFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasBound()); - - ASSERT_TRUE(mof.getSubformula(1).isGameFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().isRewardOperatorFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isEventuallyFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); - - ASSERT_TRUE(mof.getSubformula(2).isGameFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().isProbabilityOperatorFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasOptimalityType()); - ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getOptimalityType())); -} \ No newline at end of file From 4fd16ff45fd40f270099326b483ff6d0e6f641f3 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 14:03:11 +0200 Subject: [PATCH 58/59] removed conflict marker --- src/test/storm/parser/PrismParserTest.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index 51945865d..b28f94f0d 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -138,7 +138,6 @@ TEST(PrismParser, ComplexTest) { EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(2ul, result.getNumberOfPlayers()); EXPECT_EQ(5ul, result.getNumberOfLabels()); ->>>>>>> d7e3f7ed6 (added a smg to PrismParserTest.cpp) } TEST(PrismParser, UnboundedTest) { From 7550934b2e54d3838d5bad8f9fe47ae6a8daead5 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 10 Sep 2021 14:03:18 +0200 Subject: [PATCH 59/59] fixed scheduler print after large merge --- src/storm/storage/Scheduler.cpp | 81 +++++++++------------------------ 1 file changed, 21 insertions(+), 60 deletions(-) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index a7acff700..08bf13d65 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -182,6 +182,7 @@ namespace storm { if (!isMemorylessScheduler()) { out << " with " << getNumberOfMemoryStates() << " memory states"; } + out << ":" << std::endl; STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << (isMemorylessScheduler() ? "" : " memory updates: ") << std::endl; @@ -203,6 +204,11 @@ namespace storm { bool firstMemoryState = true; for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + // Ignore dontCare states + if(skipDontCareStates && isDontCare(state, memoryState)) { + continue; + } + // Indent if this is not the first memory state if (firstMemoryState) { firstMemoryState = false; @@ -216,26 +222,6 @@ namespace storm { } stateString << " "; - bool firstMemoryState = true; - for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { - - // Ignore dontCare states - if(skipDontCareStates && isDontCare(state, memoryState)) { - continue; - } - - // Indent if this is not the first memory state - if (firstMemoryState) { - firstMemoryState = false; - } else { - out << std::setw(widthOfStates) << ""; - out << " "; - } - // Print the memory state info - if (!isMemorylessScheduler()) { - out << "m="<< memoryState << std::setw(8) << ""; - } - // Print choice info SchedulerChoice const& choice = schedulerChoices[memoryState][state]; if (choice.isDefined()) { @@ -275,51 +261,26 @@ namespace storm { stateString << "undefined."; } - // Print memory updates - if(!isMemorylessScheduler()) { - stateString << std::setw(widthOfStates) << ""; - // The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state. - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; - bool firstUpdate = true; - for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { - if (firstUpdate) { - firstUpdate = false; - } else { - stateString << ", "; - } - stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - } - } - } - - // Print memory updates - if(!isMemorylessScheduler()) { - out << std::setw(widthOfStates) << ""; - // The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state. - for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { - uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; - bool firstUpdate = true; - for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { - if (firstUpdate) { - firstUpdate = false; - } else { - out << ", "; - } - out << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; + // Print memory updates + if(!isMemorylessScheduler()) { + stateString << std::setw(widthOfStates) << ""; + // The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state. + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + bool firstUpdate = true; + for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) { + if (firstUpdate) { + firstUpdate = false; + } else { + stateString << ", "; } - + stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; } - } - - out << std::endl; } - stateString << stateString.str(); - stateString << std::endl; + out << stateString.str(); + out << std::endl; } } if (numOfSkippedStatesWithUniqueChoice > 0) {