testing for writing to global vars from action-labelled models

CHANGELOG.md

@@ -18,6 +18,7 @@ Version 1.6.x
 - API: Simulation of prism-models 
 - API: Model-builder takes a callback function to prevent extension of particular actions, prism-to-explicit mapping can be exported
 - API: Export of dice-formatted expressions
+- Prism-language/explicit builder: Allow action names in commands writing to global variables if these clearly do not write to actions. 
 - Prism-language: n-ary predicates are supported (e.g., ExactlyOneOf)
 - Added support for continuous integration with Github Actions.
 - `storm-pars`: Exploit monotonicity for computing extremal values and parameter space partitioning.

resources/examples/testfiles/pomdp/globalvars.prism

@@ -0,0 +1,11 @@
+pomdp
+
+global s : [0..4] init 0;
+
+module F1
+[a] true -> (s'=1);
+endmodule
+
+module F2
+[b] true -> (s'=2);
+endmodule

src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp

@@ -131,6 +131,9 @@ TEST(ExplicitPrismModelBuilderTest, POMdp) {
     program = storm::utility::prism::preprocess(program, "slippery=0.4");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
 
+    program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/globalvars.prism");
+    model = storm::builder::ExplicitModelBuilder<double>(program).build();
+
     program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism");
     program = storm::utility::prism::preprocess(program, "sl=0.4");
     model = storm::builder::ExplicitModelBuilder<double>(program).build();