iMC changes inside of storm-pars

resources/examples/testfiles/pdtmc/only_p.pm

@@ -0,0 +1,15 @@
+dtmc
+
+const double p;
+
+module test
+
+	// local state
+	s : [0..1] init 0;
+
+	[] s=0 -> p : (s'=0) + (1-p) : (s'=1);
+	[] s=1 -> 1 : (s'=1);
+
+endmodule
+
+label "target" = s=1;

src/storm-cli-utilities/model-handling.h

@@ -572,14 +572,14 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseMarkovA
 template<typename ValueType>
 std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseModelBisimulation(
     std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input,
-    storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
+    storm::settings::modules::BisimulationSettings const& bisimulationSettings, bool graphPreserving = true) {
     storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
     if (bisimulationSettings.isWeakBisimulationSet()) {
         bisimType = storm::storage::BisimulationType::Weak;
     }
 
     STORM_LOG_INFO("Performing bisimulation minimization...");
-    return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType);
+    return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType, graphPreserving);
 }
 
 template<typename ValueType>

src/storm-pars-cli/feasibility.cpp

@@ -1,5 +1,8 @@
 #include "storm-pars-cli/feasibility.h"
+#include <optional>
 
+#include "storm-pars/modelchecker/region/RegionSplittingStrategy.h"
+#include "storm-pars/storage/ParameterRegion.h"
 #include "storm/api/verification.h"
 
 #include "storm/settings/SettingsManager.h"
@@ -110,9 +113,7 @@ void runFeasibilityWithGD(std::shared_ptr<storm::models::sparse::Model<ValueType
 
     STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException,
                     "Gradient descent is currently only supported for DTMCs.");
-    STORM_LOG_THROW(!task->isRegionSet(), storm::exceptions::NotSupportedException, "Gradient descent only works with *the* graph-preserving region.");
     std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
-
     STORM_LOG_THROW(task->getFormula().isProbabilityOperatorFormula() || task->getFormula().isRewardOperatorFormula(), storm::exceptions::NotSupportedException,
                     "Input formula needs to be either a probability operator formula or a reward operator formula.");
     STORM_LOG_THROW(task->isBoundSet(), storm::exceptions::NotImplementedException, "GD (right now) requires an explicitly given bound.");
@@ -145,14 +146,19 @@ void runFeasibilityWithGD(std::shared_ptr<storm::models::sparse::Model<ValueType
         return;
     }
 
-    boost::optional<std::map<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>>
+    std::optional<std::map<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>>
         startPoint;
 
+    std::optional<storage::ParameterRegion<storm::RationalFunction>> region;
+    if (task->isRegionSet()) {
+        region = task->getRegion();
+    }
+
     STORM_PRINT("Finding an extremum using Gradient Descent\n");
     storm::utility::Stopwatch derivativeWatch(true);
     storm::derivative::GradientDescentInstantiationSearcher<storm::RationalFunction, double> gdsearch(
         *dtmc, *method, derSettings.getLearningRate(), derSettings.getAverageDecay(), derSettings.getSquaredAverageDecay(), derSettings.getMiniBatchSize(),
-        derSettings.getTerminationEpsilon(), startPoint, *constraintMethod, derSettings.isPrintJsonSet());
+        derSettings.getTerminationEpsilon(), startPoint, *constraintMethod, region, derSettings.isPrintJsonSet());
 
     gdsearch.setup(Environment(), task);
     auto instantiationAndValue = gdsearch.gradientDescent();
@@ -194,13 +200,21 @@ void runFeasibilityWithPLA(std::shared_ptr<storm::models::sparse::Model<ValueTyp
     // TODO handle omittedParameterss
     auto regionVerificationSettings = storm::settings::getModule<storm::settings::modules::RegionVerificationSettings>();
     auto engine = regionVerificationSettings.getRegionCheckEngine();
-    bool generateSplitEstimates = regionVerificationSettings.isSplittingThresholdSet();
+
+    auto regionSplittingStrategy = modelchecker::RegionSplittingStrategy();
+
+    regionSplittingStrategy.heuristic = regionVerificationSettings.getRegionSplittingHeuristic();
+    regionSplittingStrategy.estimateKind = regionVerificationSettings.getRegionSplittingEstimateMethod();
+    if (regionVerificationSettings.isSplittingThresholdSet()) {
+        regionSplittingStrategy.maxSplitDimensions = regionVerificationSettings.getSplittingThreshold();
+    }
 
     if (task->isBoundSet()) {
         storm::utility::Stopwatch watch(true);
-        auto valueValuation = storm::api::computeExtremalValue<ValueType>(
-            model, storm::api::createTask<ValueType>(task->getFormula().asSharedPointer(), true), task->getRegion(), engine, direction,
-            storm::utility::zero<ValueType>(), !task->isMaxGapRelative(), monotonicitySettings, task->getBound().getInvertedBound(), generateSplitEstimates);
+        auto const& settings = storm::api::RefinementSettings<ValueType>{model, storm::api::createTask<ValueType>(task->getFormula().asSharedPointer(), true),
+                                                                         engine, regionSplittingStrategy};
+        auto valueValuation = storm::api::computeExtremalValue<ValueType>(settings, task->getRegion(), direction, storm::utility::zero<ValueType>(),
+                                                                          !task->isMaxGapRelative(), task->getBound().getInvertedBound());
         watch.stop();
 
         printFeasibilityResult(task->getBound().isSatisfied(valueValuation.first), valueValuation, watch);
@@ -210,9 +224,10 @@ void runFeasibilityWithPLA(std::shared_ptr<storm::models::sparse::Model<ValueTyp
 
         ValueType precision = storm::utility::convertNumber<ValueType>(task->getMaximalAllowedGap().value());
         storm::utility::Stopwatch watch(true);
-        auto valueValuation = storm::api::computeExtremalValue<ValueType>(model, storm::api::createTask<ValueType>(task->getFormula().asSharedPointer(), true),
-                                                                          task->getRegion(), engine, direction, precision, !task->isMaxGapRelative(),
-                                                                          monotonicitySettings, std::nullopt, generateSplitEstimates);
+        auto const& settings = storm::api::RefinementSettings<ValueType>{model, storm::api::createTask<ValueType>(task->getFormula().asSharedPointer(), true),
+                                                                         engine, regionSplittingStrategy};
+        auto valueValuation = storm::api::computeExtremalValue<ValueType>(settings, task->getRegion(), direction, storm::utility::zero<ValueType>(),
+                                                                          !task->isMaxGapRelative(), std::nullopt);
         watch.stop();
 
         printFeasibilityResult(true, valueValuation, watch);

src/storm-pars-cli/storm-pars.cpp

@@ -13,6 +13,7 @@
 
 #include "storm-pars/derivative/SparseDerivativeInstantiationModelChecker.h"
 #include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h"
+#include "storm-pars/modelchecker/region/RegionSplittingStrategy.h"
 #include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
 #include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"
 
@@ -36,6 +37,7 @@
 #include "storm-parsers/parser/KeyValueParser.h"
 #include "storm/api/storm.h"
 
+#include "storm/environment/Environment.h"
 #include "storm/exceptions/BaseException.h"
 #include "storm/exceptions/InvalidSettingsException.h"
 #include "storm/exceptions/NotSupportedException.h"
@@ -82,6 +84,19 @@ std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared
     } else if (regionSettings.isRegionBoundSet()) {
         result = storm::api::createRegion<ValueType>(regionSettings.getRegionBoundString(), *model);
     }
+    if (!regionSettings.isNotGraphPreservingSet()) {
+        for (auto const& region : result) {
+            for (auto const& variable : region.getVariables()) {
+                if (region.getLowerBoundary(variable) <= storm::utility::zero<typename storm::utility::parametric::CoefficientType<ValueType>::type>() ||
+                    region.getUpperBoundary(variable) >= storm::utility::one<typename storm::utility::parametric::CoefficientType<ValueType>::type>()) {
+                    STORM_LOG_WARN(
+                        "Region" << region
+                                 << " appears to not preserve the graph structure of the parametric model. If this is the case, --not-graph-preserving.");
+                    break;
+                }
+            }
+        }
+    }
     return result;
 }
 
@@ -202,6 +217,7 @@ PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Mo
     auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
     auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
     auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
+    auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
 
     PreprocessResult result(model, false);
     // TODO: why only simplify in these modes
@@ -218,8 +234,8 @@ PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Mo
     }
 
     if (mpi.applyBisimulation) {
-        result.model =
-            storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
+        result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input,
+                                                                     bisimulationSettings, !regionSettings.isNotGraphPreservingSet());
         result.changed = true;
     }
 
@@ -230,12 +246,17 @@ PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Mo
         result.changed = true;
     }
 
-    if (parametricSettings.isTimeTravellingEnabled()) {
+    if (parametricSettings.isBigStepEnabled()) {
         transformer::TimeTravelling tt;
         auto formulas = storm::api::extractFormulasFromProperties(input.properties);
         modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> checkTask(*formulas[0]);
-        result.model = std::make_shared<storm::models::sparse::Dtmc<RationalFunction>>(
-            tt.timeTravel(*result.model->template as<storm::models::sparse::Dtmc<RationalFunction>>(), checkTask));
+        auto bigStepResult = tt.bigStep(*result.model->template as<storm::models::sparse::Dtmc<RationalFunction>>(), checkTask);
+        result.model = std::make_shared<storm::models::sparse::Dtmc<RationalFunction>>(bigStepResult.first);
+
+        if (mpi.applyBisimulation) {
+            result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input,
+                                                                         bisimulationSettings, !regionSettings.isNotGraphPreservingSet());
+        }
         result.changed = true;
     }
 
@@ -329,11 +350,14 @@ void verifyRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<V
 
     auto const& rvs = storm::settings::getModule<storm::settings::modules::RegionVerificationSettings>();
     auto engine = rvs.getRegionCheckEngine();
-    bool generateSplitEstimates = rvs.isSplittingThresholdSet();
-    std::optional<uint64_t> maxSplitsPerStep = generateSplitEstimates ? std::make_optional(rvs.getSplittingThreshold()) : std::nullopt;
+    auto splittingHeuristic = rvs.getRegionSplittingHeuristic();
+    auto estimateKind = rvs.getRegionSplittingEstimateMethod();
+    uint64_t maxSplitsPerStep = rvs.isSplittingThresholdSet() ? rvs.getSplittingThreshold() : std::numeric_limits<uint64_t>::max();
+
+    auto splittingStrategy = modelchecker::RegionSplittingStrategy(splittingHeuristic, maxSplitsPerStep, estimateKind);
     storm::utility::Stopwatch watch(true);
-    if (storm::api::verifyRegion<ValueType>(model, *(property.getRawFormula()), region, engine, monotonicitySettings, generateSplitEstimates,
-                                            maxSplitsPerStep)) {
+    auto const& settings = storm::api::RefinementSettings<ValueType>{model, *(property.getRawFormula()), engine, splittingStrategy, monotonicitySettings};
+    if (storm::api::verifyRegion<ValueType>(settings, region)) {
         STORM_PRINT_AND_LOG("Formula is satisfied by all parameter instantiations.\n");
     } else {
         STORM_PRINT_AND_LOG("Formula is not satisfied by all parameter instantiations.\n");
@@ -354,9 +378,10 @@ void parameterSpacePartitioningWithSparseEngine(std::shared_ptr<storm::models::s
     auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
     auto rvs = storm::settings::getModule<storm::settings::modules::RegionVerificationSettings>();
     auto partitionSettings = storm::settings::getModule<storm::settings::modules::PartitionSettings>();
+    auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
 
     ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(partitionSettings.getCoverageThreshold());
-    boost::optional<uint64_t> optionalDepthLimit;
+    std::optional<uint64_t> optionalDepthLimit;
     if (partitionSettings.isDepthLimitSet()) {
         optionalDepthLimit = partitionSettings.getDepthLimit();
     }
@@ -366,19 +391,46 @@ void parameterSpacePartitioningWithSparseEngine(std::shared_ptr<storm::models::s
 
     auto engine = rvs.getRegionCheckEngine();
     STORM_PRINT_AND_LOG(" using " << engine);
+
+    auto splittingStrategy = modelchecker::RegionSplittingStrategy();
+
+    splittingStrategy.heuristic = rvs.getRegionSplittingHeuristic();
+    splittingStrategy.estimateKind = rvs.getRegionSplittingEstimateMethod();
+    if (rvs.isSplittingThresholdSet()) {
+        splittingStrategy.maxSplitDimensions = rvs.getSplittingThreshold();
+    }
+
+    bool graphPreserving = !regionSettings.isNotGraphPreservingSet();
+
+    auto parsedDiscreteVars = storm::api::parseVariableList<ValueType>(regionSettings.getDiscreteVariablesString(), *model);
+    std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> discreteVariables(parsedDiscreteVars.begin(), parsedDiscreteVars.end());
+
+    STORM_PRINT_AND_LOG(" and splitting heuristic " << splittingStrategy.heuristic);
     if (monotonicitySettings.useMonotonicity) {
         STORM_PRINT_AND_LOG(" with local monotonicity and");
     }
 
     STORM_PRINT_AND_LOG(" with iterative refinement until "
-                        << (1.0 - partitionSettings.getCoverageThreshold()) * 100.0 << "% is covered."
+                        << (1.0 - partitionSettings.getCoverageThreshold()) * 100.0 << "\% is covered."
                         << (partitionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(partitionSettings.getDepthLimit()) + "." : "") << '\n');
 
     storm::cli::printModelCheckingProperty(property);
     storm::utility::Stopwatch watch(true);
+    Environment env;
+
+    auto settings = storm::api::RefinementSettings<ValueType>{
+        model,
+        storm::api::createTask<ValueType>(property.getRawFormula(), true),
+        engine,
+        splittingStrategy,
+        monotonicitySettings,
+        discreteVariables,
+        true,  // allow model simplification
+        graphPreserving,
+        false  // preconditions not yet validated
+    };
     std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(
-        model, storm::api::createTask<ValueType>((property.getRawFormula()), true), regions.front(), engine, refinementThreshold, optionalDepthLimit,
-        storm::modelchecker::RegionResultHypothesis::Unknown, false, monotonicitySettings, monThresh);
+        settings, regions.front(), refinementThreshold, optionalDepthLimit, storm::modelchecker::RegionResultHypothesis::Unknown, monThresh);
     watch.stop();
     printInitialStatesResult<ValueType>(result, &watch);
 
@@ -394,6 +446,7 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
     auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
     auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
     auto sampleSettings = storm::settings::getModule<storm::settings::modules::SamplingSettings>();
+    auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
 
     STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse || mpi.engine == storm::utility::Engine::Hybrid || mpi.engine == storm::utility::Engine::Dd,
                     storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
@@ -457,6 +510,7 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
         STORM_LOG_INFO("Solution function mode started.");
         STORM_LOG_THROW(regions.empty(), storm::exceptions::InvalidSettingsException,
                         "Solution function computations cannot be restricted to specific regions");
+        STORM_LOG_ERROR_COND(!regionSettings.isNotGraphPreservingSet(), "Solution function computations assume graph preservation.");
 
         if (model->isSparseModel()) {
             computeSolutionFunctionsWithSparseEngine(model->as<storm::models::sparse::Model<ValueType>>(), input);

src/storm-pars/analysis/MonotonicityKind.cpp

@@ -0,0 +1,34 @@
+#include "storm-pars/analysis/MonotonicityKind.h"
+
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/utility/macros.h"
+
+namespace storm::analysis {
+std::ostream& operator<<(std::ostream& out, MonotonicityKind kind) {
+    switch (kind) {
+        case MonotonicityKind::Incr:
+            out << "MonIncr";
+            break;
+        case MonotonicityKind::Decr:
+            out << "MonDecr";
+            break;
+        case MonotonicityKind::Constant:
+            out << "Constant";
+            break;
+        case MonotonicityKind::Not:
+            out << "NotMon";
+            break;
+        case MonotonicityKind::Unknown:
+            out << "Unknown";
+            break;
+        default:
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
+                            "Could not get a string from the region monotonicity check result. The case has not been implemented");
+    }
+    return out;
+}
+
+bool isMonotone(MonotonicityKind kind) {
+    return kind == MonotonicityKind::Incr || kind == MonotonicityKind::Decr || kind == MonotonicityKind::Constant;
+}
+}  // namespace storm::analysis

src/storm-pars/analysis/MonotonicityKind.h

@@ -0,0 +1,21 @@
+#pragma once
+
+#include <iostream>
+
+namespace storm::analysis {
+/*!
+ * The results of monotonicity checking for a single Parameter Region
+ */
+enum class MonotonicityKind {
+    Incr,     /*!< the result is monotonically increasing */
+    Decr,     /*!< the result is monotonically decreasing */
+    Constant, /*!< the result is constant */
+    Not,      /*!< the result is not monotonic */
+    Unknown   /*!< the monotonicity result is unknown */
+};
+
+std::ostream& operator<<(std::ostream& out, MonotonicityKind kind);
+
+bool isMonotone(MonotonicityKind kind);
+
+}  // namespace storm::analysis