Bounds & co for pgcl.

Former-commit-id: 24797ada48 [formerly 8ec467baf1]
Former-commit-id: 75260b0b73

src/builder/JaniProgramGraphBuilder.cpp

@@ -1,16 +1,62 @@
 #include "JaniProgramGraphBuilder.h"
+
 #include "src/storage/jani/EdgeDestination.h"
 
 namespace storm {
     namespace builder {
         unsigned JaniProgramGraphBuilder::janiVersion = 1;
         
+        void JaniProgramGraphBuilder::addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) {
+            for (auto const& v : programGraph.getVariables()) {
+                if (isConstant(v.first)) {
+                    storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first));
+                    model.addConstant(constant);
+                } else if (v.second.hasBooleanType()) {
+                    storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false);
+                    automaton.addVariable(*janiVar);
+                    variables.emplace(v.first, janiVar);
+                } else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) {
+                    storm::storage::IntegerInterval const& bounds = variableBounds(v.first);
+                    if (bounds.hasLeftBound()) {
+                        if (bounds.hasRightBound()) {
+                            storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get()));
+                            variables.emplace(v.first, janiVar);
+                            automaton.addVariable(*janiVar);
+                        } else {
+                            // Not yet supported.
+                            assert(false);
+                        }
+                    } else {
+                        // Not yet supported.
+                        assert(false);
+                    }
+                } else {
+                    storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first));
+                    if(isRewardVariable(v.first)) {
+                        model.addVariable(*janiVar);
+                    } else {
+                        automaton.addVariable(*janiVar);
+                    }
+                    variables.emplace(v.first, janiVar);
+                    
+                }
+            }
+        }
+        
+        
+        
         storm::jani::OrderedAssignments JaniProgramGraphBuilder::buildOrderedAssignments(storm::jani::Automaton& automaton, storm::ppg::DeterministicProgramAction const& act) {
             std::vector<storm::jani::Assignment> vec;
             uint64_t level = 0;
             for(auto const& group : act) {
                 for(auto const& assignment : group) {
-                    vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level);
+                    if(isRewardVariable(assignment.first)) {
+                        std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> eval;
+                        eval.emplace((variables.at(assignment.first))->getExpressionVariable(), expManager->integer(0));
+                        vec.emplace_back(*(variables.at(assignment.first)), assignment.second.substitute(eval).simplify(), level);
+                    } else {
+                        vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level);
+                    }
                 }
                 ++level;
             }

src/builder/JaniProgramGraphBuilder.h

@@ -1,4 +1,5 @@
 #include <string>
+#include <unordered_map>
 
 #include "src/storage/ppg/ProgramGraph.h"
 #include "src/storage/jani/Model.h"
@@ -45,6 +46,10 @@ namespace storm {
             
         
             void restrictAllVariables(int64_t from, int64_t to) {
+                restrictAllVariables(storm::storage::IntegerInterval(from, to));
+            }
+            
+            void restrictAllVariables(storm::storage::IntegerInterval const& restr) {
                 for (auto const& v : programGraph.getVariables()) {
                     if(isConstant(v.first)) {
                         continue;
@@ -53,7 +58,7 @@ namespace storm {
                         continue; // Currently we ignore user bounds if we have bounded integers;
                     }
                     if(v.second.hasIntegerType() ) {
-                        userVariableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to));
+                        userVariableRestrictions.emplace(v.first, restr);
                     }
                 }
             }
@@ -63,7 +68,7 @@ namespace storm {
                 storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager);
                 storm::jani::Automaton mainAutomaton("main");
                 addProcedureVariables(*model, mainAutomaton);
-                janiLocId = addProcedureLocations(mainAutomaton);
+                janiLocId = addProcedureLocations(*model, mainAutomaton);
                 addVariableOoBLocations(mainAutomaton);
                 addEdges(mainAutomaton);
                 model->addAutomaton(mainAutomaton);
@@ -117,47 +122,23 @@ namespace storm {
                 return std::find(constants.begin(), constants.end(), i) != constants.end();
             }
             
-            void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) {
-                for (auto const& v : programGraph.getVariables()) {
-                    if (isConstant(v.first)) {
-                        storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first));
-                        model.addConstant(constant);
-                    } else if (v.second.hasBooleanType()) {
-                        storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false);
-                        automaton.addVariable(*janiVar);
-                        variables.emplace(v.first, janiVar);
-                    } else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) {
-                        storm::storage::IntegerInterval const& bounds = variableBounds(v.first);
-                        if (bounds.hasLeftBound()) {
-                            if (bounds.hasRightBound()) {
-                                storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get()));
-                                variables.emplace(v.first, janiVar);
-                                automaton.addVariable(*janiVar);
-                            } else {
-                                // Not yet supported.
-                                assert(false);
-                            }
-                        } else {
-                            // Not yet supported.
-                            assert(false);
-                        }
-                    } else {
-                        storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first));
-                        if(isRewardVariable(v.first)) {
-                            model.addVariable(*janiVar);
-                        } else {
-                            automaton.addVariable(*janiVar);
-                        }
-                        variables.emplace(v.first, janiVar);
-                        
-                    }
-                }
-            }
+            void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton);
             
-            std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Automaton& automaton) {
+            std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Model& model, storm::jani::Automaton& automaton) {
                 std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> result;
+                std::map<std::string, storm::jani::BooleanVariable const*> labelVars;
+                std::set<std::string> labels = programGraph.getLabels();
+                for(auto const& label : labels) {
+                    storm::jani::BooleanVariable janiVar(label, expManager->declareBooleanVariable(label), expManager->boolean(false), true);
+                    labelVars.emplace(label, &model.addVariable(janiVar));
+                }
+                
                 for (auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
                     storm::jani::Location janiLoc(janiLocationName(it->second.id()));
+                    for(auto const& label : programGraph.getLabels(it->second.id())) {
+                        assert(labelVars.count(label) > 0);
+                        janiLoc.addTransientAssignment(storm::jani::Assignment(*(labelVars.at(label)), expManager->boolean(true)));
+                    }
                     result[it->second.id()] = automaton.addLocation(janiLoc);
                     if (it->second.isInitial()) {
                         automaton.addInitialLocation(result[it->second.id()]);

src/settings/modules/PGCLSettings.cpp

@@ -28,7 +28,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("descriptio", "description of the variable restrictions").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("description", "description of the variable restrictions").build()).build());
             }
             
             bool PGCLSettings::isPgclFileSet() const {

src/storage/IntegerInterval.cpp

@@ -1,2 +1,30 @@
 #include "IntegerInterval.h"
 
+#include <iostream>
+#include <string>
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+bool starts_with(const std::string& s1, const std::string& s2) {
+    return s2.size() <= s1.size() && s1.compare(0, s2.size(), s2) == 0;
+}
+
+namespace storm {
+    namespace storage {
+        IntegerInterval parseIntegerInterval(std::string const& stringRepr) {
+            
+            
+            if(starts_with(stringRepr, "[") && stringRepr.at(stringRepr.size()-1) == ']') {
+                auto split = stringRepr.find(",");
+                std::string first = stringRepr.substr(1,split-1);
+                
+                std::string second = stringRepr.substr(split+1, stringRepr.size() - split - 2);
+                return IntegerInterval(stoi(first), stoi(second));
+                
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot parse " << stringRepr << " as integer interval");
+            }
+        }
+    }
+}

src/storage/IntegerInterval.h

@@ -95,5 +95,6 @@ namespace storm {
         };
         
         std::ostream& operator<<(std::ostream& os, IntegerInterval const& i);
+        IntegerInterval parseIntegerInterval(std::string const& stringRepr);
     }
 }

src/storage/ppg/ProgramGraph.h

@@ -49,10 +49,19 @@ namespace storm {
                 return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second);
             }
             
-            ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool aborted = false, std::vector<std::string> const& labels = {}) {
+            ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool observeViolated = false, bool aborted = false, std::vector<std::string> const& labels = {}) {
                 ProgramLocationIdentifier newId = freeLocationIndex();
                 assert(!hasLocation(newId));
                 locationLabels[newId] = labels;
+                if (successfulTermination) {
+                    locationLabels[newId].push_back(succesfulTerminationLabel);
+                }
+                if (observeViolated) {
+                    locationLabels[newId].push_back(observeViolatedLabel);
+                }
+                if (aborted) {
+                    locationLabels[newId].push_back(abortLabel);
+                }
                 return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second);
             }
             
@@ -98,7 +107,19 @@ namespace storm {
                 return res;
             }
             
+            std::set<std::string> getLabels() const {
+                std::set<std::string> result;
+                for(auto const& locEntry : locationLabels) {
+                    for(auto const& label : locEntry.second) {
+                        result.insert(label);
+                    }
+                }
+                return result;
+            }
             
+            std::vector<std::string> getLabels(ProgramLocationIdentifier loc) const {
+                return locationLabels.at(loc);
+            }
             
             bool hasLabel(ProgramLocationIdentifier loc, std::string const& label) const {
                 return std::find(locationLabels.at(loc).begin(), locationLabels.at(loc).end(), label) != locationLabels.at(loc).end();
@@ -288,8 +309,9 @@ namespace storm {
             ProgramEdgeIdentifier newEdgeId = 0;
             ProgramActionIdentifier newActionId = 1;
             ProgramActionIdentifier noActionId = 0;
-            std::string succesfulTerminationLabel = "__ret0__";
-            std::string abortLabel = "__ret1__";
+            std::string succesfulTerminationLabel = "_ret0_";
+            std::string abortLabel = "_ret1_";
+            std::string observeViolatedLabel = "_viol_";
             
             
         };

src/storm-pgcl.cpp

@@ -77,6 +77,11 @@ int main(const int argc, const char** argv) {
         }
         if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
             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;