possibility to disable reward variable creation

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

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) {
+            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;
             
             
         };