added check for non-linearity to JANI menu game abstractor

src/storm/abstraction/MenuGameRefiner.cpp

@@ -441,7 +441,6 @@ namespace storm {
             
             std::map<storm::expressions::Variable, storm::expressions::Variable> oldToNewVariables;
             for (auto const& variable : oldVariables) {
-                std::cout << "got old variable " << variable.getName() << std::endl;
                 oldToNewVariables[variable] = expressionManager.getVariable(variable.getName());
             }
             std::map<storm::expressions::Variable, storm::expressions::Expression> lastSubstitution;
@@ -474,7 +473,6 @@ namespace storm {
                 // Retrieve the variable updates that the predecessor needs to perform to get to the current state.
                 auto variableUpdates = abstractor.get().getVariableUpdates(std::get<1>(decodedPredecessor), std::get<2>(decodedPredecessor));
                 for (auto const& update : variableUpdates) {
-                    std::cout << "looking up old variable " << update.first.getName() << std::endl;
                     storm::expressions::Variable newVariable = oldToNewVariables.at(update.first);
                     if (update.second.hasBooleanType()) {
                         predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(oldToNewVariables.at(update.first)), update.second.changeManager(expressionManager).substitute(substitution)));

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -32,7 +32,10 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression({model.getAutomaton(0)})}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
+            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
+                
+                // Check whether the model is linear as the abstraction requires this.
+                STORM_LOG_THROW(model.isLinear(), storm::exceptions::WrongFormatException, "Cannot create abstract model from non-linear model.");
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.

src/storm/storage/jani/Assignment.cpp

@@ -1,5 +1,7 @@
 #include "storm/storage/jani/Assignment.h"
 
+#include "storm/storage/expressions/LinearityCheckVisitor.h"
+
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotImplementedException.h"
 
@@ -42,6 +44,11 @@ namespace storm  {
             return level;
         }
         
+        bool Assignment::isLinear() const {
+            storm::expressions::LinearityCheckVisitor linearityChecker;
+            return linearityChecker.check(this->getAssignedExpression());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
             stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression();
             return stream;

src/storm/storage/jani/Assignment.h

@@ -52,6 +52,11 @@ namespace storm {
              */
             int64_t getLevel() const;
             
+            /*!
+             * Checks the assignment for linearity.
+             */
+            bool isLinear() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
             
         private:

src/storm/storage/jani/Automaton.cpp

@@ -499,5 +499,18 @@ namespace storm {
             return false;
         }
         
+        bool Automaton::isLinear() const {
+            bool result = true;
+
+            for (auto const& location : this->getLocations()) {
+                result &= location.isLinear();
+            }
+            
+            for (auto const& templateEdge : templateEdges) {
+                result &= templateEdge->isLinear();
+            }
+            
+            return result;
+        }
     }
 }

src/storm/storage/jani/Automaton.h

@@ -266,7 +266,7 @@ namespace storm {
              * Retrieves the edges of the automaton.
              */
             std::vector<Edge> const& getEdges() const;
-
+            
             /*!
              * Retrieves the set of action indices that are labels of edges of this automaton.
              */
@@ -364,6 +364,11 @@ namespace storm {
              */
             bool usesAssignmentLevels() const;
             
+            /*!
+             * Checks the automaton for linearity.
+             */
+            bool isLinear() const;
+            
         private:
             /// The name of the automaton.
             std::string name;

src/storm/storage/jani/Location.cpp

@@ -38,5 +38,9 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        bool Location::isLinear() const {
+            return assignments.areLinear();
+        }
+        
     }
 }

src/storm/storage/jani/Location.h

@@ -49,6 +49,11 @@ namespace storm {
              */
             void checkValid() const;
             
+            /*!
+             * Checks the automaton for linearity.
+             */
+            bool isLinear() const;
+            
         private:
             /// The name of the location.
             std::string name;

src/storm/storage/jani/Model.cpp

@@ -5,6 +5,8 @@
 #include "storm/storage/jani/Compositions.h"
 #include "storm/storage/jani/CompositionInformationVisitor.h"
 
+#include "storm/storage/expressions/LinearityCheckVisitor.h"
+
 #include "storm/utility/combinatorics.h"
 
 #include "storm/utility/macros.h"
@@ -911,6 +913,14 @@ namespace storm {
             return initialStatesRestriction;
         }
         
+        storm::expressions::Expression Model::getInitialStatesExpression() const {
+            std::vector<std::reference_wrapper<storm::jani::Automaton const>> allAutomata;
+            for (auto const& automaton : this->getAutomata()) {
+                allAutomata.push_back(automaton);
+            }
+            return getInitialStatesExpression(allAutomata);
+        }
+        
         storm::expressions::Expression Model::getInitialStatesExpression(std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& automata) const {
             // Start with the restriction of variables.
             storm::expressions::Expression result = initialStatesRestriction;
@@ -1117,6 +1127,19 @@ namespace storm {
             return false;
         }
         
+        bool Model::isLinear() const {
+            bool result = true;
+            
+            storm::expressions::LinearityCheckVisitor linearityChecker;
+            result &= linearityChecker.check(this->getInitialStatesExpression());
+            
+            for (auto const& automaton : this->getAutomata()) {
+                result &= automaton.isLinear();
+            }
+            
+            return result;
+        }
+        
         Model Model::createModelFromAutomaton(Automaton const& automaton) const {
             // Copy the full model
             Model newModel(*this);

src/storm/storage/jani/Model.h

@@ -335,13 +335,18 @@ namespace storm {
              * Gets the expression restricting the legal initial values of the global variables.
              */
             storm::expressions::Expression const& getInitialStatesRestriction() const;
-            
+
+            /*!
+             * Retrieves the expression defining the legal initial values of the variables.
+             */
+            storm::expressions::Expression getInitialStatesExpression() const;
+
             /*!
              * Retrieves the expression defining the legal initial values of the variables.
              *
              * @param automata The resulting expression will also characterize the legal initial states for these automata.
              */
-            storm::expressions::Expression getInitialStatesExpression(std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& automata = {}) const;
+            storm::expressions::Expression getInitialStatesExpression(std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& automata) const;
             
             /*!
              * Determines whether this model is a deterministic one in the sense that each state only has one choice.
@@ -417,6 +422,12 @@ namespace storm {
              */
             bool usesAssignmentLevels() const;
             
+            /*!
+             * Checks the model for linearity. A model is linear if all expressions appearing in guards and assignments
+             * are linear.
+             */
+            bool isLinear() const;
+            
             void makeStandardJaniCompliant();
             
             /// The name of the silent action.

src/storm/storage/jani/OrderedAssignments.cpp

@@ -157,6 +157,14 @@ namespace storm {
             return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable());
         }
         
+        bool OrderedAssignments::areLinear() const {
+            bool result = true;
+            for (auto const& assignment : getAllAssignments()) {
+                result &= assignment.isLinear();
+            }
+            return result;
+        }
+        
         std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments) {
             stream << "[";
             for(auto const& e : assignments.allAssignments) {

src/storm/storage/jani/OrderedAssignments.h

@@ -124,6 +124,11 @@ namespace storm {
              */
             void changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping);
 
+            /*!
+             * Checks the assignments for linearity.
+             */
+            bool areLinear() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
             
         private:

src/storm/storage/jani/TemplateEdge.cpp

@@ -2,6 +2,8 @@
 
 #include "storm/storage/jani/Model.h"
 
+#include "storm/storage/expressions/LinearityCheckVisitor.h"
+
 namespace storm {
     namespace jani {
         
@@ -134,5 +136,15 @@ namespace storm {
             return false;
         }
         
+        bool TemplateEdge::isLinear() const {
+            storm::expressions::LinearityCheckVisitor linearityChecker;
+            
+            bool result = linearityChecker.check(this->getGuard());
+            for (auto const& destination : destinations) {
+                result &= destination.isLinear();
+            }
+            return result;
+        }
+        
     }
 }

src/storm/storage/jani/TemplateEdge.h

@@ -84,6 +84,11 @@ namespace storm {
              */
             bool usesAssignmentLevels() const;
 
+            /*!
+             * Checks the template edge for linearity.
+             */
+            bool isLinear() const;
+            
         private:
             // The guard of the template edge.
             storm::expressions::Expression guard;

src/storm/storage/jani/TemplateEdgeDestination.cpp

@@ -46,5 +46,9 @@ namespace storm {
         bool TemplateEdgeDestination::usesAssignmentLevels() const {
             return assignments.hasMultipleLevels();
         }
+        
+        bool TemplateEdgeDestination::isLinear() const {
+            return assignments.areLinear();
+        }
     }
 }

src/storm/storage/jani/TemplateEdgeDestination.h

@@ -39,6 +39,11 @@ namespace storm {
              */
             bool usesAssignmentLevels() const;
             
+            /*!
+             * Checks the template edge destination for linearity.
+             */
+            bool isLinear() const;
+            
         private:
             // The (ordered) assignments to make when choosing this destination.
             OrderedAssignments assignments;