towards nice pgcl - jani support

Former-commit-id: 4465a9566a [formerly c5fd489dab]
Former-commit-id: 34f78bdd4f

src/builder/JaniProgramGraphBuilder.cpp

@@ -47,7 +47,13 @@ namespace storm {
             storm::expressions::Expression newGuard;
             newGuard = expManager->boolean(true);
             if (edge.getAction().isProbabilistic()) {
-            
+                // No check necessary currently, but at least we should statically check that the bounds are okay.
+                storm::ppg::ProbabilisticProgramAction const& act = static_cast<storm::ppg::ProbabilisticProgramAction const&>(edge.getAction());
+                if (isUserRestrictedVariable(act.getVariableIdentifier())) {
+                    storm::storage::IntegerInterval const& bound = variableRestrictions.at(act.getVariableIdentifier());
+                    storm::storage::IntegerInterval supportInterval = act.getSupportInterval();
+                    STORM_LOG_THROW(bound.contains(supportInterval), storm::exceptions::NotSupportedException, "User provided bounds must contain all constant expressions");
+                }
             } else {
                 storm::ppg::DeterministicProgramAction const& act = static_cast<storm::ppg::DeterministicProgramAction const&>(edge.getAction());
                 STORM_LOG_THROW(act.nrLevels() <= 1, storm::exceptions::NotSupportedException, "Multi-level assignments with user variable bounds not supported");
@@ -81,7 +87,10 @@ namespace storm {
             for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
                 ppg::ProgramLocation const& loc = it->second;
                 if (loc.nrOutgoingEdgeGroups() == 0) {
-                    // TODO deadlock!
+                    storm::jani::OrderedAssignments oa;
+                    storm::jani::EdgeDestination dest(janiLocId.at(loc.id()), expManager->integer(1), oa);
+                    storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, expManager->boolean(true), {dest});
+                    automaton.addEdge(e);
                 } else if (loc.nrOutgoingEdgeGroups() == 1) {
                     for(auto const& edge :  **(loc.begin())) {
                         std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> checks = addVariableChecks(*edge);

src/builder/JaniProgramGraphBuilder.h

@@ -25,7 +25,7 @@ namespace storm {
             static unsigned janiVersion;
             
             JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) {
-                transients = programGraph.transientVariables();
+                rewards = programGraph.rewardVariables();
             }
             
             virtual ~JaniProgramGraphBuilder() {
@@ -41,9 +41,11 @@ namespace storm {
         
             void restrictAllVariables(int64_t from, int64_t to) {
                 for (auto const& v : programGraph.getVariables()) {
+                    if(v.second.hasIntegerType()) {
                         variableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to));
                     }
                 }
+            }
             
             storm::jani::Model* build(std::string const& name = "program_graph") {
                 expManager = programGraph.getExpressionManager();
@@ -78,25 +80,29 @@ namespace storm {
             std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge);
             
             bool isUserRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) {
-                return variableRestrictions.count(i) == 1 && !isTransientVariable(i);
+                return variableRestrictions.count(i) == 1 && !isRewardVariable(i);
             }
             
             bool isRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) {
                 // Might be different from user restricted in near future.
-                return variableRestrictions.count(i) == 1 && !isTransientVariable(i);
+                return variableRestrictions.count(i) == 1 && !isRewardVariable(i);
             }
             
-            bool isTransientVariable(storm::ppg::ProgramVariableIdentifier i) {
-                return std::find(transients.begin(), transients.end(), i) != transients.end();
+            bool isRewardVariable(storm::ppg::ProgramVariableIdentifier i) {
+                return std::find(rewards.begin(), rewards.end(), i) != rewards.end();
             }
             
             void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) {
                 for (auto const& v : programGraph.getVariables()) {
-                    if(isRestrictedVariable(v.first) && !isTransientVariable(v.first)) {
+                    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 = variableRestrictions.at(v.first);
                         if (bounds.hasLeftBound()) {
                             if (bounds.hasRightBound()) {
-                                storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, expManager->integer(0), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get()));
+                                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 {
@@ -108,8 +114,8 @@ namespace storm {
                             assert(false);
                         }
                     } else {
-                        storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, expManager->integer(0), isTransientVariable(v.first));
-                        if(isTransientVariable(v.first)) {
+                        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);
@@ -134,7 +140,7 @@ namespace storm {
             
             void addVariableOoBLocations(storm::jani::Automaton& automaton) {
                 for(auto const& restr : variableRestrictions) {
-                    if(!isTransientVariable(restr.first)) {
+                    if(!isRewardVariable(restr.first)) {
                         storm::jani::Location janiLoc(janiVariableOutOfBoundsLocationName(restr.first));
                         uint64_t locId = automaton.addLocation(janiLoc);
                         varOutOfBoundsLocations[restr.first] = locId;
@@ -143,7 +149,7 @@ namespace storm {
                 }
             }
             /// Transient variables
-            std::vector<storm::ppg::ProgramVariableIdentifier> transients;
+            std::vector<storm::ppg::ProgramVariableIdentifier> rewards;
             /// Restrictions on variables
             std::map<uint64_t, storm::storage::IntegerInterval> variableRestrictions;
             /// Locations for variables that would have gone ot o

src/builder/ProgramGraphBuilder.h

@@ -108,7 +108,7 @@ namespace storm {
             ProgramGraphBuilder(storm::pgcl::PgclProgram const& program)
             : program(program)
             {
-                graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariables());
+                graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariableDeclarations());
                 noActionId = graph->getNoActionId();
                 
             }
@@ -116,10 +116,10 @@ namespace storm {
             void run() {
                 currentStack.push_back(graph->addLocation(true));
                 // Terminal state.
-                nextStack.push_back(graph->addLocation(false));
+                nextStack.push_back(graph->addLocation(false, true));
                 // Observe Violated State.
                 if (program.hasObserve()) {
-                    observeFailedState = graph->addLocation();
+                    observeFailedState = graph->addLocation(false, false, true);
                 }
                 buildBlock(program);
             }

src/storage/pgcl/PgclProgram.cpp

@@ -4,11 +4,12 @@
 
 namespace storm {
     namespace pgcl {
-        PgclProgram::PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve) :
+        PgclProgram::PgclProgram(std::vector<VariableDeclaration> variables, vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve) :
             PgclBlock(statements,
                       expressions, hasLoop, hasNondet, hasObserve),
-            locationToStatement(locationToStatement)
+            locationToStatement(locationToStatement),variables(variables)
         {
+            // Intentionally left empty.
         }
 
         
@@ -25,6 +26,10 @@ namespace storm {
             return vars;
         }
         
+        std::vector<storm::pgcl::VariableDeclaration> const& PgclProgram::getVariableDeclarations() const {
+            return variables;
+        }
+
         std::ostream& operator<<(std::ostream& stream, PgclProgram& program) {
             storm::pgcl::StatementPrinterVisitor printer(stream);
             for(iterator statement = program.begin(); statement != program.end(); statement++) {

src/storage/pgcl/PgclProgram.h

@@ -2,6 +2,7 @@
 
 #include <vector>
 #include "Block.h"
+#include "VariableDeclaration.h"
 #include "src/storage/pgcl/Statement.h"
 #include "src/storage/pgcl/StatementPrinterVisitor.h"
 #include "src/storage/expressions/ExpressionManager.h"
@@ -36,7 +37,7 @@ namespace storm {
              * statement.
              * @param hasParam Whether the program is parameterized.
              */
-            PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve);
+            PgclProgram(std::vector<VariableDeclaration> variables, vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve);
             
             PgclProgram(const PgclProgram & orig) = default;
             
@@ -48,6 +49,9 @@ namespace storm {
             vector getLocationToStatementVector();
             
             std::vector<storm::expressions::Variable> getVariables() const;
+            std::vector<storm::pgcl::VariableDeclaration> const& getVariableDeclarations() const;
+            
+            
             
         private:
             /**
@@ -56,6 +60,7 @@ namespace storm {
              * recursion is resolved here.
              */
             vector locationToStatement;
+            std::vector<storm::pgcl::VariableDeclaration> variables;
         };
         /**
          * Prints every statement of the program along with their location

src/storage/pgcl/VariableDeclaration.cpp

@@ -0,0 +1 @@
+#include "VariableDeclaration.h"

src/storage/pgcl/VariableDeclaration.h

@@ -0,0 +1,36 @@
+#pragma once
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+
+namespace storm {
+    namespace pgcl {
+        class VariableDeclaration {
+        public:
+
+            VariableDeclaration(storm::expressions::Variable const& var, storm::expressions::Expression const& exp)
+            : variable(var), initialValue(exp)
+            {
+                // Not implemented.
+            }
+            
+            storm::expressions::Variable const& getVariable() const {
+                return variable;
+            }
+            
+            storm::expressions::Expression const& getInitialValueExpression() const {
+                return initialValue;
+            }
+            
+        private:
+            storm::expressions::Variable variable;
+            storm::expressions::Expression initialValue;
+            
+        };
+    }
+}
+
+
+
+
+

src/storage/ppg/ProgramAction.h

@@ -1,5 +1,6 @@
 #pragma once
 #include "defines.h"
+#include "src/storage/IntegerInterval.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/Variable.h"
 #include "src/storage/expressions/ExpressionManager.h"
@@ -57,6 +58,24 @@ namespace storm {
             
             std::string const& getVariableName() const;
             
+            ProgramVariableIdentifier getVariableIdentifier() const {
+                return var;
+            }
+            
+            storm::storage::IntegerInterval getSupportInterval() const {
+                assert(!values.empty());
+                int64_t min = values.front().value;
+                int64_t max = values.front().value;
+                for (auto const& valEntry : values) {
+                    if (valEntry.value < min) {
+                        min = valEntry.value;
+                    } else if (valEntry.value > max) {
+                        max = valEntry.value;
+                    }
+                }
+                return storm::storage::IntegerInterval(min, max);
+            }
+            
             iterator begin() {
                 return values.begin();
             }

src/storage/ppg/ProgramEdgeGroup.h

@@ -8,6 +8,7 @@ namespace storm {
         
         class ProgramEdgeGroup {
         public:
+            using iterator = std::vector<ProgramEdge*>::iterator;
             using const_iterator = std::vector<ProgramEdge*>::const_iterator;
             
             ProgramEdgeGroup(ProgramGraph* graph, ProgramEdgeGroupIdentifier id, ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability)
@@ -33,6 +34,14 @@ namespace storm {
                 return edges.back();
             }
             
+            iterator begin() {
+                return edges.begin();
+            }
+            
+            iterator end() {
+                return edges.end();
+            }
+            
             const_iterator begin() const {
                 return edges.begin();
             }

src/storage/ppg/ProgramGraph.cpp

@@ -5,7 +5,7 @@
 namespace storm {
     namespace ppg {
         
-        std::vector<ProgramVariableIdentifier> ProgramGraph::transientVariables() const {
+        std::vector<ProgramVariableIdentifier> ProgramGraph::noeffectVariables() const {
             std::vector<ProgramVariableIdentifier> transientCandidates = variablesNotInGuards();
             bool removedCandidate = true; // tmp
             while(removedCandidate && !transientCandidates.empty()) {
@@ -29,6 +29,58 @@ namespace storm {
             return transientCandidates;
         }
         
+        std::pair<bool,bool> ProgramGraph::checkIfRewardVariableHelper(storm::expressions::Variable const& var, std::unordered_map<ProgramActionIdentifier, DeterministicProgramAction> const& detActions) const {
+            bool pos = true;
+            bool first = true;
+            for (auto const& act : detActions) {
+                for (auto const& group : act.second) {
+                    for (auto const& assignment : group) {
+                        if (assignment.first == var.getIndex()) {
+                            //storm::expressions::Expression expr = (assignment.second - var.getExpression()).simplify();
+                            if(!assignment.second.isLinear()) {
+                                return {false, true};
+                            }
+                            auto const& vars = assignment.second.getVariables();
+                            if(vars.empty() || vars.size() > 1) {
+                                return {false, true};
+                            }
+                            if(vars.begin()->getIndex() == assignment.first) {
+                                std::map<storm::expressions::Variable, storm::expressions::Expression> eta0;
+                                std::map<storm::expressions::Variable, storm::expressions::Expression> eta1;
+                                eta0.emplace(var, expManager->integer(0));
+                                eta1.emplace(var, expManager->integer(1));
+                                if(assignment.second.substitute(eta1).evaluateAsInt() - assignment.second.substitute(eta0).evaluateAsInt() != 1) {
+                                    return {false, true};
+                                }
+                                if(assignment.second.substitute(eta0).evaluateAsInt() < 0) {
+                                    if(!first && pos) {
+                                        return {false, true};
+                                    }
+                                    pos = false;
+                                }
+                                first = false;
+                            }
+                        }
+                    }
+                }
+            }
+            return {true, pos};
+        }
+        
+        std::vector<ProgramVariableIdentifier> ProgramGraph::rewardVariables() const {
+            std::vector<ProgramVariableIdentifier> rewardCandidates = noeffectVariables();
+            std::vector<ProgramVariableIdentifier> result;
+            for (auto const& var : rewardCandidates) {
+                if(variables.at(var).hasIntegerType()) {
+                    // TODO add some checks here; refine the evaluate as int stuff.
+                    if(initialValues.at(var).evaluateAsInt() == 0 && checkIfRewardVariableHelper(variables.at(var), this->deterministicActions).first) {
+                        result.push_back(var);
+                    }
+                }
+            }
+            return result;
+        }
+        
         std::vector<ProgramVariableIdentifier> ProgramGraph::variablesNotInGuards() const {
             std::vector<ProgramVariableIdentifier> result;
             std::set<storm::expressions::Variable> contained;
@@ -36,11 +88,6 @@ namespace storm {
                 for (auto const& edgegroup : loc.second) {
                     for (auto const& edge : *edgegroup) {
                         auto conditionVars = edge->getCondition().getVariables();
-                        std::cout << "Guard " << edge->getCondition() << " contains ";
-                        for (auto const& cv : conditionVars) {
-                            std::cout << cv.getName() << ", ";
-                        }
-                        std::cout << std::endl;
                         contained.insert(conditionVars.begin(), conditionVars.end());
                     }
                 }
@@ -54,6 +101,18 @@ namespace storm {
             return result;
         }
         
+//        void ProgramGraph::mergeActions() {
+//            auto initialLocs = initialLocations();
+//            assert(initialLocs.size() == 1);
+//            // For now, we only follow the unique path.
+//            ProgramLocationIdentifier currentLocId = initialLocs.front();
+//            while(locations.at(currentLocId).hasUniqueSuccessor()) {
+//                auto& edgeGroup = **locations.at(currentLocId()).begin();
+//                auto& edge = **edgeGroup.begin();
+//                
+//            }
+//        }
+        
         void ProgramGraph::printDot(std::ostream& os) const {
             os << "digraph ppg {" << std::endl;
             

src/storage/ppg/ProgramGraph.h

@@ -10,6 +10,8 @@
 #include "ProgramEdgeGroup.h"
 #include "ProgramAction.h"
 
+#include "src/storage/pgcl/VariableDeclaration.h"
+
 namespace storm {
     namespace ppg {
         /**
@@ -21,9 +23,10 @@ namespace storm {
             using EdgeGroupIterator = ProgramLocation::EdgeGroupIterator;
             using ConstLocationIterator = std::unordered_map<ProgramLocationIdentifier, ProgramLocation>::const_iterator;
             
-            ProgramGraph(std::shared_ptr<storm::expressions::ExpressionManager> const& expManager, std::vector<storm::expressions::Variable> const& variables) : expManager(expManager), variables() {
+            ProgramGraph(std::shared_ptr<storm::expressions::ExpressionManager> const& expManager, std::vector<storm::pgcl::VariableDeclaration> const& variables) : variables(), expManager(expManager) {
                 for(auto const& v : variables) {
-                    this->variables.emplace(v.getIndex(), v);
+                    this->variables.emplace(v.getVariable().getIndex(), v.getVariable());
+                    this->initialValues.emplace(v.getVariable().getIndex(), v.getInitialValueExpression());
                 }
                 // No Action:
                 deterministicActions.emplace(noActionId, DeterministicProgramAction(this, noActionId));
@@ -46,9 +49,10 @@ namespace storm {
                 return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second);
             }
             
-            ProgramLocation* addLocation(bool isInitial = false) {
+            ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool aborted = false, std::vector<std::string> const& labels = {}) {
                 ProgramLocationIdentifier newId = freeLocationIndex();
                 assert(!hasLocation(newId));
+                locationLabels[newId] = labels;
                 return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second);
             }
             
@@ -92,9 +96,25 @@ namespace storm {
                 }
                 
                 return res;
+            }
+            
             
+            
+            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();
             }
             
+            bool hasSuccessfulTerminationLabel(ProgramLocationIdentifier loc) const {
+                return hasLabel(loc, succesfulTerminationLabel);
+            }
+            
+            bool hasAbortLabel(ProgramLocationIdentifier loc) const {
+                return hasLabel(loc, abortLabel);
+            }
+            
+            bool hasTerminationLabel(ProgramLocationIdentifier loc) const {
+                return hasSuccessfulTerminationLabel(loc) || hasAbortLabel(loc);
+            }
             
             ProgramActionIdentifier getNoActionId() const {
                 return noActionId;
@@ -163,6 +183,11 @@ namespace storm {
                 return variables.size();
             }
             
+            storm::expressions::Expression getInitialValue(ProgramVariableIdentifier v) const {
+                return initialValues.at(v);
+            }
+            
+            void collectInitialValues();
             
             ConstLocationIterator locationBegin() const {
                 return locations.begin();
@@ -180,7 +205,10 @@ namespace storm {
                 return expManager;
             }
             
-            std::vector<ProgramVariableIdentifier> transientVariables() const;
+            std::vector<ProgramVariableIdentifier> noeffectVariables() const;
+            
+            std::vector<ProgramVariableIdentifier> rewardVariables() const;
+            
             
             void checkValid() {
                 
@@ -195,11 +223,25 @@ namespace storm {
             void printDot(std::ostream& os) const;
         protected:
             
+            
+            std::vector<ProgramLocationIdentifier> initialLocationIdentifiers() const {
+                std::vector<ProgramLocationIdentifier> result;
+                for (auto const& loc : locations) {
+                    if(loc.second.isInitial()) {
+                        result.push_back(loc.first);
+                    }
+                }
+                return result;
+            }
+            
             /**
              *  Returns the set of variables which do not occur in guards.
              */
             std::vector<ProgramVariableIdentifier> variablesNotInGuards() const;
             
+            std::pair<bool,bool> checkIfRewardVariableHelper(storm::expressions::Variable const& var, std::unordered_map<ProgramActionIdentifier, DeterministicProgramAction> const& detActions) const;
+
+            
             ProgramLocation& getLocation(ProgramLocationIdentifier id) {
                 return locations.at(id);
             }
@@ -228,7 +270,10 @@ namespace storm {
             std::unordered_map<ProgramLocationIdentifier, ProgramLocation> locations;
             storm::expressions::Expression initialValueRestriction;
             std::unordered_map<ProgramVariableIdentifier, storm::expressions::Variable> variables;
-            
+            ///
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Expression> initialValues;
+            // If heavily used, then it might be better to use a bitvector and a seperate list for the names.
+            std::unordered_map<ProgramVariableIdentifier, std::vector<std::string>> locationLabels;
             std::shared_ptr<storm::expressions::ExpressionManager> expManager;
         private:
             // Helper for IDs, may be changed later.
@@ -237,6 +282,9 @@ namespace storm {
             ProgramEdgeIdentifier newEdgeId = 0;
             ProgramActionIdentifier newActionId = 1;
             ProgramActionIdentifier noActionId = 0;
+            std::string succesfulTerminationLabel = "__ret0__";
+            std::string abortLabel = "__ret1__";
+            
             
         };
     }

src/storage/ppg/ProgramLocation.h

@@ -46,6 +46,10 @@ namespace storm {
                 return false;
             }
             
+            bool hasUniqueSuccessor() const {
+                return nrOutgoingEdgeGroups() == 1 && !hasNonDeterminism();
+            }
+            
             const_iterator begin() const {
                 return edgeGroups.begin();
             }

src/storm-pgcl.cpp

@@ -34,7 +34,7 @@ void initializeSettings() {
     storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
 }
 
-int handleJani(storm::jani::Model& model) {
+void handleJani(storm::jani::Model& model) {
     if (!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
         // For now, we have to have a jani file
         storm::jani::JsonExporter::toStream(model, std::cout);