From 158ddc0533091358cf1baa7b5e5a786015e32866 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 19 Dec 2016 12:48:55 +0100 Subject: [PATCH] equipped automata in JANI models with expression variable representing their location --- src/storm/generator/VariableInformation.cpp | 2 +- src/storm/parser/JaniParser.cpp | 2 +- .../storage/expressions/ExpressionManager.cpp | 4 ++++ src/storm/storage/expressions/ExpressionManager.h | 2 ++ src/storm/storage/expressions/Variable.cpp | 8 ++++++++ src/storm/storage/expressions/Variable.h | 3 ++- src/storm/storage/jani/Automaton.cpp | 6 +++++- src/storm/storage/jani/Automaton.h | 15 ++++++++++++++- src/storm/storage/jani/Model.cpp | 2 +- src/storm/storage/prism/ToJaniConverter.cpp | 2 +- 10 files changed, 39 insertions(+), 7 deletions(-) diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index f81ea5c57..d904ae545 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -79,7 +79,7 @@ namespace storm { } for (auto const& automaton : model.getAutomata()) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); - locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); + locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 53968df6f..0d36b6201 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -958,7 +958,7 @@ namespace storm { storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure, storm::jani::Model const& parentModel) { STORM_LOG_THROW(automatonStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Each automaton must have a name"); std::string name = getString(automatonStructure.at("name"), " the name field for automaton"); - storm::jani::Automaton automaton(name); + storm::jani::Automaton automaton(name, expressionManager->declareIntegerVariable("_loc_" + name)); STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations."); std::unordered_map locIds; for(auto const& locEntry : automatonStructure.at("locations")) { diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 13fa5be6d..3072c30e0 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -56,6 +56,10 @@ namespace storm { // Intentionally left empty. } + ExpressionManager::~ExpressionManager() { + // Intentionally left empty. + } + std::shared_ptr ExpressionManager::clone() const { return std::shared_ptr(new ExpressionManager(*this)); } diff --git a/src/storm/storage/expressions/ExpressionManager.h b/src/storm/storage/expressions/ExpressionManager.h index 05cc11a2c..9630a719d 100644 --- a/src/storm/storage/expressions/ExpressionManager.h +++ b/src/storm/storage/expressions/ExpressionManager.h @@ -71,6 +71,8 @@ namespace storm { */ ExpressionManager(); + ~ExpressionManager(); + /*! * Creates a new expression manager with the same set of variables. */ diff --git a/src/storm/storage/expressions/Variable.cpp b/src/storm/storage/expressions/Variable.cpp index 12fccaaca..0259ab3e5 100644 --- a/src/storm/storage/expressions/Variable.cpp +++ b/src/storm/storage/expressions/Variable.cpp @@ -3,9 +3,17 @@ namespace storm { namespace expressions { + Variable::Variable() { + // Intentionally left empty. + } + Variable::Variable(std::shared_ptr const& manager, uint_fast64_t index) : manager(manager), index(index) { // Intentionally left empty. } + + Variable::~Variable() { + // Intentionally left empty. + } bool Variable::operator==(Variable const& other) const { return manager == other.manager && index == other.index; diff --git a/src/storm/storage/expressions/Variable.h b/src/storm/storage/expressions/Variable.h index 7163c92c4..f93a4dfd5 100644 --- a/src/storm/storage/expressions/Variable.h +++ b/src/storm/storage/expressions/Variable.h @@ -17,7 +17,8 @@ namespace storm { // This class captures a simple variable. class Variable { public: - Variable() = default; + Variable(); + ~Variable(); /*! * Constructs a variable with the given index and type. diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 563b08f25..ad6bf5c57 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -50,7 +50,7 @@ namespace storm { } } - Automaton::Automaton(std::string const& name) : name(name) { + Automaton::Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable) : name(name), locationExpressionVariable(locationExpressionVariable) { // Add a sentinel element to the mapping from locations to starting indices. locationToStartingIndex.push_back(0); } @@ -166,6 +166,10 @@ namespace storm { } return mapping; } + + storm::expressions::Variable const& Automaton::getLocationExpressionVariable() const { + return locationExpressionVariable; + } Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) { auto it = locationToIndex.find(name); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index ad7a46542..19bf93e27 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -95,7 +95,12 @@ namespace storm { /*! * Creates an empty automaton. */ - Automaton(std::string const& name); + Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable); + + Automaton(Automaton const& other) = default; + Automaton& operator=(Automaton const& other) = default; + Automaton(Automaton&& other) = default; + Automaton& operator=(Automaton&& other) = default; /*! * Retrieves the name of the automaton. @@ -207,6 +212,11 @@ namespace storm { */ std::map buildIdToLocationNameMap() const; + /*! + * Retrieves the expression variable that represents the location of this automaton. + */ + storm::expressions::Variable const& getLocationExpressionVariable() const; + /*! * Retrieves the edges of the location with the given name. */ @@ -357,6 +367,9 @@ namespace storm { private: /// The name of the automaton. std::string name; + + /// The expression variable representing the location of this automaton. + storm::expressions::Variable locationExpressionVariable; /// The set of variables of this automaton. VariableSet variables; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 8de253c0b..abc49644d 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -418,7 +418,7 @@ namespace storm { ParallelComposition const& parallelComposition = systemComposition.asParallelComposition(); // Create the new automaton that will hold the flattened system. - Automaton newAutomaton(this->getName() + "_flattening"); + Automaton newAutomaton(this->getName() + "_flattened", expressionManager->declareIntegerVariable("_loc_flattened_" + this->getName())); std::map> variableRemapping; for (auto const& variable : getGlobalVariables()) { diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 0abb873cb..a544c9d83 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -146,7 +146,7 @@ namespace storm { // Keep track of the action indices contained in this module. std::set actionIndicesOfModule; - storm::jani::Automaton automaton(module.getName()); + storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName())); for (auto const& variable : module.getIntegerVariables()) { storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];