Monitor Verification (ATVA25) and conditional model checking (CAV25)

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

@@ -154,7 +154,7 @@ struct ModelProcessingInformation {
     bool transformToJani;
 
     // Which data type is to be used for numbers ...
-    enum class ValueType { FinitePrecision, Exact, Parametric };
+    enum class ValueType { FinitePrecision, Exact, Parametric, FinitePrecisionInterval, ExactInterval };
     ValueType buildValueType;         // ... during model building
     ValueType verificationValueType;  // ... during model verification
 
@@ -222,9 +222,17 @@ inline ModelProcessingInformation getModelProcessingInformation(SymbolicInput co
     if (generalSettings.isParametricSet()) {
         mpi.verificationValueType = ModelProcessingInformation::ValueType::Parametric;
     } else if (generalSettings.isExactSet()) {
-        mpi.verificationValueType = ModelProcessingInformation::ValueType::Exact;
+        if (generalSettings.isIntervalSet()) {
+            mpi.verificationValueType = ModelProcessingInformation::ValueType::ExactInterval;
+        } else {
+            mpi.verificationValueType = ModelProcessingInformation::ValueType::Exact;
+        }
     } else {
-        mpi.verificationValueType = ModelProcessingInformation::ValueType::FinitePrecision;
+        if (generalSettings.isIntervalSet()) {
+            mpi.verificationValueType = ModelProcessingInformation::ValueType::FinitePrecisionInterval;
+        } else {
+            mpi.verificationValueType = ModelProcessingInformation::ValueType::FinitePrecision;
+        }
     }
     auto originalVerificationValueType = mpi.verificationValueType;
 
@@ -270,6 +278,12 @@ inline ModelProcessingInformation getModelProcessingInformation(SymbolicInput co
                 case ModelProcessingInformation::ValueType::FinitePrecision:
                     return storm::utility::canHandle<double>(
                         mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
+                case ModelProcessingInformation::ValueType::FinitePrecisionInterval:
+                    return storm::utility::canHandle<storm::Interval>(
+                        mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
+                case ModelProcessingInformation::ValueType::ExactInterval:
+                    return storm::utility::canHandle<storm::RationalInterval>(
+                        mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get());
             }
             return false;
         };
@@ -381,6 +395,10 @@ auto applyValueType(ModelProcessingInformation::ValueType vt, auto const& callba
             return callback.template operator()<storm::RationalNumber>();
         case Parametric:
             return callback.template operator()<storm::RationalFunction>();
+        case FinitePrecisionInterval:
+            return callback.template operator()<storm::Interval>();
+        case ExactInterval:
+            return callback.template operator()<storm::RationalInterval>();
     }
     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected value type.");
 }
@@ -400,6 +418,10 @@ auto applyDdLibValueType(storm::dd::DdType dd, ModelProcessingInformation::Value
                     return callback.template operator()<Sylvan, storm::RationalNumber>();
                 case Parametric:
                     return callback.template operator()<Sylvan, storm::RationalFunction>();
+                case FinitePrecisionInterval:
+                    return callback.template operator()<Sylvan, storm::Interval>();
+                case ExactInterval:
+                    return callback.template operator()<Sylvan, storm::RationalInterval>();
             }
     }
     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected DDType or value type.");
@@ -591,8 +613,12 @@ std::shared_ptr<storm::models::ModelBase> buildModelExplicit(storm::settings::mo
         storm::parser::DirectEncodingValueType valueType{Default};
         if constexpr (std::is_same_v<ValueType, double>) {
             valueType = Double;
+        } else if constexpr (std::is_same_v<ValueType, storm::Interval>) {
+            valueType = DoubleInterval;
         } else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
             valueType = Rational;
+        } else if constexpr (std::is_same_v<ValueType, storm::RationalInterval>) {
+            valueType = RationalInterval;
         } else {
             static_assert(std::is_same_v<ValueType, storm::RationalFunction>, "Unexpected value type.");
             valueType = Parametric;
@@ -1285,30 +1311,38 @@ inline std::vector<std::vector<storm::expressions::Expression>> parseInjectedRef
 
 template<storm::dd::DdType DdType, typename ValueType>
 void verifyWithAbstractionRefinementEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
-    STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
-    storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
-    storm::gbar::api::AbstractionRefinementOptions options(
-        parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()),
-        parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates()));
-
-    verifyProperties<ValueType>(input, [&input, &options, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
-                                                                std::shared_ptr<storm::logic::Formula const> const& states) {
-        STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
-        return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, input.model.get(),
-                                                                                          storm::api::createTask<ValueType>(formula, true), options);
-    });
+    if constexpr (storm::IsIntervalType<ValueType>) {
+        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support interval value types.");
+    } else {
+        STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
+        storm::settings::modules::AbstractionSettings const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
+        storm::gbar::api::AbstractionRefinementOptions options(
+            parseConstraints(input.model->getManager(), abstractionSettings.getConstraintString()),
+            parseInjectedRefinementPredicates(input.model->getManager(), abstractionSettings.getInjectedRefinementPredicates()));
+
+        verifyProperties<ValueType>(input, [&input, &options, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
+                                                                    std::shared_ptr<storm::logic::Formula const> const& states) {
+            STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
+            return storm::gbar::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(mpi.env, input.model.get(),
+                                                                                              storm::api::createTask<ValueType>(formula, true), options);
+        });
+    }
 }
 
 template<typename ValueType>
 void verifyWithExplorationEngine(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
-    STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
-    STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException,
-                    "Exploration does not support other data-types than floating points.");
-    verifyProperties<ValueType>(
-        input, [&input, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
-            STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
-            return storm::api::verifyWithExplorationEngine<ValueType>(mpi.env, input.model.get(), storm::api::createTask<ValueType>(formula, true));
-        });
+    if constexpr (storm::IsIntervalType<ValueType>) {
+        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exploration engine does not support interval value types.");
+    } else {
+        STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
+        STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException,
+                        "Exploration does not support other data-types than floating points.");
+        verifyProperties<ValueType>(
+            input, [&input, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
+                return storm::api::verifyWithExplorationEngine<ValueType>(mpi.env, input.model.get(), storm::api::createTask<ValueType>(formula, true));
+            });
+    }
 }
 
 template<typename ValueType>
@@ -1336,7 +1370,7 @@ void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const&
 
         std::unique_ptr<storm::modelchecker::CheckResult> filter;
         if (filterForInitialStates) {
-            filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
+            filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>>(sparseModel->getInitialStates());
         } else if (!states->isTrueFormula()) {  // No need to apply filter if it is the formula 'true'
             filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, createTask(states, false));
         }
@@ -1382,6 +1416,13 @@ void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const&
                     auto const& paretoRes = result->template asExplicitParetoCurveCheckResult<ValueType>();
                     storm::api::exportParetoScheduler(sparseModel, paretoRes.getPoints(), paretoRes.getSchedulers(), schedulerExportPath.string());
                 }
+            } else if (result->isExplicitQualitativeCheckResult()) {
+                if constexpr (storm::IsIntervalType<ValueType>) {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for interval models is not supported.");
+                } else {
+                    storm::api::exportScheduler(sparseModel, result->template asExplicitQualitativeCheckResult<ValueType>().getScheduler(),
+                                                schedulerExportPath.string());
+                }
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this value type.");
             }

src/storm-counterexamples/api/counterexamples.cpp

@@ -45,7 +45,7 @@ std::shared_ptr<storm::counterexamples::Counterexample> computeKShortestPathCoun
 
     storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula();
     std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
-    storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
+    storm::modelchecker::ExplicitQualitativeCheckResult<double> const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult<double>();
 
     // Check if counterexample is even possible
     storm::storage::BitVector phiStates(model->getNumberOfStates(), true);

src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -1022,8 +1022,8 @@ class MILPMinimalLabelSetGenerator {
             std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(env, untilFormula.getLeftSubformula());
             std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(env, untilFormula.getRightSubformula());
 
-            storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
-            storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
+            storm::modelchecker::ExplicitQualitativeCheckResult<T> const& leftQualitativeResult = leftResult->template asExplicitQualitativeCheckResult<T>();
+            storm::modelchecker::ExplicitQualitativeCheckResult<T> const& rightQualitativeResult = rightResult->template asExplicitQualitativeCheckResult<T>();
 
             phiStates = leftQualitativeResult.getTruthValuesVector();
             psiStates = rightQualitativeResult.getTruthValuesVector();
@@ -1032,7 +1032,7 @@ class MILPMinimalLabelSetGenerator {
 
             std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
 
-            storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
+            storm::modelchecker::ExplicitQualitativeCheckResult<T> const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult<T>();
 
             phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true);
             psiStates = subQualitativeResult.getTruthValuesVector();

src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -2157,8 +2157,8 @@ class SMTMinimalLabelSetGenerator {
             std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(env, untilFormula.getLeftSubformula());
             std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(env, untilFormula.getRightSubformula());
 
-            storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
-            storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
+            storm::modelchecker::ExplicitQualitativeCheckResult<T> const& leftQualitativeResult = leftResult->template asExplicitQualitativeCheckResult<T>();
+            storm::modelchecker::ExplicitQualitativeCheckResult<T> const& rightQualitativeResult = rightResult->template asExplicitQualitativeCheckResult<T>();
 
             result.phiStates = leftQualitativeResult.getTruthValuesVector();
             result.psiStates = rightQualitativeResult.getTruthValuesVector();
@@ -2167,7 +2167,7 @@ class SMTMinimalLabelSetGenerator {
 
             std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
 
-            storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
+            storm::modelchecker::ExplicitQualitativeCheckResult<T> const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult<T>();
 
             result.phiStates = storm::storage::BitVector(model.getNumberOfStates(), true);
             result.psiStates = subQualitativeResult.getTruthValuesVector();

src/storm-dft/modelchecker/DFTModelChecker.cpp

@@ -463,7 +463,7 @@ std::vector<ValueType> DFTModelChecker<ValueType>::checkModel(std::shared_ptr<st
             storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property, true)));
 
         if (result) {
-            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>(model->getInitialStates()));
             ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
             results.push_back(resultValue);
         } else {

src/storm-pars-cli/sampling.h

@@ -115,7 +115,7 @@ void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput c
                 valuationWatch.stop();
 
                 if (result) {
-                    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates()));
+                    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<SolveValueType>(model.getInitialStates()));
                 }
                 printInitialStatesResult<ValueType>(result, &valuationWatch, &valuation);
 

src/storm-pars-cli/solutionFunctions.h

@@ -31,7 +31,7 @@ void computeSolutionFunctionsWithSparseEngine(std::shared_ptr<storm::models::spa
             std::unique_ptr<storm::modelchecker::CheckResult> result =
                 storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
             if (result) {
-                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>(model->getInitialStates()));
             }
             return result;
         },

src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp

@@ -143,20 +143,20 @@ void SparseDerivativeInstantiationModelChecker<FunctionType, ConstantType>::spec
     if (this->currentFormula->isRewardOperatorFormula()) {
         auto subformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
             this->currentFormula->asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
-        target = propositionalChecker.check(subformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
+        target = propositionalChecker.check(subformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
     } else {
         if (this->currentFormula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
             auto rightSubformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
                 this->currentFormula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula());
             auto leftSubformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
                 this->currentFormula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula());
-            target = propositionalChecker.check(rightSubformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
-            avoid = propositionalChecker.check(leftSubformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            target = propositionalChecker.check(rightSubformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
+            avoid = propositionalChecker.check(leftSubformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
             avoid.complement();
         } else {
             auto subformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
                 this->currentFormula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
-            target = propositionalChecker.check(subformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            target = propositionalChecker.check(subformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
         }
     }
     initialStateModel = model.getStates("init").getNextSetIndex(0);