From 7af89f5a6f2e5616b453686aa30a800c6663c419 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 6 Sep 2016 22:50:44 +0200
Subject: [PATCH] real transient variables and assignments are now added in
PRISM to JANI transformation
Former-commit-id: 45ccd460710bc785a1b16b7a7e9311bf6fdd406f [formerly a8d1de9c6afbc0d45873c993307e5eeb381bbd9c]
Former-commit-id: 6aa6dbae52d8596630cef396fcf28fa0600bdbab
---
src/builder/DdJaniModelBuilder.cpp | 18 ++++-
src/generator/JaniNextStateGenerator.cpp | 4 +-
src/storage/jani/Assignment.cpp | 4 +
src/storage/jani/Assignment.h | 5 ++
src/storage/jani/Automaton.cpp | 18 ++++-
src/storage/jani/Automaton.h | 10 +++
src/storage/jani/BoundedIntegerVariable.cpp | 7 +-
src/storage/jani/BoundedIntegerVariable.h | 5 ++
src/storage/jani/Edge.cpp | 21 +++++
src/storage/jani/Edge.h | 15 ++++
src/storage/jani/EdgeDestination.cpp | 13 ++++
src/storage/jani/EdgeDestination.h | 5 ++
src/storage/jani/Location.cpp | 4 +
src/storage/jani/Location.h | 5 ++
src/storage/jani/Model.cpp | 25 +-----
src/storage/jani/Variable.cpp | 7 +-
src/storage/jani/Variable.h | 5 ++
src/storage/jani/VariableSet.cpp | 10 +++
src/storage/jani/VariableSet.h | 7 +-
src/storage/prism/ToJaniConverter.cpp | 85 ++++++++++++++++++---
20 files changed, 232 insertions(+), 41 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 9397ed925..4909245fa 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -188,11 +188,15 @@ namespace storm {
this->model.getSystemComposition().accept(*this, boost::none);
STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
- // Then, check that the model does not contain unbounded integer variables.
+ // Then, check that the model does not contain unbounded integer or non-transient real variables.
STORM_LOG_THROW(!this->model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables.");
for (auto const& automaton : this->model.getAutomata()) {
STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'.");
}
+ STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables.");
+ for (auto const& automaton : this->model.getAutomata()) {
+ STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
+ }
// Based on this assumption, we create the variables.
return createVariables();
@@ -256,6 +260,11 @@ namespace storm {
// Create global variables.
storm::dd::Bdd<Type> globalVariableRanges = result.manager->getBddOne();
for (auto const& variable : this->model.getGlobalVariables()) {
+ // Only create the variable if it's non-transient.
+ if (variable.isTransientVariable()) {
+ continue;
+ }
+
createVariable(variable, result);
globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
}
@@ -274,6 +283,11 @@ namespace storm {
// Then create variables for the variables of the automaton.
for (auto const& variable : automaton.getVariables()) {
+ // Only create the variable if it's non-transient.
+ if (variable.isTransientVariable()) {
+ continue;
+ }
+
createVariable(variable, result);
identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
@@ -391,7 +405,7 @@ namespace storm {
// Iterate over all assignments (boolean and integer) and build the DD for it.
std::set<storm::expressions::Variable> assignedVariables;
- for (auto const& assignment : destination.getAssignments()) {
+ for (auto const& assignment : destination.getNonTransientAssignments()) {
// Record the variable as being written.
STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName());
assignedVariables.insert(assignment.getExpressionVariable());
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 0b2fad41a..ba76f4e86 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -179,8 +179,8 @@ namespace storm {
// within the types, the assignments to variables are ordered (in ascending order) by the expression variables.
// This is guaranteed for JANI models, by sorting the assignments as soon as an edge destination is created.
- auto assignmentIt = destination.getAssignments().begin();
- auto assignmentIte = destination.getAssignments().end();
+ auto assignmentIt = destination.getNonTransientAssignments().begin();
+ auto assignmentIte = destination.getNonTransientAssignments().end();
// Iterate over all boolean assignments and carry them out.
auto boolIt = this->variableInformation.booleanVariables.begin();
diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp
index cea0b9eec..559fc685b 100644
--- a/src/storage/jani/Assignment.cpp
+++ b/src/storage/jani/Assignment.cpp
@@ -31,6 +31,10 @@ namespace storm {
return this->variable.get().isTransientVariable();
}
+ void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ this->setAssignedExpression(this->getAssignedExpression().substitute(substitution));
+ }
+
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression();
return stream;
diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h
index dbdfb7edd..24cc9d10c 100644
--- a/src/storage/jani/Assignment.h
+++ b/src/storage/jani/Assignment.h
@@ -37,6 +37,11 @@ namespace storm {
*/
void setAssignedExpression(storm::expressions::Expression const& expression);
+ /*!
+ * Substitutes all variables in all expressions according to the given substitution.
+ */
+ void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
/**
* Retrieves whether the assignment assigns to a transient variable.
*/
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 9227a4c5b..1a38adea8 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -108,7 +108,11 @@ namespace storm {
Location const& Automaton::getLocation(uint64_t index) const {
return locations[index];
}
-
+
+ Location& Automaton::getLocation(uint64_t index) {
+ 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());
@@ -358,6 +362,18 @@ namespace storm {
return result;
}
+ void Automaton::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ for (auto& variable : this->getVariables().getBoundedIntegerVariables()) {
+ variable.substitute(substitution);
+ }
+
+ this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution));
+
+ for (auto& edge : this->getEdges()) {
+ edge.substitute(substitution);
+ }
+ }
+
void Automaton::finalize(Model const& containingModel) {
for (auto& edge : edges) {
edge.finalize(containingModel);
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index e46fc44be..d023fa36c 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -158,6 +158,11 @@ namespace storm {
*/
Location const& getLocation(uint64_t index) const;
+ /*!
+ * Retrieves the location with the given index.
+ */
+ Location& getLocation(uint64_t index);
+
/*!
* Adds the given location to the automaton.
*/
@@ -268,6 +273,11 @@ namespace storm {
*/
std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
+ /*!
+ * Substitutes all variables in all expressions according to the given substitution.
+ */
+ void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
/*!
* Finalizes the building of this automaton. Subsequent changes to the automaton require another call to this
* method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.
diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp
index 58173bb76..37b458ba4 100644
--- a/src/storage/jani/BoundedIntegerVariable.cpp
+++ b/src/storage/jani/BoundedIntegerVariable.cpp
@@ -21,7 +21,6 @@ namespace storm {
// Intentionally left empty.
}
-
storm::expressions::Expression const& BoundedIntegerVariable::getLowerBound() const {
return lowerBound;
}
@@ -46,6 +45,12 @@ namespace storm {
return true;
}
+ void BoundedIntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ Variable::substitute(substitution);
+ this->setLowerBound(this->getLowerBound().substitute(substitution));
+ this->setUpperBound(this->getUpperBound().substitute(substitution));
+ }
+
std::shared_ptr<BoundedIntegerVariable> makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient, boost::optional<storm::expressions::Expression> lowerBound, boost::optional<storm::expressions::Expression> upperBound) {
STORM_LOG_THROW(lowerBound && upperBound, storm::exceptions::NotImplementedException, "Jani Bounded Integer variables (for now) have to be bounded from both sides");
if (initValue) {
diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h
index 1c68bd239..733024b3d 100644
--- a/src/storage/jani/BoundedIntegerVariable.h
+++ b/src/storage/jani/BoundedIntegerVariable.h
@@ -52,6 +52,11 @@ namespace storm {
virtual bool isBoundedIntegerVariable() const override;
+ /*!
+ * Substitutes all variables in all expressions according to the given substitution.
+ */
+ virtual void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) override;
+
private:
// The expression defining the lower bound of the variable.
storm::expressions::Expression lowerBound;
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
index 430838b61..e1ac1a274 100644
--- a/src/storage/jani/Edge.cpp
+++ b/src/storage/jani/Edge.cpp
@@ -49,6 +49,27 @@ namespace storm {
destinations.push_back(destination);
}
+ std::vector<Assignment>& Edge::getTransientAssignments() {
+ return transientAssignments;
+ }
+
+ std::vector<Assignment> const& Edge::getTransientAssignments() const {
+ return transientAssignments;
+ }
+
+ void Edge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ this->setGuard(this->getGuard().substitute(substitution));
+ if (this->hasRate()) {
+ this->setRate(this->getRate().substitute(substitution));
+ }
+ for (auto& assignment : this->getTransientAssignments()) {
+ assignment.substitute(substitution);
+ }
+ for (auto& destination : this->getDestinations()) {
+ destination.substitute(substitution);
+ }
+ }
+
void Edge::finalize(Model const& containingModel) {
for (auto const& destination : getDestinations()) {
for (auto const& assignment : destination.getAssignments()) {
diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h
index f56685984..47358bb05 100644
--- a/src/storage/jani/Edge.h
+++ b/src/storage/jani/Edge.h
@@ -64,6 +64,21 @@ namespace storm {
*/
void addDestination(EdgeDestination const& destination);
+ /*!
+ * Retrieves the transient assignments of this edge.
+ */
+ std::vector<Assignment>& getTransientAssignments();
+
+ /*!
+ * Retrieves the transient assignments of this edge.
+ */
+ std::vector<Assignment> const& getTransientAssignments() const;
+
+ /*!
+ * Substitutes all variables in all expressions according to the given substitution.
+ */
+ void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
/*!
* Finalizes the building of this edge. Subsequent changes to the edge require another call to this
* method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.
diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp
index f49b15eac..c59018e38 100644
--- a/src/storage/jani/EdgeDestination.cpp
+++ b/src/storage/jani/EdgeDestination.cpp
@@ -72,6 +72,19 @@ namespace storm {
return transientAssignments;
}
+ void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ this->setProbability(this->getProbability().substitute(substitution));
+ for (auto& assignment : this->getAssignments()) {
+ assignment.substitute(substitution);
+ }
+ for (auto& assignment : this->getTransientAssignments()) {
+ assignment.substitute(substitution);
+ }
+ for (auto& assignment : this->getNonTransientAssignments()) {
+ assignment.substitute(substitution);
+ }
+ }
+
bool EdgeDestination::hasAssignment(Assignment const& assignment) const {
for (auto const& containedAssignment : assignments) {
if (containedAssignment == assignment) {
diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h
index 9d3f8326d..02da155e1 100644
--- a/src/storage/jani/EdgeDestination.h
+++ b/src/storage/jani/EdgeDestination.h
@@ -66,6 +66,11 @@ namespace storm {
*/
std::vector<Assignment> const& getTransientAssignments() const;
+ /*!
+ * Substitutes all variables in all expressions according to the given substitution.
+ */
+ void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
/*!
* Retrieves whether this assignment is made when choosing this destination.
*
diff --git a/src/storage/jani/Location.cpp b/src/storage/jani/Location.cpp
index 2f1f1f6b7..32d17531e 100644
--- a/src/storage/jani/Location.cpp
+++ b/src/storage/jani/Location.cpp
@@ -18,6 +18,10 @@ namespace storm {
return transientAssignments;
}
+ void Location::addTransientAssignment(storm::jani::Assignment const& assignment) {
+ transientAssignments.push_back(assignment);
+ }
+
void Location::checkValid() const {
for(auto const& assignment : transientAssignments) {
STORM_LOG_THROW(assignment.isTransientAssignment(), storm::exceptions::InvalidJaniException, "Only transient assignments are allowed in locations.");
diff --git a/src/storage/jani/Location.h b/src/storage/jani/Location.h
index 461b68e1f..e80faedf9 100644
--- a/src/storage/jani/Location.h
+++ b/src/storage/jani/Location.h
@@ -29,6 +29,11 @@ namespace storm {
*/
std::vector<Assignment> const& getTransientAssignments() const;
+ /*!
+ * Adds the given transient assignment to this location.
+ */
+ void addTransientAssignment(storm::jani::Assignment const& assignment);
+
/*!
* Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments.
*/
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 08a243c06..9d0dcb7d0 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -310,9 +310,7 @@ namespace storm {
// Substitute constants in all global variables.
for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
- variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
- variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
- variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
+ variable.substitute(constantSubstitution);
}
// Substitute constants in initial states expression.
@@ -320,26 +318,7 @@ namespace storm {
// Substitute constants in variables of automata and their edges.
for (auto& automaton : result.getAutomata()) {
- for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
- variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
- variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
- variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
- }
-
- automaton.setInitialStatesRestriction(automaton.getInitialStatesExpression().substitute(constantSubstitution));
-
- for (auto& edge : automaton.getEdges()) {
- edge.setGuard(edge.getGuard().substitute(constantSubstitution));
- if (edge.hasRate()) {
- edge.setRate(edge.getRate().substitute(constantSubstitution));
- }
- for (auto& destination : edge.getDestinations()) {
- destination.setProbability(destination.getProbability().substitute(constantSubstitution));
- for (auto& assignment : destination.getAssignments()) {
- assignment.setAssignedExpression(assignment.getAssignedExpression().substitute(constantSubstitution));
- }
- }
- }
+ automaton.substitute(constantSubstitution);
}
return result;
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index 4027ea112..763179013 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -16,7 +16,6 @@ namespace storm {
// Intentionally left empty.
}
-
storm::expressions::Variable const& Variable::getExpressionVariable() const {
return variable;
}
@@ -89,5 +88,11 @@ namespace storm {
return static_cast<RealVariable const&>(*this);
}
+ void Variable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+ if (this->hasInitExpression()) {
+ this->setInitExpression(this->getInitExpression().substitute(substitution));
+ }
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index 8d25bfd36..fa56e0a8d 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -73,6 +73,11 @@ namespace storm {
RealVariable& asRealVariable();
RealVariable const& asRealVariable() const;
+ /*!
+ * Substitutes all variables in all expressions according to the given substitution.
+ */
+ virtual void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
private:
// The name of the variable.
std::string name;
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index 27806a132..7b304e68d 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -174,6 +174,16 @@ namespace storm {
return !realVariables.empty();
}
+ bool VariableSet::containsNonTransientRealVariables() const {
+ for (auto const& variable : realVariables) {
+ if (!variable->isTransientVariable()) {
+ std::cout << "var " << variable->getName() << "is non-transient " << std::endl;
+ return true;
+ }
+ }
+ return false;
+ }
+
bool VariableSet::empty() const {
return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables());
}
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index 651787df5..4156faec1 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -184,10 +184,15 @@ namespace storm {
bool containsUnboundedIntegerVariables() const;
/*!
- * Retrieves whether the set of variables contains an unbounded integer variable.
+ * Retrieves whether the set of variables contains a real variable.
*/
bool containsRealVariables() const;
+ /*!
+ * Retrieves whether the set of variables contains a non-transient real variable.
+ */
+ bool containsNonTransientRealVariables() const;
+
/*!
* Retrieves whether this variable set is empty.
*/
diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp
index 2e5631ebc..7c3d859b2 100644
--- a/src/storage/prism/ToJaniConverter.cpp
+++ b/src/storage/prism/ToJaniConverter.cpp
@@ -6,6 +6,9 @@
#include "src/storage/prism/CompositionToJaniVisitor.h"
#include "src/storage/jani/Model.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/NotImplementedException.h"
+
namespace storm {
namespace prism {
@@ -91,8 +94,53 @@ namespace storm {
}
}
+ // Go through the reward models and construct assignments to the transient variables that are to be added to
+ // edges and transient assignments that are added to the locations.
+ std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments;
+ std::vector<storm::jani::Assignment> transientLocationAssignments;
+ for (auto const& rewardModel : program.getRewardModels()) {
+ auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName());
+ storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName(), newExpressionVariable, true));
+
+ if (rewardModel.hasStateRewards()) {
+ storm::expressions::Expression transientLocationExpression;
+ for (auto const& stateReward : rewardModel.getStateRewards()) {
+ storm::expressions::Expression rewardTerm = stateReward.getStatePredicateExpression().isTrue() ? stateReward.getRewardValueExpression() : storm::expressions::ite(stateReward.getStatePredicateExpression(), stateReward.getRewardValueExpression(), manager->rational(0));
+ if (transientLocationExpression.isInitialized()) {
+ transientLocationExpression = transientLocationExpression + rewardTerm;
+ } else {
+ transientLocationExpression = rewardTerm;
+ }
+ }
+ transientLocationAssignments.emplace_back(newTransientVariable, transientLocationExpression);
+ }
+
+ std::map<uint_fast64_t, storm::expressions::Expression> actionIndexToExpression;
+ for (auto const& actionReward : rewardModel.getStateActionRewards()) {
+ storm::expressions::Expression rewardTerm = actionReward.getStatePredicateExpression().isTrue() ? actionReward.getRewardValueExpression() : storm::expressions::ite(actionReward.getStatePredicateExpression(), actionReward.getRewardValueExpression(), manager->rational(0));
+ auto it = actionIndexToExpression.find(janiModel.getActionIndex(actionReward.getActionName()));
+ if (it != actionIndexToExpression.end()) {
+ it->second = it->second + rewardTerm;
+ } else {
+ actionIndexToExpression[janiModel.getActionIndex(actionReward.getActionName())] = rewardTerm;
+ }
+ }
+
+ for (auto const& entry : actionIndexToExpression) {
+ auto it = transientEdgeAssignments.find(entry.first);
+ if (it != transientEdgeAssignments.end()) {
+ it->second.push_back(storm::jani::Assignment(newTransientVariable, entry.second));
+ } else {
+ std::vector<storm::jani::Assignment> assignments = {storm::jani::Assignment(newTransientVariable, entry.second)};
+ transientEdgeAssignments.emplace(entry.first, assignments);
+ }
+ }
+ STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
+ }
+
// 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.
+ bool firstModule = true;
for (auto const& module : program.getModules()) {
storm::jani::Automaton automaton(module.getName());
for (auto const& variable : module.getIntegerVariables()) {
@@ -124,8 +172,16 @@ namespace storm {
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);
+ uint64_t onlyLocationIndex = automaton.addLocation(storm::jani::Location("l"));
+ automaton.addInitialLocation(onlyLocationIndex);
+
+ // If we are translating the first module, we need to add the transient assignments to the location.
+ if (firstModule) {
+ storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex);
+ for (auto const& assignment : transientLocationAssignments) {
+ onlyLocation.addTransientAssignment(assignment);
+ }
+ }
for (auto const& command : module.getCommands()) {
boost::optional<storm::expressions::Expression> rateExpression;
@@ -147,20 +203,29 @@ namespace storm {
}
if (rateExpression) {
- destinations.push_back(storm::jani::EdgeDestination(onlyLocation, manager->integer(1) / rateExpression.get(), assignments));
+ destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, manager->integer(1) / rateExpression.get(), assignments));
} else {
- destinations.push_back(storm::jani::EdgeDestination(onlyLocation, update.getLikelihoodExpression(), assignments));
+ destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, update.getLikelihoodExpression(), assignments));
}
}
- automaton.addEdge(storm::jani::Edge(onlyLocation, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations));
+
+ // Create the edge object so we can add transient assignments.
+ storm::jani::Edge newEdge(onlyLocationIndex, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations);
+
+ // Then add the transient assignments for the rewards.
+ auto transientEdgeAssignmentsToAdd = transientEdgeAssignments.find(janiModel.getActionIndex(command.getActionName()));
+ if (transientEdgeAssignmentsToAdd != transientEdgeAssignments.end()) {
+ for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
+ newEdge.addTransientAssignment(assignment);
+ }
+ }
+
+ // Finally add the constructed edge.
+ automaton.addEdge(newEdge);
}
janiModel.addAutomaton(automaton);
- }
-
- // Translate the reward models.
- for (auto const& rewardModel : program.getRewardModels()) {
-
+ firstModule = false;
}
// Create an initial state restriction if there was an initial construct in the program.