diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 2417d03ee..c4f67d17b 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -321,6 +321,15 @@ namespace storm { STORM_LOG_THROW(expr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << "."); } + storm::jani::Variable getLValue(std::string const& ident, storm::jani::VariableSet const& globalVars, storm::jani::VariableSet const& localVars, std::string const& scopeDescription) { + if(localVars.hasVariable(ident)) { + return globalVars.getVariable(ident); + } else if(globalVars.hasVariable(ident)) { + return globalVars.getVariable(ident); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); + } + } storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const &ident,std::string const& scopeDescription, std::unordered_map> const& localVars) { if(localVars.count(ident) == 1) { @@ -552,10 +561,21 @@ namespace storm { 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")) { - STORM_LOG_THROW(locEntry.count("name"), storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name"); + STORM_LOG_THROW(locEntry.count("name") == 1, storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name"); std::string locName = getString(locEntry.at("name"), "location of automaton " + name); STORM_LOG_THROW(locIds.count(locName) == 0, storm::exceptions::InvalidJaniException, "Location with name '" + locName + "' already exists in automaton '" + name + "'"); - uint64_t id = automaton.addLocation(storm::jani::Location(locName)); + + //STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType())); + std::vector transientAssignments; + for(auto const& transientValueEntry : locEntry.at("transient-values")) { + STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to"); + STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value"); + storm::jani::Variable lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')"); + STORM_LOG_THROW(lhs.isTransientVariable(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); + storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); + transientAssignments.emplace_back(lhs, rhs); + } + uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments)); locIds.emplace(locName, id); } STORM_LOG_THROW(automatonStructure.count("initial-locations") == 1, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have initial locations."); @@ -639,7 +659,7 @@ namespace storm { // value STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - assignments.emplace_back(getVariableOrConstantExpression(refstring, "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars), assignmentExpr); + assignments.emplace_back(getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"), assignmentExpr); } edgeDestinations.emplace_back(locIds.at(targetLoc), probExpr, assignments); } diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp index cea88f23e..469446729 100644 --- a/src/storage/jani/Assignment.cpp +++ b/src/storage/jani/Assignment.cpp @@ -3,12 +3,16 @@ namespace storm { namespace jani { - Assignment::Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression) : variable(variable), expression(expression) { + Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression) : variable(variable), expression(expression) { // Intentionally left empty. } + storm::jani::Variable const& Assignment::getVariable() const { + return variable.get(); + } + storm::expressions::Variable const& Assignment::getExpressionVariable() const { - return variable; + return variable.get().getExpressionVariable(); } storm::expressions::Expression const& Assignment::getAssignedExpression() const { @@ -19,8 +23,12 @@ namespace storm { this->expression = expression; } + bool Assignment::isTransientAssignment() const { + return this->variable.get().isTransientVariable(); + } + std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { - stream << assignment.getExpressionVariable().getName() << " := " << assignment.getAssignedExpression(); + stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression(); return stream; } diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h index 58c078d20..e4b562863 100644 --- a/src/storage/jani/Assignment.h +++ b/src/storage/jani/Assignment.h @@ -1,6 +1,8 @@ #pragma once -#include "src/storage/expressions/Variable.h" +#include + +#include "src/storage/jani/Variable.h" #include "src/storage/expressions/Expression.h" namespace storm { @@ -11,8 +13,13 @@ namespace storm { /*! * Creates an assignment of the given expression to the given variable. */ - Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression); + Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression); + /*! + * Retrieves the expression variable that is written in this assignment. + */ + storm::jani::Variable const& getVariable() const; + /*! * Retrieves the expression variable that is written in this assignment. */ @@ -28,11 +35,16 @@ namespace storm { */ void setAssignedExpression(storm::expressions::Expression const& expression); + /** + * Retrieves whether the assignment assigns to a transient variable. + */ + bool isTransientAssignment() const; + friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment); private: // The variable being assigned. - storm::expressions::Variable variable; + std::reference_wrapper variable; // The expression that is being assigned to the variable. storm::expressions::Expression expression; diff --git a/src/storage/jani/Location.cpp b/src/storage/jani/Location.cpp index 84b45ebaf..2f1f1f6b7 100644 --- a/src/storage/jani/Location.cpp +++ b/src/storage/jani/Location.cpp @@ -1,9 +1,12 @@ #include "src/storage/jani/Location.h" +#include "src/storage/jani/Assignment.h" +#include "src/exceptions/InvalidJaniException.h" +#include "src/utility/macros.h" namespace storm { namespace jani { - Location::Location(std::string const& name) : name(name) { + Location::Location(std::string const& name, std::vector const& transientAssignments) : name(name), transientAssignments(transientAssignments) { // Intentionally left empty. } @@ -11,5 +14,15 @@ namespace storm { return name; } + std::vector const& Location::getTransientAssignments() const { + return transientAssignments; + } + + void Location::checkValid() const { + for(auto const& assignment : transientAssignments) { + STORM_LOG_THROW(assignment.isTransientAssignment(), storm::exceptions::InvalidJaniException, "Only transient assignments are allowed in locations."); + } + } + } } \ No newline at end of file diff --git a/src/storage/jani/Location.h b/src/storage/jani/Location.h index 56a08ab2c..349534d06 100644 --- a/src/storage/jani/Location.h +++ b/src/storage/jani/Location.h @@ -1,25 +1,42 @@ #pragma once #include +#include +#include "src/storage/jani/Assignment.h" namespace storm { namespace jani { + /** + * Jani Location: + * + * Whereas Jani Locations also support invariants, we do not have support for them (as we do not support any of the allowed model types) + */ class Location { public: /*! * Creates a new location. */ - Location(std::string const& name); + Location(std::string const& name, std::vector const& transientAssignments = {}); /*! * Retrieves the name of the location. */ std::string const& getName() const; + /*! + * + */ + std::vector const& getTransientAssignments() const; + + /*! + * Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments. + */ + void checkValid() const; private: // The name of the location. std::string name; + std::vector transientAssignments; }; } diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index c1a1e4cf0..bc50af09b 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1511,6 +1511,7 @@ namespace storm { } storm::jani::Model Program::toJani(bool allVariablesGlobal) const { +#if 0 // Start by creating an empty JANI model. storm::jani::ModelType modelType; switch (this->getModelType()) { @@ -1639,7 +1640,7 @@ namespace storm { for (auto const& update : command.getUpdates()) { std::vector assignments; for (auto const& assignment : update.getAssignments()) { - assignments.push_back(storm::jani::Assignment(assignment.getVariable(), assignment.getExpression())); + assignments.push_back(storm::jani::Assignment(assignment.getVariable().getName(), assignment.getExpression())); } if (rateExpression) { @@ -1668,6 +1669,7 @@ namespace storm { janiModel.finalize(); return janiModel; +#endif } std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {