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().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().isProgramVariableRestrictionSet()) { // TODO More fine grained control storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule().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 userVariableRestrictions; - /// Locations for variables that would have gone ot o + /// Locations for variables that would have gone out of bounds std::map varOutOfBoundsLocations; std::map janiLocId; std::map variables; @@ -176,6 +178,8 @@ namespace storm { std::shared_ptr expManager; /// The program graph to be translated storm::ppg::ProgramGraph const& programGraph; + /// Settings + JaniProgramGraphBuilderSetting pgbs; };