sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed MDP tests 

Former-commit-id: 058bcbc4c6
main
sjunges 9 years ago
parent
d97b0b2897
commit
19bf801456
1 changed files with 10 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp

9
test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp
View File

@ -20,13 +20,15 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
std::string formulaFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaFile, program);
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505");
@ -64,6 +66,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(mdpModelchecker->getSettings().doApprox());
ASSERT_TRUE(mdpModelchecker->getSettings().doSample());
@ -85,12 +88,15 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54");
@ -110,6 +116,7 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(mdpModelchecker->getSettings().doApprox());
ASSERT_TRUE(mdpModelchecker->getSettings().doSample());
ASSERT_FALSE(mdpModelchecker->getSettings().doSmt());

Write Preview
Loading…
Cancel
Save