From bcdc2a4247b71f6e65235e87a72e72ad06129729 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 21 Dec 2016 10:53:59 +0100 Subject: [PATCH] added check for non-linearity to JANI menu game abstractor --- src/storm/abstraction/MenuGameRefiner.cpp | 2 -- .../jani/JaniMenuGameAbstractor.cpp | 5 +++- src/storm/storage/jani/Assignment.cpp | 7 ++++++ src/storm/storage/jani/Assignment.h | 5 ++++ src/storm/storage/jani/Automaton.cpp | 13 +++++++++++ src/storm/storage/jani/Automaton.h | 7 +++++- src/storm/storage/jani/Location.cpp | 4 ++++ src/storm/storage/jani/Location.h | 5 ++++ src/storm/storage/jani/Model.cpp | 23 +++++++++++++++++++ src/storm/storage/jani/Model.h | 15 ++++++++++-- src/storm/storage/jani/OrderedAssignments.cpp | 8 +++++++ src/storm/storage/jani/OrderedAssignments.h | 5 ++++ src/storm/storage/jani/TemplateEdge.cpp | 12 ++++++++++ src/storm/storage/jani/TemplateEdge.h | 5 ++++ .../storage/jani/TemplateEdgeDestination.cpp | 4 ++++ .../storage/jani/TemplateEdgeDestination.h | 5 ++++ 16 files changed, 119 insertions(+), 6 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 78b32010c..a2458dd6d 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -441,7 +441,6 @@ namespace storm { std::map oldToNewVariables; for (auto const& variable : oldVariables) { - std::cout << "got old variable " << variable.getName() << std::endl; oldToNewVariables[variable] = expressionManager.getVariable(variable.getName()); } std::map 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))); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 04002c400..1b162d3bb 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -32,7 +32,10 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr 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::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr 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. diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 38fb62603..3b4f97a63 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/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; diff --git a/src/storm/storage/jani/Assignment.h b/src/storm/storage/jani/Assignment.h index c9f56b16b..46c0a467e 100644 --- a/src/storm/storage/jani/Assignment.h +++ b/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: diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index f3dac4889..8fc6a80dd 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/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; + } } } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 19bf93e27..f67283030 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -266,7 +266,7 @@ namespace storm { * Retrieves the edges of the automaton. */ std::vector 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; diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp index 9922ffe4f..b957d5e9a 100644 --- a/src/storm/storage/jani/Location.cpp +++ b/src/storm/storage/jani/Location.cpp @@ -38,5 +38,9 @@ namespace storm { // Intentionally left empty. } + bool Location::isLinear() const { + return assignments.areLinear(); + } + } } diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h index 9d6f409da..b2bda7b23 100644 --- a/src/storm/storage/jani/Location.h +++ b/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; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index f62e98547..d13c823ca 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/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> allAutomata; + for (auto const& automaton : this->getAutomata()) { + allAutomata.push_back(automaton); + } + return getInitialStatesExpression(allAutomata); + } + storm::expressions::Expression Model::getInitialStatesExpression(std::vector> 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); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 0a79ab8d2..dffefef76 100644 --- a/src/storm/storage/jani/Model.h +++ b/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> const& automata = {}) const; + storm::expressions::Expression getInitialStatesExpression(std::vector> 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. diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 6433b0cfb..9f8b166df 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/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) { diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index c6318bafd..f45206461 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -124,6 +124,11 @@ namespace storm { */ void changeAssignmentVariables(std::map> const& remapping); + /*! + * Checks the assignments for linearity. + */ + bool areLinear() const; + friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments); private: diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 4446d7e10..ef4adadf2 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/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; + } + } } diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index 5839f3daa..a68fba7c3 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/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; diff --git a/src/storm/storage/jani/TemplateEdgeDestination.cpp b/src/storm/storage/jani/TemplateEdgeDestination.cpp index 0330d61f3..e374f7322 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.cpp +++ b/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(); + } } } diff --git a/src/storm/storage/jani/TemplateEdgeDestination.h b/src/storm/storage/jani/TemplateEdgeDestination.h index 8398f8717..5285c0b8d 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.h +++ b/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;