diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index f87f4c652..44e35f5c7 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -8,355 +8,391 @@ #include "storm-pars/api/storm-pars.h" #include "storm/api/storm.h" -TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; - std::string formulaAsString = "P<=0.84 [F s=5 ]"; - std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - - // Program and formula - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; - std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; - std::string constantsAsString = "pL=0.9,TOAck=0.5"; - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; - std::string formulaAsString = "R>2.5 [ C<=300]"; - std::string constantsAsString = "pL=0.9,TOAck=0.5"; - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; - std::string formulaAsString = "P<=0.84 [F s=5 ]"; - std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - - // Program and formula - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto regionChecker = storm::api::initializeValidatingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; - std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; - std::string constantsAsString = "pL=0.9,TOAck=0.5"; - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeValidatingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; - std::string formulaAsString = "R>2.5 [ C<=300]"; - std::string constantsAsString = "pL=0.9,TOAck=0.5"; - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeValidatingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; - std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; - std::string constantsAsString = ""; - carl::VariablePool::getInstance().clear(); - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; - std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; - std::string constantsAsString = ""; //!! this model will have 4 parameters - carl::VariablePool::getInstance().clear(); - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; - std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]"; - std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); - auto allVioHardRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; - std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]"; - std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); - auto allVioHardRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; - std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]"; - std::string constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5 - carl::VariablePool::getInstance().clear(); - - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.9<=PF<=0.99", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.8<=PF<=0.9", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.01<=PF<=0.8", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; - std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]"; - std::string constantsAsString = "PF=0.9,badC=0.2"; - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +namespace { + class DoubleViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + class RationalPiEnvironment { + public: + typedef storm::RationalNumber ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + }; + template + class SparseDtmcParameterLiftingTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + SparseDtmcParameterLiftingTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + virtual void SetUp() { carl::VariablePool::getInstance().clear(); } + virtual void TearDown() { carl::VariablePool::getInstance().clear(); } + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + DoubleViEnvironment, + RationalPiEnvironment + > TestingTypes; + + TYPED_TEST_CASE(SparseDtmcParameterLiftingTest, TestingTypes); + + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P<=0.84 [F s=5 ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { + typedef typename TestFixture::ValueType ValueType; + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { + typedef typename TestFixture::ValueType ValueType; + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [ C<=300]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { + typedef typename TestFixture::ValueType ValueType; + if (!std::is_same::value) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P<=0.84 [F s=5 ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto regionChecker = storm::api::initializeValidatingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + } + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { + typedef typename TestFixture::ValueType ValueType; + if (!std::is_same::value) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeValidatingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + } + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { + typedef typename TestFixture::ValueType ValueType; + + if (!std::is_same::value) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [ C<=300]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeValidatingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + } + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; + std::string constantsAsString = ""; + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = ""; //!! this model will have 4 parameters + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; + std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); + auto allVioHardRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(this->env(), allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; + std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); + auto allVioHardRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(this->env(), allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; + std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]"; + std::string constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5 + + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.9<=PF<=0.99", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.8<=PF<=0.9", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.01<=PF<=0.8", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; + std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]"; + std::string constantsAsString = "PF=0.9,badC=0.2"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } } - #endif diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp index b5a4138ec..3d3c97caa 100644 --- a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -8,294 +8,338 @@ #include "storm-pars/api/storm-pars.h" #include "storm/api/storm.h" -TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; - std::string formulaFile = "P<=0.17 [ F \"doubles\" ]"; - - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); - auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); - auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; - std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]"; - - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); - auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); - auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; - std::string formulaFile = "P<=0.17 [ F \"doubles\" ]"; - - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeValidatingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); - auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); - auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; - std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]"; - - carl::VariablePool::getInstance().clear(); - - storm::prism::Program program = storm::api::parseProgram(programFile); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeValidatingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); - auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); - auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, coin_Prob) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm"; - std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]"; +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +namespace { + class DoubleViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + class RationalPIEnvironment { + public: + typedef storm::RationalNumber ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + }; + template + class SparseMdpParameterLiftingTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + SparseMdpParameterLiftingTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + virtual void SetUp() { carl::VariablePool::getInstance().clear(); } + virtual void TearDown() { carl::VariablePool::getInstance().clear(); } + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + DoubleViEnvironment, + RationalPIEnvironment + > TestingTypes; + + TYPED_TEST_CASE(SparseMdpParameterLiftingTest, TestingTypes); + + TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; + std::string formulaFile = "P<=0.17 [ F \"doubles\" ]"; + - storm::prism::Program program = storm::api::parseProgram(programFile); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + storm::prism::Program program = storm::api::parseProgram(programFile); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); + auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); + auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); + TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; + std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]"; + - //start testing - auto allSatRegion = storm::api::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters); - auto exBothRegion = storm::api::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters); - auto allVioRegion = storm::api::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, brp_Prop) { + storm::prism::Program program = storm::api::parseProgram(programFile); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); + auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); + auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; - std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]"; - std::string constantsAsString = "TOMsg=0.0,TOAck=0.0"; - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } + + TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) { + typedef typename TestFixture::ValueType ValueType; + if (!std::is_same::value) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; + std::string formulaFile = "P<=0.17 [ F \"doubles\" ]"; + + + storm::prism::Program program = storm::api::parseProgram(programFile); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeValidatingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); + auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); + auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); + + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + } + } + + TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) { + typedef typename TestFixture::ValueType ValueType; + if (!std::is_same::value) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; + std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]"; + + + storm::prism::Program program = storm::api::parseProgram(programFile); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeValidatingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + auto allSatRegion = storm::api::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); + auto exBothRegion = storm::api::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); + auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); + + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + } + } + + TYPED_TEST(SparseMdpParameterLiftingTest, coin_Prob) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm"; + std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion = storm::api::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters); + auto exBothRegion = storm::api::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters); + auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.5<=p2<=0.6", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + } - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); + TYPED_TEST(SparseMdpParameterLiftingTest, brp_Prop) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]"; + std::string constantsAsString = "TOMsg=0.0,TOAck=0.0"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); + } - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, brp_Rew) { + TYPED_TEST(SparseMdpParameterLiftingTest, brp_Rew) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; - std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; - std::string constantsAsString = "pL=0.9,TOAck=0.5"; - - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - -TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { + } - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; - std::string formulaAsString = "R>2.5 [ C<=300 ]"; - std::string constantsAsString = "pL=0.9,TOAck=0.5"; - - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + TYPED_TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [ C<=300 ]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); + } - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} - - -TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; - std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; - std::string constantsAsString = ""; - carl::VariablePool::getInstance().clear(); - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + TYPED_TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; + std::string constantsAsString = ""; + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + } - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); -} + TYPED_TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { + + typedef typename TestFixture::ValueType ValueType; + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = ""; //!! this model will have 4 parameters + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(this->env(), model, storm::api::createTask(formulas[0], true)); + + //start testing + auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + auto exBothRegion=storm::api::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); + auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); + + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + + } -TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; - std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; - std::string constantsAsString = ""; //!! this model will have 4 parameters - carl::VariablePool::getInstance().clear(); - storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); - std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formulas[0], true)); - - //start testing - auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); - auto exBothRegion=storm::api::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); - auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); - - carl::VariablePool::getInstance().clear(); } - - - #endif diff --git a/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..2db2b5703 --- /dev/null +++ b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,200 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/parser/AutoParser.h" +#include "storm/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" + +TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { + std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); + storm::Environment env; + // Increase precision a little to get more accurate results + env.solver().minMax().setPrecision(env.solver().minMax().getPrecision() * storm::utility::convertNumber(1e-2)); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + + std::unique_ptr result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/36.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/36.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(2.0/36.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(2.0/36.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(3.0/36.0, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(3.0/36.0, quantitativeResult6[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(22.0/3.0, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(22.0/3.0, quantitativeResult8[0], storm::settings::getModule().getPrecision()); + + abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = stateRewardModelChecker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(22.0/3.0, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = stateRewardModelChecker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(22.0/3.0, quantitativeResult10[0], storm::settings::getModule().getPrecision()); + + abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = stateAndTransitionRewardModelChecker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(44.0/3.0, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = stateAndTransitionRewardModelChecker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(44.0/3.0, quantitativeResult12[0], storm::settings::getModule().getPrecision()); +} + +TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) { + storm::Environment env; + // Increase precision a little to get more accurate results + env.solver().minMax().setPrecision(env.solver().minMax().getPrecision() * storm::utility::convertNumber(1e-2)); + + std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(3172ull, mdp->getNumberOfStates()); + ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/16.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/16.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(30.0/7.0, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); + + result = checker.check(env, *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(30.0/7.0, quantitativeResult6[0], storm::settings::getModule().getPrecision()); +} + diff --git a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index a10f772fc..000000000 --- a/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,380 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.h" -#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/models/symbolic/Mdp.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" - -TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333333333333375, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); -} - diff --git a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index 64ca71caf..000000000 --- a/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,273 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" - -#include "storm/settings/modules/GmmxxEquationSolverSettings.h" - -#include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" - -TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333333333333375, quantitativeResult7[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult8[0], storm::settings::getModule().getPrecision()); - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> stateRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333333333333375, quantitativeResult9[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult10[0], storm::settings::getModule().getPrecision()); - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(14.666663348674774, quantitativeResult12[0], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(3172ull, mdp->getNumberOfStates()); - ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.2857120959008661, quantitativeResult6[0], storm::settings::getModule().getPrecision()); -} - -TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - storm::generator::NextStateGeneratorOptions options; - options.setBuildAllLabels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - EXPECT_EQ(4ull, model->getNumberOfStates()); - EXPECT_EQ(11ull, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(7ull, mdp->getNumberOfChoices()); - - auto solverFactory = std::make_unique>(storm::solver::MinMaxMethodSelection::PolicyIteration); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); - - storm::modelchecker::CheckTask checkTask(*formula); - checkTask.setProduceSchedulers(true); - - std::unique_ptr result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); - EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); - - checkTask = storm::modelchecker::CheckTask(*formula); - checkTask.setProduceSchedulers(true); - result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); - EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); -} - -TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); - EXPECT_EQ(3ull, model->getNumberOfStates()); - EXPECT_EQ(4ull, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(4ull, mdp->getNumberOfChoices()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); - - storm::modelchecker::CheckTask checkTask(*formula); - - std::unique_ptr result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index 494516b0d..000000000 --- a/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,272 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/LpMinMaxLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" - -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" - -TEST(LpMdpPrctlModelCheckerTest, Dice) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult8[0], storm::settings::getModule().getPrecision()); - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> stateRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult10[0], storm::settings::getModule().getPrecision()); - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(14.666666666, quantitativeResult11[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(14.666666666, quantitativeResult12[0], storm::settings::getModule().getPrecision()); -} - -TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(3172ull, mdp->getNumberOfStates()); - ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.285714286, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.285714286, quantitativeResult6[0], storm::settings::getModule().getPrecision()); -} - -TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - storm::generator::NextStateGeneratorOptions options; - options.setBuildAllLabels(); - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - EXPECT_EQ(4ull, model->getNumberOfStates()); - EXPECT_EQ(11ull, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(7ull, mdp->getNumberOfChoices()); - - auto solverFactory = std::make_unique>(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); - - storm::modelchecker::CheckTask checkTask(*formula); - checkTask.setProduceSchedulers(true); - - std::unique_ptr result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); - EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); - - checkTask = storm::modelchecker::CheckTask(*formula); - checkTask.setProduceSchedulers(true); - result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); - EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); - EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); -} - -// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is -// currently not implemented and also not supported by PRISM. -TEST(LpMdpPrctlModelCheckerTest, TinyRewards) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); - EXPECT_EQ(3ull, model->getNumberOfStates()); - EXPECT_EQ(4ull, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(4ull, mdp->getNumberOfChoices()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); - - storm::modelchecker::CheckTask checkTask(*formula); - - std::unique_ptr result = checker.check(checkTask); - - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp similarity index 63% rename from src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp rename to src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp index e700f347e..ed3abb16b 100644 --- a/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp @@ -14,181 +14,7 @@ #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm/parser/AutoParser.h" -TEST(NativeMdpPrctlModelCheckerTest, Dice) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult8[0], storm::settings::getModule().getPrecision()); - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> stateRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult10[0], storm::settings::getModule().getPrecision()); - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(14.6666677, quantitativeResult11[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(14.666663348674774, quantitativeResult12[0], storm::settings::getModule().getPrecision()); -} - -TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(3172ull, mdp->getNumberOfStates()); - ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(4.2857120959008661, quantitativeResult6[0], storm::settings::getModule().getPrecision()); -} - -TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) { +TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp; @@ -207,7 +33,7 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -239,7 +65,7 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -257,7 +83,6 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::getModule().getPrecision()); EXPECT_NEAR(.5, quantitativeResult2[1], storm::settings::getModule().getPrecision()); } - { matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); matrixBuilder.newRowGroup(0); @@ -280,7 +105,7 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -338,7 +163,7 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) { } } -TEST(NativeMdpPrctlModelCheckerTest, LRA) { +TEST(LraMdpPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp; @@ -366,7 +191,7 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -488,7 +313,7 @@ TEST(NativeMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..dcdb3c70e --- /dev/null +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -0,0 +1,278 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "test/storm_gtest.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/settings/SettingsManager.h" +#include "storm/api/builder.h" +#include "storm/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/parser/AutoParser.h" + +namespace { + class SparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + // TODO: this should be part of the environment + static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } + }; + class SparseDoubleSoundValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + // TODO: this should be part of the environment + static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } + }; + class SparseRationalPolicyIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + // TODO: this should be part of the environment + static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } + }; + class SparseRationalRationalSearchEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); + return env; + } + // TODO: this should be part of the environment + static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } + }; + + template + class MdpPrctlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Mdp SparseModelType; + typedef typename storm::models::symbolic::Mdp SymbolicModelType; + + MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + bool isSymbolicModel() const { return std::is_same::value; } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + return result; + } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + return std::make_shared>(*model); + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { + return std::make_shared>(*model); + } else if (TestType::engine() == storm::settings::modules::CoreSettings::Engine::Dd) { + return std::make_shared>(*model); + } + } + + bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQualitativeCheckResult().forallTrue(); + } + + ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); + } + + private: + storm::Environment _environment; + + std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { + if (isSparseModel()) { + return std::make_unique(model->template as()->getInitialStates()); + } else { + return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); + } + } + }; + + typedef ::testing::Types< + SparseDoubleValueIterationEnvironment, + SparseDoubleSoundValueIterationEnvironment, + SparseRationalPolicyIterationEnvironment, + SparseRationalRationalSearchEnvironment + > TestingTypes; + + TYPED_TEST_CASE(MdpPrctlModelCheckerTest, TestingTypes); + + + TYPED_TEST(MdpPrctlModelCheckerTest, Dice) { + std::string formulasString = "Pmin=? [F \"two\"]"; + formulasString += "; Pmax=? [F \"two\"]"; + formulasString += "; Pmin=? [F \"three\"]"; + formulasString += "; Pmax=? [F \"three\"]"; + formulasString += "; Pmin=? [F \"four\"]"; + formulasString += "; Pmax=? [F \"four\"]"; + formulasString += "; Rmin=? [F \"done\"]"; + formulasString += "; Rmax=? [F \"done\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(169ul, model->getNumberOfStates()); + EXPECT_EQ(436ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[6]); + EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[7]); + EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) { + std::string formulasString = "Pmin=? [F \"elected\"]"; + formulasString += "; Pmax=? [F \"elected\"]"; + formulasString += "; Pmin=? [F<=25 \"elected\"]"; + formulasString += "; Pmax=? [F<=25 \"elected\"]"; + formulasString += "; Rmin=? [F \"elected\"]"; + formulasString += "; Rmax=? [F \"elected\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(3172ul, model->getNumberOfStates()); + EXPECT_EQ(7144ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) { + std::string formulasString = "Rmin=? [F \"target\"]"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(3ul, model->getNumberOfStates()); + EXPECT_EQ(4ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } +} \ No newline at end of file diff --git a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index a981a0929..000000000 --- a/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,374 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.h" -#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/parser/FormulaParser.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/models/symbolic/Mdp.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/modules/GeneralSettings.h" - -#include "storm/settings/modules/NativeEquationSolverSettings.h" - -TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::HybridMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857120959008661, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..751a28ed2 --- /dev/null +++ b/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,142 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +#include "storm/parser/AutoParser.h" +#include "storm/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" + +namespace { + class DoubleViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + class DoubleSoundViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().setForceSoundness(true); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + }; + class DoublePIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + class RationalPIEnvironment { + public: + typedef storm::RationalNumber ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + }; + // class RationalRationalSearchEnvironment { + // public: + // typedef storm::RationalNumber ValueType; + // static storm::Environment createEnvironment() { + // storm::Environment env; + // env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); + // return env; + // } + // }; + + template + class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + DoubleViEnvironment, + DoubleSoundViEnvironment, + DoublePIEnvironment, + RationalPIEnvironment + //RationalRationalSearchEnvironment + > TestingTypes; + + TYPED_TEST_CASE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes); + + + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) { + typedef typename TestFixture::ValueType ValueType; + + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + storm::generator::NextStateGeneratorOptions options; + options.setBuildAllLabels(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); + EXPECT_EQ(4ull, model->getNumberOfStates()); + EXPECT_EQ(11ull, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->template as>(); + + EXPECT_EQ(7ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + checkTask.setProduceSchedulers(true); + + std::unique_ptr result = checker.check(this->env(), checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); + + checkTask = storm::modelchecker::CheckTask(*formula); + checkTask.setProduceSchedulers(true); + result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); + } +} \ No newline at end of file diff --git a/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp index c4b5156ad..e5843b4e1 100644 --- a/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -10,8 +10,10 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm/environment/Environment.h" TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(T>=5/3 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // true @@ -25,11 +27,11 @@ TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } diff --git a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index ad9699e46..d2c116358 100644 --- a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -15,9 +15,11 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm/environment/Environment.h" TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { - + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -28,7 +30,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); storm::RationalNumber p1 = storm::utility::convertNumber(11.0); p1 /= storm::utility::convertNumber(6.0); @@ -45,7 +47,8 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { - + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -54,7 +57,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::api::buildSparseModel(program, formulas)->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); // we do our checks with rationals to avoid numerical issues when doing polytope computations... @@ -74,6 +77,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) "; @@ -83,7 +87,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::api::buildSparseModel(program, formulas)->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {1.266666667,0.1617571721,0.5}; @@ -104,6 +108,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true @@ -115,16 +120,17 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj std::shared_ptr> ma = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative @@ -137,16 +143,17 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) uint_fast64_t const initState = *ma->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(1.3, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi( Pmax=? [ F<=0.1 \"one_job_finished\"], Pmin=? [F<=0.2 \"all_jobs_finished\"]) "; @@ -156,7 +163,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::api::buildSparseModel(program, formulas)->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {0.2591835573, 0.01990529674}; diff --git a/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index 760184e40..7b2479ec3 100644 --- a/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -8,8 +8,10 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm/environment/Environment.h" TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical @@ -25,18 +27,18 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } - TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; std::string formulasAsString = "multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical @@ -48,7 +50,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 025497515..3f73da77e 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -10,9 +10,11 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/constants.h" #include "storm/api/storm.h" +#include "storm/environment/Environment.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small) { - + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; std::string constantsDef = "N=2"; std::string formulasAsString = "Pmax=? [ F{\"r\"}<=1 x=N ] "; @@ -62,6 +64,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; std::string constantsDef = "N=10"; @@ -94,6 +97,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm"; std::string constantsDef = ""; @@ -154,6 +158,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm"; std::string constantsDef = "N=1000,K=2,reset=true"; @@ -182,6 +187,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"; std::string constantsDef = ""; @@ -207,6 +213,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm"; std::string constantsDef = ""; @@ -273,6 +280,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; std::string constantsDef = "N=2"; @@ -292,19 +300,19 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_EQ(storm::utility::convertNumber(0.5), result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_EQ(storm::utility::convertNumber(0.125), result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_EQ(storm::utility::convertNumber(0.0), result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[3]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p1 = {storm::utility::convertNumber(0.5), storm::utility::convertNumber(0.5)}; std::vector q1 = {storm::utility::convertNumber(0.125), storm::utility::convertNumber(0.75)}; @@ -313,7 +321,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[4]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p2 = {storm::utility::convertNumber(0.0), storm::utility::convertNumber(0.75)}; expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p2})); @@ -324,7 +332,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[5]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p3 = {storm::utility::convertNumber(0.0), storm::utility::convertNumber(-0.75)}; std::vector q3 = {storm::utility::convertNumber(-0.5), storm::utility::convertNumber(0.0)}; @@ -337,6 +345,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; std::string constantsDef = "N=10"; @@ -353,17 +362,17 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber(0.5), 5); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::pow(storm::utility::convertNumber(0.5), 15); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("2539/4096"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); @@ -372,6 +381,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm"; std::string constantsDef = ""; @@ -393,42 +403,42 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); storm::RationalNumber expectedResult = storm::utility::convertNumber("1/5"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("0"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("0"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[3]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("1/50"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[4]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("0"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[5]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("1/50"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[6]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[6]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("1/50"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[7]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[7]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p = {storm::utility::convertNumber("1/10"), storm::utility::convertNumber("0")}; std::vector q = {storm::utility::convertNumber("0"), storm::utility::convertNumber("19/100")}; @@ -440,6 +450,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm"; std::string constantsDef = "N=1000,K=2,reset=true"; @@ -455,17 +466,18 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"; std::string constantsDef = ""; @@ -481,12 +493,12 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { std::unique_ptr result; - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); storm::RationalNumber expectedResult = storm::utility::convertNumber("29487882838281/35184372088832"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p = {storm::utility::convertNumber("29487882838281/35184372088832"), storm::utility::convertNumber("7/8")}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p})); @@ -496,6 +508,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm"; std::string constantsDef = ""; @@ -520,14 +533,14 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) { storm::RationalNumber expectedResult = storm::utility::convertNumber("81/100"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p1 = {storm::utility::convertNumber("1"), storm::utility::convertNumber("27/64")}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p1})); EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p2 = {storm::utility::convertNumber("1"), storm::utility::convertNumber("243/640")}; std::vector q2 = {storm::utility::convertNumber("81/256"), storm::utility::convertNumber("27/64")}; @@ -535,7 +548,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) { EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[3]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector p3 = {storm::utility::convertNumber("81/160"), storm::utility::convertNumber("243/640")}; std::vector q3 = {storm::utility::convertNumber("2187/10240"), storm::utility::convertNumber("27/64")}; diff --git a/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 22af2f899..947cbde55 100644 --- a/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -10,9 +10,10 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" - +#include "storm/environment/Environment.h" TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical @@ -26,21 +27,22 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical @@ -52,12 +54,13 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical @@ -69,12 +72,13 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm"; std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; @@ -86,11 +90,12 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { + storm::Environment env; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_dpm100.nm"; std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical @@ -102,7 +107,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(121.6128842, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); } diff --git a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index ebeb02282..000000000 --- a/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,377 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/logic/Formulas.h" -#include "storm/utility/solver.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "storm/parser/FormulaParser.h" -#include "storm/parser/PrismParser.h" -#include "storm/builder/DdPrismModelBuilder.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/modules/NativeEquationSolverSettings.h" - -#include "storm/settings/modules/GeneralSettings.h" - -TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("coinflips"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(169ul, model->getNumberOfStates()); - EXPECT_EQ(436ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333317041397095, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(4.2856904569131631, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856904569131631, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); - storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(3172ul, model->getNumberOfStates()); - EXPECT_EQ(7144ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: this precision bound is not really good. - EXPECT_NEAR(4.2857, quantitativeResult5.getMin(), 100 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857, quantitativeResult5.getMax(), 100 * storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: this precision bound is not really good. - EXPECT_NEAR(4.2857, quantitativeResult6.getMin(), 100 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2857, quantitativeResult6.getMax(), 100 * storm::settings::getModule().getPrecision()); -} diff --git a/src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index a2e6825f8..000000000 --- a/src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,192 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" -#include "storm/solver/TopologicalMinMaxLinearEquationSolver.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/TopologicalValueIterationEquationSolverSettings.h" -#include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" - -#include "storm-config.h" - -TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { - //storm::settings::Settings* s = storm::settings::Settings::getInstance(); - std::shared_ptr> mdp = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew")->as>(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(mdp->getNumberOfStates(), 169ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); - - std::unique_ptr result = mc.check(*formula); - - ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = mc.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = mc.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif - - // ------------- state rewards -------------- - std::shared_ptr> stateRewardMdp = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", "")->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateRewardModelChecker.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(7.333329499, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(7.33333151, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif - - // -------------------------------- state and transition reward ------------------------ - std::shared_ptr> stateAndTransitionRewardMdp = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew")->as>(); - - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique>()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(14.6666581, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); - - result = stateAndTransitionRewardModelChecker.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(14.666658998, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(14.666663, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif -} - -TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> mdp = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew")->as>(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::make_unique>()); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = mc.check(*formula); - - ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1), - storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(1, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = mc.check(*formula); - - ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = mc.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(4.285701547, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = mc.check(*formula); - -#ifdef STORM_HAVE_CUDA - ASSERT_NEAR(4.285689611, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#else - ASSERT_NEAR(4.285703591, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -#endif -} diff --git a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp index b23b56456..9a6048bf3 100644 --- a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp @@ -1,19 +1,19 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "test/storm/testmacros.h" +#include "test/storm_gtest.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" #include "storm/storage/SparseMatrix.h" -#if GTEST_HAS_PARAM_TEST namespace { class DoubleViEnvironment { public: typedef double ValueType; + static const bool isExact = false; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -24,6 +24,7 @@ namespace { class DoubleSoundViEnvironment { public: typedef double ValueType; + static const bool isExact = false; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -35,6 +36,7 @@ namespace { class DoubleTopologicalViEnvironment { public: typedef double ValueType; + static const bool isExact = false; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); @@ -45,6 +47,7 @@ namespace { class DoublePIEnvironment { public: typedef double ValueType; + static const bool isExact = false; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); @@ -55,6 +58,7 @@ namespace { class RationalPIEnvironment { public: typedef storm::RationalNumber ValueType; + static const bool isExact = true; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); @@ -64,6 +68,7 @@ namespace { class RationalRationalSearchEnvironment { public: typedef storm::RationalNumber ValueType; + static const bool isExact = true; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); @@ -77,7 +82,7 @@ namespace { typedef typename TestType::ValueType ValueType; MinMaxLinearEquationSolverTest() : _environment(TestType::createEnvironment()) {} storm::Environment const& env() const { return _environment; } - ValueType precision() const { return storm::utility::convertNumber(1e-6);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} private: storm::Environment _environment; @@ -167,9 +172,6 @@ namespace { } } -#else - TEST(MinMaxLinearEquationSolverTest, ValueParameterizedTestsAreNotSupportedOnThisPlatform) {} -#endif diff --git a/src/test/storm/testmacros.h b/src/test/storm/testmacros.h deleted file mode 100644 index fae24e125..000000000 --- a/src/test/storm/testmacros.h +++ /dev/null @@ -1,30 +0,0 @@ -#pragma once - -#include -#include - -#include "storm/utility/constants.h" -#include "gtest/gtest.h" - -#define STORM_EXPECT_NEAR(val1, val2, abs_error) \ -do { \ - if (std::is_same::type>::type, double>::value) { \ - EXPECT_NEAR(storm::utility::convertNumber(val1), \ - storm::utility::convertNumber(val2), \ - storm::utility::convertNumber(abs_error)); \ - } else if (storm::utility::isZero(abs_error)) { \ - EXPECT_EQ(val1, val2); \ - } else { \ - auto valueDifference = val1; \ - valueDifference -= val2; \ - valueDifference = storm::utility::abs(valueDifference); \ - EXPECT_LT(storm::utility::abs(valueDifference), abs_error); \ - if (valueDifference > abs_error) { \ - std::cout << "Expected " << val2 \ - << " (approx " << storm::utility::convertNumber(val2) \ - << ") but got " << val1 \ - << " (approx " << storm::utility::convertNumber(val1) \ - << ")." << std::endl; \ - } \ - } \ -} while (false) \ No newline at end of file diff --git a/src/test/storm_gtest.h b/src/test/storm_gtest.h new file mode 100644 index 000000000..8631e8fde --- /dev/null +++ b/src/test/storm_gtest.h @@ -0,0 +1,28 @@ +#pragma once + +#include "gtest/gtest.h" + +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/utility/constants.h" + + +namespace testing { + namespace internal { + + GTEST_API_ AssertionResult DoubleNearPredFormat(const char* expr1, + const char* expr2, + const char* abs_error_expr, + storm::RationalNumber val1, + storm::RationalNumber val2, + storm::RationalNumber abs_error) { + const storm::RationalNumber diff = storm::utility::abs(val1 - val2); + if (diff <= abs_error) return AssertionSuccess(); + return AssertionFailure() + << "The difference between " << expr1 << " and " << expr2 + << " is " << diff << " (approx. " << storm::utility::convertNumber(diff) << "), which exceeds " << abs_error_expr << ", where\n" + << expr1 << " evaluates to " << val1 << " (approx. " << storm::utility::convertNumber(val1) << "),\n" + << expr2 << " evaluates to " << val2 << " (approx. " << storm::utility::convertNumber(val2) << "),\n" + << abs_error_expr << " evaluates to " << abs_error << " (approx. " << storm::utility::convertNumber(abs_error) << ")."; + } + } +}