Implemented support for verifying IDTMCs

resources/examples/testfiles/idtmc/brp-32-2-intervals.pm

@@ -0,0 +1,145 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+// DTMC with interval probabilities for channels (Storm IMDP/IDTMC extension)
+
+dtmc
+
+// number of chunks
+const int N = 32;
+// maximum number of retransmissions
+const int MAX = 2;
+
+module sender
+
+	s : [0..6];
+	// 0 idle
+	// 1 next_frame
+	// 2 wait_ack
+	// 3 retransmit
+	// 4 success
+	// 5 error
+	// 6 wait sync
+	srep : [0..3];
+	// 0 bottom
+	// 1 not ok (nok)
+	// 2 do not know (dk)
+	// 3 ok (ok)
+	nrtr : [0..MAX];
+	i : [0..N];
+	bs : bool;
+	s_ab : bool;
+	fs : bool;
+	ls : bool;
+
+	// idle
+	[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+	// next_frame
+	[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+	// wait_ack
+	[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+	[TO_Msg] (s=2) -> (s'=3);
+	[TO_Ack] (s=2) -> (s'=3);
+	// retransmit
+	[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+	[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+	[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+	// success
+	[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+	[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+	// error
+	[SyncWait] (s=5) -> (s'=6);
+	// wait sync
+	[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+	r : [0..5];
+	// 0 new_file
+	// 1 fst_safe
+	// 2 frame_received
+	// 3 frame_reported
+	// 4 idle
+	// 5 resync
+	rrep : [0..4];
+	// 0 bottom
+	// 1 fst
+	// 2 inc
+	// 3 ok
+	// 4 nok
+	fr : bool;
+	lr : bool;
+	br : bool;
+	r_ab : bool;
+	recv : bool;
+
+	// new_file
+	[SyncWait] (r=0) -> (r'=0);
+	[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=true);
+	// fst_safe_frame
+	[] (r=1) -> (r'=2) & (r_ab'=br);
+	// frame_received
+	[] (r=2) & (r_ab=br) & (fr=true)  & (lr=false) -> (r'=3) & (rrep'=1);
+	[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+	[] (r=2) & (r_ab=br) & (fr=false) & (lr=true)  -> (r'=3) & (rrep'=3);
+	[aA] (r=2) & !(r_ab=br) -> (r'=4);
+	// frame_reported
+	[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+	// idle
+	[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=true);
+	[SyncWait] (r=4) & (ls=true)  -> (r'=5);
+	[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+	// resync
+	[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+module checker // prevents more than one frame being set
+
+	T : bool;
+
+	[NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+// ------------------------------------------------------------------
+// Channels with interval probabilities (IMDP-style ranges)
+// These match the spirit of the DRN ranges like [0.98,1] and [0.0001,0.02]
+// ------------------------------------------------------------------
+
+module channelK
+
+	k : [0..2];
+
+	// idle  -- message transfer may succeed or be lost
+	// (success prob in [0.98, 1], loss prob in [0.0001, 0.02])
+	[aF] (k=0) -> [0.98, 1] : (k'=1) + [0.0001, 0.02] : (k'=2);
+
+	// sending
+	[aG] (k=1) -> (k'=0);
+	// lost
+	[TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+	l : [0..2];
+
+	// idle  -- ack transfer may succeed or be lost
+	// (success prob in [0.99, 1], loss prob in [0.0001, 0.01])
+	[aA] (l=0) -> [0.99, 1] : (l'=1) + [0.0001, 0.01] : (l'=2);
+
+	// sending
+	[aB] (l=1) -> (l'=0);
+	// lost
+	[TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+rewards
+	[aF] i=1 : 1;
+endrewards
+
+label "error" = s=5;

resources/examples/testfiles/idtmc/die-intervals.pm

@@ -0,0 +1,29 @@
+// Knuth's model of a fair die using unfair coins, where the bias is controlled by nature.
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the dice
+	d : [0..6] init 0;
+
+	[] s=0 -> [1/3, 2/3] : (s'=1) + [1/3, 2/3] : (s'=2);
+	[] s=1 -> [1/3, 2/3] : (s'=3) + [1/3, 2/3] : (s'=4);
+	[] s=2 -> [1/3, 2/3] : (s'=5) + [1/3, 2/3] : (s'=6);
+	[] s=3 -> [1/3, 2/3] : (s'=1) + [1/3, 2/3] : (s'=7) & (d'=1);
+	[] s=4 -> [1/3, 2/3] : (s'=7) & (d'=2) + [1/3, 2/3] : (s'=7) & (d'=3);
+	[] s=5 -> [1/3, 2/3] : (s'=7) & (d'=4) + [1/3, 2/3] : (s'=7) & (d'=5);
+	[] s=6 -> [1/3, 2/3] : (s'=2) + [1/3, 2/3] : (s'=7) & (d'=6);
+	[] s=7 -> 1: (s'=7);
+
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards
+
+label "one" = s=7&d=1;
+label "two" = s=7&d=2;
+label "three" = s=7&d=3;
+label "done" = s=7;

resources/examples/testfiles/idtmc/tiny-01.drn

@@ -0,0 +1,20 @@
+@type: DTMC
+@parameters
+
+@reward_models
+
+@nr_states
+3
+@nr_choices
+3
+@model
+state 0 init
+	action 0
+		1 : [0.3, 0.5]
+		2 : [0.5, 0.7]
+state 1 target
+	action 0
+		1 : [1, 1]
+state 2
+	action 0
+		2 : [1, 1]

resources/examples/testfiles/idtmc/tiny-02.drn

@@ -0,0 +1,20 @@
+@type: DTMC
+@parameters
+
+@reward_models
+
+@nr_states
+3
+@nr_choices
+3
+@model
+state 0 init target
+	action 0
+		1 : [0.3, 0.5]
+		2 : [0.5, 0.7]
+state 1
+	action 0
+		1 : [1, 1]
+state 2 target
+	action 0
+		2 : [1, 1]

resources/examples/testfiles/idtmc/tiny-03.drn

@@ -0,0 +1,23 @@
+@type: DTMC
+@parameters
+
+@reward_models
+cost
+@nr_states
+4
+@nr_choices
+4
+@model
+state 0 init [0]
+	action 0
+		1 : [0.3, 0.7]
+		2 : [0.3, 0.7]
+state 1 [5]
+	action 0
+		3 : [1, 1]
+state 2 [10]
+	action 0
+		3 : [1, 1]
+state 3 target [0]
+    action 0
+        3 : [1, 1]

resources/examples/testfiles/idtmc/tiny-04.drn

@@ -0,0 +1,26 @@
+@type: DTMC
+@parameters
+
+@reward_models
+cost
+@nr_states
+5
+@nr_choices
+5
+@model
+state 0 init [0]
+	action 0
+		1 : [0.3, 0.7]
+		2 : [0.3, 0.7]
+state 1 [5]
+	action 0
+		3 : [1, 1]
+state 2 [10]
+	action 0
+		4 : [1, 1]
+state 3 target [0]
+    action 0
+        3 : [1, 1]
+state 4 [1]
+    action 0
+        4 : [1, 1]

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

@@ -1295,8 +1295,18 @@ void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const&
     auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
     auto verificationCallback = [&sparseModel, &ioSettings, &mpi](std::shared_ptr<storm::logic::Formula const> const& formula,
                                                                   std::shared_ptr<storm::logic::Formula const> const& states) {
-        bool filterForInitialStates = states->isInitialFormula();
-        auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+        auto createTask = [&ioSettings](auto const& f, bool onlyInitialStates) {
+            if constexpr (storm::IsIntervalType<ValueType>) {
+                STORM_LOG_THROW(ioSettings.isUncertaintyResolutionModeSet(), storm::exceptions::InvalidSettingsException,
+                                "Uncertainty resolution mode required for uncertain (interval) models.");
+                return storm::api::createTask<ValueType>(f, storm::solver::convert(ioSettings.getUncertaintyResolutionMode()), onlyInitialStates);
+            } else {
+                (void)ioSettings;  // suppress unused lambda capture warning. [[maybe_unused]] doesn't work for lambda captures.
+                return storm::api::createTask<ValueType>(f, onlyInitialStates);
+            }
+        };
+        bool const filterForInitialStates = states->isInitialFormula();
+        auto task = createTask(formula, filterForInitialStates);
         if (ioSettings.isExportSchedulerSet()) {
             task.setProduceSchedulers(true);
         }
@@ -1306,7 +1316,7 @@ void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const&
         if (filterForInitialStates) {
             filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(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, storm::api::createTask<ValueType>(states, false));
+            filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, createTask(states, false));
         }
         if (result && filter) {
             result->filter(filter->asQualitativeCheckResult());

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -26,6 +26,7 @@
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/solver/OptimizationDirection.h"
+#include "storm/solver/UncertaintyResolutionMode.h"
 #include "storm/solver/multiplier/Multiplier.h"
 #include "storm/storage/BitVector.h"
 #include "storm/utility/constants.h"
@@ -437,7 +438,7 @@ std::vector<ConstantType> SparseDtmcParameterLiftingModelChecker<SparseModelType
         solver->setHasUniqueSolution();
         solver->setHasNoEndComponents();
         // Uncertainty is not robust (=adversarial)
-        solver->setUncertaintyIsRobust(false);
+        solver->setUncertaintyResolutionMode(UncertaintyResolutionMode::Cooperative);
         if (lowerResultBound)
             solver->setLowerBound(lowerResultBound.value());
         if (upperResultBound) {

src/storm/api/verification.h

@@ -30,6 +30,7 @@
 #include "storm/settings/modules/AbstractionSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/EliminationSettings.h"
+#include "storm/settings/modules/IOSettings.h"
 
 #include "storm/storage/SymbolicModelDescription.h"
 
@@ -41,11 +42,22 @@ namespace storm {
 namespace api {
 
 template<typename ValueType>
+    requires(!storm::IsIntervalType<ValueType>)
 storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> createTask(std::shared_ptr<const storm::logic::Formula> const& formula,
                                                                             bool onlyInitialStatesRelevant = false) {
     return storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula, onlyInitialStatesRelevant);
 }
 
+template<typename ValueType>
+    requires(storm::IsIntervalType<ValueType>)
+storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> createTask(std::shared_ptr<const storm::logic::Formula> const& formula,
+                                                                            storm::UncertaintyResolutionMode uncertaintyResolution,
+                                                                            bool onlyInitialStatesRelevant = false) {
+    storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> checkTask(*formula, onlyInitialStatesRelevant);
+    checkTask.setUncertaintyResolutionMode(uncertaintyResolution);
+    return checkTask;
+}
+
 //
 // Verifying with Exploration engine
 //
@@ -93,24 +105,27 @@ template<typename ValueType>
 std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
                                                                          std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> const& dtmc,
                                                                          storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
-    if constexpr (storm::IsIntervalType<ValueType>) {
-        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify interval DTMCs.");
+    std::unique_ptr<storm::modelchecker::CheckResult> result;
+    if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination &&
+        storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) {
+        if constexpr (storm::IsIntervalType<ValueType>) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "We do not yet support using the elimination checker with intervals models.");
+        }
+        auto newTask = task.template convertValueType<
+            typename storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>>::SolutionType>();
+        storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
+        if (modelchecker.canHandle(newTask)) {
+            result = modelchecker.check(env, newTask);
+        }
     } else {
-        std::unique_ptr<storm::modelchecker::CheckResult> result;
-        if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination &&
-            storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) {
-            storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
-            if (modelchecker.canHandle(task)) {
-                result = modelchecker.check(env, task);
-            }
-        } else {
-            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
-            if (modelchecker.canHandle(task)) {
-                result = modelchecker.check(env, task);
-            }
+        storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
+        auto newTask =
+            task.template convertValueType<typename storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>::SolutionType>();
+        if (modelchecker.canHandle(newTask)) {
+            result = modelchecker.check(env, newTask);
         }
-        return result;
     }
+    return result;
 }
 
 template<typename ValueType>