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)