diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp
index e5d21d941..61523ef72 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@@ -19,10 +19,8 @@
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidArgumentException.h"
-#include "storm/utility/Stopwatch.h"
#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
-#include "storm/settings/modules/DebugSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
namespace storm {
@@ -32,24 +30,25 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
ParameterLifting<SparseModelType, ConstantType>::ParameterLifting(SparseModelType const& parametricModel) : parametricModel(parametricModel){
+ initializationStopwatch.start();
STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Parameter lifting requires models with only one initial state");
+ initializationStopwatch.stop();
}
template <typename SparseModelType, typename ConstantType>
void ParameterLifting<SparseModelType, ConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+ initializationStopwatch.start();
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a property where only the value in the initial states is relevant.");
STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property.");
- storm::utility::Stopwatch sw(true);
simplifyParametricModel(checkTask);
- sw.stop();
- std::cout << "SIStats: " << sw << std::endl;
initializeUnderlyingCheckers();
currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask), storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property.");
instantiationChecker->specifyFormula(*currentCheckTask);
parameterLiftingChecker->specifyFormula(*currentCheckTask);
+ initializationStopwatch.stop();
}
template <typename SparseModelType, typename ConstantType>
@@ -57,16 +56,20 @@ namespace storm {
RegionCheckResult result = initialResult;
// Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
+ instantiationCheckerStopwatch.start();
if (result == RegionCheckResult::Unknown) {
result = instantiationChecker->check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()] ? RegionCheckResult::CenterSat : RegionCheckResult::CenterViolated;
}
+ instantiationCheckerStopwatch.stop();
// try to prove AllSat or AllViolated, depending on the obtained result
+ parameterLiftingCheckerStopwatch.start();
if(result == RegionCheckResult::ExistsSat || result == RegionCheckResult::CenterSat) {
// show AllSat:
if(parameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
result = RegionCheckResult::AllSat;
} else if (sampleVerticesOfRegion) {
+ parameterLiftingCheckerStopwatch.stop(); instantiationCheckerStopwatch.start();
// Check if there is a point in the region for which the property is violated
auto vertices = region.getVerticesOfRegion(region.getVariables());
for (auto const& v : vertices) {
@@ -74,12 +77,14 @@ namespace storm {
result = RegionCheckResult::ExistsBoth;
}
}
+ instantiationCheckerStopwatch.stop(); parameterLiftingCheckerStopwatch.start();
}
} else if (result == RegionCheckResult::ExistsViolated || result == RegionCheckResult::CenterViolated) {
// show AllViolated:
if(!parameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
result = RegionCheckResult::AllViolated;
} else if (sampleVerticesOfRegion) {
+ parameterLiftingCheckerStopwatch.stop(); instantiationCheckerStopwatch.start();
// Check if there is a point in the region for which the property is satisfied
auto vertices = region.getVerticesOfRegion(region.getVariables());
for (auto const& v : vertices) {
@@ -87,41 +92,12 @@ namespace storm {
result = RegionCheckResult::ExistsBoth;
}
}
+ instantiationCheckerStopwatch.stop(); parameterLiftingCheckerStopwatch.start();
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
}
-
- // TODO remove this:
- if(storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet() && storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismInputSet() && storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {
- std::vector<storm::utility::parametric::Valuation<typename SparseModelType::ValueType>> points;
- if(result == RegionCheckResult::AllSat || result == RegionCheckResult::AllViolated) {
- points = region.getVerticesOfRegion(region.getVariables());
- points.push_back(region.getCenterPoint());
- } else if (result == RegionCheckResult::CenterSat || result == RegionCheckResult::CenterViolated) {
- points.push_back(region.getCenterPoint());
- }
- if(!points.empty()) std::cout << "VALIDATE_REGION:" << region.toString(true) << std::endl;
- for (auto const& p : points) {
- if((result == RegionCheckResult::AllSat) || (result == RegionCheckResult::CenterSat)) {
- std::cout << "EXPECTTRUE:";
- } else {
- std::cout << "EXPECTFALSE:";
- }
- std::cout << "STORMEXECUTABLE --prism " << storm::settings::getModule<storm::settings::modules::IOSettings>().getPrismInputFilename()
- << " --prop " << storm::settings::getModule<storm::settings::modules::IOSettings>().getProperty();
- if( storm::settings::getModule<storm::settings::modules::IOSettings>().isConstantsSet()) {
- std::cout << " -const " << storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString() << ",";
- }
- for(auto varDef = p.begin(); varDef != p.end(); ++varDef) {
- if(varDef!=p.begin()) std::cout << ",";
- std::cout << varDef->first << "=" << storm::utility::convertNumber<double>(varDef->second);
- }
- std::cout << std::endl;
- }
- }
-
-
+ parameterLiftingCheckerStopwatch.stop();
return result;
}
@@ -129,8 +105,6 @@ namespace storm {
std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const {
STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
- storm::utility::Stopwatch sw(true);
-
auto areaOfParameterSpace = region.area();
auto fractionOfUndiscoveredArea = storm::utility::one<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
auto fractionOfAllSatArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
@@ -138,7 +112,7 @@ namespace storm {
std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> regions;
regions.emplace_back(region, RegionCheckResult::Unknown);
- storm::storage::BitVector resultRegions(1, true);
+ storm::storage::BitVector resultRegions(1, false);
uint_fast64_t indexOfCurrentRegion = 0;
while (fractionOfUndiscoveredArea > threshold) {
@@ -151,30 +125,36 @@ namespace storm {
case RegionCheckResult::AllSat:
fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
fractionOfAllSatArea += currentRegion.area() / areaOfParameterSpace;
+ resultRegions.set(indexOfCurrentRegion, true);
break;
case RegionCheckResult::AllViolated:
fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace;
+ resultRegions.set(indexOfCurrentRegion, true);
break;
default:
std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
currentRegion.split(currentRegion.getCenterPoint(), newRegions);
- resultRegions.grow(regions.size() + newRegions.size(), true);
+ resultRegions.grow(regions.size() + newRegions.size(), false);
RegionCheckResult initResForNewRegions = (res == RegionCheckResult::CenterSat) ? RegionCheckResult::ExistsSat :
((res == RegionCheckResult::CenterViolated) ? RegionCheckResult::ExistsViolated :
RegionCheckResult::Unknown);
for(auto& newRegion : newRegions) {
regions.emplace_back(std::move(newRegion), initResForNewRegions);
}
- resultRegions.set(indexOfCurrentRegion, false);
break;
}
++indexOfCurrentRegion;
}
resultRegions.resize(regions.size());
- sw.stop();
- std::cout << "REStats: " << sw << std::endl;
+ if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+ STORM_PRINT_AND_LOG("Parameter Lifting Statistics:" << std::endl);
+ STORM_PRINT_AND_LOG(" Analyzed a total of " << indexOfCurrentRegion << " regions." << std::endl);
+ STORM_PRINT_AND_LOG(" Initialization took " << initializationStopwatch << " seconds." << std::endl);
+ STORM_PRINT_AND_LOG(" Checking sampled models took " << instantiationCheckerStopwatch << " seconds." << std::endl);
+ STORM_PRINT_AND_LOG(" Checking lifted models took " << parameterLiftingCheckerStopwatch << " seconds." << std::endl);
+ }
return storm::utility::vector::filterVector(regions, resultRegions);
}
diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h
index e05f0e183..1557a00d0 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.h
+++ b/src/storm/modelchecker/parametric/ParameterLifting.h
@@ -5,9 +5,9 @@
#include "storm/modelchecker/parametric/RegionCheckResult.h"
#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
-#include "storm/storage/ParameterRegion.h"
-
#include "storm/modelchecker/CheckTask.h"
+#include "storm/storage/ParameterRegion.h"
+#include "storm/utility/Stopwatch.h"
namespace storm {
namespace modelchecker{
@@ -59,7 +59,7 @@ namespace storm {
std::unique_ptr<SparseParameterLiftingModelChecker<SparseModelType, ConstantType>> parameterLiftingChecker;
std::unique_ptr<SparseInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
-
+ mutable storm::utility::Stopwatch initializationStopwatch, instantiationCheckerStopwatch, parameterLiftingCheckerStopwatch;
};
} //namespace parametric
diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
index 90dfd89fd..1370f48cc 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
@@ -18,25 +18,16 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
- this->swInstantiation.start();
auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
- this->swInstantiation.stop();
STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(instantiatedModel);
// Check if there are some optimizations implemented for the specified property
- this->swCheck.start();
if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
- auto result = checkWithHint(modelChecker);
- this->swCheck.stop();
- return result;
- //return checkWithHint(modelChecker);
+ return checkWithHint(modelChecker);
} else {
STORM_LOG_WARN("Checking without hint"); // todo:remove this warning
- auto result = modelChecker.check(*this->currentCheckTask);
- this->swCheck.stop();
- return result;
- //return modelChecker.check(*this->currentCheckTask);
+ return modelChecker.check(*this->currentCheckTask);
}
}
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
index 40d20c21f..6578bd58c 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
@@ -166,10 +166,7 @@ namespace storm {
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
}
- this->swInstantiation.start();
parameterLifter->specifyRegion(region, dirForParameters);
- this->swInstantiation.stop();
- this->swCheck.start();
// Set up the solver
auto solver = solverFactory->create(parameterLifter->getMatrix());
@@ -201,7 +198,6 @@ namespace storm {
result[maybeState] = *maybeStateResIt;
++maybeStateResIt;
}
- this->swCheck.stop();
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
}
diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
index 474082ff8..7d5788728 100644
--- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
@@ -6,8 +6,6 @@
#include "storm/modelchecker/hints/ModelCheckerHint.h"
#include "storm/utility/parametric.h"
-#include "storm/utility/Stopwatch.h"
-
namespace storm {
namespace modelchecker {
namespace parametric {
@@ -20,11 +18,6 @@ namespace storm {
public:
SparseInstantiationModelChecker(SparseModelType const& parametricModel);
-
- ~SparseInstantiationModelChecker() {
- std::cout << "INStats (instantiation/check): " << swInstantiation << "\t" << swCheck << std::endl;
- }
-
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
@@ -37,8 +30,6 @@ namespace storm {
SparseModelType const& parametricModel;
std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
- storm::utility::Stopwatch swInstantiation, swCheck;
-
private:
// store the current formula. Note that currentCheckTask only stores a reference to the formula.
std::shared_ptr<storm::logic::Formula const> currentFormula;
diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
index cfc13cda2..34debd0f5 100644
--- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
@@ -19,24 +19,15 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
- this->swInstantiation.start();
auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
- this->swInstantiation.stop();
STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(instantiatedModel);
// Check if there are some optimizations implemented for the specified property
- this->swCheck.start();
if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
- auto result = checkWithResultHint(modelChecker);
- this->swCheck.stop();
- return result;
- //return checkWithResultHint(modelChecker);
+ return checkWithResultHint(modelChecker);
} else {
- auto result = modelChecker.check(*this->currentCheckTask);
- this->swCheck.stop();
- return result;
- //return modelChecker.check(*this->currentCheckTask);
+ return modelChecker.check(*this->currentCheckTask);
}
}
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
index e8bcb9256..e7060e42b 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
@@ -200,10 +200,7 @@ namespace storm {
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
}
- this->swInstantiation.start();
parameterLifter->specifyRegion(region, dirForParameters);
- this->swInstantiation.stop();
- this->swCheck.start();
// Set up the solver
auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix());
@@ -241,7 +238,6 @@ namespace storm {
result[maybeState] = *maybeStateResIt;
++maybeStateResIt;
}
- this->swCheck.stop();
return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
}
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
index ff9a4a7f9..e16cff9b1 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
@@ -22,7 +22,6 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
- swInit.start();
reset();
currentFormula = checkTask.getFormula().asSharedPointer();
currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
@@ -46,7 +45,6 @@ namespace storm {
specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
}
}
- swInit.stop();
}
template <typename SparseModelType, typename ConstantType>
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
index 0d5629dda..3eaa520ec 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
@@ -7,8 +7,6 @@
#include "storm/solver/OptimizationDirection.h"
#include "storm/utility/parametric.h"
-#include "storm/utility/Stopwatch.h"
-
namespace storm {
namespace modelchecker {
namespace parametric {
@@ -24,10 +22,6 @@ namespace storm {
public:
SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
- ~SparseParameterLiftingModelChecker() {
- std::cout << "PLStats (init/instantiation/check): " << swInit << "\t" << swInstantiation << "\t" << swCheck << std::endl;
- }
-
virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
@@ -56,8 +50,6 @@ namespace storm {
SparseModelType const& parametricModel;
std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
- storm::utility::Stopwatch swInit, swInstantiation, swCheck;
-
private:
// store the current formula. Note that currentCheckTask only stores a reference to the formula.
std::shared_ptr<storm::logic::Formula const> currentFormula;
diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp
index 8d6b82447..cb42bfd4b 100644
--- a/src/storm/settings/modules/CoreSettings.cpp
+++ b/src/storm/settings/modules/CoreSettings.cpp
@@ -53,9 +53,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, parameterLiftingOptionName, false, "Sets whether parameter lifting is applied.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("parameterspace", "The considered parameter-space given in format a<=x<=b,c<=y<=d").build())
- .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The refinement converges as soon as the fraction of unknown area falls below this threshold").setDefaultValueDouble(0.05).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, parameterLiftingOptionName, false, "Sets whether parameter lifting is applied.").build());
std::vector<std::string> smtSolvers = {"z3", "mathsat"};
this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.")
@@ -98,14 +96,6 @@ namespace storm {
return this->getOption(parameterLiftingOptionName).getHasOptionBeenSet();
}
- std::string CoreSettings::getParameterLiftingParameterSpace() const {
- return this->getOption(parameterLiftingOptionName).getArgumentByName("parameterspace").getValueAsString();
- }
-
- double CoreSettings::getParameterLiftingThreshold() const {
- return this->getOption(parameterLiftingOptionName).getArgumentByName("threshold").getValueAsDouble();
- }
-
storm::solver::LpSolverType CoreSettings::getLpSolver() const {
std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString();
if (lpSolverName == "gurobi") {
diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h
index 5f681b319..719449dd2 100644
--- a/src/storm/settings/modules/CoreSettings.h
+++ b/src/storm/settings/modules/CoreSettings.h
@@ -87,17 +87,6 @@ namespace storm {
*/
bool isParameterLiftingSet() const;
- /*!
- * Retrieves a string that defines the parameter space considered for parameter lifting
- * @return A string that defines the parameter space considered for parameter lifting
- */
- std::string getParameterLiftingParameterSpace() const;
-
- /*!
- * Retrieves the refinement threshold that is considered for parameter lifting
- */
- double getParameterLiftingThreshold() const;
-
/*!
* Retrieves the selected LP solver.
*
diff --git a/src/storm/settings/modules/ParametricSettings.cpp b/src/storm/settings/modules/ParametricSettings.cpp
index ba7470ac2..844f214c3 100644
--- a/src/storm/settings/modules/ParametricSettings.cpp
+++ b/src/storm/settings/modules/ParametricSettings.cpp
@@ -16,6 +16,8 @@ namespace storm {
const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy";
const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path";
const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile";
+ const std::string ParametricSettings::parameterSpaceOptionName = "parameterspace";
+ const std::string ParametricSettings::refinementThresholdOptionName = "refinementthreshold";
const std::string ParametricSettings::derivativesOptionName = "derivatives";
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
@@ -25,6 +27,10 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, parameterSpaceOptionName, true, "Sets the considered parameter-space (i.e., the initial region) for parameter lifting.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("region", "The parameter-space (given in format a<=x<=b,c<=y<=d).").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, refinementThresholdOptionName, true, "Parameter space refinement converges if the fraction of unknown area falls below this threshold.")
+ .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The threshold").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, true, "Sets whether to generate the derivatives of the resulting rational function.").build());
}
@@ -36,6 +42,18 @@ namespace storm {
return this->getOption(exportResultDestinationPathOptionName).getArgumentByName("path").getValueAsString();
}
+ bool ParametricSettings::isParameterSpaceSet() const {
+ return this->getOption(parameterSpaceOptionName).getHasOptionBeenSet();
+ }
+
+ std::string ParametricSettings::getParameterSpace() const {
+ return this->getOption(parameterSpaceOptionName).getArgumentByName("region").getValueAsString();
+ }
+
+ double ParametricSettings::getRefinementThreshold() const {
+ return this->getOption(refinementThresholdOptionName).getArgumentByName("threshold").getValueAsDouble();
+ }
+
bool ParametricSettings::exportToSmt2File() const {
return this->getOption(exportSmt2DestinationPathOptionName).getHasOptionBeenSet();
}
diff --git a/src/storm/settings/modules/ParametricSettings.h b/src/storm/settings/modules/ParametricSettings.h
index 0629eebe7..ac0cd9673 100644
--- a/src/storm/settings/modules/ParametricSettings.h
+++ b/src/storm/settings/modules/ParametricSettings.h
@@ -39,6 +39,22 @@ namespace storm {
*/
std::string exportResultPath() const;
+ /*!
+ * Retrieves whether the parameter space was declared
+ */
+ bool isParameterSpaceSet() const;
+
+ /*!
+ * Retrieves the given parameter spcae
+ */
+ std::string getParameterSpace() const;
+
+ /*!
+ * Retrieves the threshold considered for iterative region refinement.
+ * The refinement converges as soon as the fraction of unknown area falls below this threshold
+ */
+ double getRefinementThreshold() const;
+
/**
* Retrieves whether the encoding of the transition system should be exported to a file.
* @return True iff the smt file should be encoded.
@@ -70,6 +86,8 @@ namespace storm {
const static std::string encodeSmt2StrategyOptionName;
const static std::string exportSmt2DestinationPathOptionName;
const static std::string exportResultDestinationPathOptionName;
+ const static std::string parameterSpaceOptionName;
+ const static std::string refinementThresholdOptionName;
const static std::string derivativesOptionName;
};
diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp
index b251b9043..e76baf059 100644
--- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp
+++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp
@@ -9,8 +9,8 @@
#include "storm/transformer/GoalStateMerger.h"
#include "storm/utility/graph.h"
-#include <storm/exceptions/NotSupportedException.h>
-#include <storm/exceptions/UnexpectedException.h>
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace transformer {
diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp
index 2524b8438..4ee323397 100644
--- a/src/storm/transformer/SparseParametricMdpSimplifier.cpp
+++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp
@@ -11,8 +11,8 @@
#include "storm/utility/graph.h"
#include "storm/utility/vector.h"
-#include <storm/exceptions/NotSupportedException.h>
-#include <storm/exceptions/UnexpectedException.h>
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace transformer {
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index d2ff2e97c..9f5bbbb0f 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -316,61 +316,81 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
inline void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
+ storm::utility::Stopwatch parameterLiftingStopWatch(true);
auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel);
auto rewParameters = storm::models::sparse::getRewardParameters(*markovModel);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
- auto initialRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingParameterSpace(), modelParameters);
- auto refinementThreshold = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingThreshold());
+ STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::ParametricSettings>().isParameterSpaceSet(), storm::exceptions::InvalidSettingsException, "Invoked Parameter lifting but no parameter space was defined.");
+ auto parameterSpaceAsString = storm::settings::getModule<storm::settings::modules::ParametricSettings>().getParameterSpace();
+ auto parameterSpace = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion(parameterSpaceAsString, modelParameters);
+ auto refinementThreshold = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(storm::settings::getModule<storm::settings::modules::ParametricSettings>().getRefinementThreshold());
std::vector<std::pair<storm::storage::ParameterRegion<storm::RationalFunction>, storm::modelchecker::parametric::RegionCheckResult>> result;
- std::cout << "Performing parameter lifting for property " << *formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ...";
- std::cout.flush();
+ STORM_PRINT_AND_LOG("Performing parameter lifting for property " << *formula << " with parameter space " << parameterSpace.toString(true) << " and refinement threshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ..." << std::endl);
storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> task(*formula, true);
if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(task);
- result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
+ result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
} else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(task);
- result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
+ result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type.");
}
- std::cout << "done!" << std::endl;
+
auto satArea = storm::utility::zero<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>();
auto unsatArea = storm::utility::zero<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>();
uint_fast64_t numOfSatRegions = 0;
uint_fast64_t numOfUnsatRegions = 0;
for (auto const& res : result) {
- // std::cout << res.first.toString(true) << "\t (";
switch (res.second) {
case storm::modelchecker::parametric::RegionCheckResult::AllSat:
- // std::cout << "safe";
satArea += res.first.area();
++numOfSatRegions;
break;
case storm::modelchecker::parametric::RegionCheckResult::AllViolated:
- // std::cout << "unsafe";
unsatArea += res.first.area();
++numOfUnsatRegions;
break;
default:
- // std::cout << "unknown";
+ STORM_LOG_ERROR("Unexpected result for region " << res.first.toString(true) << " : " << res.second << ".");
break;
}
- // std::cout << ")" << std::endl;
}
- std::cout << std::endl
- << "Found " << numOfSatRegions << " safe regions, "
- << numOfUnsatRegions << " unsafe regions, and "
- << result.size() - numOfSatRegions - numOfUnsatRegions << " unknown regions." << std::endl
- << storm::utility::convertNumber<double>(satArea / initialRegion.area()) * 100 << "% of the parameter space is safe, and "
- << storm::utility::convertNumber<double>(unsatArea / initialRegion.area()) * 100 << "% of the parameter space is unsafe." << std::endl;
+
+ STORM_PRINT_AND_LOG("Done! Found " << numOfSatRegions << " safe regions, "
+ << numOfUnsatRegions << " unsafe regions, and "
+ << result.size() - numOfSatRegions - numOfUnsatRegions << " unknown regions." << std::endl);
+ STORM_PRINT_AND_LOG(storm::utility::convertNumber<double>(satArea / parameterSpace.area()) * 100 << "% of the parameter space is safe, and "
+ << storm::utility::convertNumber<double>(unsatArea / parameterSpace.area()) * 100 << "% of the parameter space is unsafe." << std::endl);
+ parameterLiftingStopWatch.stop();
+ STORM_PRINT_AND_LOG("Model checking with parameter lifting took " << parameterLiftingStopWatch << " seconds." << std::endl);
+
+ if (storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultToFile()) {
+ std::string path = storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath();
+ STORM_PRINT_AND_LOG("Exporting result to path " << path << "." << std::endl);
+ std::ofstream filestream;
+ storm::utility::openFile(path, filestream);
+
+ for (auto const& res : result) {
+ switch (res.second) {
+ case storm::modelchecker::parametric::RegionCheckResult::AllSat:
+ filestream << "safe: " << res.first.toString(true) << std::endl;
+ break;
+ case storm::modelchecker::parametric::RegionCheckResult::AllViolated:
+ filestream << "unsafe: " << res.first.toString(true) << std::endl;
+ break;
+ default:
+ break;
+ }
+ }
+ }
}
#endif