From 9f82c3442943147424b3e4f31d6c0ea36314ee09 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 23 Jun 2017 15:11:34 +0200 Subject: [PATCH] storm-pars library --- src/CMakeLists.txt | 5 +- src/storm-pars/CMakeLists.txt | 40 ++ src/storm-pars/api/parametric.h | 45 ++ src/storm-pars/api/region.h | 126 ++++ src/storm-pars/api/storm-pars.h | 4 + .../SparseDtmcInstantiationModelChecker.cpp | 238 ++++--- .../SparseDtmcInstantiationModelChecker.h | 42 +- .../SparseInstantiationModelChecker.cpp | 60 +- .../SparseInstantiationModelChecker.h | 60 +- .../SparseMdpInstantiationModelChecker.cpp | 276 ++++---- .../SparseMdpInstantiationModelChecker.h | 40 +- .../modelchecker/region/RegionCheckEngine.cpp | 25 + .../modelchecker/region/RegionCheckEngine.h | 19 + .../region/RegionModelChecker.cpp | 245 ++------ .../modelchecker/region/RegionModelChecker.h | 107 ++-- .../modelchecker/region/RegionResult.cpp | 62 +- .../modelchecker/region/RegionResult.h | 32 +- ...SparseDtmcParameterLiftingModelChecker.cpp | 480 +++++++------- .../SparseDtmcParameterLiftingModelChecker.h | 65 +- .../region/SparseDtmcRegionChecker.cpp | 65 -- .../region/SparseDtmcRegionChecker.h | 27 - .../SparseMdpParameterLiftingModelChecker.cpp | 595 +++++++++--------- .../SparseMdpParameterLiftingModelChecker.h | 82 +-- .../region/SparseMdpRegionChecker.cpp | 70 --- .../region/SparseMdpRegionChecker.h | 28 - .../SparseParameterLiftingModelChecker.cpp | 182 ++++-- .../SparseParameterLiftingModelChecker.h | 106 ++-- .../results/RegionCheckResult.cpp | 112 ++++ .../modelchecker/results/RegionCheckResult.h | 40 ++ .../results/RegionRefinementCheckResult.cpp | 100 +++ .../results/RegionRefinementCheckResult.h | 30 + .../parser/ParameterRegionParser.cpp | 97 +++ src/storm-pars/parser/ParameterRegionParser.h | 47 ++ .../settings/modules/ParametricSettings.cpp | 62 +- .../settings/modules/ParametricSettings.h | 34 +- .../settings/modules/RegionSettings.cpp | 82 +++ .../settings/modules/RegionSettings.h | 71 +++ src/storm-pars/storage/ParameterRegion.cpp | 63 +- src/storm-pars/storage/ParameterRegion.h | 24 +- .../transformer/ParameterLifter.cpp | 2 +- src/storm-pars/transformer/ParameterLifter.h | 4 +- .../SparseParametricDtmcSimplifier.cpp | 2 +- .../SparseParametricDtmcSimplifier.h | 2 +- .../SparseParametricMdpSimplifier.cpp | 2 +- .../SparseParametricMdpSimplifier.h | 2 +- .../SparseParametricModelSimplifier.cpp | 2 +- src/storm-pars/utility/ModelInstantiator.cpp | 2 +- src/storm-pars/utility/ModelInstantiator.h | 2 +- src/storm-pars/utility/parameterlifting.h | 35 +- src/storm-pars/utility/parametric.cpp | 2 +- 50 files changed, 2172 insertions(+), 1773 deletions(-) create mode 100644 src/storm-pars/CMakeLists.txt create mode 100644 src/storm-pars/api/parametric.h create mode 100644 src/storm-pars/api/region.h create mode 100644 src/storm-pars/api/storm-pars.h create mode 100644 src/storm-pars/modelchecker/region/RegionCheckEngine.cpp create mode 100644 src/storm-pars/modelchecker/region/RegionCheckEngine.h delete mode 100644 src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp delete mode 100644 src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h delete mode 100644 src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp delete mode 100644 src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h create mode 100644 src/storm-pars/modelchecker/results/RegionCheckResult.cpp create mode 100644 src/storm-pars/modelchecker/results/RegionCheckResult.h create mode 100644 src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp create mode 100644 src/storm-pars/modelchecker/results/RegionRefinementCheckResult.h create mode 100644 src/storm-pars/parser/ParameterRegionParser.cpp create mode 100644 src/storm-pars/parser/ParameterRegionParser.h create mode 100644 src/storm-pars/settings/modules/RegionSettings.cpp create mode 100644 src/storm-pars/settings/modules/RegionSettings.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bd0f67e7f..e9059930d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -9,6 +9,9 @@ add_subdirectory(storm-gspn) add_subdirectory(storm-gspn-cli) add_subdirectory(storm-dft) add_subdirectory(storm-dft-cli) +add_subdirectory(storm-pars) +add_subdirectory(storm-pars-cli) + add_subdirectory(test) -set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) \ No newline at end of file +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) diff --git a/src/storm-pars/CMakeLists.txt b/src/storm-pars/CMakeLists.txt new file mode 100644 index 000000000..4e2ec1e0f --- /dev/null +++ b/src/storm-pars/CMakeLists.txt @@ -0,0 +1,40 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pars/*.h ${PROJECT_SOURCE_DIR}/src/storm-pars/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-pars) + + + +file(GLOB_RECURSE STORM_PARS_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.cpp) +file(GLOB_RECURSE STORM_PARS_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.h) + + +# Create storm-pars. +add_library(storm-pars SHARED ${STORM_PARS_SOURCES} ${STORM_PARS_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-pars PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-pars) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-pars PUBLIC storm ${STORM_PARS_LINK_LIBRARIES}) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_PARS_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_PARS_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_pars_headers DEPENDS ${STORM_PARS_OUTPUT_HEADERS} ${STORM_PARS_HEADERS}) +add_dependencies(storm-pars copy_storm_pars_headers) + +# installation +install(TARGETS storm-pars RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm-pars/api/parametric.h b/src/storm-pars/api/parametric.h new file mode 100644 index 000000000..66f263a3f --- /dev/null +++ b/src/storm-pars/api/parametric.h @@ -0,0 +1,45 @@ +#pragma once + +#include + +#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 + bool simplifyParametricModel(std::shared_ptr const& inputModel, std::shared_ptr const& inputFormula, std::shared_ptr& outputModel, std::shared_ptr& outputFormula) { + + if (inputModel->isOfType(storm::models::ModelType::Dtmc)) { + auto const& dtmc = *inputModel->template as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(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>(); + auto simplifier = storm::transformer::SparseParametricMdpSimplifier>(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; + + } + } +} diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h new file mode 100644 index 000000000..8dffe156b --- /dev/null +++ b/src/storm-pars/api/region.h @@ -0,0 +1,126 @@ +#pragma once + +#include +#include +#include +#include +#include + +#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/SparseMdpParameterLiftingModelChecker.h" +#include "storm-pars/parser/ParameterRegionParser.h" + +#include "storm/api/transformation.h" +#include "storm/models/sparse/Model.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + + namespace api { + + + enum class RegionModelCheckerType { + ParameterLifting, + ExactParameterLifting, + ValidatingParameterLifting + }; + + template + std::vector> parseRegions(std::string const& inputString, std::set::VariableType> const& consideredVariables) { + // If the given input string looks like a file (containing a dot and there exists a file with that name), + // we try to parse it as a file, otherwise we assume it's a region string. + if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { + return storm::parser::ParameterRegionParser().parseMultipleRegionsFromFile(inputString, consideredVariables); + } else { + return storm::parser::ParameterRegionParser().parseMultipleRegions(inputString, consideredVariables); + } + } + + template + std::vector> parseRegions(std::string const& inputString, storm::models::sparse::Model const& model) { + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + return parseRegions(inputString, modelParameters); + } + + template + std::unique_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + // Treat continuous time models + if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model..."); + std::vector> 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(discreteTimeModel, task); + } + + // Obtain the region model checker + std::unique_ptr> result; + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto const& dtmc = *model->template as>(); + result = std::make_unique, ConstantType>>(dtmc); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + auto const& mdp = *model->template as>(); + result = std::make_unique, ConstantType>>(mdp); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); + } + + result->specifyFormula(task); + + return result; + } + + template + std::unique_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + // todo + return nullptr; + } + + template + std::unique_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, RegionModelCheckerType checkerType) { + switch (checkerType) { + case RegionModelCheckerType::ParameterLifting: + return initializeParameterLiftingRegionModelChecker(model, task); + case RegionModelCheckerType::ExactParameterLifting: + return initializeParameterLiftingRegionModelChecker(model, task); + case RegionModelCheckerType::ValidatingParameterLifting: + return initializeValidatingRegionModelChecker(model, task); + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected region model checker type."); + } + return nullptr; + } + + template + std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, RegionModelCheckerType checkerType) { + auto regionChecker = initializeRegionModelChecker(model, task, checkerType); + return regionChecker->analyzeRegions(regions, true); + } + + + template + td::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, ValueType const& refinementThreshold) { + auto regionChecker = initializeRegionModelChecker(model, task, checkerType); + return regionChecker->performRegionRefinement(region, refinementThreshold); + } + + + template + void exportRegionCheckResultToFile(std::unique_ptr> const& checkResult, std::string const& filename) { + + std::ofstream filestream; + storm::utility::openFile(path, filestream); + for (auto const& res : checkResult->getRegionResults()) { + filestream << res.second << ": " << res.first << std::endl; + } + } + + } +} diff --git a/src/storm-pars/api/storm-pars.h b/src/storm-pars/api/storm-pars.h new file mode 100644 index 000000000..f7b15dda0 --- /dev/null +++ b/src/storm-pars/api/storm-pars.h @@ -0,0 +1,4 @@ +#pragma once + +#include "storm-pars/api/region.h" +#include "storm-pars/api/parametric.h" diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp index 6b3d376a8..14d433e58 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp @@ -1,4 +1,4 @@ -#include "SparseDtmcInstantiationModelChecker.h" +#include "storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h" #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -10,43 +10,112 @@ #include "storm/exceptions/InvalidStateException.h" namespace storm { namespace modelchecker { - namespace parametric { + + template + SparseDtmcInstantiationModelChecker::SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker(parametricModel), modelInstantiator(parametricModel) { + //Intentionally left empty + } + + template + std::unique_ptr SparseDtmcInstantiationModelChecker::check(storm::utility::parametric::Valuation const& valuation) { + STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before."); + auto const& instantiatedModel = modelInstantiator.instantiate(valuation); + STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!"); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(instantiatedModel); + + // Check if there are some optimizations implemented for the specified property + if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) { + return checkReachabilityProbabilityFormula(modelChecker); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkReachabilityRewardFormula(modelChecker); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkBoundedUntilFormula(modelChecker); + } else { + return modelChecker.check(*this->currentCheckTask); + } + } + + template + std::unique_ptr SparseDtmcInstantiationModelChecker::checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { - template - SparseDtmcInstantiationModelChecker::SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker(parametricModel), modelInstantiator(parametricModel) { - //Intentionally left empty + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); } - - template - std::unique_ptr SparseDtmcInstantiationModelChecker::check(storm::utility::parametric::Valuation const& valuation) { - STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before."); - auto const& instantiatedModel = modelInstantiator.instantiate(valuation); - STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!"); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(instantiatedModel); - - // Check if there are some optimizations implemented for the specified property - if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) { - return checkReachabilityProbabilityFormula(modelChecker); - } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { - return checkReachabilityRewardFormula(modelChecker); - } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { - return checkBoundedUntilFormula(modelChecker); - } else { - return modelChecker.check(*this->currentCheckTask); - } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + + // Check the formula and store the result as a hint for the next call. + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - - template - std::unique_ptr SparseDtmcInstantiationModelChecker::checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { - - if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { - this->currentCheckTask->setHint(std::make_shared>()); - } - ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; - - // Check the formula and store the result as a hint for the next call. - // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), + [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } + + return result; + } + + template + std::unique_ptr SparseDtmcInstantiationModelChecker::checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + + // Check the formula and store the result as a hint for the next call. + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + } + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with reward zero since a valuation might set a reward to zero + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } + + return result; + } + + template + std::unique_ptr SparseDtmcInstantiationModelChecker::checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + std::unique_ptr result; + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // We extract the maybestates from the quantitative result + // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { result = modelChecker.check(*this->currentCheckTask); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); @@ -57,93 +126,22 @@ namespace storm { hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), - [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } - - return result; + storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint()); + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } else { + result = modelChecker.check(*this->currentCheckTask); } - template - std::unique_ptr SparseDtmcInstantiationModelChecker::checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { - - if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { - this->currentCheckTask->setHint(std::make_shared>()); - } - ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; - - // Check the formula and store the result as a hint for the next call. - // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula - if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - result = modelChecker.check(*this->currentCheckTask); - this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - } else { - auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); - result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - } - - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with reward zero since a valuation might set a reward to zero - std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } - - return result; - } - - template - std::unique_ptr SparseDtmcInstantiationModelChecker::checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { - - if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { - this->currentCheckTask->setHint(std::make_shared>()); - } - std::unique_ptr result; - ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // We extract the maybestates from the quantitative result - // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula - if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - result = modelChecker.check(*this->currentCheckTask); - hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - } else { - auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); - result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - } - - storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps - std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } else { - result = modelChecker.check(*this->currentCheckTask); - } - - return result; - } - - template class SparseDtmcInstantiationModelChecker, double>; - template class SparseDtmcInstantiationModelChecker, storm::RationalNumber>; - + return result; } + + template class SparseDtmcInstantiationModelChecker, double>; + template class SparseDtmcInstantiationModelChecker, storm::RationalNumber>; + } } \ No newline at end of file diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h index 511253107..ad1ffead4 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h @@ -3,35 +3,33 @@ #include #include +#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h" +#include "storm-pars/utility/ModelInstantiator.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "storm/utility/ModelInstantiator.h" namespace storm { namespace modelchecker { - namespace parametric { + + /*! + * Class to efficiently check a formula on a parametric model with different parameter instantiations + */ + template + class SparseDtmcInstantiationModelChecker : public SparseInstantiationModelChecker { + public: + SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel); - /*! - * Class to efficiently check a formula on a parametric model with different parameter instantiations - */ - template - class SparseDtmcInstantiationModelChecker : public SparseInstantiationModelChecker { - public: - SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel); - - virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) override; + virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) override; - protected: - - // Optimizations for the different formula types - std::unique_ptr checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); - std::unique_ptr checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); - std::unique_ptr checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); - - storm::utility::ModelInstantiator> modelInstantiator; - }; - } + protected: + + // Optimizations for the different formula types + std::unique_ptr checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); + std::unique_ptr checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); + std::unique_ptr checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); + + storm::utility::ModelInstantiator> modelInstantiator; + }; } } diff --git a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp index 1a7a004d4..d81d5b9a6 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp @@ -1,4 +1,4 @@ -#include "SparseInstantiationModelChecker.h" +#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" @@ -9,36 +9,34 @@ namespace storm { namespace modelchecker { - namespace parametric { - - template - SparseInstantiationModelChecker::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), instantiationsAreGraphPreserving(false) { - //Intentionally left empty - } - - - template - void SparseInstantiationModelChecker::specifyFormula(storm::modelchecker::CheckTask const& checkTask) { - currentFormula = checkTask.getFormula().asSharedPointer(); - currentCheckTask = std::make_unique>(checkTask.substituteFormula(*currentFormula).template convertValueType()); - } - - template - void SparseInstantiationModelChecker::setInstantiationsAreGraphPreserving(bool value) { - instantiationsAreGraphPreserving = value; - } - - template - bool SparseInstantiationModelChecker::getInstantiationsAreGraphPreserving() const { - return instantiationsAreGraphPreserving; - } - - template class SparseInstantiationModelChecker, double>; - template class SparseInstantiationModelChecker, double>; - - template class SparseInstantiationModelChecker, storm::RationalNumber>; - template class SparseInstantiationModelChecker, storm::RationalNumber>; - + + template + SparseInstantiationModelChecker::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), instantiationsAreGraphPreserving(false) { + //Intentionally left empty + } + + + template + void SparseInstantiationModelChecker::specifyFormula(storm::modelchecker::CheckTask const& checkTask) { + currentFormula = checkTask.getFormula().asSharedPointer(); + currentCheckTask = std::make_unique>(checkTask.substituteFormula(*currentFormula).template convertValueType()); + } + + template + void SparseInstantiationModelChecker::setInstantiationsAreGraphPreserving(bool value) { + instantiationsAreGraphPreserving = value; } + + template + bool SparseInstantiationModelChecker::getInstantiationsAreGraphPreserving() const { + return instantiationsAreGraphPreserving; + } + + template class SparseInstantiationModelChecker, double>; + template class SparseInstantiationModelChecker, double>; + + template class SparseInstantiationModelChecker, storm::RationalNumber>; + template class SparseInstantiationModelChecker, storm::RationalNumber>; + } } diff --git a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h index d51f87f38..43ed587ec 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h +++ b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h @@ -1,44 +1,42 @@ #pragma once +#include "storm-pars/utility/parametric.h" #include "storm/logic/Formulas.h" #include "storm/modelchecker/CheckTask.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" -#include "storm/utility/parametric.h" namespace storm { namespace modelchecker { - namespace parametric { + + /*! + * Class to efficiently check a formula on a parametric model with different parameter instantiations + */ + template + class SparseInstantiationModelChecker { + public: + SparseInstantiationModelChecker(SparseModelType const& parametricModel); + virtual ~SparseInstantiationModelChecker() = default; - /*! - * Class to efficiently check a formula on a parametric model with different parameter instantiations - */ - template - class SparseInstantiationModelChecker { - public: - SparseInstantiationModelChecker(SparseModelType const& parametricModel); - virtual ~SparseInstantiationModelChecker() = default; - - void specifyFormula(CheckTask const& checkTask); - - virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) = 0; - - // If set, it is assumed that all considered model instantiations have the same underlying graph structure. - // This bypasses the graph analysis for the different instantiations. - void setInstantiationsAreGraphPreserving(bool value); - bool getInstantiationsAreGraphPreserving() const; - - protected: - - SparseModelType const& parametricModel; - std::unique_ptr> currentCheckTask; - - private: - // store the current formula. Note that currentCheckTask only stores a reference to the formula. - std::shared_ptr currentFormula; + void specifyFormula(CheckTask const& checkTask); + + virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) = 0; + + // If set, it is assumed that all considered model instantiations have the same underlying graph structure. + // This bypasses the graph analysis for the different instantiations. + void setInstantiationsAreGraphPreserving(bool value); + bool getInstantiationsAreGraphPreserving() const; + + protected: + + SparseModelType const& parametricModel; + std::unique_ptr> currentCheckTask; + + private: + // store the current formula. Note that currentCheckTask only stores a reference to the formula. + std::shared_ptr currentFormula; - bool instantiationsAreGraphPreserving; - }; - } + bool instantiationsAreGraphPreserving; + }; } } diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index 1be1e9ac8..887d3b7bf 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -1,4 +1,4 @@ -#include "SparseMdpInstantiationModelChecker.h" +#include "storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h" #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -13,161 +13,159 @@ namespace storm { namespace modelchecker { - namespace parametric { + + template + SparseMdpInstantiationModelChecker::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker(parametricModel), modelInstantiator(parametricModel) { + //Intentionally left empty + } + + template + std::unique_ptr SparseMdpInstantiationModelChecker::check(storm::utility::parametric::Valuation const& valuation) { + STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before."); + auto const& instantiatedModel = modelInstantiator.instantiate(valuation); + STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!"); + storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(instantiatedModel); + + // Check if there are some optimizations implemented for the specified property + if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) { + return checkReachabilityProbabilityFormula(modelChecker, instantiatedModel); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkReachabilityRewardFormula(modelChecker, instantiatedModel); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkBoundedUntilFormula(modelChecker); + } else { + return modelChecker.check(*this->currentCheckTask); + } + } + + template + std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { + + this->currentCheckTask->setProduceSchedulers(true); - template - SparseMdpInstantiationModelChecker::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker(parametricModel), modelInstantiator(parametricModel) { - //Intentionally left empty + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); } - - template - std::unique_ptr SparseMdpInstantiationModelChecker::check(storm::utility::parametric::Valuation const& valuation) { - STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before."); - auto const& instantiatedModel = modelInstantiator.instantiate(valuation); - STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!"); - storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(instantiatedModel); - - // Check if there are some optimizations implemented for the specified property - if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) { - return checkReachabilityProbabilityFormula(modelChecker, instantiatedModel); - } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { - return checkReachabilityRewardFormula(modelChecker, instantiatedModel); - } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { - return checkBoundedUntilFormula(modelChecker); - } else { - return modelChecker.check(*this->currentCheckTask); - } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + + // Check the formula and store the result as a hint for the next call. + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + hint.setSchedulerHint(dynamic_cast const&>(scheduler)); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } - template - std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), + [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); - this->currentCheckTask->setProduceSchedulers(true); - - if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { - this->currentCheckTask->setHint(std::make_shared>()); + // Check if there can be end components within the maybestates + if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) || + storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { + hint.setNoEndComponentsInMaybeStates(true); } - ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; - - // Check the formula and store the result as a hint for the next call. - // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula - if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - result = modelChecker.check(*this->currentCheckTask); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); - hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - hint.setSchedulerHint(dynamic_cast const&>(scheduler)); - } else { - auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); - result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); - hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); - } - - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), - [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - - // Check if there can be end components within the maybestates - if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) || - storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { - hint.setNoEndComponentsInMaybeStates(true); - } - } - - return result; } - template - std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { - - this->currentCheckTask->setProduceSchedulers(true); + return result; + } + + template + std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { + + this->currentCheckTask->setProduceSchedulers(true); + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + + // Check the formula and store the result as a hint for the next call. + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + std::unique_ptr result = modelChecker.check(*this->currentCheckTask); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + hint.setSchedulerHint(dynamic_cast const&>(scheduler)); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); + } + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with reward zero since a valuation might set a reward to zero + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); - if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { - this->currentCheckTask->setHint(std::make_shared>()); + // Check if there can be end components within the maybestates + if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) || + storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { + hint.setNoEndComponentsInMaybeStates(true); } - ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; - - // Check the formula and store the result as a hint for the next call. - // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula - if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - std::unique_ptr result = modelChecker.check(*this->currentCheckTask); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + } + return result; + } + + template + std::unique_ptr SparseMdpInstantiationModelChecker::checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + std::unique_ptr result; + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // We extract the maybestates from the quantitative result + // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - hint.setSchedulerHint(dynamic_cast const&>(scheduler)); } else { auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } - - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with reward zero since a valuation might set a reward to zero - std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - - // Check if there can be end components within the maybestates - if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) || - storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { - hint.setNoEndComponentsInMaybeStates(true); - } - } - return result; - } - - template - std::unique_ptr SparseMdpInstantiationModelChecker::checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker) { - - if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { - this->currentCheckTask->setHint(std::make_shared>()); - } - std::unique_ptr result; - ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // We extract the maybestates from the quantitative result - // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula - if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - result = modelChecker.check(*this->currentCheckTask); - hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - } else { - auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); - result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - } - storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps - std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } else { - result = modelChecker.check(*this->currentCheckTask); - } - return result; + storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint()); + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } else { + result = modelChecker.check(*this->currentCheckTask); } - - template class SparseMdpInstantiationModelChecker, double>; - template class SparseMdpInstantiationModelChecker, storm::RationalNumber>; - + return result; } + + template class SparseMdpInstantiationModelChecker, double>; + template class SparseMdpInstantiationModelChecker, storm::RationalNumber>; + } } diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h index a5570acc0..d8d5d46e8 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h @@ -2,35 +2,33 @@ #include +#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h" +#include "storm-pars/utility/ModelInstantiator.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "storm/utility/ModelInstantiator.h" namespace storm { namespace modelchecker { - namespace parametric { + + /*! + * Class to efficiently check a formula on a parametric model with different parameter instantiations + */ + template + class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecker { + public: + SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel); - /*! - * Class to efficiently check a formula on a parametric model with different parameter instantiations - */ - template - class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecker { - public: - SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel); - - virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) override; + virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) override; - protected: - // Optimizations for the different formula types - std::unique_ptr checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel); - std::unique_ptr checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel); - std::unique_ptr checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker); - - storm::utility::ModelInstantiator> modelInstantiator; - }; - } + protected: + // Optimizations for the different formula types + std::unique_ptr checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel); + std::unique_ptr checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel); + std::unique_ptr checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker); + + storm::utility::ModelInstantiator> modelInstantiator; + }; } } diff --git a/src/storm-pars/modelchecker/region/RegionCheckEngine.cpp b/src/storm-pars/modelchecker/region/RegionCheckEngine.cpp new file mode 100644 index 000000000..e23be1eb1 --- /dev/null +++ b/src/storm-pars/modelchecker/region/RegionCheckEngine.cpp @@ -0,0 +1,25 @@ +#include "storm-pars/modelchecker/region/RegionCheckEngine.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + std::ostream& operator<<(std::ostream& os, RegionCheckEngine const& e) { + switch (e) { + case RegionCheckEngine::ParameterLifting: + os << "Parameter Lifting"; + break; + case RegionCheckEngine::ExactParameterLifting: + os << "Exact Parameter Lifting"; + break; + case RegionCheckEngine::ValidatingParameterLifting: + os << "Validating Parameter Lifting"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check engine. The case has not been implemented"); + } + return os; + } + } +} diff --git a/src/storm-pars/modelchecker/region/RegionCheckEngine.h b/src/storm-pars/modelchecker/region/RegionCheckEngine.h new file mode 100644 index 000000000..5ff26d691 --- /dev/null +++ b/src/storm-pars/modelchecker/region/RegionCheckEngine.h @@ -0,0 +1,19 @@ +#pragma once + +#include + +namespace storm { + namespace modelchecker { + /*! + * The considered engine for region checking + */ + enum class RegionCheckEngine { + ParameterLifting, /*!< Parameter lifting approach */ + ExactParameterLifting, /*!< Parameter lifting approach with exact arithmethics*/ + ValidatingParameterLifting, /*!< Parameter lifting approach with a) inexact (and fast) computation first and b) exact validation of obtained results second */ + }; + + std::ostream& operator<<(std::ostream& os, RegionCheckEngine const& regionCheckResult); + } +} + diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index d01fe5160..d6a457899 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -1,11 +1,10 @@ #include #include -#include "storm/modelchecker/parametric/RegionChecker.h" +#include "storm-pars/modelchecker/region/RegionModelChecker.h" #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/vector.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -18,164 +17,88 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/ParametricSettings.h" namespace storm { namespace modelchecker { - namespace parametric { - RegionCheckerSettings::RegionCheckerSettings() { - this->applyExactValidation = storm::settings::getModule().isExactValidationSet(); - } - - template - RegionChecker::RegionChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), numOfCorrectedRegions(0) { - initializationStopwatch.start(); - STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Parameter lifting requires models with only one initial state"); - initializationStopwatch.stop(); + template + RegionModelChecker::RegionModelChecker() { + // Intentionally left empty } - template - RegionCheckerSettings const& RegionChecker::getSettings() const { - return settings; - } - - template - void RegionChecker::setSettings(RegionCheckerSettings const& newSettings) { - settings = newSettings; - } - - template - void RegionChecker::specifyFormula(CheckTask 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."); + template + std::unique_ptr> RegionModelChecker::analyzeRegions(std::vector> const& regions, bool sampleVerticesOfRegion) { - simplifyParametricModel(checkTask); - initializeUnderlyingCheckers(); - currentCheckTask = std::make_unique>(checkTask.substituteFormula(*currentFormula)); - - STORM_LOG_THROW(parameterLiftingChecker->canHandle(*currentCheckTask) && - (!exactParameterLiftingChecker || exactParameterLiftingChecker->canHandle(*currentCheckTask)), - storm::exceptions::NotSupportedException, "Parameter lifting is not supported for this property."); - if (exactParameterLiftingChecker) { - exactParameterLiftingChecker->specifyFormula(*currentCheckTask); - } - parameterLiftingChecker->specifyFormula(*currentCheckTask); - instantiationChecker->specifyFormula(*currentCheckTask); - initializationStopwatch.stop(); - } - - template - RegionResult RegionChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { - RegionResult result = initialResult; - - // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated - instantiationCheckerStopwatch.start(); - if (result == RegionCheckResult::Unknown) { - result = instantiationChecker->check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()] ? RegionCheckResult::CenterSat : RegionCheckResult::CenterViolated; - } - instantiationCheckerStopwatch.stop(); + std::vector, storm::modelchecker::RegionResult>> result; - // try to prove AllSat or AllViolated, depending on the obtained result - parameterLiftingCheckerStopwatch.start(); - if(result == RegionCheckResult::ExistsSat || result == RegionCheckResult::CenterSat) { - // show AllSat: - storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; - if(parameterLiftingChecker->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { - result = RegionCheckResult::AllSat; - } else if (sampleVerticesOfRegion) { - parameterLiftingCheckerStopwatch.stop(); instantiationCheckerStopwatch.start(); - // Check if there is a point in the region for which the property is violated - auto vertices = region.getVerticesOfRegion(region.getVariables()); - for (auto const& v : vertices) { - if (!instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { - result = RegionCheckResult::ExistsBoth; - } - } - instantiationCheckerStopwatch.stop(); parameterLiftingCheckerStopwatch.start(); - } - } else if (result == RegionCheckResult::ExistsViolated || result == RegionCheckResult::CenterViolated) { - // show AllViolated: - storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize; - if(!parameterLiftingChecker->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { - result = RegionCheckResult::AllViolated; - } else if (sampleVerticesOfRegion) { - parameterLiftingCheckerStopwatch.stop(); instantiationCheckerStopwatch.start(); - // Check if there is a point in the region for which the property is satisfied - auto vertices = region.getVerticesOfRegion(region.getVariables()); - for (auto const& v : vertices) { - if (instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { - result = RegionCheckResult::ExistsBoth; - } - } - instantiationCheckerStopwatch.stop(); parameterLiftingCheckerStopwatch.start(); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult); + for (auto const& region : regions) { + storm::modelchecker::RegionResult regionRes = analyzeRegion(region, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion); + result.emplace_back(region, regionRes); } - parameterLiftingCheckerStopwatch.stop(); - return result; + + return std::make_unique>(std::move(result)); } - - template - RegionResult RegionChecker::analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionResult const& initialResult) { + + /* +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + template + RegionResult RegionModelChecker::analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionResult const& initialResult) { RegionResult numericResult = analyzeRegion(region, initialResult, false); parameterLiftingCheckerStopwatch.start(); - if (numericResult == RegionCheckResult::AllSat || numericResult == RegionCheckResult::AllViolated) { + if (numericResult == RegionResult::AllSat || numericResult == RegionResult::AllViolated) { applyHintsToExactChecker(); } - if (numericResult == RegionCheckResult::AllSat) { + 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 RegionCheckResult::AllViolated; + return RegionResult::AllViolated; } else { parameterLiftingCheckerStopwatch.stop(); - return RegionCheckResult::Unknown; + return RegionResult::Unknown; } } - } else if (numericResult == RegionCheckResult::AllViolated) { + } 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 RegionCheckResult::AllSat; + return RegionResult::AllSat; } else { parameterLiftingCheckerStopwatch.stop(); - return RegionCheckResult::Unknown; + return RegionResult::Unknown; } } } parameterLiftingCheckerStopwatch.stop(); return numericResult; } - +*/ - template - std::vector, RegionResult>> RegionChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold) { + template + std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, ParametricType const& threshold) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); + auto thresholdAsCoefficient = storm::utility::convertNumber(threshold); auto areaOfParameterSpace = region.area(); auto fractionOfUndiscoveredArea = storm::utility::one(); auto fractionOfAllSatArea = storm::utility::zero(); auto fractionOfAllViolatedArea = storm::utility::zero(); - std::queue, RegionResult>> unprocessedRegions; - std::vector, RegionResult>> result; - unprocessedRegions.emplace(region, RegionCheckResult::Unknown); + std::queue, RegionResult>> unprocessedRegions; + std::vector, RegionResult>> result; + unprocessedRegions.emplace(region, RegionResult::Unknown); uint_fast64_t numOfAnalyzedRegions = 0; - numOfCorrectedRegions = 0; CoefficientType displayedProgress = storm::utility::zero(); if (storm::settings::getModule().isShowStatisticsSet()) { STORM_PRINT_AND_LOG("Progress (solved fraction) :" << std::endl << "0% ["); - while (displayedProgress < storm::utility::one() - threshold) { + while (displayedProgress < storm::utility::one() - thresholdAsCoefficient) { STORM_PRINT_AND_LOG(" "); displayedProgress += storm::utility::convertNumber(0.01); } @@ -187,33 +110,29 @@ namespace storm { displayedProgress = storm::utility::zero(); } - while (fractionOfUndiscoveredArea > threshold) { + while (fractionOfUndiscoveredArea > thresholdAsCoefficient) { STORM_LOG_THROW(!unprocessedRegions.empty(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left."); STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (" << storm::utility::convertNumber(fractionOfUndiscoveredArea) * 100 << "% still unknown)"); auto& currentRegion = unprocessedRegions.front().first; auto& res = unprocessedRegions.front().second; - if (settings.applyExactValidation) { - res = analyzeRegionExactValidation(currentRegion, res); - } else { - res = analyzeRegion(currentRegion, res, false); - } + res = analyzeRegion(currentRegion, res, false); switch (res) { - case RegionCheckResult::AllSat: + case RegionResult::AllSat: fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace; fractionOfAllSatArea += currentRegion.area() / areaOfParameterSpace; result.push_back(std::move(unprocessedRegions.front())); break; - case RegionCheckResult::AllViolated: + case RegionResult::AllViolated: fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace; fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace; result.push_back(std::move(unprocessedRegions.front())); break; default: - std::vector> newRegions; + std::vector> newRegions; currentRegion.split(currentRegion.getCenterPoint(), newRegions); - RegionResult initResForNewRegions = (res == RegionCheckResult::CenterSat) ? RegionCheckResult::ExistsSat : - ((res == RegionCheckResult::CenterViolated) ? RegionCheckResult::ExistsViolated : - RegionCheckResult::Unknown); + RegionResult initResForNewRegions = (res == RegionResult::CenterSat) ? RegionResult::ExistsSat : + ((res == RegionResult::CenterViolated) ? RegionResult::ExistsViolated : + RegionResult::Unknown); for(auto& newRegion : newRegions) { unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions); } @@ -236,91 +155,17 @@ namespace storm { } STORM_PRINT_AND_LOG("]" << std::endl); - STORM_PRINT_AND_LOG("Parameter Lifting Statistics:" << std::endl); + STORM_PRINT_AND_LOG("Region Refinement Statistics:" << std::endl); STORM_PRINT_AND_LOG(" Analyzed a total of " << numOfAnalyzedRegions << " regions." << std::endl); - if (settings.applyExactValidation) { - STORM_PRINT_AND_LOG(" Exact validation corrected " << numOfCorrectedRegions << " regions." << std::endl); - } - STORM_PRINT_AND_LOG(" Initialization took " << initializationStopwatch << " seconds." << std::endl); - STORM_PRINT_AND_LOG(" Checking sampled models took " << instantiationCheckerStopwatch << " seconds." << std::endl); - STORM_PRINT_AND_LOG(" Checking lifted models took " << parameterLiftingCheckerStopwatch << " seconds." << std::endl); - } - return result; - } - - template - SparseModelType const& RegionChecker::getConsideredParametricModel() const { - if (simplifiedModel) { - return *simplifiedModel; - } else { - return parametricModel; } - } - - template - std::string RegionChecker::visualizeResult(std::vector, RegionResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y) { - - std::stringstream stream; - uint_fast64_t const sizeX = 128; - uint_fast64_t const sizeY = 64; - - stream << "Parameter lifting result (visualization):" << std::endl; - stream << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl; - for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl; - - CoefficientType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber(sizeX); - CoefficientType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber(sizeY); - CoefficientType printedRegionArea = deltaX * deltaY; - for (CoefficientType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) { - CoefficientType yLower = yUpper - deltaY; - stream << "#"; - for (CoefficientType xLower = parameterSpace.getLowerBoundary(x); xLower != parameterSpace.getUpperBoundary(x); xLower += deltaX) { - CoefficientType xUpper = xLower + deltaX; - bool currRegionSafe = false; - bool currRegionUnSafe = false; - bool currRegionComplete = false; - CoefficientType coveredArea = storm::utility::zero(); - for (auto const& r : result) { - CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)); - interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero()); - CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)); - interesctionSizeX = std::max(interesctionSizeX, storm::utility::zero()); - CoefficientType instersectionArea = interesctionSizeY * interesctionSizeX; - if(!storm::utility::isZero(instersectionArea)) { - currRegionSafe = currRegionSafe || r.second == RegionCheckResult::AllSat; - currRegionUnSafe = currRegionUnSafe || r.second == RegionCheckResult::AllViolated; - coveredArea += instersectionArea; - if(currRegionSafe && currRegionUnSafe) { - break; - } - if(coveredArea == printedRegionArea) { - currRegionComplete = true; - break; - } - } - } - if (currRegionComplete && currRegionSafe && !currRegionUnSafe) { - stream << "S"; - } else if (currRegionComplete && currRegionUnSafe && !currRegionSafe) { - stream << " "; - } else { - stream << "-"; - } - } - stream << "#" << std::endl; - } - for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl; - return stream.str(); + auto regionCopyForResult = region; + return std::make_unique>(std::move(result), std::move(regionCopyForResult)); } - + #ifdef STORM_HAVE_CARL - template class RegionChecker, double, storm::RationalNumber>; - template class RegionChecker, double, storm::RationalNumber>; - template class RegionChecker, storm::RationalNumber>; - template class RegionChecker, storm::RationalNumber>; + template class RegionModelChecker; #endif - } // namespace parametric } //namespace modelchecker } //namespace storm diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index 377615f1c..746c9b2d3 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -2,84 +2,49 @@ #include -#include "storm/modelchecker/parametric/RegionCheckResult.h" -#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h" -#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/results/RegionCheckResult.h" +#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h" +#include "storm-pars/modelchecker/region/RegionResult.h" +#include "storm-pars/storage/ParameterRegion.h" + #include "storm/modelchecker/CheckTask.h" -#include "storm/storage/ParameterRegion.h" -#include "storm/utility/Stopwatch.h" -#include "storm/utility/NumberTraits.h" namespace storm { namespace modelchecker{ - namespace parametric{ + + template + class RegionModelChecker { + public: - struct RegionCheckerSettings { - RegionCheckerSettings(); - - bool applyExactValidation; - }; - - template - class RegionChecker { - static_assert(storm::NumberTraits::IsExact, "Specified type for exact computations is not exact."); + typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; - public: - - typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; + RegionModelChecker(); + virtual ~RegionModelChecker() = default; + + virtual bool canHandle(CheckTask const& checkTask) const = 0; - RegionChecker(SparseModelType const& parametricModel); - virtual ~RegionChecker() = default; - - RegionCheckerSettings const& getSettings() const; - void setSettings(RegionCheckerSettings const& newSettings); - - void specifyFormula(CheckTask const& checkTask); - - /*! - * Analyzes the given region by means of parameter lifting. - * We first check whether there is one point in the region for which the property is satisfied/violated. - * If the given initialResults already indicates that there is such a point, this step is skipped. - * Then, we check whether ALL points in the region violate/satisfy the property - * - */ - RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false); - /*! - * Similar to analyze region but additionaly invokes exact parameter lifting to validate results AllSat or AllViolated - */ - RegionResult analyzeRegionExactValidation(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionCheckResult::Unknown); - - /*! - * Iteratively refines the region until parameter lifting yields a conclusive result (AllSat or AllViolated). - * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold - */ - std::vector, RegionResult>> performRegionRefinement(storm::storage::ParameterRegion const& region, CoefficientType const& threshold); - - static std::string visualizeResult(std::vector, RegionResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y); - - protected: - SparseModelType const& getConsideredParametricModel() const; - - virtual void initializeUnderlyingCheckers() = 0; - virtual void simplifyParametricModel(CheckTask const& checkTask) = 0; - virtual void applyHintsToExactChecker() = 0; - - SparseModelType const& parametricModel; - RegionCheckerSettings settings; - std::unique_ptr> currentCheckTask; - std::shared_ptr currentFormula; - std::shared_ptr simplifiedModel; - + virtual void specifyFormula(CheckTask const& checkTask) = 0; + + /*! + * Analyzes the given region. + * An initial region result can be given to simplify the analysis (e.g. if the initial result is ExistsSat, we do not check for AllViolated). + * If supported by this model checker, it is possible to sample the vertices of the region whenever AllSat/AllViolated could not be shown. + */ + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0; + + /*! + * Analyzes the given regions. + * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown. + */ + std::unique_ptr> analyzeRegions(std::vector> const& regions, bool sampleVerticesOfRegion = false) ; + + /*! + * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated). + * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold + */ + std::unique_ptr> performRegionRefinement(storm::storage::ParameterRegion const& region, ParametricType const& threshold); + + }; - std::unique_ptr> parameterLiftingChecker; - std::unique_ptr> exactParameterLiftingChecker; - std::unique_ptr> instantiationChecker; - - // Information for statistics - mutable storm::utility::Stopwatch initializationStopwatch, instantiationCheckerStopwatch, parameterLiftingCheckerStopwatch; - mutable uint_fast64_t numOfCorrectedRegions; - }; - - } //namespace parametric } //namespace modelchecker } //namespace storm diff --git a/src/storm-pars/modelchecker/region/RegionResult.cpp b/src/storm-pars/modelchecker/region/RegionResult.cpp index 48f743462..0da22a028 100644 --- a/src/storm-pars/modelchecker/region/RegionResult.cpp +++ b/src/storm-pars/modelchecker/region/RegionResult.cpp @@ -1,42 +1,40 @@ -#include "storm/modelchecker/parametric/RegionCheckResult.h" +#include "storm-pars/modelchecker/region/RegionResult.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" namespace storm { namespace modelchecker { - namespace parametric { - std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult) { - switch (regionCheckResult) { - case RegionCheckResult::Unknown: - os << "Unknown"; - break; - case RegionCheckResult::ExistsSat: - os << "ExistsSat"; - break; - case RegionCheckResult::ExistsViolated: - os << "ExistsViolated"; - break; - case RegionCheckResult::CenterSat: - os << "CenterSat"; - break; - case RegionCheckResult::CenterViolated: - os << "CenterViolated"; - break; - case RegionCheckResult::ExistsBoth: - os << "ExistsBoth"; - break; - case RegionCheckResult::AllSat: - os << "AllSat"; - break; - case RegionCheckResult::AllViolated: - os << "AllViolated"; - break; - default: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check result. The case has not been implemented"); - } - return os; + std::ostream& operator<<(std::ostream& os, RegionResult const& regionResult) { + switch (regionResult) { + case RegionResult::Unknown: + os << "Unknown"; + break; + case RegionResult::ExistsSat: + os << "ExistsSat"; + break; + case RegionResult::ExistsViolated: + os << "ExistsViolated"; + break; + case RegionResult::CenterSat: + os << "CenterSat"; + break; + case RegionResult::CenterViolated: + os << "CenterViolated"; + break; + case RegionResult::ExistsBoth: + os << "ExistsBoth"; + break; + case RegionResult::AllSat: + os << "AllSat"; + break; + case RegionResult::AllViolated: + os << "AllViolated"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region check result. The case has not been implemented"); } + return os; } } } diff --git a/src/storm-pars/modelchecker/region/RegionResult.h b/src/storm-pars/modelchecker/region/RegionResult.h index 267b6e665..1ad568f87 100644 --- a/src/storm-pars/modelchecker/region/RegionResult.h +++ b/src/storm-pars/modelchecker/region/RegionResult.h @@ -4,23 +4,21 @@ namespace storm { namespace modelchecker { - namespace parametric { - /*! - * The results for a single Parameter region - */ - enum class RegionCheckResult { - Unknown, /*!< the result is unknown */ - ExistsSat, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */ - ExistsViolated, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */ - CenterSat, /*!< the formula is satisfied for the parameter Valuation that corresponds to the center point of the region */ - CenterViolated, /*!< the formula is violated for the parameter Valuation that corresponds to the center point of the region */ - ExistsBoth, /*!< the formula is satisfied for some parameters but also violated for others */ - AllSat, /*!< the formula is satisfied for all parameters in the given region */ - AllViolated /*!< the formula is violated for all parameters in the given region */ - }; - - std::ostream& operator<<(std::ostream& os, RegionCheckResult const& regionCheckResult); - } + /*! + * The results for a single Parameter Region + */ + enum class RegionResult { + Unknown, /*!< the result is unknown */ + ExistsSat, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */ + ExistsViolated, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */ + CenterSat, /*!< the formula is satisfied for the parameter Valuation that corresponds to the center point of the region */ + CenterViolated, /*!< the formula is violated for the parameter Valuation that corresponds to the center point of the region */ + ExistsBoth, /*!< the formula is satisfied for some parameters but also violated for others */ + AllSat, /*!< the formula is satisfied for all parameters in the given region */ + AllViolated /*!< the formula is violated for all parameters in the given region */ + }; + + std::ostream& operator<<(std::ostream& os, RegionResult const& regionCheckResult); } } diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 0a802b584..bdfd17f84 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -1,4 +1,5 @@ -#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h" +#include "storm-pars/utility/parameterlifting.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" @@ -17,265 +18,278 @@ namespace storm { namespace modelchecker { - namespace parametric { - - template - SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::make_unique>()) { + + template + SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::make_unique>()) { + } + + template + SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::move(solverFactory)) { + } + + template + bool SparseDtmcParameterLiftingModelChecker::canHandle(CheckTask 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..."); } + return result; + } + + template + void SparseDtmcParameterLiftingModelChecker::specifyBoundedUntilFormula(CheckTask const& checkTask) { - template - SparseDtmcParameterLiftingModelChecker::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::move(solverFactory)) { + // get the step bound + STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); + STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); + STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); + STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); + if (checkTask.getFormula().isUpperBoundStrict()) { + STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); + --(*stepBound); } + 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 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()); - template - bool SparseDtmcParameterLiftingModelChecker::canHandle(CheckTask const& checkTask) const { - return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true)); - } + // get the maybeStates + maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound); + maybeStates &= ~psiStates; - template - void SparseDtmcParameterLiftingModelChecker::specifyBoundedUntilFormula(CheckTask const& checkTask) { - - // get the step bound - STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); - STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); - stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); - if (checkTask.getFormula().isUpperBoundStrict()) { - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); - --(*stepBound); - } - 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 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 &= ~psiStates; - - // set the result for all non-maybe states - resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one()); - - // if there are maybestates, create the parameterLifter - if (!maybeStates.empty()) { - // Create the vector of one-step probabilities to go to target states. - std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); - } - - // We know some bounds for the results so set them - lowerResultBound = storm::utility::zero(); - upperResultBound = storm::utility::one(); - } - - template - void SparseDtmcParameterLiftingModelChecker::specifyUntilFormula(CheckTask const& checkTask) { - - // get the results for the subformulas - storm::modelchecker::SparsePropositionalModelChecker 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 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(this->parametricModel.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one()); + // set the result for all non-maybe states + resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one()); + + // if there are maybestates, create the parameterLifter + if (!maybeStates.empty()) { + // Create the vector of one-step probabilities to go to target states. + std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - // if there are maybestates, create the parameterLifter - if (!maybeStates.empty()) { - // Create the vector of one-step probabilities to go to target states. - std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); - } - - // We know some bounds for the results so set them - lowerResultBound = storm::utility::zero(); - upperResultBound = storm::utility::one(); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); } - - template - void SparseDtmcParameterLiftingModelChecker::specifyReachabilityRewardFormula(CheckTask const& checkTask) { - - // get the results for the subformula - storm::modelchecker::SparsePropositionalModelChecker 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); - infinityStates.complement(); - maybeStates = ~(targetStates | infinityStates); - - // set the result for all the non-maybe states - resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity()); - - // 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."); - - typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel(); + + // We know some bounds for the results so set them + lowerResultBound = storm::utility::zero(); + upperResultBound = storm::utility::one(); + } - std::vector b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); - - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); - } + template + void SparseDtmcParameterLiftingModelChecker::specifyUntilFormula(CheckTask const& checkTask) { + + // get the results for the subformulas + storm::modelchecker::SparsePropositionalModelChecker 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 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(this->parametricModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one()); + + // if there are maybestates, create the parameterLifter + if (!maybeStates.empty()) { + // Create the vector of one-step probabilities to go to target states. + std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - // We only know a lower bound for the result - lowerResultBound = storm::utility::zero(); - + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); } - - template - void SparseDtmcParameterLiftingModelChecker::specifyCumulativeRewardFormula(CheckTask const& checkTask) { - - // Obtain the stepBound - stepBound = checkTask.getFormula().getBound().evaluateAsInt(); - if (checkTask.getFormula().isBoundStrict()) { - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); - --(*stepBound); - } - 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(this->parametricModel.getNumberOfStates()); - + + // We know some bounds for the results so set them + lowerResultBound = storm::utility::zero(); + upperResultBound = storm::utility::one(); + } + + template + void SparseDtmcParameterLiftingModelChecker::specifyReachabilityRewardFormula(CheckTask const& checkTask) { + + // get the results for the subformula + storm::modelchecker::SparsePropositionalModelChecker 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); + infinityStates.complement(); + maybeStates = ~(targetStates | infinityStates); + + // set the result for all the non-maybe states + resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity()); + + // 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."); + typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel(); + std::vector b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); - - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); - - // We only know a lower bound for the result - lowerResultBound = storm::utility::zero(); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); } - template - std::unique_ptr SparseDtmcParameterLiftingModelChecker::computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { - - if(maybeStates.empty()) { - return std::make_unique>(resultsForNonMaybeStates); - } - - parameterLifter->specifyRegion(region, dirForParameters); - - // Set up the solver - auto solver = solverFactory->create(parameterLifter->getMatrix()); - if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { - STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration"); - auto* standardSolver = dynamic_cast*>(solver.get()); - auto settings = standardSolver->getSettings(); - settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); - standardSolver->setSettings(settings); - } - if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); - if (upperResultBound) solver->setUpperBound(upperResultBound.get()); - if (!stepBound) solver->setTrackScheduler(true); - if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setSchedulerHint(std::move(minSchedChoices.get())); - if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setSchedulerHint(std::move(maxSchedChoices.get())); - 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> termCond; - 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> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false); - } else { - // Terminate if the value for ALL relevant states is already above the threshold - termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true); - } - solver->setTerminationCondition(std::move(termCond)); - } - - // Invoke the solver - if(stepBound) { - assert(*stepBound > 0); - x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::zero()); - solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound); + // We only know a lower bound for the result + lowerResultBound = storm::utility::zero(); + + } + + template + void SparseDtmcParameterLiftingModelChecker::specifyCumulativeRewardFormula(CheckTask const& checkTask) { + + // Obtain the stepBound + stepBound = checkTask.getFormula().getBound().evaluateAsInt(); + if (checkTask.getFormula().isBoundStrict()) { + STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); + --(*stepBound); + } + 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(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 b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); + + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates); + + + // We only know a lower bound for the result + lowerResultBound = storm::utility::zero(); + } + + template + storm::modelchecker::SparseInstantiationModelChecker& SparseDtmcParameterLiftingModelChecker::getInstantiationChecker() { + if (!instantiationChecker) { + instantiationChecker = std::make_unique>(this->parametricModel); + instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType()); + } + return *instantiationChecker; + } + + template + std::unique_ptr SparseDtmcParameterLiftingModelChecker::computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + + if(maybeStates.empty()) { + return std::make_unique>(resultsForNonMaybeStates); + } + + parameterLifter->specifyRegion(region, dirForParameters); + + // Set up the solver + auto solver = solverFactory->create(parameterLifter->getMatrix()); + if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { + STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration"); + auto* standardSolver = dynamic_cast*>(solver.get()); + auto settings = standardSolver->getSettings(); + settings.setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); + standardSolver->setSettings(settings); + } + if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); + if (upperResultBound) solver->setUpperBound(upperResultBound.get()); + if (!stepBound) solver->setTrackScheduler(true); + if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setSchedulerHint(std::move(minSchedChoices.get())); + if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setSchedulerHint(std::move(maxSchedChoices.get())); + 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> termCond; + 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> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false); } else { - x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); - solver->solveEquations(dirForParameters, x, parameterLifter->getVector()); - if(storm::solver::minimize(dirForParameters)) { - minSchedChoices = solver->getSchedulerChoices(); - } else { - maxSchedChoices = solver->getSchedulerChoices(); - } + // Terminate if the value for ALL relevant states is already above the threshold + termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true); } - - // Get the result for the complete model (including maybestates) - std::vector result = resultsForNonMaybeStates; - auto maybeStateResIt = x.begin(); - for(auto const& maybeState : maybeStates) { - result[maybeState] = *maybeStateResIt; - ++maybeStateResIt; + solver->setTerminationCondition(std::move(termCond)); + } + + // Invoke the solver + if(stepBound) { + assert(*stepBound > 0); + x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound); + } else { + x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + solver->solveEquations(dirForParameters, x, parameterLifter->getVector()); + if(storm::solver::minimize(dirForParameters)) { + minSchedChoices = solver->getSchedulerChoices(); + } else { + maxSchedChoices = solver->getSchedulerChoices(); } - return std::make_unique>(std::move(result)); } - - template - void SparseDtmcParameterLiftingModelChecker::reset() { - maybeStates.resize(0); - resultsForNonMaybeStates.clear(); - stepBound = boost::none; - parameterLifter = nullptr; - minSchedChoices = boost::none; - maxSchedChoices = boost::none; - x.clear(); - lowerResultBound = boost::none; - upperResultBound = boost::none; + // Get the result for the complete model (including maybestates) + std::vector result = resultsForNonMaybeStates; + auto maybeStateResIt = x.begin(); + for(auto const& maybeState : maybeStates) { + result[maybeState] = *maybeStateResIt; + ++maybeStateResIt; + } + return std::make_unique>(std::move(result)); + } + + + template + void SparseDtmcParameterLiftingModelChecker::reset() { + maybeStates.resize(0); + resultsForNonMaybeStates.clear(); + stepBound = boost::none; + instantiationChecker = nullptr; + parameterLifter = nullptr; + minSchedChoices = boost::none; + maxSchedChoices = boost::none; + x.clear(); + lowerResultBound = boost::none; + upperResultBound = boost::none; + } + + template + boost::optional> SparseDtmcParameterLiftingModelChecker::getCurrentMinScheduler() { + if (!minSchedChoices) { + return boost::none; } - template - boost::optional> SparseDtmcParameterLiftingModelChecker::getCurrentMinScheduler() { - if (!minSchedChoices) { - return boost::none; - } - - storm::storage::Scheduler result(minSchedChoices->size()); - uint_fast64_t state = 0; - for (auto const& schedulerChoice : minSchedChoices.get()) { - result.setChoice(schedulerChoice, state); - ++state; - } - - return result; + storm::storage::Scheduler result(minSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : minSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; } - - template - boost::optional> SparseDtmcParameterLiftingModelChecker::getCurrentMaxScheduler() { - if (!maxSchedChoices) { - return boost::none; - } - - storm::storage::Scheduler result(maxSchedChoices->size()); - uint_fast64_t state = 0; - for (auto const& schedulerChoice : maxSchedChoices.get()) { - result.setChoice(schedulerChoice, state); - ++state; - } - - return result; + + return result; + } + + template + boost::optional> SparseDtmcParameterLiftingModelChecker::getCurrentMaxScheduler() { + if (!maxSchedChoices) { + return boost::none; } - template class SparseDtmcParameterLiftingModelChecker, double>; - template class SparseDtmcParameterLiftingModelChecker, storm::RationalNumber>; - + storm::storage::Scheduler result(maxSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : maxSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; } + + template class SparseDtmcParameterLiftingModelChecker, double>; + template class SparseDtmcParameterLiftingModelChecker, storm::RationalNumber>; + } } diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h index 73ee17fe7..8831bbe6b 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h @@ -4,53 +4,58 @@ #include #include -#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h" +#include "storm-pars/transformer/ParameterLifter.h" +#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h" #include "storm/storage/BitVector.h" #include "storm/storage/Scheduler.h" #include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/transformer/ParameterLifter.h" #include "storm/logic/FragmentSpecification.h" namespace storm { namespace modelchecker { - namespace parametric { - template - class SparseDtmcParameterLiftingModelChecker : public SparseParameterLiftingModelChecker { - public: - SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel); - SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory); + template + class SparseDtmcParameterLiftingModelChecker : public SparseParameterLiftingModelChecker { + public: + SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel); + SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory); - virtual bool canHandle(CheckTask const& checkTask) const override; + virtual bool canHandle(CheckTask const& checkTask) const override; - boost::optional> getCurrentMinScheduler(); - boost::optional> getCurrentMaxScheduler(); + boost::optional> getCurrentMinScheduler(); + boost::optional> getCurrentMaxScheduler(); - protected: + protected: - virtual void specifyBoundedUntilFormula(CheckTask const& checkTask) override; - virtual void specifyUntilFormula(CheckTask const& checkTask) override; - virtual void specifyReachabilityRewardFormula(CheckTask const& checkTask) override; - virtual void specifyCumulativeRewardFormula(CheckTask const& checkTask) override; + virtual void specifyBoundedUntilFormula(CheckTask const& checkTask) override; + virtual void specifyUntilFormula(CheckTask const& checkTask) override; + virtual void specifyReachabilityRewardFormula(CheckTask const& checkTask) override; + virtual void specifyCumulativeRewardFormula(CheckTask const& checkTask) override; + + virtual storm::modelchecker::SparseInstantiationModelChecker& getInstantiationChecker() override; + + virtual std::unique_ptr computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; - virtual std::unique_ptr computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; + virtual void reset() override; - virtual void reset() override; + private: + + + storm::storage::BitVector maybeStates; + std::vector resultsForNonMaybeStates; + boost::optional stepBound; - private: - storm::storage::BitVector maybeStates; - std::vector resultsForNonMaybeStates; - boost::optional stepBound; + std::unique_ptr> instantiationChecker; - std::unique_ptr> parameterLifter; - std::unique_ptr> solverFactory; + std::unique_ptr> parameterLifter; + std::unique_ptr> solverFactory; - // Results from the most recent solver call. - boost::optional> minSchedChoices, maxSchedChoices; - std::vector x; - boost::optional lowerResultBound, upperResultBound; - }; - } + // Results from the most recent solver call. + boost::optional> minSchedChoices, maxSchedChoices; + std::vector x; + boost::optional lowerResultBound, upperResultBound; + }; } } diff --git a/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp deleted file mode 100644 index b280bc046..000000000 --- a/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.cpp +++ /dev/null @@ -1,65 +0,0 @@ -#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h" - -#include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h" -#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h" -#include "storm/transformer/SparseParametricDtmcSimplifier.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/sparse/Dtmc.h" -#include "storm/utility/NumberTraits.h" - -namespace storm { - namespace modelchecker { - namespace parametric { - - template - SparseDtmcRegionChecker::SparseDtmcRegionChecker(SparseModelType const& parametricModel) : RegionChecker(parametricModel) { - // Intentionally left empty - } - - template - void SparseDtmcRegionChecker::simplifyParametricModel(CheckTask const& checkTask) { - storm::transformer::SparseParametricDtmcSimplifier simplifier(this->parametricModel); - if(simplifier.simplify(checkTask.getFormula())) { - this->simplifiedModel = simplifier.getSimplifiedModel(); - this->currentFormula = simplifier.getSimplifiedFormula(); - } else { - this->simplifiedModel = nullptr; - this->currentFormula = checkTask.getFormula().asSharedPointer(); - } - } - - template - void SparseDtmcRegionChecker::initializeUnderlyingCheckers() { - if (this->settings.applyExactValidation) { - STORM_LOG_WARN_COND(!storm::NumberTraits::IsExact, "Exact validation is not necessarry if the original computation is already exact"); - this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); - } - this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); - this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); - this->instantiationChecker->setInstantiationsAreGraphPreserving(true); - } - - template - void SparseDtmcRegionChecker::applyHintsToExactChecker() { - auto dtmcPLChecker = dynamic_cast*>(this->parameterLiftingChecker.get()); - STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type"); - auto exactDtmcPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); - STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type"); - if (dtmcPLChecker->getCurrentMaxScheduler()) { - exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler()->template toValueType(); - } - if (dtmcPLChecker->getCurrentMinScheduler()) { - exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler()->template toValueType(); - } - } - -#ifdef STORM_HAVE_CARL - template class SparseDtmcRegionChecker, double, storm::RationalNumber>; - template class SparseDtmcRegionChecker, storm::RationalNumber>; -#endif - } // namespace parametric - } //namespace modelchecker -} //namespace storm - diff --git a/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h deleted file mode 100644 index 561594d2e..000000000 --- a/src/storm-pars/modelchecker/region/SparseDtmcRegionChecker.h +++ /dev/null @@ -1,27 +0,0 @@ -#pragma once - -#include - -#include "storm/modelchecker/parametric/RegionChecker.h" - -namespace storm { - namespace modelchecker{ - namespace parametric{ - - - template - class SparseDtmcRegionChecker : public RegionChecker { - - public: - SparseDtmcRegionChecker(SparseModelType const& parametricModel); - - protected: - virtual void simplifyParametricModel(CheckTask const& checkTask) override; - virtual void initializeUnderlyingCheckers() override; - virtual void applyHintsToExactChecker() override; - - }; - - } //namespace parametric - } //namespace modelchecker -} //namespace storm diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 7b8df081a..f2c6bb21b 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -1,4 +1,5 @@ -#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h" +#include "storm-pars/utility/parameterlifting.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" @@ -18,331 +19,343 @@ namespace storm { namespace modelchecker { - namespace parametric { - - template - SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::make_unique>()) { + template + SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::make_unique>()) { + } + + template + SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::move(solverFactory)) { + } + + template + bool SparseMdpParameterLiftingModelChecker::canHandle(CheckTask 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..."); } + return result; + + } + + template + void SparseMdpParameterLiftingModelChecker::specifyBoundedUntilFormula(CheckTask const& checkTask) { - template - SparseMdpParameterLiftingModelChecker::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory) : SparseParameterLiftingModelChecker(parametricModel), solverFactory(std::move(solverFactory)) { + // get the step bound + STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); + STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); + STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); + stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); + STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); + if (checkTask.getFormula().isUpperBoundStrict()) { + STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); + --(*stepBound); } - - template - bool SparseMdpParameterLiftingModelChecker::canHandle(CheckTask const& checkTask) const { - return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true)); - } - - template - void SparseMdpParameterLiftingModelChecker::specifyBoundedUntilFormula(CheckTask const& checkTask) { - - // get the step bound - STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); - STORM_LOG_THROW(checkTask.getFormula().hasUpperBound(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(checkTask.getFormula().isStepBounded(), storm::exceptions::NotSupportedException, "Expected a bounded until formula with step bounds."); - stepBound = checkTask.getFormula().getUpperBound().evaluateAsInt(); - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); - if (checkTask.getFormula().isUpperBoundStrict()) { - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); - --(*stepBound); - } - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive."); + 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 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); - maybeStates &= ~psiStates; - - // set the result for all non-maybe states - resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one()); + // get the results for the subformulas + storm::modelchecker::SparsePropositionalModelChecker 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); + maybeStates &= ~psiStates; + + // set the result for all non-maybe states + resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one()); + + // if there are maybestates, create the parameterLifter + if (!maybeStates.empty()) { + // Create the vector of one-step probabilities to go to target states. + std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - // if there are maybestates, create the parameterLifter - if (!maybeStates.empty()) { - // Create the vector of one-step probabilities to go to target states. - std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); - computePlayer1Matrix(); - - applyPreviousResultAsHint = false; - } + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); + computePlayer1Matrix(); - // We know some bounds for the results - lowerResultBound = storm::utility::zero(); - upperResultBound = storm::utility::one(); + applyPreviousResultAsHint = false; } - - template - void SparseMdpParameterLiftingModelChecker::specifyUntilFormula(CheckTask const& checkTask) { - - // get the results for the subformulas - storm::modelchecker::SparsePropositionalModelChecker 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 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); - maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); + + // We know some bounds for the results + lowerResultBound = storm::utility::zero(); + upperResultBound = storm::utility::one(); + } + + template + void SparseMdpParameterLiftingModelChecker::specifyUntilFormula(CheckTask const& checkTask) { + + // get the results for the subformulas + storm::modelchecker::SparsePropositionalModelChecker 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 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); + maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); + + // set the result for all non-maybe states + resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one()); + + // if there are maybestates, create the parameterLifter + if (!maybeStates.empty()) { + // Create the vector of one-step probabilities to go to target states. + std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second); - // set the result for all non-maybe states - resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one()); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); + computePlayer1Matrix(); - // if there are maybestates, create the parameterLifter - if (!maybeStates.empty()) { - // Create the vector of one-step probabilities to go to target states. - std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second); - - parameterLifter = std::make_unique>(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(); - } - - // We know some bounds for the results - lowerResultBound = storm::utility::zero(); - upperResultBound = storm::utility::one(); + // 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(); } - - template - void SparseMdpParameterLiftingModelChecker::specifyReachabilityRewardFormula(CheckTask const& checkTask) { - - // get the results for the subformula - storm::modelchecker::SparsePropositionalModelChecker 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()); + + // We know some bounds for the results + lowerResultBound = storm::utility::zero(); + upperResultBound = storm::utility::one(); + } + + template + void SparseMdpParameterLiftingModelChecker::specifyReachabilityRewardFormula(CheckTask const& checkTask) { + + // get the results for the subformula + storm::modelchecker::SparsePropositionalModelChecker 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); + infinityStates.complement(); + maybeStates = ~(targetStates | infinityStates); + + // set the result for all the non-maybe states + resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity()); + + // 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."); + + typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel(); + + std::vector b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); - // 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); - infinityStates.complement(); - maybeStates = ~(targetStates | infinityStates); + // 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); - // set the result for all the non-maybe states - resultsForNonMaybeStates = std::vector(this->parametricModel.getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity()); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates); + computePlayer1Matrix(); - // 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."); - - typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel(); + // 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(); + } + + // We only know a lower bound for the result + lowerResultBound = storm::utility::zero(); - std::vector 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); - - parameterLifter = std::make_unique>(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(); - } - - // We only know a lower bound for the result - lowerResultBound = storm::utility::zero(); + } + template + void SparseMdpParameterLiftingModelChecker::specifyCumulativeRewardFormula(CheckTask const& checkTask) { + + // Obtain the stepBound + stepBound = checkTask.getFormula().getBound().evaluateAsInt(); + if (checkTask.getFormula().isBoundStrict()) { + STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); + --(*stepBound); } - - template - void SparseMdpParameterLiftingModelChecker::specifyCumulativeRewardFormula(CheckTask const& checkTask) { - - // Obtain the stepBound - stepBound = checkTask.getFormula().getBound().evaluateAsInt(); - if (checkTask.getFormula().isBoundStrict()) { - STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Expected a strict upper step bound that is greater than zero."); - --(*stepBound); - } - 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(this->parametricModel.getNumberOfStates()); + 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(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 b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); - - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates); - computePlayer1Matrix(); + // 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 b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); + + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates); + computePlayer1Matrix(); - applyPreviousResultAsHint = false; - - // We only know a lower bound for the result - lowerResultBound = storm::utility::zero(); + applyPreviousResultAsHint = false; + + // We only know a lower bound for the result + lowerResultBound = storm::utility::zero(); + } + + template + storm::modelchecker::SparseInstantiationModelChecker& SparseMdpParameterLiftingModelChecker::getInstantiationChecker() { + if (!instantiationChecker) { + instantiationChecker = std::make_unique>(this->parametricModel); + instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType()); } + return *instantiationChecker; + } + + template + std::unique_ptr SparseMdpParameterLiftingModelChecker::computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { - template - std::unique_ptr SparseMdpParameterLiftingModelChecker::computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { - - if(maybeStates.empty()) { - return std::make_unique>(resultsForNonMaybeStates); - } - - parameterLifter->specifyRegion(region, dirForParameters); - - // Set up the solver - auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix()); - if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { - STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration"); - auto* standardSolver = dynamic_cast*>(solver.get()); - auto settings = standardSolver->getSettings(); - settings.setSolutionMethod(storm::solver::StandardGameSolverSettings::SolutionMethod::PolicyIteration); - standardSolver->setSettings(settings); - } - if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); - if (upperResultBound) solver->setUpperBound(upperResultBound.get()); - if (applyPreviousResultAsHint) { - solver->setTrackSchedulers(true); - x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); - if(storm::solver::minimize(dirForParameters) && minSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(minSchedChoices.get())); - if(storm::solver::maximize(dirForParameters) && maxSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(maxSchedChoices.get())); + if(maybeStates.empty()) { + return std::make_unique>(resultsForNonMaybeStates); + } + + parameterLifter->specifyRegion(region, dirForParameters); + + // Set up the solver + auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix()); + if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { + STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration"); + auto* standardSolver = dynamic_cast*>(solver.get()); + auto settings = standardSolver->getSettings(); + settings.setSolutionMethod(storm::solver::StandardGameSolverSettings::SolutionMethod::PolicyIteration); + standardSolver->setSettings(settings); + } + if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); + if (upperResultBound) solver->setUpperBound(upperResultBound.get()); + if (applyPreviousResultAsHint) { + solver->setTrackSchedulers(true); + x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + if(storm::solver::minimize(dirForParameters) && minSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(minSchedChoices.get())); + if(storm::solver::maximize(dirForParameters) && maxSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(maxSchedChoices.get())); + } else { + x.assign(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + } + 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> termCond; + 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> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false); } else { - x.assign(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + // Terminate if the value for ALL relevant states is already above the threshold + termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true); } - 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> termCond; - 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> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false); + solver->setTerminationCondition(std::move(termCond)); + } + + // Invoke the solver + if(stepBound) { + assert(*stepBound > 0); + solver->repeatedMultiply(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, ¶meterLifter->getVector(), *stepBound); + } else { + solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector()); + if(applyPreviousResultAsHint) { + if(storm::solver::minimize(dirForParameters)) { + minSchedChoices = solver->getPlayer2SchedulerChoices(); } else { - // Terminate if the value for ALL relevant states is already above the threshold - termCond = std::make_unique> (relevantStatesInSubsystem, true, this->currentCheckTask->getBoundThreshold(), true); - } - solver->setTerminationCondition(std::move(termCond)); - } - - // Invoke the solver - if(stepBound) { - assert(*stepBound > 0); - solver->repeatedMultiply(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, ¶meterLifter->getVector(), *stepBound); - } else { - solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector()); - if(applyPreviousResultAsHint) { - if(storm::solver::minimize(dirForParameters)) { - minSchedChoices = solver->getPlayer2SchedulerChoices(); - } else { - maxSchedChoices = solver->getPlayer2SchedulerChoices(); - } - player1SchedChoices = solver->getPlayer1SchedulerChoices(); + maxSchedChoices = solver->getPlayer2SchedulerChoices(); } + player1SchedChoices = solver->getPlayer1SchedulerChoices(); } - - // Get the result for the complete model (including maybestates) - std::vector result = resultsForNonMaybeStates; - auto maybeStateResIt = x.begin(); - for(auto const& maybeState : maybeStates) { - result[maybeState] = *maybeStateResIt; - ++maybeStateResIt; - } - return std::make_unique>(std::move(result)); } - template - void SparseMdpParameterLiftingModelChecker::computePlayer1Matrix() { - uint_fast64_t n = 0; - for(auto const& maybeState : maybeStates) { - 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 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){ - matrixBuilder.addNextValue(p1MatrixRow, p1MatrixRow, storm::utility::one()); - ++p1MatrixRow; - } + // Get the result for the complete model (including maybestates) + std::vector result = resultsForNonMaybeStates; + auto maybeStateResIt = x.begin(); + for(auto const& maybeState : maybeStates) { + result[maybeState] = *maybeStateResIt; + ++maybeStateResIt; + } + return std::make_unique>(std::move(result)); + } + + template + void SparseMdpParameterLiftingModelChecker::computePlayer1Matrix() { + uint_fast64_t n = 0; + for(auto const& maybeState : maybeStates) { + 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 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){ + matrixBuilder.addNextValue(p1MatrixRow, p1MatrixRow, storm::utility::one()); + ++p1MatrixRow; } - player1Matrix = matrixBuilder.build(); } - - template - void SparseMdpParameterLiftingModelChecker::reset() { - maybeStates.resize(0); - resultsForNonMaybeStates.clear(); - stepBound = boost::none; - player1Matrix = storm::storage::SparseMatrix(); - parameterLifter = nullptr; - minSchedChoices = boost::none; - maxSchedChoices = boost::none; - x.clear(); - lowerResultBound = boost::none; - upperResultBound = boost::none; - applyPreviousResultAsHint = false; + player1Matrix = matrixBuilder.build(); + } + + template + void SparseMdpParameterLiftingModelChecker::reset() { + maybeStates.resize(0); + resultsForNonMaybeStates.clear(); + stepBound = boost::none; + instantiationChecker = nullptr; + player1Matrix = storm::storage::SparseMatrix(); + parameterLifter = nullptr; + minSchedChoices = boost::none; + maxSchedChoices = boost::none; + x.clear(); + lowerResultBound = boost::none; + upperResultBound = boost::none; + applyPreviousResultAsHint = false; + } + + template + boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentMinScheduler() { + if (!minSchedChoices) { + return boost::none; } - template - boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentMinScheduler() { - if (!minSchedChoices) { - return boost::none; - } - - storm::storage::Scheduler result(minSchedChoices->size()); - uint_fast64_t state = 0; - for (auto const& schedulerChoice : minSchedChoices.get()) { - result.setChoice(schedulerChoice, state); - ++state; - } - - return result; + storm::storage::Scheduler result(minSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : minSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; } - - template - boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentMaxScheduler() { - if (!maxSchedChoices) { - return boost::none; - } - - storm::storage::Scheduler result(maxSchedChoices->size()); - uint_fast64_t state = 0; - for (auto const& schedulerChoice : maxSchedChoices.get()) { - result.setChoice(schedulerChoice, state); - ++state; - } - - return result; + + return result; + } + + template + boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentMaxScheduler() { + if (!maxSchedChoices) { + return boost::none; } - template - boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentPlayer1Scheduler() { - if (!player1SchedChoices) { - return boost::none; - } - - storm::storage::Scheduler result(player1SchedChoices->size()); - uint_fast64_t state = 0; - for (auto const& schedulerChoice : player1SchedChoices.get()) { - result.setChoice(schedulerChoice, state); - ++state; - } - - return result; + storm::storage::Scheduler result(maxSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : maxSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; } - - template class SparseMdpParameterLiftingModelChecker, double>; - template class SparseMdpParameterLiftingModelChecker, storm::RationalNumber>; + + return result; } + + template + boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentPlayer1Scheduler() { + if (!player1SchedChoices) { + return boost::none; + } + + storm::storage::Scheduler result(player1SchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : player1SchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; + } + + template class SparseMdpParameterLiftingModelChecker, double>; + template class SparseMdpParameterLiftingModelChecker, storm::RationalNumber>; } } diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h index 4e0b6e068..55504bd9e 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h @@ -4,60 +4,64 @@ #include #include -#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h" +#include "storm-pars/transformer/ParameterLifter.h" +#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h" + #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/sparse/StateType.h" #include "storm/solver/GameSolver.h" -#include "storm/transformer/ParameterLifter.h" #include "storm/storage/Scheduler.h" namespace storm { namespace modelchecker { - namespace parametric { - - template - class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker { - public: - SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel); - SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory); + + template + class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker { + public: + SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel); + SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr>&& solverFactory); - virtual bool canHandle(CheckTask const& checkTask) const override; + virtual bool canHandle(CheckTask const& checkTask) const override; - boost::optional> getCurrentMinScheduler(); - boost::optional> getCurrentMaxScheduler(); - boost::optional> getCurrentPlayer1Scheduler(); + boost::optional> getCurrentMinScheduler(); + boost::optional> getCurrentMaxScheduler(); + boost::optional> getCurrentPlayer1Scheduler(); - protected: + protected: - virtual void specifyBoundedUntilFormula(CheckTask const& checkTask) override; - virtual void specifyUntilFormula(CheckTask const& checkTask) override; - virtual void specifyReachabilityRewardFormula(CheckTask const& checkTask) override; - virtual void specifyCumulativeRewardFormula(CheckTask const& checkTask) override; + virtual void specifyBoundedUntilFormula(CheckTask const& checkTask) override; + virtual void specifyUntilFormula(CheckTask const& checkTask) override; + virtual void specifyReachabilityRewardFormula(CheckTask const& checkTask) override; + virtual void specifyCumulativeRewardFormula(CheckTask const& checkTask) override; - virtual std::unique_ptr computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; + virtual storm::modelchecker::SparseInstantiationModelChecker& getInstantiationChecker() override; + + virtual std::unique_ptr computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) override; - virtual void reset() override; + virtual void reset() override; - private: - void computePlayer1Matrix(); - - storm::storage::BitVector maybeStates; - std::vector resultsForNonMaybeStates; - boost::optional stepBound; - - storm::storage::SparseMatrix player1Matrix; - std::unique_ptr> parameterLifter; - std::unique_ptr> solverFactory; - - // Results from the most recent solver call. - boost::optional> minSchedChoices, maxSchedChoices; - boost::optional> player1SchedChoices; - std::vector x; - boost::optional lowerResultBound, upperResultBound; - bool applyPreviousResultAsHint; - }; - } + private: + void computePlayer1Matrix(); + + storm::storage::BitVector maybeStates; + std::vector resultsForNonMaybeStates; + boost::optional stepBound; + + std::unique_ptr> instantiationChecker; + + storm::storage::SparseMatrix player1Matrix; + std::unique_ptr> parameterLifter; + std::unique_ptr> solverFactory; + + // Results from the most recent solver call. + boost::optional> minSchedChoices, maxSchedChoices; + boost::optional> player1SchedChoices; + std::vector x; + boost::optional lowerResultBound, upperResultBound; + bool applyPreviousResultAsHint; + }; } } diff --git a/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp deleted file mode 100644 index 9ffa707fa..000000000 --- a/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.cpp +++ /dev/null @@ -1,70 +0,0 @@ -#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h" - -#include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h" -#include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h" -#include "storm/transformer/SparseParametricMdpSimplifier.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/sparse/Mdp.h" -#include "storm/utility/NumberTraits.h" - - -namespace storm { - namespace modelchecker { - namespace parametric { - - template - SparseMdpRegionChecker::SparseMdpRegionChecker(SparseModelType const& parametricModel) : RegionChecker(parametricModel) { - // Intentionally left empty - } - - template - void SparseMdpRegionChecker::simplifyParametricModel(CheckTask const& checkTask) { - storm::transformer::SparseParametricMdpSimplifier simplifier(this->parametricModel); - if(simplifier.simplify(checkTask.getFormula())) { - this->simplifiedModel = simplifier.getSimplifiedModel(); - this->currentFormula = simplifier.getSimplifiedFormula(); - } else { - this->simplifiedModel = nullptr; - this->currentFormula = checkTask.getFormula().asSharedPointer(); - } - } - - template - void SparseMdpRegionChecker::initializeUnderlyingCheckers() { - if (this->settings.applyExactValidation) { - STORM_LOG_WARN_COND(!storm::NumberTraits::IsExact, "Exact validation is not necessarry if the original computation is already exact"); - this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); - } - this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); - this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); - this->instantiationChecker->setInstantiationsAreGraphPreserving(true); - } - - template - void SparseMdpRegionChecker::applyHintsToExactChecker() { - auto MdpPLChecker = dynamic_cast*>(this->parameterLiftingChecker.get()); - STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type"); - auto exactMdpPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); - STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type"); - if (MdpPLChecker->getCurrentMaxScheduler()) { - exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler()->template toValueType(); - } - if (MdpPLChecker->getCurrentMinScheduler()) { - exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler()->template toValueType(); - } - if (MdpPLChecker->getCurrentPlayer1Scheduler()) { - exactMdpPLChecker->getCurrentPlayer1Scheduler() = MdpPLChecker->getCurrentPlayer1Scheduler()->template toValueType(); - } - } - - -#ifdef STORM_HAVE_CARL - template class SparseMdpRegionChecker, double, storm::RationalNumber>; - template class SparseMdpRegionChecker, storm::RationalNumber>; -#endif - } // namespace parametric - } //namespace modelchecker -} //namespace storm - diff --git a/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h b/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h deleted file mode 100644 index 72c355eee..000000000 --- a/src/storm-pars/modelchecker/region/SparseMdpRegionChecker.h +++ /dev/null @@ -1,28 +0,0 @@ -#pragma once - -#include - -#include "storm/modelchecker/parametric/RegionChecker.h" - -namespace storm { - namespace modelchecker{ - namespace parametric{ - - - template - class SparseMdpRegionChecker : public RegionChecker { - - public: - SparseMdpRegionChecker(SparseModelType const& parametricModel); - - protected: - - virtual void initializeUnderlyingCheckers() override; - virtual void simplifyParametricModel(CheckTask const& checkTask) override; - virtual void applyHintsToExactChecker() override; - - }; - - } //namespace parametric - } //namespace modelchecker -} //namespace storm diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index 8c9af8957..544dd734d 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -13,82 +13,130 @@ namespace storm { namespace modelchecker { - namespace parametric { + + template + SparseParameterLiftingModelChecker::SparseParameterLiftingModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) { + //Intentionally left empty + } + + template + void SparseParameterLiftingModelChecker::specifyFormula(storm::modelchecker::CheckTask 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>(checkTask.substituteFormula(*currentFormula).template convertValueType()); - template - SparseParameterLiftingModelChecker::SparseParameterLiftingModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) { - //Intentionally left empty + if(currentCheckTask->getFormula().isProbabilityOperatorFormula()) { + auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula(); + if(probOpFormula.getSubformula().isBoundedUntilFormula()) { + specifyBoundedUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula())); + } else if(probOpFormula.getSubformula().isUntilFormula()) { + specifyUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula())); + } else if (probOpFormula.getSubformula().isEventuallyFormula()) { + specifyReachabilityProbabilityFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula())); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); + } + } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) { + auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula(); + if(rewOpFormula.getSubformula().isEventuallyFormula()) { + specifyReachabilityRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula())); + } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) { + specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula())); + } } + } + + template + RegionResult SparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + + 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."); - template - void SparseParameterLiftingModelChecker::specifyFormula(storm::modelchecker::CheckTask const& checkTask) { - reset(); - currentFormula = checkTask.getFormula().asSharedPointer(); - currentCheckTask = std::make_unique>(checkTask.substituteFormula(*currentFormula).template convertValueType()); - - if(currentCheckTask->getFormula().isProbabilityOperatorFormula()) { - auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula(); - if(probOpFormula.getSubformula().isBoundedUntilFormula()) { - specifyBoundedUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula())); - } else if(probOpFormula.getSubformula().isUntilFormula()) { - specifyUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula())); - } else if (probOpFormula.getSubformula().isEventuallyFormula()) { - specifyReachabilityProbabilityFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula())); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); - } - } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) { - auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula(); - if(rewOpFormula.getSubformula().isEventuallyFormula()) { - specifyReachabilityRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula())); - } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) { - specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula())); - } - } + 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; } - template - std::unique_ptr SparseParameterLiftingModelChecker::check(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { - auto quantitativeResult = computeQuantitativeValues(region, dirForParameters); - if(currentCheckTask->getFormula().hasQuantitativeResult()) { - return quantitativeResult; - } else { - return quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + // 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()]) { + 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; + } + } } + } 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()]) { + result = RegionResult::AllViolated; + } else if (sampleVerticesOfRegion) { + // 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; + } + } + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult); } - - template - void SparseParameterLiftingModelChecker::specifyBoundedUntilFormula(CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); - } - - template - void SparseParameterLiftingModelChecker::specifyUntilFormula(CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); - } - - template - void SparseParameterLiftingModelChecker::specifyReachabilityProbabilityFormula(CheckTask const& checkTask) { - // transform to until formula - auto untilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer()); - specifyUntilFormula(currentCheckTask->substituteFormula(*untilFormula)); - } - - template - void SparseParameterLiftingModelChecker::specifyReachabilityRewardFormula(CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); - } - - template - void SparseParameterLiftingModelChecker::specifyCumulativeRewardFormula(CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); + return result; + } + + template + std::unique_ptr SparseParameterLiftingModelChecker::check(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) { + auto quantitativeResult = computeQuantitativeValues(region, dirForParameters); + if(currentCheckTask->getFormula().hasQuantitativeResult()) { + return quantitativeResult; + } else { + return quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); } - - template class SparseParameterLiftingModelChecker, double>; - template class SparseParameterLiftingModelChecker, double>; - template class SparseParameterLiftingModelChecker, storm::RationalNumber>; - template class SparseParameterLiftingModelChecker, storm::RationalNumber>; + } + + template + void SparseParameterLiftingModelChecker::specifyBoundedUntilFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); + } + template + void SparseParameterLiftingModelChecker::specifyUntilFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); } + + template + void SparseParameterLiftingModelChecker::specifyReachabilityProbabilityFormula(CheckTask const& checkTask) { + // transform to until formula + auto untilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer()); + specifyUntilFormula(currentCheckTask->substituteFormula(*untilFormula)); + } + + template + void SparseParameterLiftingModelChecker::specifyReachabilityRewardFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); + } + + template + void SparseParameterLiftingModelChecker::specifyCumulativeRewardFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property."); + } + + template class SparseParameterLiftingModelChecker, double>; + template class SparseParameterLiftingModelChecker, double>; + template class SparseParameterLiftingModelChecker, storm::RationalNumber>; + template class SparseParameterLiftingModelChecker, storm::RationalNumber>; + } } diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h index c71d0d25d..ea53dd803 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h @@ -1,60 +1,74 @@ #pragma once +#include "storm-pars/modelchecker/region/RegionModelChecker.h" +#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h" +#include "storm-pars/storage/ParameterRegion.h" +#include "storm-pars/utility/parametric.h" + #include "storm/logic/Formulas.h" #include "storm/modelchecker/CheckTask.h" #include "storm/modelchecker/results/CheckResult.h" -#include "storm/storage/ParameterRegion.h" #include "storm/solver/OptimizationDirection.h" -#include "storm/utility/parametric.h" namespace storm { namespace modelchecker { - namespace parametric { + /*! + * Class to approximatively check a formula on a parametric model for all parameter valuations within a region + * It is assumed that all considered valuations are graph-preserving and well defined, i.e., + * * all non-const transition probabilities evaluate to some non-zero value + * * the sum of all outgoing transitions is one + */ + template + class SparseParameterLiftingModelChecker : public RegionModelChecker { + public: + SparseParameterLiftingModelChecker(SparseModelType const& parametricModel); + virtual ~SparseParameterLiftingModelChecker() = default; + + virtual void specifyFormula(CheckTask const& checkTask) override; + /*! - * Class to approximatively check a formula on a parametric model for all parameter valuations within a region - * It is assumed that all considered valuations are graph-preserving and well defined, i.e., - * * all non-const transition probabilities evaluate to some non-zero value - * * the sum of all outgoing transitions is one + * Analyzes the given region by means of parameter lifting. + * We first check whether there is one point in the region for which the property is satisfied/violated. + * If the given initialResults already indicates that there is such a point, this step is skipped. + * Then, we check whether ALL points in the region violate/satisfy the property + * */ - template - class SparseParameterLiftingModelChecker { - public: - SparseParameterLiftingModelChecker(SparseModelType const& parametricModel); - virtual ~SparseParameterLiftingModelChecker() = default; - - virtual bool canHandle(CheckTask const& checkTask) const = 0; - - void specifyFormula(CheckTask const& checkTask); - - /*! - * 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. - - * @param region the region on which parameter lifting is applied - * @param dirForParameters The optimization direction for the parameter choices. If this is, e.g., minimize, then the returned result will be a lower bound for all results induced by the parameter evaluations inside the region. - */ - std::unique_ptr check(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); - - protected: - - virtual void specifyBoundedUntilFormula(CheckTask const& checkTask); - virtual void specifyUntilFormula(CheckTask const& checkTask); - virtual void specifyReachabilityProbabilityFormula(CheckTask const& checkTask); - virtual void specifyReachabilityRewardFormula(CheckTask const& checkTask); - virtual void specifyCumulativeRewardFormula(CheckTask const& checkTask); - - virtual std::unique_ptr computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0; - - virtual void reset() = 0; - - SparseModelType const& parametricModel; - std::unique_ptr> currentCheckTask; - - private: - // store the current formula. Note that currentCheckTask only stores a reference to the formula. - std::shared_ptr currentFormula; - }; - } + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; + + /*! + * 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. + + * @param region the region on which parameter lifting is applied + * @param dirForParameters The optimization direction for the parameter choices. If this is, e.g., minimize, then the returned result will be a lower bound for all results induced by the parameter evaluations inside the region. + */ + std::unique_ptr check(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters); + + protected: + + // Resets all data that correspond to the currently defined property. + virtual void reset() = 0; + + virtual void specifyBoundedUntilFormula(CheckTask const& checkTask); + virtual void specifyUntilFormula(CheckTask const& checkTask); + virtual void specifyReachabilityProbabilityFormula(CheckTask const& checkTask); + virtual void specifyReachabilityRewardFormula(CheckTask const& checkTask); + virtual void specifyCumulativeRewardFormula(CheckTask const& checkTask); + + + virtual storm::modelchecker::SparseInstantiationModelChecker& getInstantiationChecker() = 0; + + virtual std::unique_ptr computeQuantitativeValues(storm::storage::ParameterRegion const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0; + + + SparseModelType const& parametricModel; + std::unique_ptr> currentCheckTask; + + private: + // store the current formula. Note that currentCheckTask only stores a reference to the formula. + std::shared_ptr currentFormula; + + }; } } diff --git a/src/storm-pars/modelchecker/results/RegionCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionCheckResult.cpp new file mode 100644 index 000000000..b561a67ab --- /dev/null +++ b/src/storm-pars/modelchecker/results/RegionCheckResult.cpp @@ -0,0 +1,112 @@ +#include "storm-pars/modelchecker/results/RegionCheckResult.h" + +#include + +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { + namespace modelchecker { + + template + RegionCheckResult::RegionCheckResult(std::vector, storm::modelchecker::RegionResult>> const& regionResults) : regionResults(regionResults) { + auto overallArea = storm::utility::zero::CoefficientType>(); + for (auto const& res : this->regionResults) { + overallArea += res.first.area(); + } + initFractions(overallArea); + } + + template + RegionCheckResult::RegionCheckResult(std::vector, storm::modelchecker::RegionResult>>&& regionResults) : regionResults(std::move(regionResults)) { + auto overallArea = storm::utility::zero::CoefficientType>(); + for (auto const& res : this->regionResults) { + overallArea += res.first.area(); + } + initFractions(overallArea); + } + + template + bool RegionCheckResult::isRegionCheckResult() const { + return true; + } + + template + bool RegionCheckResult::isRegionRefinementCheckResult() const { + return false; + } + + template + std::vector, storm::modelchecker::RegionResult>> const& RegionCheckResult::getRegionResults() const { + return regionResults; + } + + template + typename storm::storage::ParameterRegion::CoefficientType const& RegionCheckResult::getSatFraction() const { + return satFraction; + } + + template + typename storm::storage::ParameterRegion::CoefficientType const& RegionCheckResult::getUnsatFraction() const { + return unsatFraction; + } + + template + std::ostream& RegionCheckResult::writeToStream(std::ostream& out) const { + writeCondensedToStream(out); + out << std::endl << "Region results: " << std::endl; + for (auto const& res : this->regionResults) { + out << res.first.toString() << ": \t" << res.second << std::endl; + } + } + + template + std::ostream& RegionCheckResult::writeCondensedToStream(std::ostream& out) const { + auto oneHundred = storm::utility::convertNumber::CoefficientType>(100.0); + auto one = storm::utility::convertNumber::CoefficientType>(1.0); + out << "Fraction of satisfied area: " << (satFraction * oneHundred) << std::endl; + out << "Fraction of unsatisfied area: " << (unsatFraction * oneHundred) << std::endl; + out << "Unknown fraction: " << ((one - satFraction - unsatFraction) * oneHundred) << std::endl; + out << "Total Number of regions: " << regionResults.size() << std::endl; + std::map counters; + for (auto const& res : this->regionResults) { + ++counters[res.second]; + } + for (auto const& counter : counters) { + out << std::setw(28) << counter.first << ": " << counter.second << std::endl; + } + } + + template + std::ostream& RegionCheckResult::writeIllustrationToStream(std::ostream& out) const { + STORM_LOG_WARN("Writing illustration of region check result to a stream is not implemented."); + } + + template + void RegionCheckResult::initFractions(typename storm::storage::ParameterRegion::CoefficientType const& overallArea) { + auto satArea = storm::utility::zero::CoefficientType>(); + auto unsatArea = storm::utility::zero::CoefficientType>(); + for (auto const& res : this->regionResults) { + if (res.second == storm::modelchecker::RegionResult::AllSat) { + satArea += res.first.area(); + } else if (res.second == storm::modelchecker::RegionResult::AllViolated) { + unsatArea += res.first.area(); + } + } + satFraction = satArea / overallArea; + unsatFraction = unsatArea / overallArea; + } + + template + void RegionCheckResult::filter(QualitativeCheckResult const& filter) { + // Filtering has no effect as we only store the result w.r.t. a single state anyway. + // Hence, this is intentionally left empty. + } + + +#ifdef STORM_HAVE_CARL + template class RegionCheckResult; +#endif + } +} diff --git a/src/storm-pars/modelchecker/results/RegionCheckResult.h b/src/storm-pars/modelchecker/results/RegionCheckResult.h new file mode 100644 index 000000000..7bb144cf6 --- /dev/null +++ b/src/storm-pars/modelchecker/results/RegionCheckResult.h @@ -0,0 +1,40 @@ +#pragma once + +#include + +#include "storm/modelchecker/results/CheckResult.h" +#include "storm-pars/modelchecker/region/RegionResult.h" +#include "storm-pars/storage/ParameterRegion.h" + +namespace storm { + namespace modelchecker { + template + class RegionCheckResult : public CheckResult { + public: + + RegionCheckResult(std::vector, storm::modelchecker::RegionResult>> const& regionResults); + RegionCheckResult(std::vector, storm::modelchecker::RegionResult>>&& regionResults); + virtual ~RegionCheckResult() = default; + + virtual bool isRegionCheckResult() const; + virtual bool isRegionRefinementCheckResult() const; + + std::vector, storm::modelchecker::RegionResult>> const& getRegionResults() const; + typename storm::storage::ParameterRegion::CoefficientType const& getSatFraction() const; + typename storm::storage::ParameterRegion::CoefficientType const& getUnsatFraction() const; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + virtual std::ostream& writeCondensedToStream(std::ostream& out) const; + virtual std::ostream& writeIllustrationToStream(std::ostream& out) const; + + virtual void filter(QualitativeCheckResult const& filter) override; + + protected: + virtual void initFractions(typename storm::storage::ParameterRegion::CoefficientType const& overallArea); + + std::vector, storm::modelchecker::RegionResult>> regionResults; + typename storm::storage::ParameterRegion::CoefficientType satFraction, unsatFraction; + + }; + } +} diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp new file mode 100644 index 000000000..3cf8d1e1d --- /dev/null +++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp @@ -0,0 +1,100 @@ +#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h" + +#include + +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { + namespace modelchecker { + + template + RegionRefinementCheckResult::RegionRefinementCheckResult(std::vector, storm::modelchecker::RegionResult>> const& regionResults, storm::storage::ParameterRegion const& parameterSpace) : RegionCheckResult(regionResults), parameterSpace(parameterSpace) { + this->initFractions(this->parameterSpace.area()); + } + + + template + RegionRefinementCheckResult::RegionRefinementCheckResult(std::vector, storm::modelchecker::RegionResult>>&& regionResults, storm::storage::ParameterRegion&& parameterSpace) : RegionCheckResult(std::move(regionResults)), parameterSpace(std::move(parameterSpace)) { + this->initFractions(this->parameterSpace.area()); + } + + template + bool RegionRefinementCheckResult::isRegionRefinementCheckResult() const { + return true; + } + + template + storm::storage::ParameterRegion const& RegionRefinementCheckResult::getParameterSpace() const { + return parameterSpace; + } + + template + std::ostream& RegionRefinementCheckResult::writeIllustrationToStream(std::ostream& out) const { + if (this->getParameterSpace().getVariables().size() == 2) { + + typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; + auto x = *this->getParameterSpace().getVariables().begin(); + auto y = *(this->getParameterSpace().getVariables().rbegin()); + + uint_fast64_t const sizeX = 128; + uint_fast64_t const sizeY = 64; + + out << "Region refinement Check result (visualization):" << std::endl; + out << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl; + + CoefficientType deltaX = (getParameterSpace().getUpperBoundary(x) - getParameterSpace().getLowerBoundary(x)) / storm::utility::convertNumber(sizeX); + CoefficientType deltaY = (getParameterSpace().getUpperBoundary(y) - getParameterSpace().getLowerBoundary(y)) / storm::utility::convertNumber(sizeY); + CoefficientType printedRegionArea = deltaX * deltaY; + for (CoefficientType yUpper = getParameterSpace().getUpperBoundary(y); yUpper != getParameterSpace().getLowerBoundary(y); yUpper -= deltaY) { + CoefficientType yLower = yUpper - deltaY; + out << "#"; + for (CoefficientType xLower = getParameterSpace().getLowerBoundary(x); xLower != getParameterSpace().getUpperBoundary(x); xLower += deltaX) { + CoefficientType xUpper = xLower + deltaX; + bool currRegionSafe = false; + bool currRegionUnSafe = false; + bool currRegionComplete = false; + CoefficientType coveredArea = storm::utility::zero(); + for (auto const& r : this->getRegionResults()) { + CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)); + interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero()); + CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)); + interesctionSizeX = std::max(interesctionSizeX, storm::utility::zero()); + CoefficientType instersectionArea = interesctionSizeY * interesctionSizeX; + if(!storm::utility::isZero(instersectionArea)) { + currRegionSafe = currRegionSafe || r.second == storm::modelchecker::RegionResult::AllSat; + currRegionUnSafe = currRegionUnSafe || r.second == storm::modelchecker::RegionResult::AllViolated; + coveredArea += instersectionArea; + if(currRegionSafe && currRegionUnSafe) { + break; + } + if(coveredArea == printedRegionArea) { + currRegionComplete = true; + break; + } + } + } + if (currRegionComplete && currRegionSafe && !currRegionUnSafe) { + out << "S"; + } else if (currRegionComplete && currRegionUnSafe && !currRegionSafe) { + out << " "; + } else { + out << "-"; + } + } + out << "#" << std::endl; + } + for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl; + } else { + STORM_LOG_WARN("Writing illustration of region check result to a stream is only implemented for two parameters."); + } + return out; + } + +#ifdef STORM_HAVE_CARL + template class RegionRefinementCheckResult; +#endif + } +} diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.h b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.h new file mode 100644 index 000000000..8b37afcca --- /dev/null +++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.h @@ -0,0 +1,30 @@ +#pragma once + +#include + +#include "storm-pars/modelchecker/results/RegionCheckResult.h" +#include "storm-pars/modelchecker/region/RegionResult.h" +#include "storm-pars/storage/ParameterRegion.h" + +namespace storm { + namespace modelchecker { + template + class RegionRefinementCheckResult : public RegionCheckResult { + public: + + RegionRefinementCheckResult(std::vector, storm::modelchecker::RegionResult>> const& regionResults, storm::storage::ParameterRegion const& parameterSpace); + RegionRefinementCheckResult(std::vector, storm::modelchecker::RegionResult>>&& regionResults, storm::storage::ParameterRegion&& parameterSpace); + virtual ~RegionRefinementCheckResult() = default; + + virtual bool isRegionRefinementCheckResult() const override; + + storm::storage::ParameterRegion const& getParameterSpace() const; + + virtual std::ostream& writeIllustrationToStream(std::ostream& out) const override; + + + protected: + storm::storage::ParameterRegion parameterSpace; + }; + } +} diff --git a/src/storm-pars/parser/ParameterRegionParser.cpp b/src/storm-pars/parser/ParameterRegionParser.cpp new file mode 100644 index 000000000..f6345eef1 --- /dev/null +++ b/src/storm-pars/parser/ParameterRegionParser.cpp @@ -0,0 +1,97 @@ +#include "storm-pars/parser/ParameterRegionParser.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/utility/constants.h" +#include "storm/utility/file.h" + +namespace storm { + namespace parser { + + template + void ParameterRegionParser::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set const& consideredVariables) { + + std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<="); + STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number"); + std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2); + STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter"); + + std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2)); + //removes all whitespaces from the parameter string: + parameter.erase(std::remove_if (parameter.begin(), parameter.end(), ::isspace), parameter.end()); + STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter"); + + std::unique_ptr var; + for (auto const& v : consideredVariables) { + std::stringstream stream; + stream << v; + std::string vAsString = stream.str(); + if (parameter == stream.str()) { + var = std::make_unique(v); + } + } + STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables"); + + CoefficientType lb = storm::utility::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); + CoefficientType ub = storm::utility::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); + lowerBoundaries.emplace(std::make_pair(*var, lb)); + upperBoundaries.emplace(std::make_pair(*var, ub)); + } + + template + storm::storage::ParameterRegion ParameterRegionParser::parseRegion(std::string const& regionString, std::set const& consideredVariables) { + Valuation lowerBoundaries; + Valuation upperBoundaries; + std::vector parameterBoundaries; + boost::split(parameterBoundaries, regionString, boost::is_any_of(",")); + for (auto const& parameterBoundary : parameterBoundaries){ + if (!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space + parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables); + } + } + return storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); + } + + template + std::vector> ParameterRegionParser::parseMultipleRegions(std::string const& regionsString, std::set const& consideredVariables) { + std::vector> result; + std::vector regionsStrVec; + boost::split(regionsStrVec, regionsString, boost::is_any_of(";")); + for (auto const& regionStr : regionsStrVec){ + if (!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space + result.emplace_back(parseRegion(regionStr, consideredVariables)); + } + } + return result; + } + + template + std::vector> ParameterRegionParser::parseMultipleRegionsFromFile(std::string const& fileName, std::set const& consideredVariables) { + + // Open file and initialize result. + std::ifstream inputFileStream; + storm::utility::openFile(fileName, inputFileStream); + + std::vector> result; + + // Now try to parse the contents of the file. + try { + std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); + result = parseMultipleRegions(fileContent, consideredVariables); + } catch(std::exception& e) { + // In case of an exception properly close the file before passing exception. + storm::utility::closeFile(inputFileStream); + throw e; + } + + // Close the stream in case everything went smoothly and return result. + storm::utility::closeFile(inputFileStream); + return result; + } + +#ifdef STORM_HAVE_CARL + template class ParameterRegionParser; +#endif + } +} + diff --git a/src/storm-pars/parser/ParameterRegionParser.h b/src/storm-pars/parser/ParameterRegionParser.h new file mode 100644 index 000000000..99063a4d6 --- /dev/null +++ b/src/storm-pars/parser/ParameterRegionParser.h @@ -0,0 +1,47 @@ +#pragma once + +#include + +#include "storm-pars/storage/ParameterRegion.h" + +namespace storm { + namespace parser { + template + class ParameterRegionParser{ + public: + + typedef typename storm::storage::ParameterRegion::VariableType VariableType; + typedef typename storm::storage::ParameterRegion::CoefficientType CoefficientType; + typedef typename storm::storage::ParameterRegion::Valuation Valuation; + + /* + * Parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5". + * The results will be inserted in the given maps + * + */ + static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set const& consideredVariables); + + /* + * Parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7". + * + */ + static storm::storage::ParameterRegion parseRegion(std::string const& regionString, std::set const& consideredVariables); + + /* + * Parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4". + * + */ + static std::vector> parseMultipleRegions(std::string const& regionsString, std::set const& consideredVariables); + + + /* + * Parse multiple regions from a file + * + */ + static std::vector> parseMultipleRegionsFromFile(std::string const& fileName, std::set const& consideredVariables); + + }; + } +} + + diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index e7e764426..f57370683 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/settings/modules/ParametricSettings.h" +#include "storm-pars/settings/modules/ParametricSettings.h" #include "storm/settings/Option.h" #include "storm/settings/OptionBuilder.h" @@ -13,71 +13,27 @@ namespace storm { namespace modules { const std::string ParametricSettings::moduleName = "parametric"; - const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy"; - const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path"; - const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile"; - const std::string ParametricSettings::parameterSpaceOptionName = "parameterspace"; - const std::string ParametricSettings::refinementThresholdOptionName = "refinementthreshold"; - const std::string ParametricSettings::exactValidationOptionName = "exactvalidation"; + const std::string ParametricSettings::exportResultOptionName = "resultfile"; + const std::string ParametricSettings::simplifyOptionName = "simplify"; const std::string ParametricSettings::derivativesOptionName = "derivatives"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.") + this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, true, "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, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, parameterSpaceOptionName, true, "Sets the considered parameter-space (i.e., the initial region) for parameter lifting.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("region", "The parameter-space (given in format a<=x<=b,c<=y<=d).").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, refinementThresholdOptionName, true, "Parameter space refinement converges if the fraction of unknown area falls below this threshold.") - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The threshold").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exactValidationOptionName, true, "Sets whether numerical results from Parameter lifting should be validated with exact techniques.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, simplifyOptionName, true, "Sets whether to perform simplification steps before model analysis.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, true, "Sets whether to generate the derivatives of the resulting rational function.").build()); } bool ParametricSettings::exportResultToFile() const { - return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet(); + return this->getOption(exportResultOptionName).getHasOptionBeenSet(); } std::string ParametricSettings::exportResultPath() const { - return this->getOption(exportResultDestinationPathOptionName).getArgumentByName("path").getValueAsString(); - } - - bool ParametricSettings::isParameterSpaceSet() const { - return this->getOption(parameterSpaceOptionName).getHasOptionBeenSet(); - } - - std::string ParametricSettings::getParameterSpace() const { - return this->getOption(parameterSpaceOptionName).getArgumentByName("region").getValueAsString(); - } - - double ParametricSettings::getRefinementThreshold() const { - return this->getOption(refinementThresholdOptionName).getArgumentByName("threshold").getValueAsDouble(); - } - - bool ParametricSettings::isExactValidationSet() const { - return this->getOption(exactValidationOptionName).getHasOptionBeenSet(); - } - - bool ParametricSettings::exportToSmt2File() const { - return this->getOption(exportSmt2DestinationPathOptionName).getHasOptionBeenSet(); - } - - std::string ParametricSettings::exportSmt2Path() const { - return this->getOption(exportSmt2DestinationPathOptionName).getArgumentByName("path").getValueAsString(); + return this->getOption(exportResultOptionName).getArgumentByName("path").getValueAsString(); } - ParametricSettings::Smt2EncodingStrategy ParametricSettings::smt2EncodingStrategy() const { - std::string strategy = this->getOption(encodeSmt2StrategyOptionName).getArgumentByName("strategy").getValueAsString(); - - if(strategy == "fts") { - return Smt2EncodingStrategy::FULL_TRANSITION_SYSTEM; - } else if(strategy == "rf") { - return Smt2EncodingStrategy::RATIONAL_FUNCTION; - } else { - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'."); - } + bool ParametricSettings::isSimplifySet() const { + return this->getOption(simplifyOptionName).getHasOptionBeenSet(); } bool ParametricSettings::isDerivativesSet() const { diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 650d7bc3c..6ba91c80a 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -30,28 +30,12 @@ namespace storm { */ std::string exportResultPath() const; - /*! - * Retrieves whether the parameter space was declared - */ - bool isRegionSet() const; - - /*! - * Retrieves the given parameter spcae - */ - std::string getRegionString() const; - - /*! - * Retrieves the threshold considered for iterative region refinement. - * The refinement converges as soon as the fraction of unknown area falls below this threshold - */ - double getRefinementThreshold() const; - - /*! - * Retrieves whether exact validation should be performed - */ - bool isExactValidationSet() 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. * * @return True if the derivatives are to be generated. @@ -61,12 +45,8 @@ namespace storm { const static std::string moduleName; private: - const static std::string encodeSmt2StrategyOptionName; - const static std::string exportSmt2DestinationPathOptionName; - const static std::string exportResultDestinationPathOptionName; - const static std::string regionOptionName; - const static std::string refinementThresholdOptionName; - const static std::string exactValidationOptionName; + const static std::string exportResultOptionName; + const static std::string simplifyOptionName; const static std::string derivativesOptionName; }; diff --git a/src/storm-pars/settings/modules/RegionSettings.cpp b/src/storm-pars/settings/modules/RegionSettings.cpp new file mode 100644 index 000000000..daec46863 --- /dev/null +++ b/src/storm-pars/settings/modules/RegionSettings.cpp @@ -0,0 +1,82 @@ +#include "storm-pars/settings/modules/RegionSettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string RegionSettings::moduleName = "region"; + const std::string RegionSettings::regionOptionName = "region"; + const std::string RegionSettings::refineOptionName = "refine"; + const std::string RegionSettings::checkEngineOptionName = "engine"; + const std::string RegionSettings::printNoIllustrationOptionName = "noillustration"; + const std::string RegionSettings::printFullResultOptionName = "printfullresult"; + + RegionSettings::RegionSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, true, "Sets the region(s) considered for analysis.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be point to a file.").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, true, "Enables region refinement.") + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build()); + + std::vector engines = {"pl", "exactpl", "validatingpl"}; + this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, false, "Sets which engine is used for analyzing regions.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("pl").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, printNoIllustrationOptionName, true, "If set, no illustration of the result is printed.").build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, printFullResultOptionName, true, "If set, the full result for every region is printed.").build()); + } + + bool RegionSettings::isRegionSet() const { + return this->getOption(regionOptionName).getHasOptionBeenSet(); + } + + std::string RegionSettings::getRegionString() const { + return this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString(); + } + + bool RegionSettings::isRefineSet() const { + return this->getOption(refineOptionName).getHasOptionBeenSet(); + } + + double RegionSettings::getRefinementThreshold() const { + return this->getOption(refineOptionName).getArgumentByName("threshold").getValueAsDouble(); + } + + storm::modelchecker::RegionCheckEngine RegionSettings::getRegionCheckEngine() const { + std::string engineString = this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString(); + + storm::modelchecker::RegionCheckEngine result; + if (engineString == "pl") { + result = storm::modelchecker::RegionCheckEngine::ParameterLifting; + } else if (engineString == "exactpl") { + result = storm::modelchecker::RegionCheckEngine::ExactParameterLifting; + } else if (engineString == "validatingpl") { + result = storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown region check engine '" << engineString << "'."); + } + + return result; + } + + bool RegionSettings::isPrintNoIllustrationSet() const { + return this->getOption(printNoIllustrationOptionName).getHasOptionBeenSet(); + } + + bool RegionSettings::isPrintFullResultSet() const { + return this->getOption(printFullResultOptionName).getHasOptionBeenSet(); + } + + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-pars/settings/modules/RegionSettings.h b/src/storm-pars/settings/modules/RegionSettings.h new file mode 100644 index 000000000..fc4160f83 --- /dev/null +++ b/src/storm-pars/settings/modules/RegionSettings.h @@ -0,0 +1,71 @@ +#pragma once + +#include "storm-pars/modelchecker/region/RegionCheckEngine.h" + +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for parametric model checking. + */ + class RegionSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of parametric model checking settings. + */ + RegionSettings(); + + /*! + * Retrieves whether region(s) were declared + */ + bool isRegionSet() const; + + /*! + * Retrieves the region definition string + */ + std::string getRegionString() const; + + /*! + * Retrieves whether region refinement is enabled + */ + bool isRefineSet() const; + + /*! + * Retrieves the threshold considered for iterative region refinement. + * The refinement converges as soon as the fraction of unknown area falls below this threshold + */ + double getRefinementThreshold() const; + + /*! + * Retrieves which type of region check should be performed + */ + storm::modelchecker::RegionCheckEngine getRegionCheckEngine() const; + + /*! + * Retrieves whether no illustration of the result should be printed. + */ + bool isPrintNoIllustrationSet() const; + + /*! + * Retrieves whether the full result should be printed + */ + bool isPrintFullResultSet() const; + + const static std::string moduleName; + + private: + const static std::string regionOptionName; + const static std::string refineOptionName; + const static std::string checkEngineOptionName; + const static std::string printNoIllustrationOptionName; + const static std::string printFullResultOptionName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + diff --git a/src/storm-pars/storage/ParameterRegion.cpp b/src/storm-pars/storage/ParameterRegion.cpp index 9e5287d05..dceaa26ae 100644 --- a/src/storm-pars/storage/ParameterRegion.cpp +++ b/src/storm-pars/storage/ParameterRegion.cpp @@ -1,9 +1,8 @@ -#include "ParameterRegion.h" +#include "storm-pars/storage/ParameterRegion.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/constants.h" -#include "storm/utility/file.h" namespace storm { namespace storage { @@ -164,65 +163,7 @@ namespace storm { regionstring = regionstring.substr(0, regionstring.length() - 1) + ";"; return regionstring; } - - - template - void ParameterRegion::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set const& consideredVariables) { - - std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<="); - STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number"); - std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2); - STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter"); - - std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2)); - //removes all whitespaces from the parameter string: - parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end()); - STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter"); - - std::unique_ptr var; - for (auto const& v : consideredVariables) { - std::stringstream stream; - stream << v; - std::string vAsString = stream.str(); - if(parameter == stream.str()) { - var = std::make_unique(v); - } - } - STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << " in the set of considered variables"); - - CoefficientType lb = storm::utility::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); - lowerBoundaries.emplace(std::make_pair(*var, lb)); - upperBoundaries.emplace(std::make_pair(*var, ub)); - } - - template - ParameterRegion ParameterRegion::parseRegion(std::string const& regionString, std::set const& consideredVariables) { - Valuation lowerBoundaries; - Valuation upperBoundaries; - std::vector parameterBoundaries; - boost::split(parameterBoundaries, regionString, boost::is_any_of(",")); - for(auto const& parameterBoundary : parameterBoundaries){ - if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space - parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables); - } - } - return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); - } - - template - std::vector> ParameterRegion::parseMultipleRegions(std::string const& regionsString, std::set const& consideredVariables) { - std::vector result; - std::vector regionsStrVec; - boost::split(regionsStrVec, regionsString, boost::is_any_of(";")); - for(auto const& regionStr : regionsStrVec){ - if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space - result.emplace_back(parseRegion(regionStr, consideredVariables)); - } - } - return result; - } - + #ifdef STORM_HAVE_CARL template class ParameterRegion; #endif diff --git a/src/storm-pars/storage/ParameterRegion.h b/src/storm-pars/storage/ParameterRegion.h index add11e0be..76e645683 100644 --- a/src/storm-pars/storage/ParameterRegion.h +++ b/src/storm-pars/storage/ParameterRegion.h @@ -2,7 +2,7 @@ #include -#include "storm/utility/parametric.h" +#include "storm-pars/utility/parametric.h" namespace storm { namespace storage { @@ -62,28 +62,6 @@ namespace storm { //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5; std::string toString(bool boundariesAsDouble = false) const; - /* - * Can be used to parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5". - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. - * The results will be inserted in the given maps - * - */ - static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set const& consideredVariables); - - /* - * Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7". - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. - * - */ - static ParameterRegion parseRegion(std::string const& regionString, std::set const& consideredVariables); - - /* - * Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4". - * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. - * - */ - static std::vector parseMultipleRegions(std::string const& regionsString, std::set const& consideredVariables); - private: void init(); diff --git a/src/storm-pars/transformer/ParameterLifter.cpp b/src/storm-pars/transformer/ParameterLifter.cpp index 43c76fd55..551529c4c 100644 --- a/src/storm-pars/transformer/ParameterLifter.cpp +++ b/src/storm-pars/transformer/ParameterLifter.cpp @@ -1,4 +1,4 @@ -#include "storm/transformer/ParameterLifter.h" +#include "storm-pars/transformer/ParameterLifter.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm-pars/transformer/ParameterLifter.h b/src/storm-pars/transformer/ParameterLifter.h index e29e648a6..ab16e5a88 100644 --- a/src/storm-pars/transformer/ParameterLifter.h +++ b/src/storm-pars/transformer/ParameterLifter.h @@ -6,10 +6,10 @@ #include +#include "storm-pars/storage/ParameterRegion.h" +#include "storm-pars/utility/parametric.h" #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" -#include "storm/utility/parametric.h" -#include "storm/storage/ParameterRegion.h" #include "storm/solver/OptimizationDirection.h" namespace storm { diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp index a150efe9b..ed05131e4 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp @@ -1,4 +1,4 @@ -#include "storm/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h index 5f34b483b..efbbf231b 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h @@ -1,7 +1,7 @@ #pragma once -#include "storm/transformer/SparseParametricModelSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" namespace storm { namespace transformer { diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp index a6d8bf99e..1862936f4 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp @@ -1,4 +1,4 @@ -#include "storm/transformer/SparseParametricMdpSimplifier.h" +#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.h b/src/storm-pars/transformer/SparseParametricMdpSimplifier.h index ebe16f994..3a7c223bc 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.h +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.h @@ -1,7 +1,7 @@ #pragma once -#include "storm/transformer/SparseParametricModelSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" namespace storm { namespace transformer { diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 3dd6fbd56..343fc06e3 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -1,4 +1,4 @@ -#include "storm/transformer/SparseParametricModelSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm-pars/utility/ModelInstantiator.cpp b/src/storm-pars/utility/ModelInstantiator.cpp index e28049862..f59649ab7 100644 --- a/src/storm-pars/utility/ModelInstantiator.cpp +++ b/src/storm-pars/utility/ModelInstantiator.cpp @@ -1,4 +1,4 @@ -#include "storm/utility/ModelInstantiator.h" +#include "storm-pars/utility/ModelInstantiator.h" #include "storm/models/sparse/StandardRewardModel.h" namespace storm { diff --git a/src/storm-pars/utility/ModelInstantiator.h b/src/storm-pars/utility/ModelInstantiator.h index fa1ba8099..e96a4dda8 100644 --- a/src/storm-pars/utility/ModelInstantiator.h +++ b/src/storm-pars/utility/ModelInstantiator.h @@ -5,12 +5,12 @@ #include #include +#include "storm-pars/utility/parametric.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StochasticTwoPlayerGame.h" -#include "storm/utility/parametric.h" #include "storm/utility/constants.h" namespace storm { diff --git a/src/storm-pars/utility/parameterlifting.h b/src/storm-pars/utility/parameterlifting.h index 3c8cdbf73..a32418d91 100644 --- a/src/storm-pars/utility/parameterlifting.h +++ b/src/storm-pars/utility/parameterlifting.h @@ -3,8 +3,8 @@ #include +#include "storm-pars/utility/parametric.h" #include "storm/models/sparse/Model.h" -#include "storm/utility/parametric.h" #include "storm/utility/macros.h" #include "storm/logic/Formula.h" #include "storm/logic/FragmentSpecification.h" @@ -31,37 +31,38 @@ namespace storm { * @return true iff it was successfully validated that parameter lifting is sound on the provided model. */ template - static bool validateParameterLiftingSound(std::shared_ptr> const& model, std::shared_ptr const& formula) { + static bool validateParameterLiftingSound(storm::models::sparse::Model const& model, storm::logic::Formula const& formula) { // Check whether all numbers occurring in the model are multilinear // Transition matrix - if (model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::Ctmc)) { - for (auto const& entry : model->getTransitionMatrix()) { + if (model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp) || model.isOfType(storm::models::ModelType::Ctmc)) { + for (auto const& entry : model.getTransitionMatrix()) { if (!storm::utility::parametric::isMultiLinearPolynomial(entry.getValue())) { STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); return false; } } - } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { + auto const& ma = dynamic_cast const&>(model); // Markov Automata store the probability matrix and the exit rate vector. However, we need to considert the rate matrix. - if (!model->template as>()->isClosed()) { + if (!ma.isClosed()) { STORM_LOG_ERROR("parameter lifting requires a closed Markov automaton."); return false; } - auto const& rateVector = model->template as>()->getExitRates(); - auto const& markovianStates = model->template as>()->getMarkovianStates(); - for (uint_fast64_t state = 0; state < model->getNumberOfStates(); ++state) { + auto const& rateVector = ma.getExitRates(); + auto const& markovianStates = ma.getMarkovianStates(); + for (uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) { if (markovianStates.get(state)) { auto const& exitRate = rateVector[state]; - for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) { + for (auto const& entry : model.getTransitionMatrix().getRowGroup(state)) { if (!storm::utility::parametric::isMultiLinearPolynomial(storm::utility::simplify(entry.getValue() * exitRate))) { STORM_LOG_WARN("The input model contains a non-linear polynomial as transition rate: '" << storm::utility::simplify(entry.getValue() * exitRate) << "'. Can not validate that parameter lifting is sound on this model."); return false; } } } else { - for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) { + for (auto const& entry : model.getTransitionMatrix().getRowGroup(state)) { if (!storm::utility::parametric::isMultiLinearPolynomial(entry.getValue())) { STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); return false; @@ -75,10 +76,10 @@ namespace storm { } // Rewards - if (formula->isRewardOperatorFormula()) { - storm::models::sparse::StandardRewardModel const& rewardModel = formula->asRewardOperatorFormula().hasRewardModelName() ? - model->getRewardModel(formula->asRewardOperatorFormula().getRewardModelName()) : - model->getUniqueRewardModel(); + if (formula.isRewardOperatorFormula()) { + storm::models::sparse::StandardRewardModel const& rewardModel = formula.asRewardOperatorFormula().hasRewardModelName() ? + model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()) : + model.getUniqueRewardModel(); if (rewardModel.hasStateRewards()) { for (auto const& rew : rewardModel.getStateRewardVector()) { if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) { @@ -91,7 +92,7 @@ namespace storm { // Note: This check could also be done action-wise. std::set::type> collectedRewardParameters; if (rewardModel.hasStateActionRewards()) { - if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + if (model.isOfType(storm::models::ModelType::Ctmc) || model.isOfType(storm::models::ModelType::MarkovAutomaton)) { for (auto const& rew : rewardModel.getStateActionRewardVector()) { if (!storm::utility::parametric::isMultiLinearPolynomial(rew)) { STORM_LOG_WARN("The input model contains a non-linear polynomial as action reward: '" << rew << "'. Can not validate that parameter lifting is sound on this model."); @@ -120,7 +121,7 @@ namespace storm { } if (!collectedRewardParameters.empty()) { - std::set::type> transitionParameters = storm::models::sparse::getProbabilityParameters(*model); + std::set::type> transitionParameters = storm::models::sparse::getProbabilityParameters(model); auto rewParIt = collectedRewardParameters.begin(); auto trParIt = transitionParameters.begin(); while (rewParIt != collectedRewardParameters.end() && trParIt != transitionParameters.end()) { diff --git a/src/storm-pars/utility/parametric.cpp b/src/storm-pars/utility/parametric.cpp index 78bb0b880..3b6934a3e 100644 --- a/src/storm-pars/utility/parametric.cpp +++ b/src/storm-pars/utility/parametric.cpp @@ -1,6 +1,6 @@ #include -#include "storm/utility/parametric.h" +#include "storm-pars/utility/parametric.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/settings/SettingsManager.h"