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

renamed ParameterLifting.h -> RegionChecker.h

tempestpy_adaptions
TimQu 8 years ago
parent
ab7b31b08c
commit
ee754c96e2
9 changed files with 183 additions and 183 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. 30
      src/storm/modelchecker/parametric/RegionChecker.cpp
  2. 16
      src/storm/modelchecker/parametric/RegionChecker.h
  3. 22
      src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp
  4. 6
      src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h
  5. 22
      src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp
  6. 6
      src/storm/modelchecker/parametric/SparseMdpRegionChecker.h
  7. 36
      src/storm/utility/storm.h
  8. 130
      src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
  9. 98
      src/test/modelchecker/SparseMdpParameterLiftingTest.cpp

30
src/storm/modelchecker/parametric/ParameterLifting.cpp → src/storm/modelchecker/parametric/RegionChecker.cpp
View File

@ -1,7 +1,7 @@
#include <sstream>
#include <queue>
#include "storm/modelchecker/parametric/ParameterLifting.h"
#include "storm/modelchecker/parametric/RegionChecker.h"
#include "storm/adapters/CarlAdapter.h"
@ -25,29 +25,29 @@ namespace storm {
namespace modelchecker {
namespace parametric {
ParameterLiftingSettings::ParameterLiftingSettings() {
RegionCheckerSettings::RegionCheckerSettings() {
this->applyExactValidation = storm::settings::getModule<storm::settings::modules::ParametricSettings>().isExactValidationSet();
}
template <typename SparseModelType, typename ConstantType>
ParameterLifting<SparseModelType, ConstantType>::ParameterLifting(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
RegionChecker<SparseModelType, ConstantType>::RegionChecker(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>
ParameterLiftingSettings const& ParameterLifting<SparseModelType, ConstantType>::getSettings() const {
RegionCheckerSettings const& RegionChecker<SparseModelType, ConstantType>::getSettings() const {
return settings;
}
template <typename SparseModelType, typename ConstantType>
void ParameterLifting<SparseModelType, ConstantType>::setSettings(ParameterLiftingSettings const& newSettings) {
void RegionChecker<SparseModelType, ConstantType>::setSettings(RegionCheckerSettings const& newSettings) {
settings = newSettings;
}
template <typename SparseModelType, typename ConstantType>
void ParameterLifting<SparseModelType, ConstantType>::specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
void RegionChecker<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.");
@ -68,7 +68,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) {
RegionCheckResult RegionChecker<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) {
RegionCheckResult result = initialResult;
// Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
@ -120,7 +120,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult) {
RegionCheckResult RegionChecker<SparseModelType, ConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult) {
RegionCheckResult numericResult = analyzeRegion(region, initialResult, false);
parameterLiftingCheckerStopwatch.start();
if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) {
@ -157,7 +157,7 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold) {
std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> RegionChecker<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, CoefficientType const& threshold) {
STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
auto areaOfParameterSpace = region.area();
@ -243,7 +243,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
SparseModelType const& ParameterLifting<SparseModelType, ConstantType>::getConsideredParametricModel() const {
SparseModelType const& RegionChecker<SparseModelType, ConstantType>::getConsideredParametricModel() const {
if (simplifiedModel) {
return *simplifiedModel;
} else {
@ -252,7 +252,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
std::string ParameterLifting<SparseModelType, ConstantType>::visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> const& result, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& parameterSpace, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& x, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& y) {
std::string RegionChecker<SparseModelType, ConstantType>::visualizeResult(std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> const& result, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& parameterSpace, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& x, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::VariableType const& y) {
std::stringstream stream;
@ -306,10 +306,10 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
template class ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
template class ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
template class RegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class RegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
template class RegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
template class RegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
#endif
} // namespace parametric
} //namespace modelchecker

16
src/storm/modelchecker/parametric/ParameterLifting.h → src/storm/modelchecker/parametric/RegionChecker.h
View File

@ -13,24 +13,24 @@ namespace storm {
namespace modelchecker{
namespace parametric{
struct ParameterLiftingSettings {
ParameterLiftingSettings();
struct RegionCheckerSettings {
RegionCheckerSettings();
bool applyExactValidation;
};
template<typename SparseModelType, typename ConstantType>
class ParameterLifting {
class RegionChecker {
public:
typedef typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType CoefficientType;
ParameterLifting(SparseModelType const& parametricModel);
virtual ~ParameterLifting() = default;
RegionChecker(SparseModelType const& parametricModel);
virtual ~RegionChecker() = default;
ParameterLiftingSettings const& getSettings() const;
void setSettings(ParameterLiftingSettings const& newSettings);
RegionCheckerSettings const& getSettings() const;
void setSettings(RegionCheckerSettings const& newSettings);
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
@ -63,7 +63,7 @@ namespace storm {
virtual void applyHintsToExactChecker() = 0;
SparseModelType const& parametricModel;
ParameterLiftingSettings settings;
RegionCheckerSettings settings;
std::unique_ptr<CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>> currentCheckTask;
std::shared_ptr<storm::logic::Formula const> currentFormula;
std::shared_ptr<SparseModelType> simplifiedModel;

22
src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp → src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp
View File

@ -1,4 +1,4 @@
#include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h"
#include "storm/adapters/CarlAdapter.h"
@ -7,19 +7,19 @@
#include "storm/transformer/SparseParametricDtmcSimplifier.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Dtmc.h"
#include "SparseMdpParameterLifting.h"
#include "SparseMdpRegionChecker.h"
namespace storm {
namespace modelchecker {
namespace parametric {
template <typename SparseModelType, typename ConstantType>
SparseDtmcParameterLifting<SparseModelType, ConstantType>::SparseDtmcParameterLifting(SparseModelType const& parametricModel) : ParameterLifting<SparseModelType, ConstantType>(parametricModel) {
SparseDtmcRegionChecker<SparseModelType, ConstantType>::SparseDtmcRegionChecker(SparseModelType const& parametricModel) : RegionChecker<SparseModelType, ConstantType>(parametricModel) {
// Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
void SparseDtmcParameterLifting<SparseModelType, ConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
void SparseDtmcRegionChecker<SparseModelType, ConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
storm::transformer::SparseParametricDtmcSimplifier<SparseModelType> simplifier(this->parametricModel);
if(simplifier.simplify(checkTask.getFormula())) {
this->simplifiedModel = simplifier.getSimplifiedModel();
@ -31,11 +31,11 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
void SparseDtmcParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
void SparseDtmcRegionChecker<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
if (this->settings.applyExactValidation) {
//STORM_LOG_WARN_COND(!(std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType) , "Exact validation is not necessarry if the original computation is already exact");
//STORM_LOG_WARN_COND(!(std::is_same<ConstantType, typename RegionChecker<SparseModelType, ConstantType>::CoefficientType) , "Exact validation is not necessarry if the original computation is already exact");
STORM_LOG_WARN_COND(!(std::is_same<ConstantType, storm::RationalNumber>::value) , "Exact validation is not necessarry if the original computation is already exact");
//this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel()); // todo: use template argument instead of storm::Rational
//this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, typename RegionChecker<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel()); // todo: use template argument instead of storm::Rational
this->exactParameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, storm::RationalNumber>>(this->getConsideredParametricModel());
}
this->parameterLiftingChecker = std::make_unique<SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
@ -44,11 +44,11 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
void SparseDtmcParameterLifting<SparseModelType, ConstantType>::applyHintsToExactChecker() {
void SparseDtmcRegionChecker<SparseModelType, ConstantType>::applyHintsToExactChecker() {
auto dtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>*>(this->parameterLiftingChecker.get());
STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type");
auto exactDtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, storm::RationalNumber>*>(this->exactParameterLiftingChecker.get());
//auto exactDtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::Rational
//auto exactDtmcPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<SparseModelType, typename RegionChecker<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::Rational
STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type");
exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler();
exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler();
@ -56,8 +56,8 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template class SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
template class SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
#endif
} // namespace parametric
} //namespace modelchecker

6
src/storm/modelchecker/parametric/SparseDtmcParameterLifting.h → src/storm/modelchecker/parametric/SparseDtmcRegionChecker.h
View File

@ -2,7 +2,7 @@
#include <memory>
#include "storm/modelchecker/parametric/ParameterLifting.h"
#include "storm/modelchecker/parametric/RegionChecker.h"
namespace storm {
namespace modelchecker{
@ -10,10 +10,10 @@ namespace storm {
template<typename SparseModelType, typename ConstantType>
class SparseDtmcParameterLifting : public ParameterLifting<SparseModelType, ConstantType> {
class SparseDtmcRegionChecker : public RegionChecker<SparseModelType, ConstantType> {
public:
SparseDtmcParameterLifting(SparseModelType const& parametricModel);
SparseDtmcRegionChecker(SparseModelType const& parametricModel);
protected:
virtual void simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;

22
src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp → src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp
View File

@ -1,4 +1,4 @@
#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h"
#include "storm/adapters/CarlAdapter.h"
@ -7,19 +7,19 @@
#include "storm/transformer/SparseParametricMdpSimplifier.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Mdp.h"
#include "SparseMdpParameterLifting.h"
#include "SparseMdpRegionChecker.h"
namespace storm {
namespace modelchecker {
namespace parametric {
template <typename SparseModelType, typename ConstantType>
SparseMdpParameterLifting<SparseModelType, ConstantType>::SparseMdpParameterLifting(SparseModelType const& parametricModel) : ParameterLifting<SparseModelType, ConstantType>(parametricModel) {
SparseMdpRegionChecker<SparseModelType, ConstantType>::SparseMdpRegionChecker(SparseModelType const& parametricModel) : RegionChecker<SparseModelType, ConstantType>(parametricModel) {
// Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
void SparseMdpParameterLifting<SparseModelType, ConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
void SparseMdpRegionChecker<SparseModelType, ConstantType>::simplifyParametricModel(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
storm::transformer::SparseParametricMdpSimplifier<SparseModelType> simplifier(this->parametricModel);
if(simplifier.simplify(checkTask.getFormula())) {
this->simplifiedModel = simplifier.getSimplifiedModel();
@ -31,11 +31,11 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
void SparseMdpParameterLifting<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
void SparseMdpRegionChecker<SparseModelType, ConstantType>::initializeUnderlyingCheckers() {
if (this->settings.applyExactValidation) {
//STORM_LOG_WARN_COND(!(std::is_same<ConstantType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact"); // todo: use templated argument instead of storm::RationalNumber
//STORM_LOG_WARN_COND(!(std::is_same<ConstantType, typename RegionChecker<SparseModelType, ConstantType>::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact"); // todo: use templated argument instead of storm::RationalNumber
STORM_LOG_WARN_COND(!(std::is_same<ConstantType, storm::RationalNumber>::value), "Exact validation is not necessarry if the original computation is already exact");
//this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel()); // todo: use templated argument instead of storm::RationalNumber
//this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, typename RegionChecker<SparseModelType, ConstantType>::CoefficientType>>(this->getConsideredParametricModel()); // todo: use templated argument instead of storm::RationalNumber
this->exactParameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, storm::RationalNumber>>(this->getConsideredParametricModel());
}
this->parameterLiftingChecker = std::make_unique<SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>>(this->getConsideredParametricModel());
@ -44,11 +44,11 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
void SparseMdpParameterLifting<SparseModelType, ConstantType>::applyHintsToExactChecker() {
void SparseMdpRegionChecker<SparseModelType, ConstantType>::applyHintsToExactChecker() {
auto MdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>*>(this->parameterLiftingChecker.get());
STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type");
auto exactMdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, storm::RationalNumber>*>(this->exactParameterLiftingChecker.get());
// auto exactMdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, typename ParameterLifting<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::RationalNumber
// auto exactMdpPLChecker = dynamic_cast<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<SparseModelType, typename RegionChecker<SparseModelType, ConstantType>::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::RationalNumber
STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type");
exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler();
exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler();
@ -57,8 +57,8 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template class SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
template class SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
template class SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
template class SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
#endif
} // namespace parametric
} //namespace modelchecker

6
src/storm/modelchecker/parametric/SparseMdpParameterLifting.h → src/storm/modelchecker/parametric/SparseMdpRegionChecker.h
View File

@ -2,7 +2,7 @@
#include <memory>
#include "storm/modelchecker/parametric/ParameterLifting.h"
#include "storm/modelchecker/parametric/RegionChecker.h"
namespace storm {
namespace modelchecker{
@ -10,10 +10,10 @@ namespace storm {
template<typename SparseModelType, typename ConstantType>
class SparseMdpParameterLifting : public ParameterLifting<SparseModelType, ConstantType> {
class SparseMdpRegionChecker : public RegionChecker<SparseModelType, ConstantType> {
public:
SparseMdpParameterLifting(SparseModelType const& parametricModel);
SparseMdpRegionChecker(SparseModelType const& parametricModel);
protected:

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

@ -68,8 +68,8 @@
#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "storm/modelchecker/parametric/SparseDtmcParameterLifting.h"
#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h"
#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h"
#include "storm/utility/parameterlifting.h"
#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
@ -352,38 +352,38 @@ namespace storm {
if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
storm::modelchecker::parametric::SparseDtmcParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(task);
result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
storm::modelchecker::parametric::SparseDtmcRegionChecker <storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber> regionChecker(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
regionChecker.specifyFormula(task);
result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold);
parameterLiftingStopWatch.stop();
if (modelParameters.size() == 2) {
resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
}
} else {
storm::modelchecker::parametric::SparseDtmcParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(task);
result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
storm::modelchecker::parametric::SparseDtmcRegionChecker <storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
regionChecker.specifyFormula(task);
result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold);
parameterLiftingStopWatch.stop();
if (modelParameters.size() == 2) {
resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
}
}
} else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(task);
result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber> regionChecker(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
regionChecker.specifyFormula(task);
result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold);
parameterLiftingStopWatch.stop();
if (modelParameters.size() == 2) {
resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
}
} else {
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(task);
result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold);
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
regionChecker.specifyFormula(task);
result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold);
parameterLiftingStopWatch.stop();
if (modelParameters.size() == 2) {
resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin()));
}
}
} else {

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

@ -7,7 +7,7 @@
#include "utility/storm.h"
#include "storm/models/sparse/Model.h"
#include "modelchecker/parametric/SparseDtmcParameterLifting.h"
#include "modelchecker/parametric/SparseDtmcRegionChecker.h"
TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
@ -25,17 +25,17 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -55,17 +55,17 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -85,17 +85,17 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -116,20 +116,20 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
auto settings = parameterLiftingContext.getSettings();
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
auto settings = regionChecker.getSettings();
settings.applyExactValidation = true;
parameterLiftingContext.setSettings(settings);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
regionChecker.setSettings(settings);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -149,20 +149,20 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
auto settings = parameterLiftingContext.getSettings();
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
auto settings = regionChecker.getSettings();
settings.applyExactValidation = true;
parameterLiftingContext.setSettings(settings);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
regionChecker.setSettings(settings);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -182,20 +182,20 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
auto settings = parameterLiftingContext.getSettings();
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
auto settings = regionChecker.getSettings();
settings.applyExactValidation = true;
parameterLiftingContext.setSettings(settings);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
regionChecker.setSettings(settings);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -215,13 +215,13 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=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::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -241,17 +241,17 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -272,8 +272,8 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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);
@ -281,10 +281,10 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, regionChecker.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -305,8 +305,8 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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);
@ -314,10 +314,10 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, regionChecker.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -339,17 +339,17 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -370,13 +370,13 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}

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

@ -7,7 +7,7 @@
#include "utility/storm.h"
#include "storm/models/sparse/Model.h"
#include "storm/modelchecker/parametric/SparseMdpParameterLifting.h"
#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h"
TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
@ -24,17 +24,17 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -54,17 +54,17 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -84,17 +84,17 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -114,17 +114,17 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -142,17 +142,17 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -172,17 +172,17 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -203,17 +203,17 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -233,17 +233,17 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -264,13 +264,13 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=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::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -290,17 +290,17 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> regionChecker(*model);
regionChecker.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.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));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}

Write Preview
Loading…
Cancel
Save