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

Moved parametric model simplification inside the Parameter lifting checker

main
TimQu 8 years ago
parent
62dd371411
commit
62d50b336b
14 changed files with 288 additions and 252 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. 22
      src/storm-pars-cli/storm-pars.cpp
  2. 45
      src/storm-pars/api/parametric.h
  3. 75
      src/storm-pars/api/region.h
  4. 1
      src/storm-pars/api/storm-pars.h
  5. 41
      src/storm-pars/modelchecker/region/RegionModelChecker.cpp
  6. 6
      src/storm-pars/modelchecker/region/RegionModelChecker.h
  7. 100
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  8. 9
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
  9. 113
      src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
  10. 9
      src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
  11. 74
      src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
  12. 15
      src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
  13. 6
      src/storm-pars/settings/modules/ParametricSettings.cpp
  14. 6
      src/storm-pars/settings/modules/ParametricSettings.h

22
src/storm-pars-cli/storm-pars.cpp
View File

@ -179,25 +179,11 @@ namespace storm {
}
}
template<typename ValueType>
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::shared_ptr<storm::logic::Formula const>> performSimplification(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::shared_ptr<storm::logic::Formula const>> result;
if (!(parametricSettings.isSimplifySet() && storm::api::simplifyParametricModel<ValueType>(model, formula, result.first, result.second))) {
result = std::make_pair(model, formula);
}
return result;
}
template <typename ValueType>
void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
verifyProperties<ValueType>(input.properties,
[&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
auto simplificationResult = performSimplification(model, formula);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(simplificationResult.first, storm::api::createTask<ValueType>(simplificationResult.second, true));
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(simplificationResult.first->getInitialStates()));
return result;
},
@ -235,15 +221,13 @@ namespace storm {
STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl);
verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getRefinementThreshold());
auto simplificationResult = performSimplification(model, formula);
std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(simplificationResult.first, storm::api::createTask<ValueType>(simplificationResult.second, true), regions.front(), refinementThreshold, engine);
std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), refinementThreshold, engine);
return result;
};
} else {
STORM_PRINT_AND_LOG("." << std::endl);
verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
auto simplificationResult = performSimplification(model, formula);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(simplificationResult.first, storm::api::createTask<ValueType>(simplificationResult.second, true), regions, engine);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions, engine);
return result;
};
}

45
src/storm-pars/api/parametric.h
View File

@ -1,45 +0,0 @@
#pragma once
#include <memory>
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
#include "storm/models/sparse/Model.h"
#include "storm/logic/Formula.h"
#include "storm/utility/macros.h"
namespace storm {
namespace api {
template <typename ValueType>
bool simplifyParametricModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& inputModel, std::shared_ptr<storm::logic::Formula const> const& inputFormula, std::shared_ptr<storm::models::sparse::Model<ValueType>>& outputModel, std::shared_ptr<storm::logic::Formula const>& outputFormula) {
if (inputModel->isOfType(storm::models::ModelType::Dtmc)) {
auto const& dtmc = *inputModel->template as<storm::models::sparse::Dtmc<ValueType>>();
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(dtmc);
if (simplifier.simplify(*inputFormula)) {
outputModel = simplifier.getSimplifiedModel();
outputFormula = simplifier.getSimplifiedFormula();
return true;
}
} else if (inputModel->isOfType(storm::models::ModelType::Mdp)) {
auto const& mdp = *inputModel->template as<storm::models::sparse::Mdp<ValueType>>();
auto simplifier = storm::transformer::SparseParametricMdpSimplifier<storm::models::sparse::Mdp<ValueType>>(mdp);
if (simplifier.simplify(*inputFormula)) {
outputModel = simplifier.getSimplifiedModel();
outputFormula = simplifier.getSimplifiedFormula();
return true;
}
} else {
STORM_LOG_ERROR("Unable to simplify model with the given type.");
}
// Reaching this point means that simplification was not successful.
outputModel = nullptr;
outputFormula = nullptr;
return false;
}
}
}

75
src/storm-pars/api/region.h
View File

@ -6,14 +6,16 @@
#include <memory>
#include <boost/optional.hpp>
#include "storm-pars/storage/ParameterRegion.h"
#include "storm-pars/modelchecker/results/RegionCheckResult.h"
#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/RegionCheckEngine.h"
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h"
#include "storm-pars/parser/ParameterRegionParser.h"
#include "storm-pars/storage/ParameterRegion.h"
#include "storm-pars/utility/parameterlifting.h"
#include "storm/api/transformation.h"
#include "storm/utility/file.h"
@ -53,51 +55,86 @@ namespace storm {
template <typename ValueType>
storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables) {
auto res = parseRegions(inputString, consideredVariables);
// Handle the "empty region" case
if (inputString == "" && consideredVariables.empty()) {
return storm::storage::ParameterRegion<ValueType>();
}
auto res = parseRegions<ValueType>(inputString, consideredVariables);
STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected.");
return res.front();
}
template <typename ValueType>
storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, storm::models::ModelBase const& model) {
auto res = parseRegions(inputString, model);
// Handle the "empty region" case
if (inputString == "" && !model.hasParameters()) {
return storm::storage::ParameterRegion<ValueType>();
}
auto res = parseRegions<ValueType>(inputString, model);
STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected.");
return res.front();
}
template <typename ParametricType, typename ConstantType>
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
// Treat continuous time models
if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
auto discreteTimeModel = storm::api::transformContinuousToDiscreteTimeSparseModel(model, taskFormulaAsVector);
STORM_LOG_THROW(discreteTimeModel->isOfType(storm::models::ModelType::Dtmc) || discreteTimeModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
return initializeParameterLiftingRegionModelChecker<ParametricType, ConstantType>(discreteTimeModel, task);
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
}
// Obtain the region model checker
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> result;
if (model->isOfType(storm::models::ModelType::Dtmc)) {
auto const& dtmc = *model->template as<storm::models::sparse::Dtmc<ParametricType>>();
result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>(dtmc);
} else if (model->isOfType(storm::models::ModelType::Mdp)) {
auto const& mdp = *model->template as<storm::models::sparse::Mdp<ParametricType>>();
result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, ConstantType>>(mdp);
if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>();
} else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) {
result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, ConstantType>>();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
}
result->specifyFormula(task);
result->specify(consideredModel, task);
return result;
}
template <typename ParametricType, typename ImpreciseType, typename PreciseType>
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
// todo
return nullptr;
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
// Treat continuous time models
if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
}
// Obtain the region model checker
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> result;
if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
result = std::make_unique<storm::modelchecker::ValidatingSparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ImpreciseType, PreciseType>>();
} else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) {
result = std::make_unique<storm::modelchecker::ValidatingSparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, ImpreciseType, PreciseType>>();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
}
result->specify(consideredModel, task);
return result;
}
template <typename ValueType>

1
src/storm-pars/api/storm-pars.h
View File

@ -1,4 +1,3 @@
#pragma once
#include "storm-pars/api/region.h"
#include "storm-pars/api/parametric.h"

41
src/storm-pars/modelchecker/region/RegionModelChecker.cpp
View File

@ -40,47 +40,6 @@ namespace storm {
return std::make_unique<storm::modelchecker::RegionCheckResult<ParametricType>>(std::move(result));
}
/*
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
template <typename ParametricType, typename ConstantType, typename ExactConstantType>
RegionResult RegionModelChecker<ParametricType, ConstantType, ExactConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename ParametricType::ValueType> const& region, RegionResult const& initialResult) {
RegionResult numericResult = analyzeRegion(region, initialResult, false);
parameterLiftingCheckerStopwatch.start();
if (numericResult == RegionResult::AllSat || numericResult == RegionResult::AllViolated) {
applyHintsToExactChecker();
}
if (numericResult == RegionResult::AllSat) {
if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
// Numerical result is wrong; Check whether the region is AllViolated!
STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
++numOfCorrectedRegions;
if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
parameterLiftingCheckerStopwatch.stop();
return RegionResult::AllViolated;
} else {
parameterLiftingCheckerStopwatch.stop();
return RegionResult::Unknown;
}
}
} else if (numericResult == RegionResult::AllViolated) {
if(exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
// Numerical result is wrong; Check whether the region is AllSat!
STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
++numOfCorrectedRegions;
if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
parameterLiftingCheckerStopwatch.stop();
return RegionResult::AllSat;
} else {
parameterLiftingCheckerStopwatch.stop();
return RegionResult::Unknown;
}
}
}
parameterLiftingCheckerStopwatch.stop();
return numericResult;
}
*/
template <typename ParametricType>
std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, ParametricType const& threshold) {
STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");

6
src/storm-pars/modelchecker/region/RegionModelChecker.h
View File

@ -7,6 +7,7 @@
#include "storm-pars/modelchecker/region/RegionResult.h"
#include "storm-pars/storage/ParameterRegion.h"
#include "storm/models/ModelBase.h"
#include "storm/modelchecker/CheckTask.h"
namespace storm {
@ -21,9 +22,8 @@ namespace storm {
RegionModelChecker();
virtual ~RegionModelChecker() = default;
virtual bool canHandle(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
virtual void specifyFormula(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
/*!
* Analyzes the given region.

100
src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
View File

@ -1,5 +1,6 @@
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
#include "storm-pars/utility/parameterlifting.h"
#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@ -15,28 +16,59 @@
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
template <typename SparseModelType, typename ConstantType>
SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>()) {
SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker() : SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>()) {
// Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
// Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
bool result = checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true));
if (result) {
storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula());
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
}
bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
bool result = parametricModel->isOfType(storm::models::ModelType::Dtmc);
result &= parametricModel->isSparseModel();
result &= parametricModel->supportsParameters();
auto dtmc = parametricModel->template as<SparseModelType>();
result &= static_cast<bool>(dtmc);
result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
return result;
}
template <typename SparseModelType, typename ConstantType>
void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
auto dtmc = parametricModel->template as<SparseModelType>();
specify(dtmc, checkTask, false);
}
template <typename SparseModelType, typename ConstantType>
void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
reset();
if (skipModelSimplification) {
this->parametricModel = parametricModel;
this->specifyFormula(checkTask);
} else {
auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*parametricModel);
if (!simplifier.simplify(checkTask.getFormula())) {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
}
this->parametricModel = simplifier.getSimplifiedModel();
this->specifyFormula(checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
}
}
template <typename SparseModelType, typename ConstantType>
void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
@ -53,25 +85,25 @@ namespace storm {
STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
// get the results for the subformulas
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
// get the maybeStates
maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
maybeStates &= ~psiStates;
// set the result for all non-maybe states
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the vector of one-step probabilities to go to target states.
std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates);
}
// We know some bounds for the results so set them
@ -83,25 +115,25 @@ namespace storm {
void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
// get the results for the subformulas
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
// get the maybeStates
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->parametricModel->getBackwardTransitions(), phiStates, psiStates);
maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
// set the result for all non-maybe states
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the vector of one-step probabilities to go to target states.
std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates);
}
// We know some bounds for the results so set them
@ -113,29 +145,29 @@ namespace storm {
void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
// get the results for the subformula
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
// get the maybeStates
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates);
infinityStates.complement();
maybeStates = ~(targetStates | infinityStates);
// set the result for all the non-maybe states
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the reward vector
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix());
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates);
}
// We only know a lower bound for the result
@ -155,15 +187,15 @@ namespace storm {
STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
//Every state is a maybeState
maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
maybeStates = storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getColumnCount(), true);
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates());
// Create the reward vector
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix());
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates);
// We only know a lower bound for the result
@ -173,7 +205,7 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationChecker() {
if (!instantiationChecker) {
instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(this->parametricModel);
instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel);
instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
}
return *instantiationChecker;
@ -205,7 +237,7 @@ namespace storm {
if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) {
// If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize).
std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
if (storm::solver::minimize(dirForParameters)) {
// Terminate if the value for ALL relevant states is already below the threshold
termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);

9
src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
View File

@ -19,10 +19,13 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
class SparseDtmcParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
public:
SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel);
SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
SparseDtmcParameterLiftingModelChecker();
SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
virtual ~SparseDtmcParameterLiftingModelChecker() = default;
virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
void specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();

113
src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
View File

@ -1,5 +1,6 @@
#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
#include "storm-pars/utility/parameterlifting.h"
#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@ -16,25 +17,57 @@
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
template <typename SparseModelType, typename ConstantType>
SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker() : SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
// Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
// Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
bool result = checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
if (result) {
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
}
bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
bool result = parametricModel->isOfType(storm::models::ModelType::Mdp);
result &= parametricModel->isSparseModel();
result &= parametricModel->supportsParameters();
auto mdp = parametricModel->template as<SparseModelType>();
result &= static_cast<bool>(mdp);
result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
return result;
}
template <typename SparseModelType, typename ConstantType>
void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
auto mdp = parametricModel->template as<SparseModelType>();
specify(mdp, checkTask, false);
}
template <typename SparseModelType, typename ConstantType>
void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
reset();
if (skipModelSimplification) {
this->parametricModel = parametricModel;
this->specifyFormula(checkTask);
} else {
auto simplifier = storm::transformer::SparseParametricMdpSimplifier<SparseModelType>(*parametricModel);
if (!simplifier.simplify(checkTask.getFormula())) {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
}
this->parametricModel = simplifier.getSimplifiedModel();
this->specifyFormula(checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
}
}
template <typename SparseModelType, typename ConstantType>
@ -53,27 +86,27 @@ namespace storm {
STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
// get the results for the subformulas
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
// get the maybeStates
maybeStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
storm::utility::graph::performProbGreater0A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound) :
storm::utility::graph::performProbGreater0E(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
storm::utility::graph::performProbGreater0A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound) :
storm::utility::graph::performProbGreater0E(this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
maybeStates &= ~psiStates;
// set the result for all non-maybe states
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the vector of one-step probabilities to go to target states.
std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates);
std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, this->parametricModel->getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
computePlayer1Matrix();
applyPreviousResultAsHint = false;
@ -88,32 +121,32 @@ namespace storm {
void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
// get the results for the subformulas
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
// get the maybeStates
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
storm::utility::graph::performProb01Min(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates) :
storm::utility::graph::performProb01Max(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
storm::utility::graph::performProb01Min(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), phiStates, psiStates) :
storm::utility::graph::performProb01Max(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), phiStates, psiStates);
maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
// set the result for all non-maybe states
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the vector of one-step probabilities to go to target states.
std::vector<typename SparseModelType::ValueType> b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, this->parametricModel->getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
computePlayer1Matrix();
// Check whether there is an EC consisting of maybestates
applyPreviousResultAsHint = storm::solver::minimize(checkTask.getOptimizationDirection()) || // when minimizing, there can not be an EC within the maybestates
storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
storm::utility::graph::performProb1A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), maybeStates, ~maybeStates).full();
}
// We know some bounds for the results
@ -125,40 +158,40 @@ namespace storm {
void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
// get the results for the subformula
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
// get the maybeStates
storm::storage::BitVector infinityStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
storm::utility::graph::performProb1E(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates) :
storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
storm::utility::graph::performProb1E(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates) :
storm::utility::graph::performProb1A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates);
infinityStates.complement();
maybeStates = ~(targetStates | infinityStates);
// set the result for all the non-maybe states
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the reward vector
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix());
// We need to handle choices that lead to an infinity state.
// As a maybeState does not have reward infinity, a choice leading to an infinity state will never be picked. Hence, we can unselect the corresponding rows
storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates);
storm::storage::BitVector selectedRows = this->parametricModel->getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, selectedRows, maybeStates);
computePlayer1Matrix();
// Check whether there is an EC consisting of maybestates
applyPreviousResultAsHint = !storm::solver::minimize(checkTask.getOptimizationDirection()) || // when maximizing, there can not be an EC within the maybestates
storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
storm::utility::graph::performProb1A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), maybeStates, ~maybeStates).full();
}
// We only know a lower bound for the result
@ -178,15 +211,15 @@ namespace storm {
STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
//Every state is a maybeState
maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
maybeStates = storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getColumnCount(), true);
resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates());
// Create the reward vector
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix());
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), maybeStates);
computePlayer1Matrix();
applyPreviousResultAsHint = false;
@ -198,7 +231,7 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationChecker() {
if (!instantiationChecker) {
instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(this->parametricModel);
instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel);
instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
}
return *instantiationChecker;
@ -235,7 +268,7 @@ namespace storm {
if (this->currentCheckTask->isBoundSet() && this->currentCheckTask->getOptimizationDirection() == dirForParameters && solver->hasSchedulerHints()) {
// If we reach this point, we know that after applying the hints, the x-values can only become larger (if we maximize) or smaller (if we minimize).
std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
if (storm::solver::minimize(dirForParameters)) {
// Terminate if the value for ALL relevant states is already below the threshold
termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
@ -276,14 +309,14 @@ namespace storm {
void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computePlayer1Matrix() {
uint_fast64_t n = 0;
for(auto const& maybeState : maybeStates) {
n += this->parametricModel.getTransitionMatrix().getRowGroupSize(maybeState);
n += this->parametricModel->getTransitionMatrix().getRowGroupSize(maybeState);
}
// The player 1 matrix is the identity matrix of size n with the row groups as given by the original matrix
storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> matrixBuilder(n, n, n, true, true, maybeStates.getNumberOfSetBits());
uint_fast64_t p1MatrixRow = 0;
for (auto maybeState : maybeStates){
matrixBuilder.newRowGroup(p1MatrixRow);
for (uint_fast64_t row = this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState]; row < this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState + 1]; ++row){
for (uint_fast64_t row = this->parametricModel->getTransitionMatrix().getRowGroupIndices()[maybeState]; row < this->parametricModel->getTransitionMatrix().getRowGroupIndices()[maybeState + 1]; ++row){
matrixBuilder.addNextValue(p1MatrixRow, p1MatrixRow, storm::utility::one<storm::storage::sparse::state_type>());
++p1MatrixRow;
}

9
src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
View File

@ -20,10 +20,13 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
public:
SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel);
SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
SparseMdpParameterLiftingModelChecker();
SparseMdpParameterLiftingModelChecker(std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
virtual ~SparseMdpParameterLiftingModelChecker() = default;
virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
void specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();

74
src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
View File

@ -1,4 +1,4 @@
#include "SparseParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/logic/FragmentSpecification.h"
@ -15,14 +15,13 @@ namespace storm {
namespace modelchecker {
template <typename SparseModelType, typename ConstantType>
SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker() {
//Intentionally left empty
}
template <typename SparseModelType, typename ConstantType>
void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
STORM_LOG_ASSERT(this->canHandle(checkTask), "specified formula can not be handled by this.");
reset();
currentFormula = checkTask.getFormula().asSharedPointer();
currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
@ -52,50 +51,75 @@ namespace storm {
STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property.");
STORM_LOG_THROW(this->parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");
STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");
RegionResult result = initialResult;
// Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
if (result == RegionResult::Unknown) {
result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
}
// try to prove AllSat or AllViolated, depending on the obtained result
if (result == RegionResult::ExistsSat || result == RegionResult::CenterSat) {
// show AllSat:
storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
result = RegionResult::AllSat;
} else if (sampleVerticesOfRegion) {
// 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) {
if (!getInstantiationChecker().check(v)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
result = RegionResult::ExistsBoth;
}
}
result = sampleVertices(region, result);
}
} else if (result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) {
// show AllViolated:
storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
result = RegionResult::AllViolated;
} else if (sampleVerticesOfRegion) {
result = sampleVertices(region, result);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
}
return result;
}
template <typename SparseModelType, typename ConstantType>
RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::sampleVertices(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult) {
RegionResult result = initialResult;
if (result == RegionResult::AllSat || result == RegionResult::AllViolated) {
return result;
}
bool hasSatPoint = result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated;
bool hasViolatedPoint = result == RegionResult::ExistsSat || result == RegionResult::CenterSat;
// 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) {
if (getInstantiationChecker().check(v)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
result = RegionResult::ExistsBoth;
auto vertexIt = vertices.begin();
while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) {
if (getInstantiationChecker().check(*vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
hasSatPoint = true;
} else {
hasViolatedPoint = true;
}
++vertexIt;
}
if (hasSatPoint) {
if (hasViolatedPoint) {
result = RegionResult::ExistsBoth;
} else if (result != RegionResult::CenterSat) {
result = RegionResult::ExistsSat;
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
} else if (hasViolatedPoint && result != RegionResult::CenterViolated) {
result = RegionResult::ExistsViolated;
}
return result;
}
template <typename SparseModelType, typename ConstantType>
std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
auto quantitativeResult = computeQuantitativeValues(region, dirForParameters);
@ -106,6 +130,16 @@ namespace storm {
}
}
template <typename SparseModelType, typename ConstantType>
SparseModelType const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getConsideredParametricModel() const {
return *parametricModel;
}
template <typename SparseModelType, typename ConstantType>
CheckTask<storm::logic::Formula, ConstantType> const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentCheckTask() const {
return *currentCheckTask;
}
template <typename SparseModelType, typename ConstantType>
void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");

15
src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
View File

@ -22,10 +22,9 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
class SparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
public:
SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
SparseParameterLiftingModelChecker();
virtual ~SparseParameterLiftingModelChecker() = default;
virtual void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
/*!
* Analyzes the given region by means of parameter lifting.
@ -36,6 +35,11 @@ namespace storm {
*/
virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
/*!
* Analyzes the 2^#parameters corner points of the given region.
*/
RegionResult sampleVertices(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown);
/*!
* Checks the specified formula on the given region by applying parameter lifting (Parameter choices are lifted to nondeterministic choices)
* This yields a (sound) approximative model checking result.
@ -45,7 +49,12 @@ namespace storm {
*/
std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
SparseModelType const& getConsideredParametricModel() const;
CheckTask<storm::logic::Formula, ConstantType> const& getCurrentCheckTask() const;
protected:
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
// Resets all data that correspond to the currently defined property.
virtual void reset() = 0;
@ -62,7 +71,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
SparseModelType const& parametricModel;
std::shared_ptr<SparseModelType> parametricModel;
std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
private:

6
src/storm-pars/settings/modules/ParametricSettings.cpp
View File

@ -14,7 +14,6 @@ namespace storm {
const std::string ParametricSettings::moduleName = "parametric";
const std::string ParametricSettings::exportResultOptionName = "resultfile";
const std::string ParametricSettings::simplifyOptionName = "simplify";
const std::string ParametricSettings::derivativesOptionName = "derivatives";
const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous";
const std::string ParametricSettings::transformContinuousShortOptionName = "tc";
@ -22,7 +21,6 @@ namespace storm {
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, simplifyOptionName, false, "Sets whether to perform simplification steps before model analysis.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, transformContinuousOptionName, false, "Sets whether to transform a continuous time input model to a discrete time model.").setShortName(transformContinuousShortOptionName).build());
}
@ -35,10 +33,6 @@ namespace storm {
return this->getOption(exportResultOptionName).getArgumentByName("path").getValueAsString();
}
bool ParametricSettings::isSimplifySet() const {
return this->getOption(simplifyOptionName).getHasOptionBeenSet();
}
bool ParametricSettings::isDerivativesSet() const {
return this->getOption(derivativesOptionName).getHasOptionBeenSet();
}

6
src/storm-pars/settings/modules/ParametricSettings.h
View File

@ -30,11 +30,6 @@ namespace storm {
*/
std::string exportResultPath() const;
/*!
* Retrieves whether or not the input model should be simplified before its analysis.
*/
bool isSimplifySet() const;
/*!
* Retrieves whether or not derivatives of the resulting rational function are to be generated.
*
@ -51,7 +46,6 @@ namespace storm {
private:
const static std::string exportResultOptionName;
const static std::string simplifyOptionName;
const static std::string derivativesOptionName;
const static std::string transformContinuousOptionName;
const static std::string transformContinuousShortOptionName;

Write Preview
Loading…
Cancel
Save