Support PRISM models with Intervals and CLI Extensions

resources/examples/testfiles/imdp/coin2.prism

@@ -0,0 +1,70 @@
+// Taken from https://github.com/prismmodelchecker/prism/tree/master/prism-examples/imdps/consensus
+// This case study is based on the shared coin protocol from the randomised consensus algorithm of Aspnes and Herlihy [AH90].
+// The models here are interval MDPs which consider the effect of unreliable or adversarial behaviour in the form of a biased coin instead of a fair coin [PLSS13].
+
+// [AH90] J. Aspnes and M. Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 15(1):441-460, 1990.
+// [PLSS13] A. Puggelli, W. Li, A. L. Sangiovanni-Vincentelli and S. A. Seshia Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties In Proc. 25th International Conference on Computer Aided Verification (CAV'13), 2013.
+
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90]
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=2;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// Only process 1 is biased
+const double bias1;
+const double bias2 = 0.0;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write
+	// 2 - check
+	// 3 - finished
+
+	// local coin
+	coin1 : [0..1];
+
+	// flip coin
+	[] (pc1=0)  -> [0.5-bias1,0.5+bias1] : (coin1'=0) & (pc1'=1) + [0.5-bias1,0.5+bias1] : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2,bias1=bias2] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 ;
+label "agree" = coin1=coin2 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards

resources/examples/testfiles/imdp/robot.prism

@@ -0,0 +1,30 @@
+// Taken from https://github.com/prismmodelchecker/prism/tree/master/prism-examples/imdps/simple
+
+mdp
+
+const double delta;
+const double p = 0.5-delta;
+const double q = 0.5+delta;
+
+module M
+
+s:[0..5];
+
+[east] s=0 -> 0.6:(s'=1) + 0.4:(s'=0);
+[south] s=0 -> 0.8:(s'=3) + 0.1:(s'=1) + 0.1:(s'=4);
+[east] s=1 -> [0.8,0.9]:(s'=2) + [0.1,0.2]:(s'=1);
+[south] s=1 -> [p,q]:(s'=4) + [1-q,1-p]:(s'=2);
+[stuck] s=2 -> 1:(s'=2);
+[stuck] s=3 -> 1:(s'=3);
+[east] s=4 -> 1:(s'=5);
+[west] s=4 -> 0.6:(s'=3) + 0.4:(s'=4);
+[north] s=5 -> 0.9:(s'=2) + 0.1:(s'=5);
+[west] s=5 -> 1:(s'=4);
+
+endmodule
+
+label "hazard" = s=1;
+label "goal1" = s=5;
+label "goal2" = s=2|s=3;
+
+rewards "time" true : 1; endrewards

src/storm-cli/storm-cli.cpp

@@ -29,23 +29,7 @@ void processOptions() {
     // Export symbolic input (if requested)
     storm::cli::exportSymbolicInput(symbolicInput);
 
-#ifdef STORM_HAVE_CARL
-    switch (mpi.verificationValueType) {
-        case storm::cli::ModelProcessingInformation::ValueType::Parametric:
-            storm::cli::processInputWithValueType<storm::RationalFunction>(symbolicInput, mpi);
-            break;
-        case storm::cli::ModelProcessingInformation::ValueType::Exact:
-            storm::cli::processInputWithValueType<storm::RationalNumber>(symbolicInput, mpi);
-            break;
-        case storm::cli::ModelProcessingInformation::ValueType::FinitePrecision:
-            storm::cli::processInputWithValueType<double>(symbolicInput, mpi);
-            break;
-    }
-#else
-    STORM_LOG_THROW(mpi.verificationValueType == storm::cli::ModelProcessingInformation::ValueType::FinitePrecision, storm::exceptions::NotSupportedException,
-                    "No exact numbers or parameters are supported in this build.");
-    storm::cli::processInputWithValueType<double>(symbolicInput, mpi);
-#endif
+    storm::cli::processInput(symbolicInput, mpi);
 }
 
 void initSettings(std::string const& name, std::string const& executableName) {

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

@@ -387,8 +387,7 @@ void parameterSpacePartitioningWithSparseEngine(std::shared_ptr<storm::models::s
     }
 }
 
-template<storm::dd::DdType DdType, typename ValueType>
-void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::ModelProcessingInformation const& mpi) {
+void processInput(cli::SymbolicInput&& input, storm::cli::ModelProcessingInformation const& mpi) {
     auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
     auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
     auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
@@ -400,14 +399,20 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
     STORM_LOG_THROW(parSettings.hasOperationModeBeenSet(), storm::exceptions::InvalidSettingsException, "An operation mode must be selected with --mode");
     std::shared_ptr<storm::models::ModelBase> model;
     if (!buildSettings.isNoBuildModelSet()) {
-        model = storm::cli::buildModel<DdType, ValueType>(input, ioSettings, mpi);
+        model = storm::cli::buildModel(input, ioSettings, mpi);
     }
 
     STORM_LOG_THROW(model, storm::exceptions::InvalidSettingsException, "No input model.");
     if (model) {
         model->printModelInformationToStream(std::cout);
     }
 
+    using ValueType = storm::RationalFunction;
+    auto const DdType = storm::dd::DdType::Sylvan;
+    STORM_LOG_THROW(model->supportsParameters(), storm::exceptions::UnexpectedException, "Expected a parametric model.");
+    STORM_LOG_THROW(model->isSparseModel() || model->getDdType().value() == DdType, storm::exceptions::UnexpectedException,
+                    "Expected type of model representation.");
+
     // If minimization is active and the model is parametric, parameters might be minimized away because they are inconsequential.
     // This is the set of all such inconsequential parameters.
     std::set<RationalFunctionVariable> omittedParameters;
@@ -445,7 +450,7 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
     if (!model) {
         return;
     } else {
-        storm::cli::exportModel<DdType, ValueType>(model, input);
+        storm::cli::castAndApply(model, [&input](auto const& m) { storm::cli::exportModel(m, input); });
     }
 
     // TODO move this.
@@ -533,7 +538,10 @@ void processOptions() {
     auto symbolicInput = storm::cli::parseSymbolicInput();
     storm::cli::ModelProcessingInformation mpi;
     std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput);
-    processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput, mpi);
+    mpi.ddType = storm::dd::DdType::Sylvan;
+    mpi.buildValueType = storm::cli::ModelProcessingInformation::ValueType::Parametric;
+    mpi.verificationValueType = storm::cli::ModelProcessingInformation::ValueType::Parametric;
+    processInput(std::move(symbolicInput), mpi);
 }
 }  // namespace pars
 }  // namespace storm

src/storm-parsers/parser/PrismParserGrammar.cpp

@@ -318,9 +318,16 @@ PrismParserGrammar::PrismParserGrammar(std::string const& filename, Iterator fir
         (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
     assignmentDefinitionList.name("assignment list");
 
+    likelihoodDefinition =
+        (numericalExpression >
+         qi::lit(":"))[qi::_val = phoenix::construct<typename storm::prism::Update::ExpressionPair>(qi::_1, storm::expressions::Expression())] |
+        (qi::lit("[") > numericalExpression > qi::lit(",") > numericalExpression > qi::lit("]") >
+         qi::lit(":"))[qi::_val = phoenix::construct<typename storm::prism::Update::ExpressionPair>(qi::_1, qi::_2)];
+
     updateDefinition =
-        (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this), manager->rational(1), qi::_1, qi::_r1)] |
-         ((numericalExpression > qi::lit(":") >
+        (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this),
+                                                           typename storm::prism::Update::ExpressionPair(), qi::_1, qi::_r1)] |
+         ((likelihoodDefinition >
            assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParserGrammar::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]));
     updateDefinition.name("update");
 
@@ -808,11 +815,14 @@ storm::prism::Assignment PrismParserGrammar::createAssignment(std::string const&
     return storm::prism::Assignment(manager->getVariable(variableName), assignedExpression, this->getFilename());
 }
 
-storm::prism::Update PrismParserGrammar::createUpdate(storm::expressions::Expression likelihoodExpression,
+storm::prism::Update PrismParserGrammar::createUpdate(typename storm::prism::Update::ExpressionPair likelihoodExpressions,
                                                       std::vector<storm::prism::Assignment> const& assignments,
                                                       GlobalProgramInformation& globalProgramInformation) const {
     ++globalProgramInformation.currentUpdateIndex;
-    return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpression, assignments, this->getFilename());
+    if (!likelihoodExpressions.first.isInitialized()) {
+        likelihoodExpressions.first = manager->rational(1);
+    }
+    return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpressions, assignments, this->getFilename());
 }
 
 storm::prism::Command PrismParserGrammar::createCommand(bool markovian, boost::optional<std::string> const& actionName,
@@ -1156,8 +1166,16 @@ storm::prism::Module PrismParserGrammar::createRenamedModule(std::string const&
                                                  moduleRenaming.getLineNumber());
                     }
                 }
-                updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments,
-                                     this->getFilename(), moduleRenaming.getLineNumber());
+                if (update.isLikelihoodInterval()) {
+                    typename storm::prism::Update::ExpressionPair likelihoodInterval{
+                        update.getLikelihoodExpressionInterval().first.substitute(expressionRenaming),
+                        update.getLikelihoodExpressionInterval().second.substitute(expressionRenaming)};
+                    updates.emplace_back(globalProgramInformation.currentUpdateIndex, likelihoodInterval, assignments, this->getFilename(),
+                                         moduleRenaming.getLineNumber());
+                } else {
+                    updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming),
+                                         assignments, this->getFilename(), moduleRenaming.getLineNumber());
+                }
                 ++globalProgramInformation.currentUpdateIndex;
             }
 

src/storm-parsers/parser/PrismParserGrammar.h

@@ -250,6 +250,7 @@ class PrismParserGrammar : public qi::grammar<Iterator, storm::prism::Program(),
     qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<bool>, Skipper> commandDefinition;
     qi::rule<Iterator, std::vector<storm::prism::Update>(GlobalProgramInformation&), Skipper> updateListDefinition;
     qi::rule<Iterator, storm::prism::Update(GlobalProgramInformation&), Skipper> updateDefinition;
+    qi::rule<Iterator, typename storm::prism::Update::ExpressionPair, Skipper> likelihoodDefinition;
     qi::rule<Iterator, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList;
     qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
     qi::rule<Iterator, std::string(), Skipper> knownActionName;
@@ -379,8 +380,9 @@ class PrismParserGrammar : public qi::grammar<Iterator, storm::prism::Program(),
                                                           storm::expressions::Expression rewardValueExpression,
                                                           GlobalProgramInformation& globalProgramInformation) const;
     storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const;
-    storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments,
-                                      GlobalProgramInformation& globalProgramInformation) const;
+    storm::prism::Update createUpdate(typename storm::prism::Update::ExpressionPair likelihoodExpressions,
+                                      std::vector<storm::prism::Assignment> const& assignments, GlobalProgramInformation& globalProgramInformation) const;
+
     storm::prism::Command createCommand(bool markovianCommand, boost::optional<std::string> const& actionName, storm::expressions::Expression guardExpression,
                                         std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const;
     storm::prism::Command createDummyCommand(boost::optional<std::string> const& actionName, GlobalProgramInformation& globalProgramInformation) const;