diff --git a/CHANGELOG.md b/CHANGELOG.md index b82cfeaf9..73685fe1e 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/resources/examples/testfiles/pomdp/globalvars.prism b/resources/examples/testfiles/pomdp/globalvars.prism new file mode 100644 index 000000000..5145057d1 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index d645f6ce3..5adeac32d 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/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> model = storm::builder::ExplicitModelBuilder(program).build(); + program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/globalvars.prism"); + model = storm::builder::ExplicitModelBuilder(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(program).build();