From 1a1d46ceda13beddad4eb95399df996037b36654 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Wed, 16 Aug 2023 15:59:55 +0200 Subject: [PATCH] fixed tests because of shield export change --- src/test/storm/logic/FragmentCheckerTest.cpp | 12 +- ...ieldGenerationMdpPrctlModelCheckerTest.cpp | 57 ++++++--- ...ieldGenerationSmgRpatlModelCheckerTest.cpp | 117 +++++++++++++----- .../storm/parser/GameShieldingParserTest.cpp | 12 +- .../storm/parser/MdpShieldingParserTest.cpp | 10 +- 5 files changed, 136 insertions(+), 72 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 3583ac019..f4c039f27 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -85,13 +85,13 @@ 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\"]")); + 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 \"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\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); } @@ -202,13 +202,13 @@ 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\"]")); + 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 \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); } diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp index 7fda8f70c..91f677fc7 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm-parsers/api/properties.h" +#include "storm/api/export.h" #include "storm/models/sparse/Smg.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -99,15 +100,15 @@ namespace { 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\" ]"; + std::string formulasString = " Pmax=? [ F <5 \"done\" ]"; + formulasString += "; Pmax=? [ F <5 \"done\" ]"; + formulasString += "; Pmin=? [ F <5 \"done\" ]"; + formulasString += "; 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\" ]"; + formulasString += "; Pmax=? [ F <6 \"two\" ]"; + formulasString += "; Pmax=? [ F <6 \"two\" ]"; + formulasString += "; Pmin=? [ F <6 \"two\" ]"; + formulasString += "; Pmin=? [ F <6 \"two\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/die_selection.nm", formulasString); auto mdp = std::move(modelFormulas.first); @@ -130,66 +131,90 @@ namespace { // shielding results filename = fileNames[0]; - auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08)); + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value08)); tasks[0].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[0].isShieldingTask()); auto result = checker.check(this->env(), tasks[0]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[1]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value08)); tasks[1].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[1].isShieldingTask()); result = checker.check(this->env(), tasks[1]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[2]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value08)); tasks[2].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[2].isShieldingTask()); result = checker.check(this->env(), tasks[2]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[3]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value08)); tasks[3].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[3].isShieldingTask()); result = checker.check(this->env(), tasks[3]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); 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)); + auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value07)); tasks[4].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[4].isShieldingTask()); result = checker.check(this->env(), tasks[4]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[5]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value07)); tasks[5].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[5].isShieldingTask()); result = checker.check(this->env(), tasks[5]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[6]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value07)); tasks[6].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[6].isShieldingTask()); result = checker.check(this->env(), tasks[6]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[7]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value07)); tasks[7].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[7].isShieldingTask()); result = checker.check(this->env(), tasks[7]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(mdp, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); } diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index 096766c29..9009df76f 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -5,6 +5,7 @@ #include "storm/api/builder.h" #include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" +#include "storm/api/export.h" #include "storm-parsers/api/properties.h" #include "storm/models/sparse/Smg.h" @@ -107,23 +108,23 @@ namespace { fileNames.push_back("rightDecisionPostSafetyGamma05PminF5"); // testing create shielding expressions - 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\" ]"; + std::string formulasString = " <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=3 \"target\" ]"; + + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmin=? [ F <=5 \"target\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); auto smg = std::move(modelFormulas.first); @@ -147,131 +148,179 @@ namespace { // shielding results filename = fileNames[0]; - auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09)); + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value09)); tasks[0].setShieldingExpression(preSafetyShieldingExpression); - EXPECT_TRUE(tasks[0].isShieldingTask()); + EXPECT_TRUE(tasks[0].isShieldingTask()); auto result = checker.check(this->env(), tasks[0]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[1]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value09)); tasks[1].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[1].isShieldingTask()); result = checker.check(this->env(), tasks[1]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[2]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value09)); tasks[2].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[2].isShieldingTask()); result = checker.check(this->env(), tasks[2]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[3]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value09)); tasks[3].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[3].isShieldingTask()); result = checker.check(this->env(), tasks[3]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); 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)); + auto postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value09)); tasks[4].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[4].isShieldingTask()); result = checker.check(this->env(), tasks[4]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[5]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value09)); tasks[5].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[5].isShieldingTask()); result = checker.check(this->env(), tasks[5]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[6]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value09)); tasks[6].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[6].isShieldingTask()); result = checker.check(this->env(), tasks[6]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[7]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value09)); tasks[7].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[7].isShieldingTask()); result = checker.check(this->env(), tasks[7]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[8]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value05)); tasks[8].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[8].isShieldingTask()); result = checker.check(this->env(), tasks[8]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[9]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonRelative, value05)); tasks[9].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[9].isShieldingTask()); result = checker.check(this->env(), tasks[9]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[10]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value05)); tasks[10].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[10].isShieldingTask()); result = checker.check(this->env(), tasks[10]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[11]; - preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05)); + preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePreSafety, comparisonAbsolute, value05)); tasks[11].setShieldingExpression(preSafetyShieldingExpression); EXPECT_TRUE(tasks[11].isShieldingTask()); result = checker.check(this->env(), tasks[11]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[12]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value05)); tasks[12].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[12].isShieldingTask()); result = checker.check(this->env(), tasks[12]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[13]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonRelative, value05)); tasks[13].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[13].isShieldingTask()); result = checker.check(this->env(), tasks[13]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[14]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value05)); tasks[14].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[14].isShieldingTask()); result = checker.check(this->env(), tasks[14]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); filename = fileNames[15]; - postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05)); + postSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(typePostSafety, comparisonAbsolute, value05)); tasks[15].setShieldingExpression(postSafetyShieldingExpression); EXPECT_TRUE(tasks[15].isShieldingTask()); result = checker.check(this->env(), tasks[15]); + EXPECT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_TRUE(result->hasShield()); + storm::api::exportShield(smg, result->template asExplicitQuantitativeCheckResult().getShield() , filename + ".shield"); this->getStringsToCompare(filename, shieldingString, compareFileString); EXPECT_EQ(shieldingString, compareFileString); } diff --git a/src/test/storm/parser/GameShieldingParserTest.cpp b/src/test/storm/parser/GameShieldingParserTest.cpp index a6ed3cb88..f19cb757b 100644 --- a/src/test/storm/parser/GameShieldingParserTest.cpp +++ b/src/test/storm/parser/GameShieldingParserTest.cpp @@ -6,9 +6,8 @@ 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::string input = " <> Pmax=? [F \"label\"]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -25,15 +24,13 @@ TEST(GameShieldingParserTest, PreSafetyShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(GameShieldingParserTest, PostShieldTest) { storm::parser::FormulaParser formulaParser; - std::string filename = "postSafetyShieldFileName"; std::string value = "0.7569"; - std::string input = "<" + filename + ", PostSafety, gamma=" + value + "> <> Pmin=? [X !\"label\"]"; + std::string input = " <> Pmin=? [X !\"label\"]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -50,7 +47,6 @@ TEST(GameShieldingParserTest, PostShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(GameShieldingParserTest, OptimalShieldTest) { @@ -60,8 +56,7 @@ TEST(GameShieldingParserTest, OptimalShieldTest) { storm::parser::FormulaParser formulaParser(manager); - std::string filename = "optimalShieldFileName"; - std::string input = "<" + filename + ", Optimal> <> Pmax=? [G x>y]"; + std::string input = " <> Pmax=? [G x>y]"; std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); @@ -76,5 +71,4 @@ TEST(GameShieldingParserTest, OptimalShieldTest) { EXPECT_FALSE(shieldExpression->isPreSafetyShield()); EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } diff --git a/src/test/storm/parser/MdpShieldingParserTest.cpp b/src/test/storm/parser/MdpShieldingParserTest.cpp index 84b69d6db..5efa3e40d 100644 --- a/src/test/storm/parser/MdpShieldingParserTest.cpp +++ b/src/test/storm/parser/MdpShieldingParserTest.cpp @@ -6,9 +6,8 @@ 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::string input = " Pmax=? [F \"label\"]"; std::shared_ptr formula(nullptr); std::vector property; @@ -22,7 +21,6 @@ TEST(MdpShieldingParserTest, PreSafetyShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_FALSE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(MdpShieldingParserTest, PostShieldTest) { @@ -30,7 +28,7 @@ TEST(MdpShieldingParserTest, PostShieldTest) { std::string filename = "postSafetyShieldFileName"; std::string value = "0.95"; - std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]"; + std::string input = " Pmin=? [X !\"label\"]"; std::shared_ptr formula(nullptr); std::vector property; @@ -44,7 +42,6 @@ TEST(MdpShieldingParserTest, PostShieldTest) { EXPECT_FALSE(shieldExpression->isOptimalShield()); EXPECT_TRUE(shieldExpression->isRelative()); EXPECT_EQ(std::stod(value), shieldExpression->getValue()); - EXPECT_EQ(filename, shieldExpression->getFilename()); } TEST(MdpShieldingParserTest, OptimalShieldTest) { @@ -55,7 +52,7 @@ TEST(MdpShieldingParserTest, OptimalShieldTest) { storm::parser::FormulaParser formulaParser(manager); std::string filename = "optimalShieldFileName"; - std::string input = "<" + filename + ", Optimal> Pmax=? [G (a|x>3)]"; + std::string input = " Pmax=? [G (a|x>3)]"; std::shared_ptr formula(nullptr); std::vector property; @@ -67,5 +64,4 @@ TEST(MdpShieldingParserTest, OptimalShieldTest) { EXPECT_FALSE(shieldExpression->isPreSafetyShield()); EXPECT_FALSE(shieldExpression->isPostSafetyShield()); EXPECT_TRUE(shieldExpression->isOptimalShield()); - EXPECT_EQ(filename, shieldExpression->getFilename()); }