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

tests for step bounded properties

tempestpy_adaptions
TimQu 8 years ago
parent
0283e402ad
commit
c4dffe9a8b
3 changed files with 123 additions and 5 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      resources/examples/testfiles/prctl/two_dice.prctl
  2. 62
      src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
  3. 62
      src/test/modelchecker/SparseMdpParameterLiftingTest.cpp

4
resources/examples/testfiles/prctl/two_dice.prctl
View File

@ -1,4 +0,0 @@
P<=0.17 [ F "doubles" ]

62
src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
View File

@ -68,7 +68,36 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear(); 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::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
} }
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
@ -160,6 +189,39 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
carl::VariablePool::getInstance().clear(); 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::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, parameterLiftingContext.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";

62
src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
View File

@ -12,7 +12,37 @@
TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = STORM_TEST_RESOURCES_DIR "/prctl/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]";
std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(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 modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::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(); carl::VariablePool::getInstance().clear();
@ -128,6 +158,36 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) {
carl::VariablePool::getInstance().clear(); 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::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(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 modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {

Write Preview
Loading…
Cancel
Save