diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 77bcb3e6f..3752731f2 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp/brp16_2.pm"; - std::string const& formulaAsString = "P<=0.84 [F \"target\" ]"; + std::string const& formulaAsString = "P<=0.84 [F s=5 ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 //Build model, formula, region model checker @@ -92,7 +92,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_rewards16_2.pm"; - std::string const& formulaAsString = "R>2.5 [F \"target\" ]"; + std::string const& formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string const& constantsAsString = "pL=0.9,TOAck=0.5"; //Build model, formula, region model checker @@ -185,7 +185,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_rewards16_2.pm"; - std::string const& formulaAsString = "R>2.5 [F \"success\" ]"; + std::string const& formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; std::string const& constantsAsString = ""; //Build model, formula, region model checker @@ -232,7 +232,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_rewards16_2.pm"; - std::string const& formulaAsString = "R>2.5 [F \"target\" ]"; + std::string const& formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string const& constantsAsString = ""; //!! this model will have 4 parameters //Build model, formula, region model checker