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

fixed more compilation issues, considered the variables occurring in the model when parsing a region (otherwise, distinct variables with the same name would cause problems), adapted Tests to new interface for parameter lifting

tempestpy_adaptions
TimQu 8 years ago
parent
3686c42965
commit
38fa454ace
4 changed files with 90 additions and 53 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. 2
      src/storm/cli/entrypoints.h
  2. 6
      src/storm/utility/storm.h
  3. 103
      src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
  4. 32
      src/test/modelchecker/SparseMdpParameterLiftingTest.cpp

2
src/storm/cli/entrypoints.h
View File

@ -320,7 +320,7 @@ namespace storm {
generateCounterexamples<ValueType>(model, sparseModel, formulas);
} else if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isParameterLiftingSet()) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet(), storm::exceptions::InvalidSettingsException, "Invoked parameter lifting without enabling the parametric engine.");
performParameterLifting<ValueType>(sparseModel, formulas);
storm::performParameterLifting<ValueType>(sparseModel, formulas);
} else {
verifySparseModel<ValueType>(sparseModel, properties, onlyInitialStatesRelevant);
}

6
src/storm/utility/storm.h
View File

@ -309,13 +309,13 @@ namespace storm {
}
template<typename ParametricType>
void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<ParametricType>>, std::shared_ptr<storm::logic::Formula const> const&) {
inline void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<ParametricType>>, std::shared_ptr<storm::logic::Formula const> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting for non-parametric model.");
}
#ifdef STORM_HAVE_CARL
template<>
void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
inline void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel);
auto rewParameters = storm::models::sparse::getRewardParameters(*markovModel);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
@ -374,7 +374,7 @@ namespace storm {
#endif
template<typename ValueType>
void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
inline void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
for (auto const& formula : formulas) {
performParameterLifting(markovModel, formula);
}

103
src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp → src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
View File

@ -9,7 +9,7 @@
#include "storm/models/sparse/Model.h"
#include "modelchecker/parametric/ParameterLifting.h"
TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P<=0.84 [F s=5 ]";
@ -21,13 +21,18 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715");
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", 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));
@ -36,7 +41,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
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";
@ -47,14 +52,18 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
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 exBothHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4", modelParameters); //this region has a local maximum!
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));
@ -64,7 +73,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
}
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
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) ]";
@ -75,18 +84,22 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("");
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
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)) ]";
@ -97,13 +110,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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::storage::ParameterRegion<storm::RationalFunction>::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::storage::ParameterRegion<storm::RationalFunction>::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::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));
@ -112,7 +129,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
@ -123,15 +140,19 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
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(formulas[0]);
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
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));
@ -141,7 +162,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
@ -154,13 +175,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8");
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8", 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));
@ -169,7 +194,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
@ -181,11 +206,15 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("");
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));

32
src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp → src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
View File

@ -9,7 +9,7 @@
#include "storm/models/sparse/Model.h"
#include "storm/modelchecker/parametric/ParameterLifting.h"
TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
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\" ]";
@ -20,12 +20,16 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext->specifyFormula(*formulas[0]);
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6");
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(*formulas[0]);
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));
@ -35,7 +39,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
TEST(SparseMdpParameterLiftingTest, coin_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.pm";
std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
@ -46,13 +50,17 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
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>>();
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext->specifyFormula(*formulas[0]);
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(*formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6");
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.7,0.55<=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));
Write Preview
Loading…
Cancel
Save