From ecc1a8035841fc707d946c506109d4867ecda179 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 29 May 2016 11:05:53 +0200 Subject: [PATCH] added conversion from PRISM to JANI. Added simplistic tests for that. Former-commit-id: 5b31fa589c7f04c2265053f6ff2b9d0dd69a5138 --- src/parser/JaniParser.cpp | 2 + src/storage/jani/Action.h | 2 +- src/storage/jani/Automaton.cpp | 16 +- src/storage/jani/Automaton.h | 17 +- src/storage/jani/BooleanVariable.h | 2 +- src/storage/jani/BoundedIntegerVariable.h | 2 +- src/storage/jani/Constant.cpp | 6 +- src/storage/jani/Constant.h | 7 +- src/storage/jani/EdgeSet.cpp | 4 + src/storage/jani/EdgeSet.h | 7 +- src/storage/jani/Exporter.cpp | 412 +++++++++++++++++++ src/storage/jani/Exporter.h | 48 +++ src/storage/jani/Model.cpp | 144 ++++++- src/storage/jani/Model.h | 169 ++++++-- src/storage/jani/ModelType.cpp | 18 +- src/storage/jani/ModelType.h | 2 +- src/storage/jani/UnboundedIntegerVariable.h | 2 +- src/storage/jani/Variable.cpp | 10 + src/storage/jani/Variable.h | 5 + src/storage/jani/VariableSet.cpp | 33 +- src/storage/jani/VariableSet.h | 25 +- src/storage/prism/Program.cpp | 243 ++++++++--- src/storage/prism/Program.h | 9 + test/functional/storage/PrismProgramTest.cpp | 25 ++ 24 files changed, 1080 insertions(+), 130 deletions(-) create mode 100644 src/storage/jani/Exporter.cpp create mode 100644 src/storage/jani/Exporter.h diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index ed7b5873f..f23aa306c 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -10,6 +10,8 @@ #include #include +#include "src/utility/macros.h" + namespace storm { namespace parser { diff --git a/src/storage/jani/Action.h b/src/storage/jani/Action.h index 6e6d207f8..5b9b2567f 100644 --- a/src/storage/jani/Action.h +++ b/src/storage/jani/Action.h @@ -17,8 +17,8 @@ namespace storm { std::string const& getName() const; private: + /// The name of the action. std::string name; - }; } diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index dd8548c96..f76d0fc38 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -27,7 +27,7 @@ namespace storm { variables.addUnboundedIntegerVariable(variable); } - VariableSet const& Automaton::getVariableSet() const { + VariableSet const& Automaton::getVariables() const { return variables; } @@ -39,10 +39,15 @@ namespace storm { return locations; } + Location const& Automaton::getLocation(uint64_t index) const { + return locations[index]; + } + uint64_t Automaton::addLocation(Location const& location) { STORM_LOG_THROW(!this->hasLocation(location.getName()), storm::exceptions::WrongFormatException, "Cannot add location with name '" << location.getName() << "', because a location with this name already exists."); locationToIndex.emplace(location.getName(), locations.size()); locations.push_back(location); + edges.push_back(EdgeSet()); return locations.size() - 1; } @@ -80,5 +85,14 @@ namespace storm { return edges[index]; } + void Automaton::addEdge(Edge const& edge) { + STORM_LOG_THROW(edge.getSourceLocationId() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationId() << "'."); + edges[edge.getSourceLocationId()].addEdge(edge); + } + + uint64_t Automaton::getNumberOfLocations() const { + return edges.size(); + } + } } \ No newline at end of file diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index d065a6dc9..81e231f16 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -41,7 +41,7 @@ namespace storm { /*! * Retrieves the variables of this automaton. */ - VariableSet const& getVariableSet() const; + VariableSet const& getVariables() const; /*! * Retrieves whether the automaton has a location with the given name. @@ -61,6 +61,11 @@ namespace storm { */ std::vector const& getLocations() const; + /*! + * Retrieves the location with the given index. + */ + Location const& getLocation(uint64_t index) const; + /*! * Adds the given location to the automaton. */ @@ -96,6 +101,16 @@ namespace storm { */ EdgeSet const& getEdgesFromLocation(uint64_t index) const; + /*! + * Adds an edge to the automaton. + */ + void addEdge(Edge const& edge); + + /*! + * Retrieves the number of locations. + */ + uint64_t getNumberOfLocations() const; + private: // The name of the automaton. std::string name; diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 733dd027a..844fe55d1 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates a boolean variable. */ - BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue); + BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression()); }; } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 12577867c..b686f4a0e 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -11,7 +11,7 @@ namespace storm { /*! * Creates a bounded integer variable. */ - BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue); + BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue = storm::expressions::Expression()); /*! * Retrieves the expression defining the lower bound of the variable. diff --git a/src/storage/jani/Constant.cpp b/src/storage/jani/Constant.cpp index 4e0deff80..a85331d40 100644 --- a/src/storage/jani/Constant.cpp +++ b/src/storage/jani/Constant.cpp @@ -3,10 +3,14 @@ namespace storm { namespace jani { - Constant::Constant(std::string const& name, boost::optional const& expression) : name(name), expression(expression) { + Constant::Constant(std::string const& name, storm::expressions::Variable const& variable, boost::optional const& expression) : name(name), variable(variable), expression(expression) { // Intentionally left empty. } + std::string const& Constant::getName() const { + return name; + } + bool Constant::isDefined() const { return static_cast(expression); } diff --git a/src/storage/jani/Constant.h b/src/storage/jani/Constant.h index baf47b2c6..1cfed043d 100644 --- a/src/storage/jani/Constant.h +++ b/src/storage/jani/Constant.h @@ -15,7 +15,12 @@ namespace storm { /*! * Creates a constant. */ - Constant(std::string const& name, boost::optional const& expression = boost::none); + Constant(std::string const& name, storm::expressions::Variable const& variable, boost::optional const& expression = boost::none); + + /*! + * Retrieves the name of the constant. + */ + std::string const& getName() const; /*! * Retrieves whether the constant is defined in the sense that it has a defining expression. diff --git a/src/storage/jani/EdgeSet.cpp b/src/storage/jani/EdgeSet.cpp index fbdac5a39..25704a864 100644 --- a/src/storage/jani/EdgeSet.cpp +++ b/src/storage/jani/EdgeSet.cpp @@ -23,5 +23,9 @@ namespace storm { return edges.cend(); } + void EdgeSet::addEdge(Edge const& edge) { + edges.push_back(edge); + } + } } \ No newline at end of file diff --git a/src/storage/jani/EdgeSet.h b/src/storage/jani/EdgeSet.h index df61d7722..e9fe03fbf 100644 --- a/src/storage/jani/EdgeSet.h +++ b/src/storage/jani/EdgeSet.h @@ -14,8 +14,13 @@ namespace storm { /*! * Creates a new set of edges. */ - EdgeSet(std::vector const& edges); + EdgeSet(std::vector const& edges = std::vector()); + /*! + * Adds the edge to the edges. + */ + void addEdge(Edge const& edge); + // Methods to get an iterator to the edges. iterator begin(); iterator end(); diff --git a/src/storage/jani/Exporter.cpp b/src/storage/jani/Exporter.cpp new file mode 100644 index 000000000..e5561b9b6 --- /dev/null +++ b/src/storage/jani/Exporter.cpp @@ -0,0 +1,412 @@ +#include "src/storage/jani/Exporter.h" + +#include + +namespace storm { + namespace jani { + + void appendIndent(std::stringstream& out, uint64_t indent) { + for (uint64_t i = 0; i < indent; ++i) { + out << "\t"; + } + } + + void appendField(std::stringstream& out, std::string const& name) { + out << "\"" << name << "\": "; + } + + void appendValue(std::stringstream& out, std::string const& value) { + out << "\"" << value << "\""; + } + + void clearLine(std::stringstream& out) { + out << std::endl; + } + + std::string expressionToString(storm::expressions::Expression const& expression) { + std::stringstream s; + s << expression; + return s.str(); + } + + void Exporter::appendVersion(std::stringstream& out, uint64_t janiVersion, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "jani-version"); + } + + void Exporter::appendModelName(std::stringstream& out, std::string const& name, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "name"); + appendValue(out, name); + } + + void Exporter::appendModelType(std::stringstream& out, storm::jani::ModelType const& modelType, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "type"); + } + + void Exporter::appendAction(std::stringstream& out, storm::jani::Action const& action, uint64_t indent) const { + appendIndent(out, indent); + out << "{" << std::endl; + appendIndent(out, indent + 1); + appendField(out, "name"); + appendValue(out, action.getName()); + clearLine(out); + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendActions(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "actions"); + out << " [" << std::endl; + + for (uint64_t index = 0; index < model.actions.size(); ++index) { + appendAction(out, model.actions[index], indent + 1); + if (index < model.actions.size() - 1) { + out << ","; + } + clearLine(out); + } + + appendIndent(out, indent); + out << "]"; + } + + void Exporter::appendVariable(std::stringstream& out, storm::jani::BooleanVariable const& variable, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "name"); + appendValue(out, variable.getName()); + out << ","; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "type"); + appendValue(out, "bool"); + out << ","; + clearLine(out); + appendIndent(out, indent); + appendField(out, "initial-value"); + appendValue(out, expressionToString(variable.getInitialValue())); + clearLine(out); + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendBoundedIntegerVariableType(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const { + out << " {"; + clearLine(out); + + appendIndent(out, indent); + appendField(out, "kind"); + appendValue(out, "bounded"); + clearLine(out); + + appendIndent(out, indent); + appendField(out, "base"); + appendValue(out, "int"); + clearLine(out); + + appendIndent(out, indent); + appendField(out, "lower-bound"); + appendValue(out, expressionToString(variable.getLowerBound())); + clearLine(out); + + appendIndent(out, indent); + appendField(out, "upper-bound"); + appendValue(out, expressionToString(variable.getLowerBound())); + clearLine(out); + + appendIndent(out, indent - 1); + out << "}"; + } + + void Exporter::appendVariable(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "name"); + appendValue(out, variable.getName()); + out << ","; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "type"); + appendBoundedIntegerVariableType(out, variable, indent + 2); + out << ","; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "initial-value"); + appendValue(out, expressionToString(variable.getInitialValue())); + clearLine(out); + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendVariable(std::stringstream& out, storm::jani::UnboundedIntegerVariable const& variable, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "name"); + appendValue(out, variable.getName()); + out << ","; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "type"); + appendValue(out, "int"); + out << ","; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "initial-value"); + appendValue(out, expressionToString(variable.getInitialValue())); + clearLine(out); + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendVariables(std::stringstream& out, storm::jani::VariableSet const& variables, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "variables"); + out << " ["; + clearLine(out); + + for (auto const& variable : variables.getBooleanVariables()) { + appendVariable(out, variable, indent + 1); + clearLine(out); + } + for (auto const& variable : variables.getBoundedIntegerVariables()) { + appendVariable(out, variable, indent + 1); + clearLine(out); + } + for (auto const& variable : variables.getUnboundedIntegerVariables()) { + appendVariable(out, variable, indent + 1); + clearLine(out); + } + + appendIndent(out, indent); + out << "]"; + } + + void Exporter::appendLocation(std::stringstream& out, storm::jani::Location const& location, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "name"); + appendValue(out, location.getName()); + clearLine(out); + + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendLocations(std::stringstream& out, storm::jani::Automaton const& automaton, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "locations"); + out << " ["; + clearLine(out); + + for (auto const& location : automaton.getLocations()) { + appendLocation(out, location, indent + 1); + out << ","; + clearLine(out); + } + + appendIndent(out, indent); + out << "]"; + } + + void Exporter::appendAssignment(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Assignment const& assignment, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "ref"); + storm::jani::Variable const& variable = model.getVariables().hasVariable(assignment.getExpressionVariable()) ? model.getVariables().getVariable(assignment.getExpressionVariable()) : automaton.getVariables().getVariable(assignment.getExpressionVariable()); + appendValue(out, variable.getName()); + out << ","; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "value"); + appendValue(out, expressionToString(assignment.getAssignedExpression())); + clearLine(out); + + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendEdgeDestination(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "probability"); + appendValue(out, expressionToString(destination.getProbability())); + out << ","; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "location"); + appendValue(out, automaton.getLocation(destination.getLocationId()).getName()); + out << ","; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "assignments"); + out << " ["; + clearLine(out); + + for (uint64_t index = 0; index < destination.getAssignments().size(); ++index) { + appendAssignment(out, model, automaton, destination.getAssignments()[index], indent + 2); + if (index < destination.getAssignments().size() - 1) { + out << ","; + } + clearLine(out); + } + + appendIndent(out, indent + 1); + out << "]"; + clearLine(out); + + appendIndent(out, indent); + out << "}"; + clearLine(out); + } + + void Exporter::appendEdge(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Edge const& edge, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "location"); + appendValue(out, automaton.getLocation(edge.getSourceLocationId()).getName()); + out << ","; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "action"); + appendValue(out, model.getAction(edge.getActionId()).getName()); + out << ","; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "guard"); + appendValue(out, expressionToString(edge.getGuard())); + out << ","; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "destinations"); + out << " ["; + clearLine(out); + + for (auto const& destination : edge.getDestinations()) { + appendEdgeDestination(out, model, automaton, destination, indent + 2); + } + + appendIndent(out, indent + 1); + out << "]"; + clearLine(out); + + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendEdges(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "edges"); + out << " ["; + clearLine(out); + + for (uint64_t location = 0; location < automaton.getNumberOfLocations(); ++location) { + for (auto const& edge : automaton.getEdgesFromLocation(location)) { + appendEdge(out, model, automaton, edge, indent + 1); + out << ","; + clearLine(out); + } + } + + appendIndent(out, indent); + out << "]"; + clearLine(out); + } + + void Exporter::appendAutomaton(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const { + appendIndent(out, indent); + out << "{"; + clearLine(out); + + appendIndent(out, indent + 1); + appendField(out, "name"); + appendValue(out, automaton.getName()); + clearLine(out); + appendVariables(out, automaton.getVariables(), indent + 1); + out << ","; + clearLine(out); + + appendLocations(out, automaton, indent + 1); + out << ","; + clearLine(out); + appendIndent(out, indent + 1); + appendField(out, "initial-location"); + appendValue(out, std::to_string(automaton.getInitialLocationIndex())); + clearLine(out); + + appendEdges(out, model, automaton, indent + 1); + + appendIndent(out, indent); + out << "}"; + } + + void Exporter::appendAutomata(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const { + appendIndent(out, indent); + appendField(out, "automata"); + out << " ["; + clearLine(out); + + for (uint64_t index = 0; index < model.automata.size(); ++index) { + appendAutomaton(out, model, model.automata[index], indent + 1); + if (index < model.automata.size() - 1) { + out << ","; + } + clearLine(out); + } + + appendIndent(out, indent); + out << "]"; + } + + std::string Exporter::toJaniString(storm::jani::Model const& model) const { + std::stringstream out; + + out << "{" << std::endl; + appendVersion(out, model.getJaniVersion(), 1); + out << ","; + clearLine(out); + appendModelName(out, model.getName(), 1); + out << ","; + clearLine(out); + appendModelType(out, model.getModelType(), 1); + out << ","; + clearLine(out); + appendActions(out, model, 1); + clearLine(out); + appendVariables(out, model.getVariables(), 1); + clearLine(out); + appendAutomata(out, model, 1); + clearLine(out); + out << "}" << std::endl; + + return out.str(); + } + + } +} \ No newline at end of file diff --git a/src/storage/jani/Exporter.h b/src/storage/jani/Exporter.h new file mode 100644 index 000000000..7b0a1990b --- /dev/null +++ b/src/storage/jani/Exporter.h @@ -0,0 +1,48 @@ +#pragma once + +#include +#include + +#include "src/storage/jani/Model.h" + +namespace storm { + namespace jani { + + class Exporter { + public: + Exporter() = default; + + std::string toJaniString(storm::jani::Model const& model) const; + + private: + void appendVersion(std::stringstream& out, uint64_t janiVersion, uint64_t indent) const; + + void appendModelName(std::stringstream& out, std::string const& name, uint64_t indent) const; + + void appendModelType(std::stringstream& out, storm::jani::ModelType const& modelType, uint64_t indent) const; + + void appendAction(std::stringstream& out, storm::jani::Action const& action, uint64_t indent) const; + + void appendActions(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const; + + void appendVariables(std::stringstream& out, storm::jani::VariableSet const& variables, uint64_t indent) const; + + void appendVariable(std::stringstream& out, storm::jani::BooleanVariable const& variable, uint64_t indent) const; + void appendVariable(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const; + void appendBoundedIntegerVariableType(std::stringstream& out, storm::jani::BoundedIntegerVariable const& variable, uint64_t indent) const; + void appendVariable(std::stringstream& out, storm::jani::UnboundedIntegerVariable const& variable, uint64_t indent) const; + + void appendAutomata(std::stringstream& out, storm::jani::Model const& model, uint64_t indent) const; + void appendAutomaton(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const; + + void appendLocation(std::stringstream& out, storm::jani::Location const& location, uint64_t indent) const; + void appendLocations(std::stringstream& out, storm::jani::Automaton const& automaton, uint64_t indent) const; + + void appendAssignment(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Assignment const& assignment, uint64_t indent) const; + void appendEdgeDestination(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, uint64_t indent) const; + void appendEdge(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, storm::jani::Edge const& edge, uint64_t indent) const; + void appendEdges(std::stringstream& out, storm::jani::Model const& model, storm::jani::Automaton const& automaton, uint64_t indent) const; + }; + + } +} \ No newline at end of file diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 615cdd7e2..87149f611 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -1,54 +1,154 @@ -#include #include "src/storage/jani/Model.h" +#include "src/storage/expressions/ExpressionManager.h" + +#include "src/storage/jani/AutomatonComposition.h" +#include "src/storage/jani/ParallelComposition.h" +#include "src/storage/jani/RenameComposition.h" + +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace jani { - Model::Model(std::string const& name, ModelType const& modelType, uint64_t version) : name(name), modelType(modelType), version(version) { + static const std::string SILENT_ACTION_NAME = ""; + + Model::Model() { // Intentionally left empty. } - - uint64_t Model::addAction(Action const& act) { - STORM_LOG_THROW(actionToIndex.count(act.getName()) == 0, storm::exceptions::InvalidJaniException, "Action with name " + act.getName() + " already exists"); - actionToIndex.emplace(act.getName(), actions.size()); - actions.push_back(act); + + Model::Model(std::string const& name, ModelType const& modelType, uint64_t version, boost::optional> const& expressionManager) : name(name), modelType(modelType), version(version), composition(nullptr) { + // Use the provided manager or create a new one. + if (expressionManager) { + this->expressionManager = expressionManager.get(); + } else { + this->expressionManager = std::make_shared(); + } + + // Add a prefined action that represents the silent action. + silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME)); + } + + uint64_t Model::getJaniVersion() const { + return version; + } + + ModelType const& Model::getModelType() const { + return modelType; + } + + std::string const& Model::getName() const { + return name; + } + + uint64_t Model::addAction(Action const& action) { + auto it = actionToIndex.find(action.getName()); + STORM_LOG_THROW(it == actionToIndex.end(), storm::exceptions::WrongFormatException, "Action with name '" << action.getName() << "' already exists"); + actionToIndex.emplace(action.getName(), actions.size()); + actions.push_back(action); return actions.size() - 1; } - - bool Model::hasAction(std::string const &name) const { - return actionToIndex.count(name) != 0; + + Action const& Model::getAction(uint64_t index) const { + return actions[index]; } - + + bool Model::hasAction(std::string const& name) const { + return actionToIndex.find(name) != actionToIndex.end(); + } + uint64_t Model::getActionIndex(std::string const& name) const { - assert(this->hasAction(name)); - return actionToIndex.at(name); + auto it = actionToIndex.find(name); + STORM_LOG_THROW(it != actionToIndex.end(), storm::exceptions::WrongFormatException, "Unable to retrieve index of unknown action '" << name << "'."); + return it->second; } - - - void Model::checkSupported() const { - //TODO + + uint64_t Model::addConstant(Constant const& constant) { + auto it = constantToIndex.find(constant.getName()); + STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists."); + constantToIndex.emplace(constant.getName(), constants.size()); + constants.push_back(constant); + return constants.size() - 1; } - + + void Model::addBooleanVariable(BooleanVariable const& variable) { + globalVariables.addBooleanVariable(variable); + } + + void Model::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) { + globalVariables.addBoundedIntegerVariable(variable); + } + + void Model::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) { + globalVariables.addUnboundedIntegerVariable(variable); + } + + VariableSet const& Model::getVariables() const { + return globalVariables; + } + + storm::expressions::ExpressionManager& Model::getExpressionManager() { + return *expressionManager; + } + + storm::expressions::ExpressionManager const& Model::getExpressionManager() const { + return *expressionManager; + } + + uint64_t Model::addAutomaton(Automaton const& automaton) { + auto it = automatonToIndex.find(automaton.getName()); + STORM_LOG_THROW(it == automatonToIndex.end(), storm::exceptions::WrongFormatException, "Automaton with name '" << automaton.getName() << "' already exists."); + automatonToIndex.emplace(automaton.getName(), automata.size()); + automata.push_back(automaton); + return automata.size() - 1; + } + + std::shared_ptr Model::getStandardSystemComposition() const { + std::set fullSynchronizationAlphabet = getActionNames(false); + + std::shared_ptr current; + current = std::make_shared(this->automata.front().getName()); + for (uint64_t index = 1; index < automata.size(); ++index) { + current = std::make_shared(current, std::make_shared(automata[index].getName()), fullSynchronizationAlphabet); + } + return current; + } + + Composition const& Model::getSystemComposition() const { + return *composition; + } + + std::set Model::getActionNames(bool includeSilent) const { + std::set result; + for (auto const& entry : actionToIndex) { + if (includeSilent || entry.second != silentActionIndex) { + result.insert(entry.first); + } + } + return result; + } + bool Model::checkValidity(bool logdbg) const { // TODO switch to exception based return value. - + if (version == 0) { if(logdbg) STORM_LOG_DEBUG("Jani version is unspecified"); return false; } - + if(modelType == ModelType::UNDEFINED) { if(logdbg) STORM_LOG_DEBUG("Model type is unspecified"); return false; } - + if(automata.empty()) { if(logdbg) STORM_LOG_DEBUG("No automata specified"); return false; } // All checks passed. return true; - + } } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 3c20f08c1..a01571707 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -1,25 +1,55 @@ #pragma once -#include "src/utility/macros.h" +#include #include "src/storage/jani/Action.h" #include "src/storage/jani/ModelType.h" #include "src/storage/jani/Automaton.h" +#include "src/storage/jani/Constant.h" +#include "src/storage/jani/Composition.h" namespace storm { + namespace expressions { + class ExpressionManager; + } + namespace jani { - + + class Exporter; + class Model { public: + friend class Exporter; + + /*! + * Creates an uninitialized model. + */ + Model(); + /*! * Creates an empty model with the given type. */ - Model(std::string const& name, ModelType const& modelType, uint64_t version = 1); - + Model(std::string const& name, ModelType const& modelType, uint64_t version = 1, boost::optional> const& expressionManager = boost::none); + + /*! + * Retrieves the JANI-version of the model. + */ + uint64_t getJaniVersion() const; + + /*! + * Retrieves the type of the model. + */ + ModelType const& getModelType() const; + + /*! + * Retrievest the name of the model. + */ + std::string const& getName() const; + /** * Checks whether the model has an action with the given name. - * - * @param name The name to look for. + * + * @param name The name to look for. */ bool hasAction(std::string const& name) const; @@ -35,39 +65,122 @@ namespace storm { * * @return the index for this action. */ - uint64_t addAction(Action const& act); - + uint64_t addAction(Action const& action); + /*! - * Does some simple checks to determine whether the model is supported by Prism. - * Mainly checks abscence of features the parser supports. - * - * Throws UnsupportedModelException if something is wrong + * Retrieves the action with the given index. */ - // TODO add engine as argument to check this for several engines. - void checkSupported() const; + Action const& getAction(uint64_t index) const; + + /*! + * Adds the given constant to the model. + */ + uint64_t addConstant(Constant const& constant); + + /*! + * Adds the given boolean variable to this model. + */ + void addBooleanVariable(BooleanVariable const& variable); + + /*! + * Adds the given bounded integer variable to this model. + */ + void addBoundedIntegerVariable(BoundedIntegerVariable const& variable); + + /*! + * Adds the given unbounded integer variable to this model. + */ + void addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable); + + /*! + * Retrieves the variables of this automaton. + */ + VariableSet const& getVariables() const; + + /*! + * Retrieves the manager responsible for the expressions in the JANI model. + */ + storm::expressions::ExpressionManager& getExpressionManager(); - /*! + /*! + * Retrieves the manager responsible for the expressions in the JANI model. + */ + storm::expressions::ExpressionManager const& getExpressionManager() const; + + /*! + * Adds the given automaton to the automata of this model. + */ + uint64_t addAutomaton(Automaton const& automaton); + + /*! + * Sets the system composition expression of the JANI model. + */ + void setSystemComposition(std::shared_ptr const& composition); + + /*! + * Gets the system composition as the standard, fully-synchronizing parallel composition. + */ + std::shared_ptr getStandardSystemComposition() const; + + /*! + * Retrieves the system composition expression. + */ + Composition const& getSystemComposition() const; + + /*! + * Retrieves the set of action names. + */ + std::set getActionNames(bool includeSilent = true) const; + + /*! + * Retrieves the name of the silent action. + */ + std::string const& getSilentActionName() const; + + /*! * Checks if the model is valid JANI, which should be verified before any further operations are applied to a model. */ - bool checkValidity(bool logdbg = true) const; + bool checkValidity(bool logdbg = true) const; + private: - /// The model name + /// The model name. std::string name; - /// The list of automata - std::vector automata; - /// A mapping from names to automata indices - std::unordered_map automatonToIndex; - /// The list with actions - std::vector actions; - /// A mapping from names to action indices - std::unordered_map actionToIndex; - + /// The type of the model. ModelType modelType; + /// The JANI-version used to specify the model. uint64_t version; - - + + /// The manager responsible for the expressions in this model. + std::shared_ptr expressionManager; + + /// The list of actions. + std::vector actions; + + /// A mapping from names to action indices. + std::unordered_map actionToIndex; + + /// The index of the silent action. + uint64_t silentActionIndex; + + /// The constants defined by the model. + std::vector constants; + + /// A mapping from names to constants. + std::unordered_map constantToIndex; + + /// The global variables of the model. + VariableSet globalVariables; + + /// The list of automata. + std::vector automata; + + /// A mapping from names to automata indices. + std::unordered_map automatonToIndex; + + /// An expression describing how the system is composed of the automata. + std::shared_ptr composition; }; } } diff --git a/src/storage/jani/ModelType.cpp b/src/storage/jani/ModelType.cpp index 09a28f7e0..68f974786 100644 --- a/src/storage/jani/ModelType.cpp +++ b/src/storage/jani/ModelType.cpp @@ -17,6 +17,9 @@ namespace storm { case ModelType::MDP: stream << "mdp"; break; + case ModelType::CTMDP: + stream << "ctmdp"; + break; case ModelType::MA: stream << "ma"; break; @@ -31,22 +34,25 @@ namespace storm { } ModelType getModelType(std::string const& input) { - if(input == "dtmc") { + if (input == "dtmc") { return ModelType::DTMC; } - if(input == "ctmc") { + if (input == "ctmc") { return ModelType::CTMC; } - if(input == "mdp") { + if (input == "mdp") { return ModelType::MDP; } - if(input == "ma") { + if (input == "ctmdp") { + return ModelType::CTMDP; + } + if (input == "ma") { return ModelType::MA; } - if(input == "pta") { + if (input == "pta") { return ModelType::PTA; } - if(input == "sta") { + if (input == "sta") { return ModelType::STA; } return ModelType::UNDEFINED; diff --git a/src/storage/jani/ModelType.h b/src/storage/jani/ModelType.h index 80a78ad49..b6bebae32 100644 --- a/src/storage/jani/ModelType.h +++ b/src/storage/jani/ModelType.h @@ -5,7 +5,7 @@ namespace storm { namespace jani { - enum class ModelType {UNDEFINED = 0, DTMC = 1, CTMC = 2, MDP = 3, MA = 4, PTA = 5, STA = 6}; + enum class ModelType {UNDEFINED = 0, DTMC = 1, CTMC = 2, MDP = 3, CTMDP = 4, MA = 5, PTA = 6, STA = 7}; ModelType getModelType(std::string const& input); std::ostream& operator<<(std::ostream& stream, ModelType const& type); diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h index c6fdf2405..94bb52836 100644 --- a/src/storage/jani/UnboundedIntegerVariable.h +++ b/src/storage/jani/UnboundedIntegerVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates an unbounded integer variable. */ - UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue); + UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression()); }; } diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 93e419804..9601d7684 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -1,5 +1,7 @@ #include "src/storage/jani/Variable.h" +#include + namespace storm { namespace jani { @@ -11,9 +13,17 @@ namespace storm { return variable; } + bool Variable::hasInitialValue() const { + return initialValue.isInitialized(); + } + std::string const& Variable::getName() const { return name; } + storm::expressions::Expression const& Variable::getInitialValue() const { + return initialValue; + } + } } \ No newline at end of file diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index 2bb5326af..b0cbf5d5a 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -31,6 +31,11 @@ namespace storm { */ storm::expressions::Expression const& getInitialValue() const; + /*! + * Retrieves whether the variable has an initial value. + */ + bool hasInitialValue() const; + private: // The name of the variable. std::string name; diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index d6adf3430..8afed1b1c 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -97,29 +97,32 @@ namespace storm { void VariableSet::addBooleanVariable(BooleanVariable const& variable) { STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists."); booleanVariables.push_back(variable); - variables.emplace(variable.getName(), booleanVariables.back()); + nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); + variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(0, booleanVariables.size() - 1)); } void VariableSet::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) { STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists."); boundedIntegerVariables.push_back(variable); - variables.emplace(variable.getName(), boundedIntegerVariables.back()); + nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); + variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(1, boundedIntegerVariables.size() - 1)); } void VariableSet::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) { STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists."); unboundedIntegerVariables.push_back(variable); - variables.emplace(variable.getName(), unboundedIntegerVariables.back()); + nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); + variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(2, boundedIntegerVariables.size() - 1)); } bool VariableSet::hasVariable(std::string const& name) const { - return variables.find(name) != variables.end(); + return nameToVariable.find(name) != nameToVariable.end(); } Variable const& VariableSet::getVariable(std::string const& name) const { - auto it = variables.find(name); - STORM_LOG_THROW(it != variables.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << name << "'."); - return it->second.get(); + auto it = nameToVariable.find(name); + STORM_LOG_THROW(it != nameToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << name << "'."); + return getVariable(it->second); } detail::VariableSetIterator VariableSet::begin() const { @@ -130,5 +133,21 @@ namespace storm { return detail::VariableSetIterator(*this, unboundedIntegerVariables.end()); } + Variable const& VariableSet::getVariable(storm::expressions::Variable const& variable) const { + auto it = variableToVariable.find(variable); + STORM_LOG_THROW(it != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << variable.getName() << "'."); + + if (it->second.first == 0) { + return booleanVariables[it->second.second]; + } else if (it->second.first == 1) { + return boundedIntegerVariables[it->second.second]; + } else { + return unboundedIntegerVariables[it->second.second]; + } + } + + bool VariableSet::hasVariable(storm::expressions::Variable const& variable) const { + return variableToVariable.find(variable) != variableToVariable.end(); + } } } \ No newline at end of file diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index fe3e4ef30..d5a03a345 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -121,7 +121,17 @@ namespace storm { * Retrieves the variable with the given name. */ Variable const& getVariable(std::string const& name) const; + + /*! + * Retrieves whether this variable set contains a variable with the expression variable. + */ + bool hasVariable(storm::expressions::Variable const& variable) const; + /*! + * Retrieves the variable object associated with the given expression variable (if any). + */ + Variable const& getVariable(storm::expressions::Variable const& variable) const; + /*! * Retrieves an iterator to the variables in this set. */ @@ -131,19 +141,22 @@ namespace storm { * Retrieves the end iterator to the variables in this set. */ detail::VariableSetIterator end() const; - + private: - // The boolean variables in this set. + /// The boolean variables in this set. std::vector booleanVariables; - // The bounded integer variables in this set. + /// The bounded integer variables in this set. std::vector boundedIntegerVariables; - // The unbounded integer variables in this set. + /// The unbounded integer variables in this set. std::vector unboundedIntegerVariables; - // A set of all variable names currently in use. - std::map> variables; + /// A set of all variable names currently in use. + std::map nameToVariable; + + /// A mapping from expression variables to their variable objects. + std::map> variableToVariable; }; } diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 128c28246..42cd1eb8a 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -13,8 +13,11 @@ #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/InvalidOperationException.h" #include "src/solver/SmtSolver.h" +#include "src/storage/jani/Model.h" + #include "src/storage/prism/CompositionVisitor.h" #include "src/storage/prism/Compositions.h" @@ -45,7 +48,7 @@ namespace storm { virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override { std::set subSynchronizingActionIndices = boost::any_cast>(composition.getSubcomposition().accept(*this, data)); - + std::set newSynchronizingActionIndices = subSynchronizingActionIndices; for (auto const& namePair : composition.getActionRenaming()) { if (!program.hasAction(namePair.first)) { @@ -79,7 +82,7 @@ namespace storm { subSynchronizingActionIndices.erase(it); } } - + return subSynchronizingActionIndices; } @@ -96,7 +99,7 @@ namespace storm { virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override { std::set leftSynchronizingActionIndices = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); std::set rightSynchronizingActionIndices = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); - + std::set synchronizingActionIndices; std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin())); @@ -132,18 +135,18 @@ namespace storm { Program::Program(std::shared_ptr manager, ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::map const& actionToIndexMap, std::vector const& rewardModels, std::vector