From 0920390430fab92e212d675b72ea22e16905fc6d Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 20 Mar 2019 10:32:45 +0100 Subject: [PATCH] Fixed permissive scheduler tests (GitHub issue #38). --- .../MilpPermissiveSchedulerTest.cpp | 15 ++++++++++----- .../SmtPermissiveSchedulerTest.cpp | 10 +++++++--- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index a6b0a34fd..f8a2f5aaa 100644 --- a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -19,13 +19,18 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::string formulaString = ""; + formulaString += "P>=0.10 [ F \"one\"];\n"; + formulaString += "P>=0.17 [ F \"one\"];\n"; + formulaString += "P<=0.10 [ F \"one\"];\n"; + formulaString += "P<=0.17 [ F \"one\"];\n"; + auto formulas = formulaParser.parseFromString(formulaString); - auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula(); + auto const& formula02 = formulas[0].getRawFormula()->asProbabilityOperatorFormula(); ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType())); - auto formula001 = formulaParser.parseSingleFormulaFromString("P>=0.17 [ F \"one\"]")->asProbabilityOperatorFormula(); - - auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.10 [ F \"one\"]")->asProbabilityOperatorFormula(); - auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.17 [ F \"one\"]")->asProbabilityOperatorFormula(); + auto const& formula001 = formulas[1].getRawFormula()->asProbabilityOperatorFormula(); + auto const& formula02b = formulas[2].getRawFormula()->asProbabilityOperatorFormula(); + auto const& formula001b = formulas[3].getRawFormula()->asProbabilityOperatorFormula(); // Customize and perform model-building. storm::generator::NextStateGeneratorOptions options; diff --git a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index 1b873a935..dedb5e36e 100644 --- a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -20,14 +20,18 @@ TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) { storm::Environment env; storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program); + std::string formulaString = ""; + formulaString += "P<=0.16 [ F \"one\"];\n"; + formulaString += "P<=0.05 [ F \"one\"];\n"; + auto formulas = formulaParser.parseFromString(formulaString); + auto const& formula02b = formulas[0].getRawFormula()->asProbabilityOperatorFormula(); + auto const& formula001b = formulas[1].getRawFormula()->asProbabilityOperatorFormula(); + // auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula(); // ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType())); // auto formula001 = formulaParser.parseSingleFormulaFromString("P>=0.17 [ F \"one\"]")->asProbabilityOperatorFormula(); - auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.16 [ F \"one\"]")->asProbabilityOperatorFormula(); - auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.05 [ F \"one\"]")->asProbabilityOperatorFormula(); - // Customize and perform model-building. storm::generator::NextStateGeneratorOptions options(formula02b);