From 9e2bc9b341f9da72a6161effcfb2fdcf925618f1 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sat, 22 May 2021 20:24:36 -0700
Subject: [PATCH] testing for writing to global vars from action-labelled
 models

---
 CHANGELOG.md                                          |  1 +
 resources/examples/testfiles/pomdp/globalvars.prism   | 11 +++++++++++
 .../storm/builder/ExplicitPrismModelBuilderTest.cpp   |  3 +++
 3 files changed, 15 insertions(+)
 create mode 100644 resources/examples/testfiles/pomdp/globalvars.prism

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<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();