Add CVaR model checking for sparse MDP rewards

resources/examples/testfiles/mdp/cvar_bad_mec_mdp.nm

@@ -0,0 +1,16 @@
+mdp
+
+module main
+    s : [0..3] init 0;
+
+    [] s=0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+    [] s=1 -> 1 : (s'=1);
+    [] s=2 -> 1 : (s'=3);
+    [] s=3 -> 1 : (s'=2);
+endmodule
+
+label "target" = s=1;
+
+rewards "term"
+    s=1 : 4;
+endrewards

resources/examples/testfiles/mdp/cvar_branching_tradeoff_mdp.nm

@@ -0,0 +1,41 @@
+mdp
+
+module main
+    s : [0..10] init 0;
+
+    // Start: direct safe/balanced/risky options, plus an adaptive branch.
+    [safe]     s=0 -> 1 : (s'=3);
+    [balanced] s=0 -> 3/4 : (s'=1) + 1/4 : (s'=5);
+    [adaptive] s=0 -> 1/2 : (s'=8) + 1/2 : (s'=9);
+    [risky]    s=0 -> 1/2 : (s'=10) + 1/2 : (s'=7);
+
+    // Duplicate terminal rewards at 6 and 12 make threshold splitting observable.
+    [] s=1 -> 1 : (s'=1);
+    [] s=2 -> 1 : (s'=2);
+    [] s=3 -> 1 : (s'=3);
+    [] s=4 -> 1 : (s'=4);
+    [] s=5 -> 1 : (s'=5);
+    [] s=6 -> 1 : (s'=6);
+    [] s=7 -> 1 : (s'=7);
+
+    // After the adaptive probabilistic split, the scheduler can react to good/bad news.
+    [cash] s=8 -> 1 : (s'=4);
+    [push] s=8 -> 1/2 : (s'=6) + 1/2 : (s'=7);
+
+    [cash] s=9 -> 1 : (s'=2);
+    [push] s=9 -> 1/2 : (s'=10) + 1/2 : (s'=4);
+
+    [] s=10 -> 1 : (s'=10);
+endmodule
+
+label "target" = s=1 | s=2 | s=3 | s=4 | s=5 | s=6 | s=7 | s=10;
+
+rewards "term"
+    s=1 : 6;
+    s=2 : 6;
+    s=3 : 7;
+    s=4 : 10;
+    s=5 : 12;
+    s=6 : 12;
+    s=7 : 20;
+endrewards

resources/examples/testfiles/mdp/cvar_nonabsorbing_target_mdp.nm

@@ -0,0 +1,15 @@
+mdp
+
+module main
+    s : [0..2] init 0;
+
+    [] s=0 -> 1 : (s'=1);
+    [] s=1 -> 1 : (s'=2);
+    [] s=2 -> 1 : (s'=2);
+endmodule
+
+label "target" = s=1;
+
+rewards "term"
+    s=1 : 5;
+endrewards

resources/examples/testfiles/mdp/cvar_simple_mdp.nm

@@ -0,0 +1,19 @@
+mdp
+
+module main
+    s : [0..3] init 0;
+
+    [] s=0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+    [] s=0 -> 1 : (s'=3);
+    [] s=1 -> 1 : (s'=1);
+    [] s=2 -> 1 : (s'=2);
+    [] s=3 -> 1 : (s'=3);
+endmodule
+
+label "target" = s=1 | s=2 | s=3;
+
+rewards "term"
+    s=1 : 1;
+    s=2 : 3;
+    s=3 : 2;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_branching_tradeoff_mdp.nm

@@ -0,0 +1,21 @@
+
+mdp
+
+module main
+    s : [0..3] init 0;
+
+    [safe] s=0 -> 1 : (s'=3);
+    [risky] s=0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+    [low] s=1 -> 1 : (s'=3);
+    [high] s=2 -> 1 : (s'=3);
+    [] s=3 -> 1 : (s'=3);
+endmodule
+
+label "goal" = s=3;
+
+rewards "cost"
+    [safe] true : 6;
+    [risky] true : 1;
+    [low] true : 1;
+    [high] true : 7;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_deterministic_mdp.nm

@@ -0,0 +1,16 @@
+mdp
+
+module main
+    s : [0..2] init 0;
+
+    [step0] s=0 -> 1 : (s'=1);
+    [step1] s=1 -> 1 : (s'=2);
+    [] s=2 -> 1 : (s'=2);
+endmodule
+
+label "goal" = s=2;
+
+rewards "cost"
+    [step0] true : 2;
+    [step1] true : 3;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_reward_delayed_challenger_mdp.nm

@@ -0,0 +1,20 @@
+mdp
+
+module main
+    s : [0..3] init 0;
+
+    [det] s=0 -> 1 : (s'=3);
+    [lottery] s=0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+    [low] s=1 -> 1 : (s'=3);
+    [high] s=2 -> 1 : (s'=3);
+    [] s=3 -> 1 : (s'=3);
+endmodule
+
+label "goal" = s=3;
+
+rewards "reward"
+    [det] true : 6;
+    [lottery] true : 1;
+    [low] true : 7;
+    [high] true : 99;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_reward_geometric_mdp.nm

@@ -0,0 +1,14 @@
+mdp
+
+module main
+    s : [0..1] init 0;
+
+    [step] s=0 -> 1/2 : (s'=0) + 1/2 : (s'=1);
+    [] s=1 -> 1 : (s'=1);
+endmodule
+
+label "goal" = s=1;
+
+rewards "reward"
+    [step] true : 1;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_reward_prob1a_choice_violation_mdp.nm

@@ -0,0 +1,16 @@
+mdp
+
+module main
+    s : [0..1] init 0;
+
+    [loop] s=0 -> 1 : (s'=0);
+    [exit] s=0 -> 1 : (s'=1);
+    [] s=1 -> 1 : (s'=1);
+endmodule
+
+label "goal" = s=1;
+
+rewards "reward"
+    [loop] true : 1;
+    [exit] true : 1;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_reward_prob1a_probabilistic_violation_mdp.nm

@@ -0,0 +1,16 @@
+mdp
+
+module main
+    s : [0..2] init 0;
+
+    [split] s=0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+    [loop] s=1 -> 1 : (s'=1);
+    [] s=2 -> 1 : (s'=2);
+endmodule
+
+label "goal" = s=2;
+
+rewards "reward"
+    [split] true : 1;
+    [loop] true : 1;
+endrewards

resources/examples/testfiles/mdp/cvar_ssp_reward_safe_risky_mdp.nm

@@ -0,0 +1,20 @@
+mdp
+
+module main
+    s : [0..3] init 0;
+
+    [safe] s=0 -> 1 : (s'=3);
+    [risky] s=0 -> 1/5 : (s'=1) + 4/5 : (s'=2);
+    [low] s=1 -> 1 : (s'=3);
+    [high] s=2 -> 1 : (s'=3);
+    [] s=3 -> 1 : (s'=3);
+endmodule
+
+label "goal" = s=3;
+
+rewards "reward"
+    [safe] true : 6;
+    [risky] true : 1;
+    [low] true : 1;
+    [high] true : 9;
+endrewards

resources/examples/testfiles/mdp/cvar_target_reaching_mec_mdp.nm

@@ -0,0 +1,23 @@
+mdp
+
+module main
+    s : [0..4] init 0;
+
+    [] s=0 -> 1 : (s'=1);
+
+    [cycle12] s=1 -> 1 : (s'=2);
+    [takeLow] s=1 -> 1 : (s'=3);
+
+    [cycle21] s=2 -> 1 : (s'=1);
+    [takeRisk] s=2 -> 1/2 : (s'=3) + 1/2 : (s'=4);
+
+    [] s=3 -> 1 : (s'=3);
+    [] s=4 -> 1 : (s'=4);
+endmodule
+
+label "target" = s=3 | s=4;
+
+rewards "term"
+    s=3 : 4;
+    s=4 : 10;
+endrewards

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

@@ -432,6 +432,9 @@ inline std::pair<SymbolicInput, ModelProcessingInformation> preprocessSymbolicIn
     SymbolicInput output = input;
 
     // Preprocess properties (if requested)
+    STORM_LOG_THROW(!(ioSettings.isPropertiesAsMultiSet() && ioSettings.isCvarSet()), storm::exceptions::InvalidArgumentException,
+                    "Options '--propsasmulti' and '--cvar' can not be combined.");
+
     if (ioSettings.isPropertiesAsMultiSet()) {
         STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidArgumentException,
                         "Can not translate properties to multi-objective formula because no properties were specified.");
@@ -440,6 +443,14 @@ inline std::pair<SymbolicInput, ModelProcessingInformation> preprocessSymbolicIn
         output.properties = {storm::api::createMultiObjectiveProperty(output.properties, false)};
     }
 
+    if (ioSettings.isCvarSet()) {
+        STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidArgumentException,
+                        "Can not translate properties to a CVaR formula because no properties were specified.");
+        STORM_LOG_THROW(output.properties.size() == 1, storm::exceptions::InvalidArgumentException,
+                        "The '--cvar' option currently requires exactly one selected property.");
+        output.properties = {storm::api::createCvarProperty(output.properties.front(), ioSettings.getCvarAlpha())};
+    }
+
     // Substitute constant definitions in symbolic input.
     std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
     std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;

src/storm/api/properties.cpp

@@ -2,14 +2,31 @@
 
 #include <boost/algorithm/string.hpp>
 
-#include "storm/logic/Formula.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/logic/Formulas.h"
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/Property.h"
 #include "storm/storage/prism/Program.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
 
 namespace storm {
 namespace api {
+namespace {
+
+storm::RationalNumber parseCvarAlpha(std::string const& input) {
+    std::string strippedInput = boost::algorithm::trim_copy(input);
+    STORM_LOG_THROW(!strippedInput.empty(), storm::exceptions::InvalidArgumentException, "Unable to parse CVaR alpha '" << input << "'.");
+
+    storm::RationalNumber alpha = storm::utility::convertNumber<storm::RationalNumber>(strippedInput);
+
+    STORM_LOG_THROW(storm::utility::zero<storm::RationalNumber>() < alpha && alpha < storm::utility::one<storm::RationalNumber>(),
+                    storm::exceptions::InvalidArgumentException, "The CVaR alpha must be in the open interval (0, 1).");
+    return alpha;
+}
+
+}  // namespace
 
 std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties,
                                                                    std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
@@ -67,6 +84,17 @@ std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromPro
     return formulas;
 }
 
+storm::jani::Property createCvarProperty(storm::jani::Property const& property, storm::RationalNumber const& alpha) {
+    STORM_LOG_WARN_COND(property.getFilter().isDefault(),
+                        "Non-default property filter of property " << property.getName() << " will be dropped during conversion to CVaR property.");
+    auto cvarFormula = std::make_shared<storm::logic::CvarFormula>(alpha, property.getRawFormula());
+    return storm::jani::Property(property.getName(), cvarFormula, property.getUndefinedConstants(), property.getComment());
+}
+
+storm::jani::Property createCvarProperty(storm::jani::Property const& property, std::string const& alpha) {
+    return createCvarProperty(property, parseCvarAlpha(alpha));
+}
+
 storm::jani::Property createMultiObjectiveProperty(std::vector<storm::jani::Property> const& properties, bool lexicographic) {
     std::set<storm::expressions::Variable> undefConstants;
     std::string name = "";

src/storm/api/properties.h

@@ -7,6 +7,8 @@
 #include <string>
 #include <vector>
 
+#include "storm/adapters/RationalNumberAdapter.h"
+
 namespace storm {
 
 namespace jani {
@@ -36,6 +38,8 @@ std::vector<storm::jani::Property> substituteTranscendentalNumbersInProperties(s
 std::vector<storm::jani::Property> filterProperties(std::vector<storm::jani::Property> const& properties,
                                                     boost::optional<std::set<std::string>> const& propertyFilter);
 std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties);
+storm::jani::Property createCvarProperty(storm::jani::Property const& property, storm::RationalNumber const& alpha);
+storm::jani::Property createCvarProperty(storm::jani::Property const& property, std::string const& alpha);
 storm::jani::Property createMultiObjectiveProperty(std::vector<storm::jani::Property> const& properties, bool lexicographic);
 
 }  // namespace api

src/storm/environment/SubEnvironment.cpp

@@ -48,6 +48,7 @@ void SubEnvironment<EnvironmentType>::assertInitialized() const {
 
 template class SubEnvironment<InternalEnvironment>;
 
+template class SubEnvironment<CvarModelCheckerEnvironment>;
 template class SubEnvironment<ConditionalModelCheckerEnvironment>;
 template class SubEnvironment<MultiObjectiveModelCheckerEnvironment>;
 template class SubEnvironment<ModelCheckerEnvironment>;

src/storm/environment/modelchecker/AllModelCheckerEnvironments.h

@@ -1,5 +1,6 @@
 #pragma once
 
 #include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h"
+#include "storm/environment/modelchecker/CvarModelCheckerEnvironment.h"
 #include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
-#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
+#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"

src/storm/environment/modelchecker/CvarModelCheckerEnvironment.cpp

@@ -0,0 +1,34 @@
+#include "storm/environment/modelchecker/CvarModelCheckerEnvironment.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CvarSettings.h"
+
+namespace storm {
+
+CvarModelCheckerEnvironment::CvarModelCheckerEnvironment() {
+    auto const& cvarSettings = storm::settings::getModule<storm::settings::modules::CvarSettings>();
+    method = cvarSettings.getCvarMethod();
+    interpretationSelection = cvarSettings.getInterpretationSelection();
+}
+
+CvarModelCheckerEnvironment::~CvarModelCheckerEnvironment() {
+    // Intentionally left empty
+}
+
+storm::modelchecker::cvar::CvarMethod const& CvarModelCheckerEnvironment::getMethod() const {
+    return method;
+}
+
+void CvarModelCheckerEnvironment::setMethod(storm::modelchecker::cvar::CvarMethod value) {
+    method = value;
+}
+
+storm::modelchecker::cvar::CvarInterpretationSelection const& CvarModelCheckerEnvironment::getInterpretationSelection() const {
+    return interpretationSelection;
+}
+
+void CvarModelCheckerEnvironment::setInterpretationSelection(storm::modelchecker::cvar::CvarInterpretationSelection value) {
+    interpretationSelection = value;
+}
+
+}  // namespace storm