From 4cfbaa3a3367b4f49732a041b419d3f741929ce9 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 10:26:51 +0200 Subject: [PATCH] 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)