fixed unit tests

changed shield specification in tests

examples/shields/01_pre_shield_extraction.py

@@ -32,18 +32,18 @@ def pre_shield_extraction():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    test = formulas[0].shielding_expression
-    print(test)
-    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) #TODO Parameter for shield expression would be nice to have
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification) #, shielding_expression=shield_specification)
+
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
     
     assert result.has_scheduler
     assert result.has_shield
     
     shield = result.shield
+    pre_scheduler = shield.construct()
     
     for state_id in model.states:
-        choices = shield.construct().get_choice(state_id)
+        choices = pre_scheduler.get_choice(state_id)
         print(F"Allowed choices in state {state_id}, are {choices.choice_map} ")
 
 

examples/shields/02_post_shield_extraction.py

@@ -20,7 +20,7 @@ for allowed actions.
 
 def post_shield_extraction():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -33,14 +33,17 @@ def post_shield_extraction():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+    
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
     assert result.has_scheduler
     assert result.has_shield
     
     shield = result.shield
+    post_scheduler = shield.construct()
   
     for state_id in model.states:
-        choices = shield.construct().get_choice(state_id)
+        choices = post_scheduler.get_choice(state_id)
         print(F"Applied corrections in state {state_id}, are {choices.choice_map} ")
 
 

examples/shields/03_optimal_shield_extraction.py

@@ -22,17 +22,19 @@ def optimal_shield_extraction():
     options.set_build_all_labels()
     model = stormpy.build_sparse_model_with_options(program, options)
    
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
-
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.OPTIMAL) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
+    
     assert result.has_scheduler
     assert result.has_shield
    
     shield = result.shield
 
     state_ids = [x for x in model.states]
+    scheduler = shield.construct()
 
     for state_id in state_ids[0:50]:
-        choices = shield.construct().get_choice(state_id)
+        choices = scheduler.get_choice(state_id)
         print(F"Corrections in state {state_id}, are {choices.choice_map} ")
     
 

examples/shields/04_pre_shield_export.py

@@ -17,7 +17,7 @@ to a file
 
 def pre_schield():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -30,7 +30,10 @@ def pre_schield():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+    
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.Absolute, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
+    
     assert result.has_scheduler
     assert result.has_shield
     

examples/shields/05_post_shield_export.py

@@ -17,7 +17,7 @@ to a file
 
 def pre_schield():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<PostSafety, gamma=1> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -30,7 +30,8 @@ def pre_schield():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
     assert result.has_scheduler
     assert result.has_shield
     

examples/shields/06_optimal_shield_export.py

@@ -16,7 +16,7 @@ to a file
 
 def optimal_shield_export():
     path = stormpy.examples.files.prism_smg_lights
-    formula_str = "<Optimal> <<shield>> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]"
+    formula_str = "<<shield>> R{\"differenceWithInterferenceCost\"}min=? [ LRA ]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -27,7 +27,8 @@ def optimal_shield_export():
     options.set_build_all_labels()
     model = stormpy.build_sparse_model_with_options(program, options)
    
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.OPTIMAL)
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
     assert result.has_scheduler
     assert result.has_shield
 

examples/shields/07_pre_shield_simulator.py

@@ -15,7 +15,7 @@ Simulating a model with the usage of a pre shield
 
 def example_pre_shield_simulator():
     path = stormpy.examples.files.prism_mdp_cliff_walking
-    formula_str = "<PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -28,7 +28,10 @@ def example_pre_shield_simulator():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+    
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
+    
     assert result.has_scheduler
     assert result.has_shield
     

examples/shields/08_post_shield_simulator.py

@@ -14,7 +14,7 @@ Simulating a model with the usage of a post shield
 
 def example_post_shield_simulator():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<PostSafety, gamma=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"AgentIsInLavaAndNotDone\" ];"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]; Pmax=? [ F \"AgentIsInLavaAndNotDone\" ];"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -27,7 +27,8 @@ def example_post_shield_simulator():
 
     initial_state = model.initial_states[0]
     assert initial_state == 0
-    result = stormpy.model_checking(model, formulas[0])
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
     result2 = stormpy.model_checking(model, formulas[1], extract_scheduler=True)
 
     assert result.has_shield

examples/shields/09_pre_shield_decision_tree.py

@@ -22,7 +22,7 @@ from stormpy.decision_tree import create_decision_tree
 
 def export_shield_as_dot():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<PreSafety, lambda=0.9> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -34,8 +34,9 @@ def export_shield_as_dot():
     options.set_build_with_choice_origins(True)
     model = stormpy.build_sparse_model_with_options(program, options)
 
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) 
-
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.PRE_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
+    
     assert result.has_shield
 
     shield = result.shield

examples/shields/10_post_shield_decision_tree.py

@@ -12,7 +12,7 @@ from stormpy.decision_tree import create_decision_tree
 
 def export_shield_as_dot():
     path = stormpy.examples.files.prism_mdp_lava_simple
-    formula_str = "<PostSafety, gamma=1> Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
+    formula_str = "Pmax=? [G !\"AgentIsInLavaAndNotDone\"]"
 
     program = stormpy.parse_prism_program(path)
     formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
@@ -24,7 +24,8 @@ def export_shield_as_dot():
     options.set_build_with_choice_origins(True)
     model = stormpy.build_sparse_model_with_options(program, options)
 
-    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) 
+    shield_specification = stormpy.logic.ShieldExpression(stormpy.logic.ShieldingType.POST_SAFETY, stormpy.logic.ShieldComparison.RELATIVE, 0.9) 
+    result = stormpy.model_checking(model, formulas[0], extract_scheduler=True, shield_expression=shield_specification)
 
     assert result.has_shield
 

lib/stormpy/__init__.py

@@ -324,10 +324,7 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched
             task.set_produce_schedulers(extract_scheduler)
 
             if shield_expression is not None:
-                task.set_shielding_expression(shield_expression)
-            elif property.is_shielding_property():
-                task.set_shielding_expression(property.shielding_expression)
-
+                task.set_shielding_expression(shield_expression)            
 
             return core._model_checking_sparse_engine(model, task, environment=environment)
 

src/core/core.cpp

@@ -119,9 +119,9 @@ void define_build(py::module& m) {
     m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
 
-    m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask"));
-    m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder<storm::RationalNumber>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask"));
-    m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask"));
+    m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr);
+    m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder<storm::RationalNumber>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr);
+    m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<storm::RationalFunction>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr);
 
     py::class_<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder", "Model builder for sparse models")
         .def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model")
@@ -150,6 +150,9 @@ void define_build(py::module& m) {
             .def("set_build_choice_labels", &storm::builder::BuilderOptions::setBuildChoiceLabels, "Build with choice labels", py::arg("new_value")=true)
             .def("set_build_all_labels" , &storm::builder::BuilderOptions::setBuildAllLabels, "Build with all state labels", py::arg("new_value")=true)
             .def("set_build_all_reward_models", &storm::builder::BuilderOptions::setBuildAllRewardModels, "Build with all reward models", py::arg("new_value")=true);
+
+
+    py::class_<storm::generator::ActionMask<double>, std::shared_ptr<storm::generator::ActionMask<double>>> actionmask(m, "ActionMaskDouble");
 }
 
 void define_optimality_type(py::module& m) {

src/dft/analysis.cpp

@@ -9,8 +9,8 @@
 
 // Thin wrapper for DFT analysis
 template<typename ValueType>
-std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) {
-    typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false);
+std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant) {
+    typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant ,0.0, storm::builder::ApproximationHeuristic::DEPTH, false);
 
     std::vector<ValueType> results;
     for (auto result : dftResults) {
@@ -27,7 +27,7 @@ void define_analysis(py::module& m) {
         .def("is_relevant", &storm::utility::RelevantEvents::isRelevant, "Check whether the given name is a relevant event", py::arg("name"))
     ;
 
-    m.def("analyze_dft", &analyzeDFT<double>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=storm::utility::RelevantEvents());
+    m.def("analyze_dft", &analyzeDFT<double>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=storm::utility::RelevantEvents(), py::arg("allow_dc_for_relevant")=false);
 
     m.def("transform_dft", &storm::api::applyTransformations<double>, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"), py::arg("binary_fdeps"));
 
@@ -35,5 +35,5 @@ void define_analysis(py::module& m) {
 
     m.def("is_well_formed", &storm::api::isWellFormed<double>, "Check whether DFT is well-formed.", py::arg("dft"), py::arg("check_valid_for_analysis") = true);
 
-    m.def("compute_relevant_events", &storm::api::computeRelevantEvents<double>, "Compute relevant event ids from properties and additional relevant names", py::arg("dft"), py::arg("properties"), py::arg("additional_relevant_names") = std::vector<std::string>(), py::arg("allow_dc_relevant") = false);
+    m.def("compute_relevant_events", &storm::api::computeRelevantEvents<double>, "Compute relevant event ids from properties and additional relevant names", py::arg("dft"), py::arg("properties"), py::arg("additional_relevant_names") = std::vector<std::string>());
 }

src/logic/formulae.cpp

@@ -19,6 +19,7 @@ void define_formulae(py::module& m) {
         .value("PRE_SAFETY", storm::logic::ShieldingType::PreSafety)
         .value("OPTIMAL_PRE", storm::logic::ShieldingType::OptimalPre)
         .value("OPTIMAL_POST", storm::logic::ShieldingType::OptimalPost)
+        .value("OPTIMAL", storm::logic::ShieldingType::OptimalPost)
     ;
 
     py::enum_<storm::logic::ShieldComparison>(m, "ShieldComparison")