From 65fbe856e41479e6898a285c3bae232cc804e0f3 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Mon, 19 Dec 2016 16:30:11 +0100
Subject: [PATCH] possibility to disable reward variable creation

---
 src/storm-pgcl-cli/storm-pgcl.cpp              |  5 ++++-
 .../builder/JaniProgramGraphBuilder.h          | 18 +++++++++++-------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp
index bf5dc1c1e..b849cb264 100644
--- a/src/storm-pgcl-cli/storm-pgcl.cpp
+++ b/src/storm-pgcl-cli/storm-pgcl.cpp
@@ -76,13 +76,16 @@ int main(const int argc, const char** argv) {
             programGraphToDotFile(*progGraph);
         }
         if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
+            storm::builder::JaniProgramGraphBuilderSetting settings;
+            // To disable reward detection, uncomment the following line
+            // TODO add a setting for this.
+            // settings.filterRewardVariables = false;
             storm::builder::JaniProgramGraphBuilder builder(*progGraph);
             if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isProgramVariableRestrictionSet()) {
                 // TODO More fine grained control
                 storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getProgramVariableRestrictions());
                 builder.restrictAllVariables(restr);
             }
-            builder.restrictAllVariables(0, 120);
             storm::jani::Model* model = builder.build();
             delete progGraph;
             handleJani(*model);
diff --git a/src/storm-pgcl/builder/JaniProgramGraphBuilder.h b/src/storm-pgcl/builder/JaniProgramGraphBuilder.h
index 34b5dd5d7..beb6c1aed 100644
--- a/src/storm-pgcl/builder/JaniProgramGraphBuilder.h
+++ b/src/storm-pgcl/builder/JaniProgramGraphBuilder.h
@@ -19,15 +19,21 @@ namespace storm {
         };
         
         struct JaniProgramGraphBuilderSetting {
+            /// Method how to obtain domain for the variables; currently only unrestricted is supported
             JaniProgramGraphVariableDomainMethod variableDomainMethod = JaniProgramGraphVariableDomainMethod::Unrestricted;
+            /// If this is true, reward variables will be given special treatment, effectively removing them from the state space.
+            /// Disable in order to obtain full state space.
+            bool filterRewardVariables = true;
         };
         
         class JaniProgramGraphBuilder {
         public:
             static unsigned janiVersion;
             
-            JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) {
-                rewards = programGraph.rewardVariables();
+            JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg, JaniProgramGraphBuilderSetting const& pgbs = JaniProgramGraphBuilderSetting()) : programGraph(pg), pgbs(pgbs) {
+                if (pgbs.filterRewardVariables) {
+                    rewards = programGraph.rewardVariables();
+                }
                 constants = programGraph.constants();
                 auto boundedVars = programGraph.constantAssigned();
                 for(auto const& v : boundedVars) {
@@ -41,10 +47,6 @@ namespace storm {
                 }
             }
             
-            //void addVariableRestriction(storm::expressions::Variable const& var, storm::IntegerInterval const& interval ) {
-                
-            //}
-            
         
             void restrictAllVariables(int64_t from, int64_t to) {
                 restrictAllVariables(storm::storage::IntegerInterval(from, to));
@@ -167,7 +169,7 @@ namespace storm {
             /// Restrictions on variables (provided by users)
             std::map<uint64_t, storm::storage::IntegerInterval> userVariableRestrictions;
             
-            /// Locations for variables that would have gone ot o
+            /// Locations for variables that would have gone out of bounds
             std::map<uint64_t, uint64_t> varOutOfBoundsLocations;
             std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> janiLocId;
             std::map<storm::ppg::ProgramVariableIdentifier, storm::jani::Variable*> variables;
@@ -176,6 +178,8 @@ namespace storm {
             std::shared_ptr<storm::expressions::ExpressionManager> expManager;
             /// The program graph to be translated
             storm::ppg::ProgramGraph const& programGraph;
+            /// Settings
+            JaniProgramGraphBuilderSetting pgbs;
             
             
         };