From 38fa454ace480ac4759d149452859e56f6aee793 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 9 Mar 2017 11:38:31 +0100
Subject: [PATCH] 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
---
src/storm/cli/entrypoints.h | 2 +-
src/storm/utility/storm.h | 6 +-
...cpp => SparseDtmcParameterLiftingTest.cpp} | 103 +++++++++++-------
....cpp => SparseMdpParameterLiftingTest.cpp} | 32 ++++--
4 files changed, 90 insertions(+), 53 deletions(-)
rename src/test/modelchecker/{SparseDtmcRegionModelCheckerTest.cpp => SparseDtmcParameterLiftingTest.cpp} (76%)
rename src/test/modelchecker/{SparseMdpRegionModelCheckerTest.cpp => SparseMdpParameterLiftingTest.cpp} (64%)
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index 5794c0cd6..b2f716b2a 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -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);
}
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index ef14ff617..efdb6d03a 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -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);
}
diff --git a/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
similarity index 76%
rename from src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
rename to src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
index 6eac5df24..5f43ff5e1 100644
--- a/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
+++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
@@ -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));
diff --git a/src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
similarity index 64%
rename from src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp
rename to src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
index a4952ca7f..b9949ea2f 100644
--- a/src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp
+++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
@@ -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));