From 9a5d11a5e0a32972883236bdbdbba84f6f91d9f9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 Sep 2016 17:01:09 +0200 Subject: [PATCH] adding real variables to JANI models. started to encapsulate PRISM to JANI converter Former-commit-id: a7892b3d23a78908349c15977ae6945bd2c3ed4c [formerly 411e830ca5053819b0b81a65bc772c069d597fea] Former-commit-id: 49ee7034936d1b9d68e4ab65e1f92d7066591750 --- src/storage/jani/Assignment.cpp | 2 +- src/storage/jani/Automaton.cpp | 24 ++-- src/storage/jani/Automaton.h | 11 +- src/storage/jani/Edge.cpp | 23 +++- src/storage/jani/EdgeDestination.cpp | 32 +++++ src/storage/jani/EdgeDestination.h | 21 +++ src/storage/jani/Model.cpp | 24 ++-- src/storage/jani/Model.h | 11 +- src/storage/jani/RealVariable.cpp | 19 +++ src/storage/jani/RealVariable.h | 25 ++++ src/storage/jani/Variable.cpp | 25 +++- src/storage/jani/Variable.h | 4 + src/storage/jani/VariableSet.cpp | 28 +++- src/storage/jani/VariableSet.h | 30 ++++- src/storage/prism/Program.cpp | 173 +----------------------- src/storage/prism/Program.h | 12 +- src/storage/prism/ToJaniConverter.cpp | 187 ++++++++++++++++++++++++++ src/storage/prism/ToJaniConverter.h | 20 +++ 18 files changed, 450 insertions(+), 221 deletions(-) create mode 100644 src/storage/jani/RealVariable.cpp create mode 100644 src/storage/jani/RealVariable.h create mode 100644 src/storage/prism/ToJaniConverter.cpp create mode 100644 src/storage/prism/ToJaniConverter.h diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp index 7c97d367c..cea0b9eec 100644 --- a/src/storage/jani/Assignment.cpp +++ b/src/storage/jani/Assignment.cpp @@ -8,7 +8,7 @@ namespace storm { } bool Assignment::operator==(Assignment const& other) const { - return this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()); + return this->isTransientAssignment() == other.isTransientAssignment() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()); } storm::jani::Variable const& Assignment::getVariable() const { diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index c6d8600e3..9227a4c5b 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -61,26 +61,32 @@ namespace storm { Variable const& Automaton::addVariable(Variable const &variable) { if (variable.isBooleanVariable()) { - return addBooleanVariable(variable.asBooleanVariable()); + return addVariable(variable.asBooleanVariable()); } else if (variable.isBoundedIntegerVariable()) { - return addBoundedIntegerVariable(variable.asBoundedIntegerVariable()); + return addVariable(variable.asBoundedIntegerVariable()); } else if (variable.isUnboundedIntegerVariable()) { - return addUnboundedIntegerVariable(variable.asUnboundedIntegerVariable()); + return addVariable(variable.asUnboundedIntegerVariable()); + } else if (variable.isRealVariable()) { + return addVariable(variable.asRealVariable()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type."); } } - BooleanVariable const& Automaton::addBooleanVariable(BooleanVariable const& variable) { - return variables.addBooleanVariable(variable); + BooleanVariable const& Automaton::addVariable(BooleanVariable const& variable) { + return variables.addVariable(variable); } - BoundedIntegerVariable const& Automaton::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) { - return variables.addBoundedIntegerVariable(variable); + BoundedIntegerVariable const& Automaton::addVariable(BoundedIntegerVariable const& variable) { + return variables.addVariable(variable); } - UnboundedIntegerVariable const& Automaton::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) { - return variables.addUnboundedIntegerVariable(variable); + UnboundedIntegerVariable const& Automaton::addVariable(UnboundedIntegerVariable const& variable) { + return variables.addVariable(variable); + } + + RealVariable const& Automaton::addVariable(RealVariable const& variable) { + return variables.addVariable(variable); } VariableSet& Automaton::getVariables() { diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 1a2ad61dc..e46fc44be 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -108,17 +108,22 @@ namespace storm { /*! * Adds the given Boolean variable to this automaton. */ - BooleanVariable const& addBooleanVariable(BooleanVariable const& variable); + BooleanVariable const& addVariable(BooleanVariable const& variable); /*! * Adds the given bounded integer variable to this automaton. */ - BoundedIntegerVariable const& addBoundedIntegerVariable(BoundedIntegerVariable const& variable); + BoundedIntegerVariable const& addVariable(BoundedIntegerVariable const& variable); /*! * Adds the given unbounded integer variable to this automaton. */ - UnboundedIntegerVariable const& addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable); + UnboundedIntegerVariable const& addVariable(UnboundedIntegerVariable const& variable); + + /*! + * Adds the given real variable to this automaton. + */ + RealVariable const& addVariable(RealVariable const& variable); /*! * Retrieves the variables of this automaton. diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index 40f64e537..430838b61 100644 --- a/src/storage/jani/Edge.cpp +++ b/src/storage/jani/Edge.cpp @@ -64,7 +64,28 @@ namespace storm { } void Edge::liftTransientDestinationAssignments() { - + if (!destinations.empty()) { + auto const& destination = *destinations.begin(); + + for (auto const& assignment : destination.getTransientAssignments()) { + // Check if we can lift the assignment to the edge. + bool canBeLifted = true; + for (auto const& destination : destinations) { + if (!destination.hasAssignment(assignment)) { + canBeLifted = false; + break; + } + } + + // If so, remove the assignment from all destinations. + if (canBeLifted) { + this->addTransientAssignment(assignment); + for (auto& destination : destinations) { + destination.removeAssignment(assignment); + } + } + } + } } boost::container::flat_set const& Edge::getWrittenGlobalVariables() const { diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp index c58a157e9..f49b15eac 100644 --- a/src/storage/jani/EdgeDestination.cpp +++ b/src/storage/jani/EdgeDestination.cpp @@ -72,6 +72,28 @@ namespace storm { return transientAssignments; } + bool EdgeDestination::hasAssignment(Assignment const& assignment) const { + for (auto const& containedAssignment : assignments) { + if (containedAssignment == assignment) { + return true; + } + } + return false; + } + + bool EdgeDestination::removeAssignment(Assignment const& assignment) { + bool toRemove = removeAssignment(assignment, assignments); + if (toRemove) { + if (assignment.isTransientAssignment()) { + removeAssignment(assignment, transientAssignments); + } else { + removeAssignment(assignment, nonTransientAssignments); + } + return true; + } + return false; + } + void EdgeDestination::sortAssignments(std::vector& assignments) { std::sort(assignments.begin(), assignments.end(), [] (storm::jani::Assignment const& assignment1, storm::jani::Assignment const& assignment2) { bool smaller = assignment1.getExpressionVariable().getType().isBooleanType() && !assignment2.getExpressionVariable().getType().isBooleanType(); @@ -82,5 +104,15 @@ namespace storm { }); } + bool EdgeDestination::removeAssignment(Assignment const& assignment, std::vector& assignments) { + for (auto it = assignments.begin(), ite = assignments.end(); it != ite; ++it) { + if (assignment == *it) { + assignments.erase(it); + return true; + } + } + return false; + } + } } \ No newline at end of file diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h index d22e09ab3..9d3f8326d 100644 --- a/src/storage/jani/EdgeDestination.h +++ b/src/storage/jani/EdgeDestination.h @@ -66,6 +66,20 @@ namespace storm { */ std::vector const& getTransientAssignments() const; + /*! + * Retrieves whether this assignment is made when choosing this destination. + * + * @return True iff the assignment is made. + */ + bool hasAssignment(Assignment const& assignment) const; + + /*! + * Removes the given assignment from this destination. + * + * @return True if the assignment was found and removed. + */ + bool removeAssignment(Assignment const& assignment); + private: /*! * Sorts the assignments to make all assignments to boolean variables precede all others and order the @@ -73,6 +87,13 @@ namespace storm { */ static void sortAssignments(std::vector& assignments); + /*! + * Removes the given assignment from the provided list of assignments if found. + * + * @return True if the assignment was removed. + */ + static bool removeAssignment(Assignment const& assignment, std::vector& assignments); + // The index of the destination location. uint64_t locationIndex; diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index a9fb3f25e..08a243c06 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -107,26 +107,32 @@ namespace storm { Variable const& Model::addVariable(Variable const& variable) { if (variable.isBooleanVariable()) { - return addBooleanVariable(variable.asBooleanVariable()); + return addVariable(variable.asBooleanVariable()); } else if (variable.isBoundedIntegerVariable()) { - return addBoundedIntegerVariable(variable.asBoundedIntegerVariable()); + return addVariable(variable.asBoundedIntegerVariable()); } else if (variable.isUnboundedIntegerVariable()) { - return addUnboundedIntegerVariable(variable.asUnboundedIntegerVariable()); + return addVariable(variable.asUnboundedIntegerVariable()); + } else if (variable.isRealVariable()) { + return addVariable(variable.asRealVariable()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type."); } } - BooleanVariable const& Model::addBooleanVariable(BooleanVariable const& variable) { - return globalVariables.addBooleanVariable(variable); + BooleanVariable const& Model::addVariable(BooleanVariable const& variable) { + return globalVariables.addVariable(variable); } - BoundedIntegerVariable const& Model::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) { - return globalVariables.addBoundedIntegerVariable(variable); + BoundedIntegerVariable const& Model::addVariable(BoundedIntegerVariable const& variable) { + return globalVariables.addVariable(variable); } - UnboundedIntegerVariable const& Model::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) { - return globalVariables.addUnboundedIntegerVariable(variable); + UnboundedIntegerVariable const& Model::addVariable(UnboundedIntegerVariable const& variable) { + return globalVariables.addVariable(variable); + } + + RealVariable const& Model::addVariable(RealVariable const& variable) { + return globalVariables.addVariable(variable); } VariableSet& Model::getGlobalVariables() { diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 0379cd5dd..20ca41486 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -115,17 +115,22 @@ namespace storm { /*! * Adds the given boolean variable to this model. */ - BooleanVariable const& addBooleanVariable(BooleanVariable const& variable); + BooleanVariable const& addVariable(BooleanVariable const& variable); /*! * Adds the given bounded integer variable to this model. */ - BoundedIntegerVariable const& addBoundedIntegerVariable(BoundedIntegerVariable const& variable); + BoundedIntegerVariable const& addVariable(BoundedIntegerVariable const& variable); /*! * Adds the given unbounded integer variable to this model. */ - UnboundedIntegerVariable const& addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable); + UnboundedIntegerVariable const& addVariable(UnboundedIntegerVariable const& variable); + + /*! + * Adds the given real variable to this model. + */ + RealVariable const& addVariable(RealVariable const& variable); /*! * Retrieves the variables of this automaton. diff --git a/src/storage/jani/RealVariable.cpp b/src/storage/jani/RealVariable.cpp new file mode 100644 index 000000000..8880a9a0a --- /dev/null +++ b/src/storage/jani/RealVariable.cpp @@ -0,0 +1,19 @@ +#include "src/storage/jani/RealVariable.h" + +namespace storm { + namespace jani { + + RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : storm::jani::Variable(name, variable, transient) { + // Intentionally left empty. + } + + RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : storm::jani::Variable(name, variable, initValue, transient) { + // Intentionally left empty. + } + + bool RealVariable::isRealVariable() const { + return true; + } + + } +} \ No newline at end of file diff --git a/src/storage/jani/RealVariable.h b/src/storage/jani/RealVariable.h new file mode 100644 index 000000000..74c337ed9 --- /dev/null +++ b/src/storage/jani/RealVariable.h @@ -0,0 +1,25 @@ +#pragma once + +#include "src/storage/jani/Variable.h" + +namespace storm { + namespace jani { + + class RealVariable : public Variable { + public: + /*! + * Creates a real variable without initial value. + */ + RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + + /*! + * Creates a real variable with initial value. + */ + RealVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient=false); + + virtual bool isRealVariable() const override; + }; + + + } +} \ No newline at end of file diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 57a9289a4..4027ea112 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -3,6 +3,7 @@ #include "src/storage/jani/BooleanVariable.h" #include "src/storage/jani/BoundedIntegerVariable.h" #include "src/storage/jani/UnboundedIntegerVariable.h" +#include "src/storage/jani/RealVariable.h" namespace storm { namespace jani { @@ -36,6 +37,10 @@ namespace storm { return false; } + bool Variable::isRealVariable() const { + return false; + } + bool Variable::isTransientVariable() const { return transient; } @@ -53,27 +58,35 @@ namespace storm { } BooleanVariable& Variable::asBooleanVariable() { - return dynamic_cast(*this); + return static_cast(*this); } BooleanVariable const& Variable::asBooleanVariable() const { - return dynamic_cast(*this); + return static_cast(*this); } BoundedIntegerVariable& Variable::asBoundedIntegerVariable() { - return dynamic_cast(*this); + return static_cast(*this); } BoundedIntegerVariable const& Variable::asBoundedIntegerVariable() const { - return dynamic_cast(*this); + return static_cast(*this); } UnboundedIntegerVariable& Variable::asUnboundedIntegerVariable() { - return dynamic_cast(*this); + return static_cast(*this); } UnboundedIntegerVariable const& Variable::asUnboundedIntegerVariable() const { - return dynamic_cast(*this); + return static_cast(*this); + } + + RealVariable& Variable::asRealVariable() { + return static_cast(*this); + } + + RealVariable const& Variable::asRealVariable() const { + return static_cast(*this); } } diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index 820014b03..8d25bfd36 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -13,6 +13,7 @@ namespace storm { class BooleanVariable; class BoundedIntegerVariable; class UnboundedIntegerVariable; + class RealVariable; class Variable { public: @@ -58,6 +59,7 @@ namespace storm { virtual bool isBooleanVariable() const; virtual bool isBoundedIntegerVariable() const; virtual bool isUnboundedIntegerVariable() const; + virtual bool isRealVariable() const; virtual bool isTransientVariable() const; @@ -68,6 +70,8 @@ namespace storm { BoundedIntegerVariable const& asBoundedIntegerVariable() const; UnboundedIntegerVariable& asUnboundedIntegerVariable(); UnboundedIntegerVariable const& asUnboundedIntegerVariable() const; + RealVariable& asRealVariable(); + RealVariable const& asRealVariable() const; private: // The name of the variable. diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index fe7ef300c..27806a132 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -74,7 +74,15 @@ namespace storm { return detail::ConstVariables(unboundedIntegerVariables.begin(), unboundedIntegerVariables.end()); } - BooleanVariable const& VariableSet::addBooleanVariable(BooleanVariable const& variable) { + detail::Variables VariableSet::getRealVariables() { + return detail::Variables(realVariables.begin(), realVariables.end()); + } + + detail::ConstVariables VariableSet::getRealVariables() const { + return detail::ConstVariables(realVariables.begin(), realVariables.end()); + } + + BooleanVariable const& VariableSet::addVariable(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."); std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); @@ -84,7 +92,7 @@ namespace storm { return *newVariable; } - BoundedIntegerVariable const& VariableSet::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) { + BoundedIntegerVariable const& VariableSet::addVariable(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."); std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); @@ -94,7 +102,7 @@ namespace storm { return *newVariable; } - UnboundedIntegerVariable const& VariableSet::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) { + UnboundedIntegerVariable const& VariableSet::addVariable(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."); std::shared_ptr newVariable = std::make_shared(variable); variables.push_back(newVariable); @@ -104,6 +112,16 @@ namespace storm { return *newVariable; } + RealVariable const& VariableSet::addVariable(RealVariable 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."); + std::shared_ptr newVariable = std::make_shared(variable); + variables.push_back(newVariable); + realVariables.push_back(newVariable); + nameToVariable.emplace(variable.getName(), variable.getExpressionVariable()); + variableToVariable.emplace(variable.getExpressionVariable(), newVariable); + return *newVariable; + } + bool VariableSet::hasVariable(std::string const& name) const { return nameToVariable.find(name) != nameToVariable.end(); } @@ -152,6 +170,10 @@ namespace storm { return !unboundedIntegerVariables.empty(); } + bool VariableSet::containsRealVariables() const { + return !realVariables.empty(); + } + bool VariableSet::empty() const { return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables()); } diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index 84e265ed1..651787df5 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -8,6 +8,7 @@ #include "src/storage/jani/BooleanVariable.h" #include "src/storage/jani/UnboundedIntegerVariable.h" #include "src/storage/jani/BoundedIntegerVariable.h" +#include "src/storage/jani/RealVariable.h" namespace storm { namespace jani { @@ -97,20 +98,35 @@ namespace storm { */ detail::ConstVariables getUnboundedIntegerVariables() const; + /*! + * Retrieves the real variables in this set. + */ + detail::Variables getRealVariables(); + + /*! + * Retrieves the real variables in this set. + */ + detail::ConstVariables getRealVariables() const; + /*! * Adds the given boolean variable to this set. */ - BooleanVariable const& addBooleanVariable(BooleanVariable const& variable); + BooleanVariable const& addVariable(BooleanVariable const& variable); /*! * Adds the given bounded integer variable to this set. */ - BoundedIntegerVariable const& addBoundedIntegerVariable(BoundedIntegerVariable const& variable); + BoundedIntegerVariable const& addVariable(BoundedIntegerVariable const& variable); /*! * Adds the given unbounded integer variable to this set. */ - UnboundedIntegerVariable const& addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable); + UnboundedIntegerVariable const& addVariable(UnboundedIntegerVariable const& variable); + + /*! + * Adds the given real variable to this set. + */ + RealVariable const& addVariable(RealVariable const& variable); /*! * Retrieves whether this variable set contains a variable with the given name. @@ -167,6 +183,11 @@ namespace storm { */ bool containsUnboundedIntegerVariables() const; + /*! + * Retrieves whether the set of variables contains an unbounded integer variable. + */ + bool containsRealVariables() const; + /*! * Retrieves whether this variable set is empty. */ @@ -185,6 +206,9 @@ namespace storm { /// The unbounded integer variables in this set. std::vector> unboundedIntegerVariables; + /// The real variables in this set. + std::vector> realVariables; + /// A set of all variable names currently in use. std::map nameToVariable; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index a836b5879..c92226c84 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -20,7 +20,6 @@ #include "src/storage/prism/CompositionVisitor.h" #include "src/storage/prism/Compositions.h" -#include "src/storage/prism/CompositionToJaniVisitor.h" namespace storm { namespace prism { @@ -1610,180 +1609,10 @@ namespace storm { return this->indexToActionMap.rbegin()->first; } - storm::expressions::ExpressionManager const& Program::getManager() const { + storm::expressions::ExpressionManager& Program::getManager() const { return *this->manager; } - storm::expressions::ExpressionManager& Program::getManager() { - return *this->manager; - } - - storm::jani::Model Program::toJani(bool allVariablesGlobal) const { - // Start by creating an empty JANI model. - storm::jani::ModelType modelType; - switch (this->getModelType()) { - case Program::ModelType::DTMC: modelType = storm::jani::ModelType::DTMC; - break; - case Program::ModelType::CTMC: modelType = storm::jani::ModelType::CTMC; - break; - case Program::ModelType::MDP: modelType = storm::jani::ModelType::MDP; - break; - case Program::ModelType::CTMDP: modelType = storm::jani::ModelType::CTMDP; - break; - case Program::ModelType::MA: modelType = storm::jani::ModelType::MA; - break; - default: modelType = storm::jani::ModelType::UNDEFINED; - } - storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager); - - // Add all constants of the PRISM program to the JANI model. - for (auto const& constant : constants) { - janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional(constant.getExpression()) : boost::none)); - } - - // Maintain a mapping from expression variables to JANI variables so we can fill in the correct objects when - // creating assignments. - std::map> variableToVariableMap; - - // Add all global variables of the PRISM program to the JANI model. - for (auto const& variable : globalIntegerVariables) { - if (variable.hasInitialValue()) { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } - } - for (auto const& variable : globalBooleanVariables) { - if (variable.hasInitialValue()) { - storm::jani::BooleanVariable const& createdVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false)); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } else { - storm::jani::BooleanVariable const& createdVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false)); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } - } - - // Add all actions of the PRISM program to the JANI model. - for (auto const& action : indexToActionMap) { - // Ignore the empty action as every JANI program has predefined tau action. - if (!action.second.empty()) { - janiModel.addAction(storm::jani::Action(action.second)); - } - } - - // Because of the rules of JANI, we have to make all variables of modules global that are read by other modules. - - // Create a mapping from variables to the indices of module indices that write/read the variable. - std::map> variablesToAccessingModuleIndices; - for (uint_fast64_t index = 0; index < modules.size(); ++index) { - storm::prism::Module const& module = modules[index]; - - for (auto const& command : module.getCommands()) { - std::set variables = command.getGuardExpression().getVariables(); - for (auto const& variable : variables) { - variablesToAccessingModuleIndices[variable].insert(index); - } - - for (auto const& update : command.getUpdates()) { - for (auto const& assignment : update.getAssignments()) { - variables = assignment.getExpression().getVariables(); - for (auto const& variable : variables) { - variablesToAccessingModuleIndices[variable].insert(index); - } - variablesToAccessingModuleIndices[assignment.getVariable()].insert(index); - } - } - } - } - - // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the - // previously built mapping to make variables global that are read by more than one module. - for (auto const& module : modules) { - storm::jani::Automaton automaton(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()]; - // If there is exactly one module reading and writing the variable, we can make the variable local to this module. - if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { - storm::jani::BoundedIntegerVariable const& createdVariable = automaton.addBoundedIntegerVariable(newIntegerVariable); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } else if (!accessingModuleIndices.empty()) { - // Otherwise, we need to make it global. - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addBoundedIntegerVariable(newIntegerVariable); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } - } - for (auto const& variable : module.getBooleanVariables()) { - storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); - std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; - // If there is exactly one module reading and writing the variable, we can make the variable local to this module. - if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { - storm::jani::BooleanVariable const& createdVariable = automaton.addBooleanVariable(newBooleanVariable); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } else if (!accessingModuleIndices.empty()) { - // Otherwise, we need to make it global. - storm::jani::BooleanVariable const& createdVariable = janiModel.addBooleanVariable(newBooleanVariable); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); - } - } - automaton.setInitialStatesRestriction(manager->boolean(true)); - - // Create a single location that will have all the edges. - uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l")); - automaton.addInitialLocation(onlyLocation); - - for (auto const& command : module.getCommands()) { - boost::optional rateExpression; - std::vector destinations; - if (this->getModelType() == Program::ModelType::CTMC || this->getModelType() == Program::ModelType::CTMDP) { - for (auto const& update : command.getUpdates()) { - if (rateExpression) { - rateExpression = rateExpression.get() + update.getLikelihoodExpression(); - } else { - rateExpression = update.getLikelihoodExpression(); - } - } - } - - for (auto const& update : command.getUpdates()) { - std::vector assignments; - for (auto const& assignment : update.getAssignments()) { - assignments.push_back(storm::jani::Assignment(variableToVariableMap.at(assignment.getVariable()).get(), assignment.getExpression())); - } - - if (rateExpression) { - destinations.push_back(storm::jani::EdgeDestination(onlyLocation, manager->integer(1) / rateExpression.get(), assignments)); - } else { - destinations.push_back(storm::jani::EdgeDestination(onlyLocation, update.getLikelihoodExpression(), assignments)); - } - } - automaton.addEdge(storm::jani::Edge(onlyLocation, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations)); - } - - janiModel.addAutomaton(automaton); - } - - if (this->hasInitialConstruct()) { - janiModel.setInitialStatesRestriction(this->getInitialConstruct().getInitialStatesExpression()); - } else { - janiModel.setInitialStatesRestriction(manager->boolean(true)); - } - - // Set the standard system composition. This is possible, because we reject non-standard compositions anyway. - if (this->specifiesSystemComposition()) { - CompositionToJaniVisitor visitor; - janiModel.setSystemComposition(visitor.toJani(this->getSystemCompositionConstruct().getSystemComposition(), janiModel)); - } else { - janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); - } - - janiModel.finalize(); - - return janiModel; - } - void Program::createMissingInitialValues() { for (auto& variable : globalBooleanVariables) { if (!variable.hasInitialValue()) { diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 41ef5f173..9233d5014 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -566,18 +566,8 @@ namespace storm { * * @return The manager responsible for the expressions of this program. */ - storm::expressions::ExpressionManager const& getManager() const; + storm::expressions::ExpressionManager& getManager() const; - /*! - * Retrieves the manager responsible for the expressions of this program. - * - * @return The manager responsible for the expressions of this program. - */ - storm::expressions::ExpressionManager& getManager(); - - /*! - * - */ std::unordered_map buildCommandIndexToActionNameMap() const; std::unordered_map buildCommandIndexToActionIndex() const; diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp new file mode 100644 index 000000000..c340035ee --- /dev/null +++ b/src/storage/prism/ToJaniConverter.cpp @@ -0,0 +1,187 @@ +#include "src/storage/prism/ToJaniConverter.h" + +#include "src/storage/expressions/ExpressionManager.h" + +#include "src/storage/prism/Program.h" +#include "src/storage/prism/CompositionToJaniVisitor.h" +#include "src/storage/jani/Model.h" + +namespace storm { + namespace prism { + + storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal) { + std::shared_ptr manager = program.getManager().getSharedPointer(); + + // Start by creating an empty JANI model. + storm::jani::ModelType modelType; + switch (program.getModelType()) { + case Program::ModelType::DTMC: modelType = storm::jani::ModelType::DTMC; + break; + case Program::ModelType::CTMC: modelType = storm::jani::ModelType::CTMC; + break; + case Program::ModelType::MDP: modelType = storm::jani::ModelType::MDP; + break; + case Program::ModelType::CTMDP: modelType = storm::jani::ModelType::CTMDP; + break; + case Program::ModelType::MA: modelType = storm::jani::ModelType::MA; + break; + default: modelType = storm::jani::ModelType::UNDEFINED; + } + storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager); + + // Add all constants of the PRISM program to the JANI model. + for (auto const& constant : program.getConstants()) { + janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional(constant.getExpression()) : boost::none)); + } + + // Maintain a mapping from expression variables to JANI variables so we can fill in the correct objects when + // creating assignments. + std::map> variableToVariableMap; + + // Add all global variables of the PRISM program to the JANI model. + for (auto const& variable : program.getGlobalIntegerVariables()) { + if (variable.hasInitialValue()) { + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else { + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } + } + for (auto const& variable : program.getGlobalBooleanVariables()) { + if (variable.hasInitialValue()) { + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false)); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else { + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false)); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } + } + + // Add all actions of the PRISM program to the JANI model. + for (auto const& action : indexToActionMap) { + // Ignore the empty action as every JANI program has predefined tau action. + if (!action.second.empty()) { + janiModel.addAction(storm::jani::Action(action.second)); + } + } + + // Because of the rules of JANI, we have to make all variables of modules global that are read by other modules. + + // Create a mapping from variables to the indices of module indices that write/read the variable. + std::map> variablesToAccessingModuleIndices; + for (uint_fast64_t index = 0; index < program.getNumberOfModules(); ++index) { + storm::prism::Module const& module = program.getModule(index); + + for (auto const& command : module.getCommands()) { + std::set variables = command.getGuardExpression().getVariables(); + for (auto const& variable : variables) { + variablesToAccessingModuleIndices[variable].insert(index); + } + + for (auto const& update : command.getUpdates()) { + for (auto const& assignment : update.getAssignments()) { + variables = assignment.getExpression().getVariables(); + for (auto const& variable : variables) { + variablesToAccessingModuleIndices[variable].insert(index); + } + variablesToAccessingModuleIndices[assignment.getVariable()].insert(index); + } + } + } + } + + // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the + // previously built mapping to make variables global that are read by more than one module. + for (auto const& module : program.getModules()) { + storm::jani::Automaton automaton(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()]; + // If there is exactly one module reading and writing the variable, we can make the variable local to this module. + if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { + storm::jani::BoundedIntegerVariable const& createdVariable = automaton.addVariable(newIntegerVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else if (!accessingModuleIndices.empty()) { + // Otherwise, we need to make it global. + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newIntegerVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } + } + for (auto const& variable : module.getBooleanVariables()) { + storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); + std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; + // If there is exactly one module reading and writing the variable, we can make the variable local to this module. + if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { + storm::jani::BooleanVariable const& createdVariable = automaton.addVariable(newBooleanVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else if (!accessingModuleIndices.empty()) { + // Otherwise, we need to make it global. + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(newBooleanVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } + } + automaton.setInitialStatesRestriction(manager->boolean(true)); + + // Create a single location that will have all the edges. + uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l")); + automaton.addInitialLocation(onlyLocation); + + for (auto const& command : module.getCommands()) { + boost::optional rateExpression; + std::vector destinations; + if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP) { + for (auto const& update : command.getUpdates()) { + if (rateExpression) { + rateExpression = rateExpression.get() + update.getLikelihoodExpression(); + } else { + rateExpression = update.getLikelihoodExpression(); + } + } + } + + for (auto const& update : command.getUpdates()) { + std::vector assignments; + for (auto const& assignment : update.getAssignments()) { + assignments.push_back(storm::jani::Assignment(variableToVariableMap.at(assignment.getVariable()).get(), assignment.getExpression())); + } + + if (rateExpression) { + destinations.push_back(storm::jani::EdgeDestination(onlyLocation, manager->integer(1) / rateExpression.get(), assignments)); + } else { + destinations.push_back(storm::jani::EdgeDestination(onlyLocation, update.getLikelihoodExpression(), assignments)); + } + } + automaton.addEdge(storm::jani::Edge(onlyLocation, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations)); + } + + janiModel.addAutomaton(automaton); + } + + // Translate the reward models. + for (auto const& rewardModel : program.getRewardModels()) { + + } + + // Create an initial state restriction if there was an initial construct in the program. + if (program.hasInitialConstruct()) { + janiModel.setInitialStatesRestriction(program.getInitialConstruct().getInitialStatesExpression()); + } else { + janiModel.setInitialStatesRestriction(manager->boolean(true)); + } + + // Set the standard system composition. This is possible, because we reject non-standard compositions anyway. + if (program.specifiesSystemComposition()) { + CompositionToJaniVisitor visitor; + janiModel.setSystemComposition(visitor.toJani(program.getSystemCompositionConstruct().getSystemComposition(), janiModel)); + } else { + janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); + } + + janiModel.finalize(); + + return janiModel; + } + + } +} \ No newline at end of file diff --git a/src/storage/prism/ToJaniConverter.h b/src/storage/prism/ToJaniConverter.h new file mode 100644 index 000000000..55bed5549 --- /dev/null +++ b/src/storage/prism/ToJaniConverter.h @@ -0,0 +1,20 @@ +#pragma once + +namespace storm { + namespace jani { + class Model; + } + + namespace prism { + + class Program; + + class ToJaniConverter { + public: + ToJaniConverter(); + + storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false) const; + }; + + } +} \ No newline at end of file