diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index 44e35f5c7..b00b44c0d 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -79,6 +79,36 @@ namespace { 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_no_simplification) { + 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), false, false); + + //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;