diff --git a/src/builder/jit/Choice.cpp b/src/builder/jit/Choice.cpp
index 52477d00a..5173591fa 100644
--- a/src/builder/jit/Choice.cpp
+++ b/src/builder/jit/Choice.cpp
@@ -23,7 +23,7 @@ namespace storm {
template <typename IndexType, typename ValueType>
void Choice<IndexType, ValueType>::add(Choice<IndexType, ValueType>&& choice) {
- distribution.add(std::move(choice.getDistribution()));
+ distribution.add(std::move(choice.getMutableDistribution()));
}
template <typename IndexType, typename ValueType>
@@ -41,6 +41,11 @@ namespace storm {
rewards.push_back(value);
}
+ template <typename IndexType, typename ValueType>
+ void Choice<IndexType, ValueType>::addReward(uint64_t index, ValueType const& value) {
+ rewards[index] += value;
+ }
+
template <typename IndexType, typename ValueType>
void Choice<IndexType, ValueType>::addRewards(std::vector<ValueType>&& values) {
rewards = std::move(values);
@@ -51,13 +56,28 @@ namespace storm {
return rewards;
}
+ template <typename IndexType, typename ValueType>
+ void Choice<IndexType, ValueType>::setRewards(std::vector<ValueType>&& rewards) {
+ this->rewards = std::move(rewards);
+ }
+
+ template <typename IndexType, typename ValueType>
+ void Choice<IndexType, ValueType>::resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue) {
+ rewards.resize(numberOfRewards, fillValue);
+ }
+
+ template <typename IndexType, typename ValueType>
+ std::size_t Choice<IndexType, ValueType>::getNumberOfRewards() const {
+ return rewards.size();
+ }
+
template <typename IndexType, typename ValueType>
void Choice<IndexType, ValueType>::compress() {
distribution.compress();
}
template <typename IndexType, typename ValueType>
- Distribution<IndexType, ValueType>& Choice<IndexType, ValueType>::getDistribution() {
+ Distribution<IndexType, ValueType>& Choice<IndexType, ValueType>::getMutableDistribution() {
return distribution;
}
diff --git a/src/builder/jit/Choice.h b/src/builder/jit/Choice.h
index 6ed4bb63a..400bb9dbe 100644
--- a/src/builder/jit/Choice.h
+++ b/src/builder/jit/Choice.h
@@ -23,6 +23,11 @@ namespace storm {
*/
void addReward(ValueType const& value);
+ /*!
+ * Adds the given value to the reward with the given index of this choice.
+ */
+ void addReward(uint64_t index, ValueType const& value);
+
/*!
* Adds the given choices rewards to this choice.
*/
@@ -33,13 +38,28 @@ namespace storm {
*/
std::vector<ValueType> const& getRewards() const;
+ /*!
+ * Sets the given values as the rewards of this choice.
+ */
+ void setRewards(std::vector<ValueType>&& rewards);
+
+ /*!
+ * Resizes the rewards to the desired size and filles newly created values with the provided value.
+ */
+ void resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue);
+
+ /*!
+ * Retrieves the number of rewards of this choice.
+ */
+ std::size_t getNumberOfRewards() const;
+
/*!
* Compresses the underlying distribution.
*/
void compress();
private:
- Distribution<IndexType, ValueType>& getDistribution();
+ Distribution<IndexType, ValueType>& getMutableDistribution();
/// The distribution of this choice.
Distribution<IndexType, ValueType> distribution;
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 1b6e7859e..8a1e6806f 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -10,6 +10,8 @@
#include "src/storage/jani/AutomatonComposition.h"
#include "src/storage/jani/ParallelComposition.h"
+#include "src/builder/RewardModelInformation.h"
+
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/StandardRewardModel.h"
@@ -44,35 +46,34 @@ namespace storm {
}
// Construct vector of the automata to be put in parallel.
- storm::jani::Composition const& topLevelComposition = model.getSystemComposition();
+ storm::jani::Composition const& topLevelComposition = this->model.getSystemComposition();
if (topLevelComposition.isAutomatonComposition()) {
- parallelAutomata.push_back(model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName()));
+ parallelAutomata.push_back(this->model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName()));
} else {
STORM_LOG_ASSERT(topLevelComposition.isParallelComposition(), "Expected parallel composition.");
storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition();
for (auto const& composition : parallelComposition.getSubcompositions()) {
STORM_LOG_ASSERT(composition->isAutomatonComposition(), "Expected flat parallel composition.");
- parallelAutomata.push_back(model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()));
+ parallelAutomata.push_back(this->model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()));
}
}
- // FIXME: just for testing purposes.
for (auto& automaton : this->model.getAutomata()) {
automaton.pushEdgeAssignmentsToDestinations();
}
for (auto const& automaton : parallelAutomata) {
- automatonToLocationVariable.emplace(automaton.get().getName(), model.getManager().declareFreshIntegerVariable(false, automaton.get().getName() + "_"));
+ automatonToLocationVariable.emplace(automaton.get().getName(), this->model.getManager().declareFreshIntegerVariable(false, automaton.get().getName() + "_"));
}
// If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
#ifdef STORM_HAVE_CARL
- if (!std::is_same<ValueType, storm::RationalFunction>::value && model.hasUndefinedConstants()) {
+ if (!std::is_same<ValueType, storm::RationalFunction>::value && this->model.hasUndefinedConstants()) {
#else
- if (model.hasUndefinedConstants()) {
+ if (this->model.hasUndefinedConstants()) {
#endif
- std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
+ std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = this->model.getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
@@ -88,7 +89,7 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
- else if (std::is_same<ValueType, storm::RationalFunction>::value && !model.undefinedConstantsAreGraphPreserving()) {
+ else if (std::is_same<ValueType, storm::RationalFunction>::value && !this->model.undefinedConstantsAreGraphPreserving()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed.");
}
#endif
@@ -114,6 +115,7 @@ namespace storm {
#include "src/builder/jit/JitModelBuilderInterface.h"
#include "src/builder/jit/StateBehaviour.h"
#include "src/builder/jit/ModelComponentsBuilder.h"
+#include "src/builder/RewardModelInformation.h"
namespace storm {
namespace builder {
@@ -402,7 +404,7 @@ namespace storm {
public:
typedef std::vector<Destination> ContainerType;
- Edge() : edgeEnabledFunction(nullptr) {
+ Edge() : edgeEnabledFunction(nullptr), edgeTransientFunction(nullptr) {
// Intentionally left empty.
}
@@ -444,7 +446,7 @@ namespace storm {
ContainerType destinations;
};
- void locations_perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& out) {
+ void locations_perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) {
{% for location in locations %}if ({$location.guard}) {
{% for assignment in location.assignments %}transientOut.{$assignment.variable} = {$assignment.value};{% endfor %}
}
@@ -461,17 +463,20 @@ namespace storm {
initialStates.push_back(state);
}{% endfor %}
{% for edge in nonsynch_edges %}{
- edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}{% if edge.transient_assignments %}, edge_perform_{$edge.name}{% endif %});
+ edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name});
{% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name});
{% endfor %}
}
{% endfor %}
{% for edge in synch_edges %}{
- edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}{% if edge.transient_assignments %}, edge_perform_{$edge.name}{% endif %});
+ edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name});
{% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name});
{% endfor %}
}
{% endfor %}
+ {% for reward in rewards %}
+ modelComponentsBuilder.registerRewardModel(RewardModelInformation("{$reward.name}", {$reward.location_rewards}, {$reward.edge_rewards} || {$reward.destination_rewards}, false));
+ {% endfor %}
}
virtual storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* build() override {
@@ -495,7 +500,7 @@ namespace storm {
this->modelComponentsBuilder.registerLabel("deadlock", stateIds.size());
for (auto const& stateEntry : stateIds) {
- auto const& state = stateEntry.first;
+ auto const& in = stateEntry.first;
{% for label in labels %}if ({$label.predicate}) {
this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1);
}
@@ -540,6 +545,9 @@ namespace storm {
TransientVariables transientIn;
TransientVariables transientOut;
locations_perform(currentState, transientIn, transientOut);
+ {% for reward in location_rewards %}
+ behaviour.addStateReward(transientOut.{$reward.variable});
+ {% endfor %}
// Explore all edges that do not take part in synchronization vectors.
exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore);
@@ -564,17 +572,27 @@ namespace storm {
void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
{% for edge in nonsynch_edges %}{
if ({$edge.guard}) {
- TransientVariables transientIn;
- TransientVariables transientOut;
- {% if edge.transient_assignments %}
- edge_perform_{$edge.name}(in, transientIn, transientOut);
- {% endif %}
Choice<IndexType, ValueType>& choice = behaviour.addChoice();
+ choice.resizeRewards({$edge_destination_rewards_count}, 0);
+ {
+ TransientVariables transient;
+ {% if edge.transient_assignments %}
+ edge_perform_{$edge.name}(in, transient, transient);
+ {% endif %}
+ {% for reward in edge_rewards %}
+ choice.addReward({$reward.index}, transient.{$reward.variable});
+ {% endfor %}
+ }
{% for destination in edge.destinations %}{
StateType out(in);
+ TransientVariables transientIn;
+ TransientVariables transientOut;
destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.transient_variables_in_destinations %}, transientIn, transientOut{% endif %});
IndexType outStateIndex = getOrAddIndex(out, statesToExplore);
choice.add(outStateIndex, {$destination.value});
+ {% for reward in destination_rewards %}
+ choice.addReward({$reward.index}, transientOut.{$reward.variable});
+ {% endfor %}
}
{% endfor %}
}
@@ -649,9 +667,11 @@ namespace storm {
generateVariables(modelData);
cpptempl::data_list initialStates = generateInitialStates();
modelData["initialStates"] = cpptempl::make_data(initialStates);
+
+ // We need to generate the reward information before the edges, because we already use it there.
+ generateRewards(modelData);
generateEdges(modelData);
generateLocations(modelData);
- generateRewards(modelData);
cpptempl::data_list labels = generateLabels();
modelData["labels"] = cpptempl::make_data(labels);
cpptempl::data_list terminalExpressions = generateTerminalExpressions();
@@ -767,7 +787,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateBooleanVariable(storm::jani::BooleanVariable const& variable) {
cpptempl::data_map result;
- result["name"] = registerVariable(variable.getExpressionVariable());
+ result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient());
if (variable.hasInitExpression()) {
result["init"] = asString(variable.getInitExpression().evaluateAsBool());
}
@@ -788,7 +808,7 @@ namespace storm {
uint64_t range = static_cast<uint64_t>(upperBound - lowerBound + 1);
uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
- result["name"] = registerVariable(variable.getExpressionVariable());
+ result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient());
result["numberOfBits"] = std::to_string(numberOfBits);
if (variable.hasInitExpression()) {
result["init"] = asString(variable.getInitExpression().evaluateAsInt() - lowerBound);
@@ -801,7 +821,7 @@ namespace storm {
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateUnboundedIntegerVariable(storm::jani::UnboundedIntegerVariable const& variable) {
cpptempl::data_map result;
- result["name"] = registerVariable(variable.getExpressionVariable());
+ result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient());
if (variable.hasInitExpression()) {
result["init"] = asString(variable.getInitExpression().evaluateAsInt());
}
@@ -813,7 +833,7 @@ namespace storm {
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateRealVariable(storm::jani::RealVariable const& variable) {
cpptempl::data_map result;
- result["name"] = registerVariable(variable.getExpressionVariable());
+ result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient());
if (variable.hasInitExpression()) {
result["init"] = asString(variable.getInitExpression().evaluateAsDouble());
}
@@ -825,7 +845,7 @@ namespace storm {
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLocationVariable(storm::jani::Automaton const& automaton) {
cpptempl::data_map result;
- result["name"] = registerVariable(getLocationVariable(automaton));
+ result["name"] = registerVariable(getLocationVariable(automaton), false);
result["numberOfBits"] = static_cast<uint64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
return result;
@@ -946,7 +966,11 @@ namespace storm {
assignments.push_back(generateAssignment(assignment));
}
locationData["assignments"] = cpptempl::make_data(assignments);
- locationData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(getLocationVariable(automaton) == this->model.getManager().integer(locationIndex)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+ if (automaton.getNumberOfLocations() > 1) {
+ locationData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(getLocationVariable(automaton) == this->model.getManager().integer(locationIndex)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+ } else {
+ locationData["guard"] = asString(true);
+ }
++locationIndex;
}
if (!locationData["assignments"]->empty()) {
@@ -959,14 +983,12 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateRewards(cpptempl::data_map& modelData) {
- cpptempl::data_list rewards;
-
// Extract the reward models from the program based on the names we were given.
- std::vector<std::reference_wrapper<storm::jani::Variable const>> rewardVariables;
+ std::vector<storm::expressions::Variable> rewardVariables;
auto const& globalVariables = model.getGlobalVariables();
for (auto const& rewardModelName : this->options.getRewardModelNames()) {
if (globalVariables.hasVariable(rewardModelName)) {
- rewardVariables.push_back(globalVariables.getVariable(rewardModelName));
+ rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
} else {
STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
@@ -979,17 +1001,93 @@ namespace storm {
bool foundTransientVariable = false;
for (auto const& transientVariable : globalVariables.getTransientVariables()) {
if (transientVariable.isUnboundedIntegerVariable() || transientVariable.isRealVariable()) {
- rewardVariables.push_back(transientVariable);
+ rewardVariables.push_back(transientVariable.getExpressionVariable());
foundTransientVariable = true;
break;
}
}
STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable.");
}
+
+ std::vector<storm::builder::RewardModelInformation> rewardModels;
+ cpptempl::data_list rewards;
+ cpptempl::data_list locationRewards;
+ cpptempl::data_list edgeRewards;
+ cpptempl::data_list destinationRewards;
+ uint64_t rewardModelIndex = 0;
+ uint64_t stateActionRewardCount = 0;
+ for (auto const& variable : rewardVariables) {
+ bool hasLocationRewards = false;
+ bool hasEdgeRewards = false;
+ bool hasDestinationRewards = false;
+
+ for (auto const& automatonRef : parallelAutomata) {
+ storm::jani::Automaton const& automaton = automatonRef.get();
+
+ for (auto const& location : automaton.getLocations()) {
+ for (auto const& assignment : location.getAssignments()) {
+ if (assignment.getExpressionVariable() == variable) {
+ hasLocationRewards = true;
+ break;
+ }
+ }
+ }
+
+ for (auto const& edge : automaton.getEdges()) {
+ for (auto const& assignment : edge.getAssignments()) {
+ if (assignment.getExpressionVariable() == variable) {
+ hasEdgeRewards = true;
+ }
+ }
+
+ for (auto const& destination : edge.getDestinations()) {
+ for (auto const& assignment : destination.getOrderedAssignments()) {
+ if (assignment.getExpressionVariable() == variable) {
+ hasDestinationRewards = true;
+ }
+ }
+ }
+ }
+ }
+
+ rewardModels.emplace_back(variable.getName(), hasLocationRewards, hasEdgeRewards || hasDestinationRewards, false);
+
+ if (hasEdgeRewards || hasDestinationRewards) {
+ ++stateActionRewardCount;
+ }
+
+ cpptempl::data_map reward;
+ reward["name"] = variable.getName();
+ reward["location_rewards"] = asString(hasLocationRewards);
+ reward["edge_rewards"] = asString(hasEdgeRewards);
+ reward["destination_rewards"] = asString(hasDestinationRewards);
+ rewards.push_back(reward);
+
+ if (hasLocationRewards) {
+ cpptempl::data_map locationReward;
+ locationReward["variable"] = variable.getName();
+ locationRewards.push_back(locationReward);
+ }
+ if (hasEdgeRewards) {
+ cpptempl::data_map edgeReward;
+ edgeReward["variable"] = variable.getName();
+ edgeReward["index"] = asString(rewardModelIndex);
+ edgeRewards.push_back(edgeReward);
+ }
+ if (hasDestinationRewards) {
+ cpptempl::data_map destinationReward;
+ destinationReward["index"] = asString(rewardModelIndex);
+ destinationReward["variable"] = variable.getName();
+ destinationRewards.push_back(destinationReward);
+ }
+ ++rewardModelIndex;
+ }
-
-
+ modelData["location_rewards"] = cpptempl::make_data(locationRewards);
+ modelData["edge_rewards"] = cpptempl::make_data(edgeRewards);
+ modelData["destination_rewards"] = cpptempl::make_data(destinationRewards);
modelData["rewards"] = cpptempl::make_data(rewards);
+ modelData["edge_destination_rewards_count"] = asString(stateActionRewardCount);
}
template <typename ValueType, typename RewardModelType>
@@ -1053,7 +1151,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
- cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateSynchronizationVector(storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) {
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) {
std::stringstream vectorSource;
uint64_t numberOfActionInputs = synchronizationVector.getNumberOfActionInputs();
@@ -1130,14 +1228,19 @@ namespace storm {
indent(vectorSource, indentLevel + 1) << "}" << std::endl;
}
indent(vectorSource, indentLevel + 1) << "IndexType outStateIndex = getOrAddIndex(out, statesToExplore);" << std::endl;
- indent(vectorSource, indentLevel + 1) << "choice.add(outStateIndex, ";
+ indent(vectorSource, indentLevel + 1) << "ValueType probability = ";
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
vectorSource << "destination" << index << ".value()";
if (index + 1 < numberOfActionInputs) {
vectorSource << " * ";
}
}
- vectorSource << ");" << std::endl;
+ vectorSource << ";" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "choice.add(outStateIndex, probability);";
+
+ std::stringstream tmp;
+ indent(tmp, indentLevel + 1) << "{% for reward in destination_rewards %}choice.addReward({$reward.index}, probability * transientOut.{$reward.variable});" << std::endl;
+ indent(tmp, indentLevel + 1) << "{% endfor %}" << std::endl;
indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
indent(vectorSource, indentLevel) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
@@ -1184,19 +1287,32 @@ namespace storm {
vectorSource << ", ";
}
}
+ if (index > 0) {
+ vectorSource << ", TransientVariables const& transientIn, TransientVariables& transientOut";
+ }
vectorSource << ") {" << std::endl;
+ if (index == 0) {
+ indent(vectorSource, indentLevel + 1) << "TransientVariables transientIn;" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "TransientVariables transientOut;" << std::endl;
+ }
indent(vectorSource, indentLevel + 1) << "for (auto const& edge" << index << " : edges[" << index << "]) {" << std::endl;
+ indent(vectorSource, indentLevel + 2) << "edge" << index << ".perform(in, transientIn, transientOut);" << std::endl;
if (index + 1 < numberOfActionInputs) {
indent(vectorSource, indentLevel + 2) << "performSynchronizedEdges_" << synchronizationVectorIndex << "_" << (index + 1) << "(in, edges, behaviour, statesToExplore, ";
for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) {
- vectorSource << "edge" << innerIndex;
- if (innerIndex + 1 <= index) {
- vectorSource << ", ";
- }
+ vectorSource << "edge" << innerIndex << ", ";
}
- vectorSource << ");" << std::endl;
+ vectorSource << "transientIn, transientOut);" << std::endl;
} else {
indent(vectorSource, indentLevel + 2) << "Choice<IndexType, ValueType>& choice = behaviour.addChoice();" << std::endl;
+
+ std::stringstream tmp;
+ indent(tmp, indentLevel + 2) << "choice.resizeRewards({$edge_destination_rewards_count}, 0);" << std::endl;
+ indent(tmp, indentLevel + 2) << "{% for reward in edge_rewards %}choice.addReward({$reward.index}, transientOut.{$reward.variable});" << std::endl;
+ indent(tmp, indentLevel + 2) << "{% endfor %}" << std::endl;
+
+ vectorSource << cpptempl::parse(tmp.str(), modelData);
+
indent(vectorSource, indentLevel + 2) << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, ";
for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) {
vectorSource << "edge" << innerIndex << ", ";
@@ -1308,7 +1424,7 @@ namespace storm {
}
if (createVector) {
- cpptempl::data_map vector = generateSynchronizationVector(parallelComposition, synchronizationVector, synchronizationVectorIndex);
+ cpptempl::data_map vector = generateSynchronizationVector(modelData, parallelComposition, synchronizationVector, synchronizationVectorIndex);
vectors.push_back(vector);
}
++synchronizationVectorIndex;
@@ -1500,7 +1616,7 @@ namespace storm {
std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::registerVariable(storm::expressions::Variable const& variable, bool transient) {
std::string variableName;
- // Technically, we would need to catch all keywords here...
+ // FIXME: Technically, we would need to catch all keywords here...
if (variable.getName() == "default") {
variableName = "__default";
} else {
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h
index f6ced6195..bb0f47aa0 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.h
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h
@@ -66,7 +66,7 @@ namespace storm {
cpptempl::data_list generateLabels();
cpptempl::data_list generateTerminalExpressions();
void generateEdges(cpptempl::data_map& modelData);
- cpptempl::data_map generateSynchronizationVector(storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex);
+ cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex);
cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments);
cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge);
diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp
index 550cb43b2..21056d4b8 100644
--- a/src/builder/jit/StateBehaviour.cpp
+++ b/src/builder/jit/StateBehaviour.cpp
@@ -2,6 +2,8 @@
#include "src/adapters/CarlAdapter.h"
+#include "src/utility/constants.h"
+
namespace storm {
namespace builder {
namespace jit {
@@ -47,9 +49,42 @@ namespace storm {
if (choices.size() > 1) {
if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) {
std::size_t totalCount = choices.size();
+
+ ValueType totalExitRate = modelType == storm::jani::ModelType::DTMC ? static_cast<ValueType>(totalCount) : storm::utility::zero<ValueType>();
+
+ if (choices.front().getNumberOfRewards() > 0) {
+ std::vector<ValueType> newRewards(choices.front().getNumberOfRewards());
+
+ if (modelType == storm::jani::ModelType::CTMC) {
+ for (auto const& choice : choices) {
+ ValueType massOfChoice = storm::utility::zero<ValueType>();
+ for (auto const& entry : choices.front().getDistribution()) {
+ massOfChoice += entry.getValue();
+ }
+
+ auto outIt = newRewards.begin();
+ for (auto const& reward : choice.getRewards()) {
+ *outIt += reward * massOfChoice / totalExitRate;
+ ++outIt;
+ }
+ }
+ } else {
+ for (auto const& choice : choices) {
+ auto outIt = newRewards.begin();
+ for (auto const& reward : choice.getRewards()) {
+ *outIt += reward / totalExitRate;
+ ++outIt;
+ }
+ }
+ }
+
+ choices.front().setRewards(std::move(newRewards));
+ }
+
for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) {
choices.front().add(std::move(*it));
}
+
choices.resize(1);
choices.front().compress();
@@ -89,6 +124,7 @@ namespace storm {
template <typename IndexType, typename ValueType>
void StateBehaviour<IndexType, ValueType>::clear() {
choices.clear();
+ stateRewards.clear();
expanded = false;
}
diff --git a/src/builder/jit/StateBehaviour.h b/src/builder/jit/StateBehaviour.h
index 02e343674..52c4d0318 100644
--- a/src/builder/jit/StateBehaviour.h
+++ b/src/builder/jit/StateBehaviour.h
@@ -27,7 +27,7 @@ namespace storm {
* Adds the given state rewards to the behavior of the state.
*/
void addStateRewards(std::vector<ValueType>&& stateRewards);
-
+
/*!
* Retrieves the rewards for this state.
*/
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 71a61b4fe..5d8dd23dd 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -315,6 +315,9 @@ namespace storm {
*/
bool containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
+ /*!
+ * Pushes the edge assignments to the corresponding destinations.
+ */
void pushEdgeAssignmentsToDestinations();
/*!
diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp
index 5a30ec00e..0cb150759 100644
--- a/src/storage/jani/Edge.cpp
+++ b/src/storage/jani/Edge.cpp
@@ -114,13 +114,13 @@ namespace storm {
}
void Edge::pushAssignmentsToDestinations() {
- assert(!destinations.empty());
+ STORM_LOG_ASSERT(!destinations.empty(), "Need non-empty destinations for this transformation.");
for (auto const& assignment : this->getAssignments()) {
for (auto& destination : destinations) {
destination.addAssignment(assignment);
}
}
- assignments = OrderedAssignments();
+ this->assignments.clear();
}
boost::container::flat_set<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {
diff --git a/src/storage/jani/OrderedAssignments.cpp b/src/storage/jani/OrderedAssignments.cpp
index e8b994a59..5109120af 100644
--- a/src/storage/jani/OrderedAssignments.cpp
+++ b/src/storage/jani/OrderedAssignments.cpp
@@ -80,6 +80,12 @@ namespace storm {
return allAssignments.empty();
}
+ void OrderedAssignments::clear() {
+ allAssignments.clear();
+ transientAssignments.clear();
+ nonTransientAssignments.clear();
+ }
+
int_fast64_t OrderedAssignments::getLowestLevel() const {
return allAssignments.front()->getLevel();
}
diff --git a/src/storage/jani/OrderedAssignments.h b/src/storage/jani/OrderedAssignments.h
index e4556c3e2..04472ad16 100644
--- a/src/storage/jani/OrderedAssignments.h
+++ b/src/storage/jani/OrderedAssignments.h
@@ -47,6 +47,11 @@ namespace storm {
*/
bool empty() const;
+ /*!
+ * Removes all assignments from this set.
+ */
+ void clear();
+
/*!
* Retrieves the lowest level among all assignments. Note that this may only be called if there is at least
* one assignment.