From 2471036df4a77d4188d9d9a4725b9fb0b4637287 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 27 Oct 2016 17:00:47 +0200
Subject: [PATCH] more work on jit-thing: transitioning to proper handling of
synchronizing edges
Former-commit-id: 3af177219259e1b31832040af09ff4c99b93bb17 [formerly 890c529dd16e0db64aaf266ba1ef4c269e7de7a7]
Former-commit-id: 818295a085752e57daa899c0fbcc84d54ad4f7f5
---
.../jit/ExplicitJitJaniModelBuilder.cpp | 181 ++++++++++++++----
src/builder/jit/ExplicitJitJaniModelBuilder.h | 10 +-
src/generator/JaniNextStateGenerator.cpp | 100 +++++-----
src/generator/PrismNextStateGenerator.cpp | 40 ++--
src/settings/SettingsManager.cpp | 2 +
src/settings/modules/JitBuilderSettings.cpp | 42 ++++
src/settings/modules/JitBuilderSettings.h | 32 ++++
src/storage/jani/Assignment.cpp | 18 +-
src/storage/jani/Assignment.h | 7 +-
src/storage/jani/OrderedAssignments.cpp | 18 +-
src/storage/jani/OrderedAssignments.h | 14 +-
src/storage/prism/Command.cpp | 3 +-
src/storage/prism/Command.h | 9 +-
src/storage/prism/Program.cpp | 2 +-
.../ExplicitJitJaniModelBuilderTest.cpp | 4 +-
15 files changed, 354 insertions(+), 128 deletions(-)
create mode 100644 src/settings/modules/JitBuilderSettings.cpp
create mode 100644 src/settings/modules/JitBuilderSettings.h
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 6efb68661..d77fab585 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -158,6 +158,57 @@ namespace storm {
private:
std::queue<StateType> storage;
};
+
+ {% for edge in nonSynchronizingEdges %}static bool enabled_{$edge.name}(StateType const& state) {
+ if ({$edge.guard}) {
+ return true;
+ }
+ return false;
+ }
+
+ static void perform_{$edge.name}(StateType const& state) {
+
+ }
+
+ static void lowestLevel_{$edge.name}() {
+ return {$edge.lowestLevel};
+ }
+
+ static void highestLevel_{$edge.name}() {
+ return {$edge.highestLevel};
+ }
+ {% endfor %}
+
+
+ {% for edge in nonSynchronizingEdges %}class Edge_{$edge.name} {
+ public:
+ bool isEnabled(StateType const& state) {
+ if ({$edge.guard}) {
+ return true;
+ }
+ return false;
+ }
+
+ {% for destination in edge.destinations %}class Destination_{$destination.name} {
+ public:
+ int_fast64_t lowestLevel() const {
+ return {$destination.lowestLevel};
+ }
+
+ int_fast64_t highestLevel() const {
+ return {$destination.highestLevel};
+ }
+
+ void performAssignments(int_fast64_t level, StateType& state) {
+ {% for level in destination.levels %}if (level == {$level.index}) {
+ {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
+ {% endfor %}
+ }{% endfor %}
+ }
+ };
+ {% endfor %}
+ };
+ {% endfor %}
class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> {
public:
@@ -166,8 +217,7 @@ namespace storm {
StateType state;
{% for assignment in state %}state.{$assignment.variable} = {$assignment.value};
{% endfor %}initialStates.push_back(state);
- }
- {% endfor %}
+ }{% endfor %}
}
virtual storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* build() override {
@@ -243,22 +293,12 @@ namespace storm {
{% for expression in terminalExpressions %}if ({$expression}) {
return true;
}
+ {% endfor %}
return false;
}
void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, StateBehaviour<IndexType, ValueType>& behaviour, StateSet& statesToExplore) {
- {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) {
- Choice<IndexType, ValueType>& choice = behaviour.addChoice();
- {% for destination in edge.destinations %}{
- StateType targetState(sourceState);
- {% for assignment in destination.nonTransientAssignments %}targetState.{$assignment.variable} = {$assignment.value};
- {% endfor %}
- IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);
- choice.add(targetStateIndex, {$destination.value});
- }
- {% endfor %}
- }
- {% endfor %}
+
}
IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) {
@@ -444,7 +484,14 @@ namespace storm {
std::string variableName = getQualifiedVariableName(variable);
variableToName[variable.getExpressionVariable()] = variableName;
- uint64_t range = static_cast<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt() + 1);
+ int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
+ int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
+
+ lowerBounds[variable.getExpressionVariable()] = lowerBound;
+ if (lowerBound != 0) {
+ lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound);
+ }
+ uint64_t range = static_cast<uint64_t>(upperBound - lowerBound + 1);
uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
boundedIntegerVariable["name"] = variableName;
@@ -463,8 +510,15 @@ namespace storm {
cpptempl::data_map boundedIntegerVariable;
std::string variableName = getQualifiedVariableName(automaton, variable);
variableToName[variable.getExpressionVariable()] = variableName;
-
- uint64_t range = static_cast<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt());
+
+ int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
+ int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
+
+ lowerBounds[variable.getExpressionVariable()] = lowerBound;
+ if (lowerBound != 0) {
+ lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound);
+ }
+ uint64_t range = static_cast<uint64_t>(upperBound - lowerBound);
uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
boundedIntegerVariable["name"] = variableName;
@@ -499,7 +553,7 @@ namespace storm {
if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) {
cpptempl::data_map label;
label["name"] = variable->getName();
- label["predicate"] = expressionTranslator.translate(model.getLabelExpression(variable->asBooleanVariable(), locationVariables), storm::expressions::ToCppTranslationOptions("state."));
+ label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable->asBooleanVariable(), locationVariables)), storm::expressions::ToCppTranslationOptions("state."));
labels.push_back(label);
}
}
@@ -508,7 +562,7 @@ namespace storm {
for (auto const& expression : this->options.getExpressionLabels()) {
cpptempl::data_map label;
label["name"] = expression.toString();
- label["predicate"] = expressionTranslator.translate(expression, storm::expressions::ToCppTranslationOptions("state."));
+ label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions("state."));
labels.push_back(label);
}
@@ -531,10 +585,10 @@ namespace storm {
if (terminalEntry.second) {
labelExpression = !labelExpression;
}
- terminalExpressions.push_back(expressionTranslator.translate(labelExpression, storm::expressions::ToCppTranslationOptions("state.")));
+ terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions("state.")));
} else {
auto expression = terminalEntry.second ? labelOrExpression.getExpression() : !labelOrExpression.getExpression();
- terminalExpressions.push_back(expressionTranslator.translate(expression, storm::expressions::ToCppTranslationOptions("state.")));
+ terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions("state.")));
}
}
@@ -545,10 +599,12 @@ namespace storm {
cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateNonSynchronizingEdges() {
cpptempl::data_list edges;
for (auto const& automaton : this->model.getAutomata()) {
+ uint64_t edgeIndex = 0;
for (auto const& edge : automaton.getEdges()) {
if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) {
- edges.push_back(generateEdge(edge));
+ edges.push_back(generateEdge(automaton, edgeIndex, edge));
}
+ ++edgeIndex;
}
}
@@ -556,31 +612,74 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
- cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateEdge(storm::jani::Edge const& edge) {
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge) {
cpptempl::data_map edgeData;
cpptempl::data_list destinations;
+ uint64_t destinationIndex = 0;
for (auto const& destination : edge.getDestinations()) {
- destinations.push_back(generateDestination(destination));
+ destinations.push_back(generateDestination(destinationIndex, destination));
+ ++destinationIndex;
}
- edgeData["guard"] = expressionTranslator.translate(edge.getGuard(), storm::expressions::ToCppTranslationOptions("sourceState."));
+ edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions("state."));
edgeData["destinations"] = cpptempl::make_data(destinations);
+ edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex);
return edgeData;
}
template <typename ValueType, typename RewardModelType>
- cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateDestination(storm::jani::EdgeDestination const& destination) {
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination) {
cpptempl::data_map destinationData;
- cpptempl::data_list nonTransientAssignments;
- for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) {
- nonTransientAssignments.push_back(generateAssignment(assignment, "targetState."));
+ cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments());
+ destinationData["name"] = asString(destinationIndex);
+ destinationData["levels"] = cpptempl::make_data(levels);
+ destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel());
+ destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel());
+
+ return destinationData;
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLevels(storm::jani::OrderedAssignments const& orderedAssignments) {
+ cpptempl::data_list levels;
+
+ auto const& assignments = orderedAssignments.getAllAssignments();
+ if (!assignments.empty()) {
+ int_fast64_t currentLevel = assignments.begin()->getLevel();
+
+ cpptempl::data_list nonTransientAssignmentData;
+ cpptempl::data_list transientAssignmentData;
+ for (auto const& assignment : assignments) {
+ if (assignment.getLevel() != currentLevel) {
+ cpptempl::data_map level;
+ level["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignmentData);
+ level["transientAssignments"] = cpptempl::make_data(transientAssignmentData);
+ level["index"] = asString(currentLevel);
+ levels.push_back(level);
+
+ nonTransientAssignmentData = cpptempl::data_list();
+ transientAssignmentData = cpptempl::data_list();
+ currentLevel = assignment.getLevel();
+ }
+
+ if (assignment.isTransient()) {
+ transientAssignmentData.push_back(generateAssignment(assignment, "state."));
+ } else {
+ nonTransientAssignmentData.push_back(generateAssignment(assignment, "state."));
+ }
+ }
+
+ // Close the last (open) level.
+ cpptempl::data_map level;
+ level["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignmentData);
+ level["transientAssignments"] = cpptempl::make_data(transientAssignmentData);
+ level["index"] = asString(currentLevel);
+ levels.push_back(level);
}
- destinationData["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignments);
- destinationData["value"] = expressionTranslator.translate(destination.getProbability(), storm::expressions::ToCppTranslationOptions("sourceState.", "double"));
- return destinationData;
+ return levels;
}
template <typename ValueType, typename RewardModelType>
@@ -604,7 +703,18 @@ namespace storm {
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateAssignment(storm::jani::Assignment const& assignment, std::string const& prefix) {
cpptempl::data_map result;
result["variable"] = getVariableName(assignment.getExpressionVariable());
- result["value"] = expressionTranslator.translate(assignment.getAssignedExpression(), prefix);
+ auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable());
+ if (lowerBoundIt != lowerBounds.end()) {
+ if (lowerBoundIt->second < 0) {
+ result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), prefix);
+ } else if (lowerBoundIt->second == 0) {
+ result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), prefix);
+ } else {
+ result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), prefix);
+ }
+ } else {
+ result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), prefix);
+ }
return result;
}
@@ -640,6 +750,11 @@ namespace storm {
return out.str();
}
+ template <typename ValueType, typename RewardModelType>
+ storm::expressions::Expression ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression) {
+ return expression.substitute(lowerBoundShiftSubstitution);
+ }
+
template <typename ValueType, typename RewardModelType>
template <typename ValueTypePrime>
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(ValueTypePrime value) const {
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h
index 5cc26167f..dd4085954 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.h
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h
@@ -55,9 +55,10 @@ namespace storm {
cpptempl::data_list generateLabels();
cpptempl::data_list generateTerminalExpressions();
cpptempl::data_list generateNonSynchronizingEdges();
+ cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments);
- cpptempl::data_map generateEdge(storm::jani::Edge const& edge);
- cpptempl::data_map generateDestination(storm::jani::EdgeDestination const& destination);
+ cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge);
+ cpptempl::data_map generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination);
template <typename ValueTypePrime>
cpptempl::data_map generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const;
@@ -73,7 +74,8 @@ namespace storm {
std::string getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::Variable const& variable) const;
std::string getLocationVariableName(storm::jani::Automaton const& automaton) const;
std::string asString(bool value) const;
-
+ storm::expressions::Expression shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression);
+
template <typename ValueTypePrime>
std::string asString(ValueTypePrime value) const;
@@ -87,6 +89,8 @@ namespace storm {
std::unordered_map<storm::expressions::Variable, std::string> variableToName;
storm::expressions::ToCppVisitor expressionTranslator;
+ std::map<storm::expressions::Variable, storm::expressions::Expression> lowerBoundShiftSubstitution;
+ std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;
};
}
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 80473c2f9..a6407acdd 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -92,7 +92,7 @@ namespace storm {
storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel());
STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
-
+
this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second));
}
}
@@ -188,7 +188,7 @@ namespace storm {
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
}
-
+
// Gather iterators to the initial locations of all the automata.
std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators;
uint64_t currentLocationVariable = 0;
@@ -270,7 +270,7 @@ namespace storm {
// Check that we processed all assignments.
STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
-
+
return newState;
}
@@ -281,7 +281,7 @@ namespace storm {
// Retrieve the locations from the state.
std::vector<uint64_t> locations = getLocations(*this->state);
-
+
// First, construct the state rewards, as we may return early if there are no choices later and we already
// need the state rewards then.
std::vector<ValueType> stateRewards(this->rewardVariables.size(), storm::utility::zero<ValueType>());
@@ -327,7 +327,7 @@ namespace storm {
// For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
// this is equal to the number of choices, which is why we initialize it like this here.
ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
-
+
// Iterate over all choices and combine the probabilities/rates into one choice.
for (auto const& choice : allChoices) {
for (auto const& stateProbabilityPair : choice) {
@@ -346,7 +346,7 @@ namespace storm {
globalChoice.addLabels(choice.getLabels());
}
}
-
+
std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
for (auto const& choice : allChoices) {
for (uint_fast64_t rewardVariableIndex = 0; rewardVariableIndex < rewardVariables.size(); ++rewardVariableIndex) {
@@ -354,7 +354,7 @@ namespace storm {
}
}
globalChoice.addRewards(std::move(stateActionRewards));
-
+
// Move the newly fused choice in place.
allChoices.clear();
allChoices.push_back(std::move(globalChoice));
@@ -404,20 +404,23 @@ namespace storm {
// Iterate over all updates of the current command.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& destination : edge.getDestinations()) {
- // Obtain target state index and add it to the list of known states. If it has not yet been
- // seen, we also add it to the set of states that have yet to be explored.
- StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
-
- // Update the choice by adding the probability/target state to it.
ValueType probability = this->evaluator->asRational(destination.getProbability());
- probability = exitRate ? exitRate.get() * probability : probability;
- choice.addProbability(stateIndex, probability);
- probabilitySum += probability;
+
+ if (probability != storm::utility::zero<ValueType>()) {
+ // Obtain target state index and add it to the list of known states. If it has not yet been
+ // seen, we also add it to the set of states that have yet to be explored.
+ StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
+
+ // Update the choice by adding the probability/target state to it.
+ probability = exitRate ? exitRate.get() * probability : probability;
+ choice.addProbability(stateIndex, probability);
+ probabilitySum += probability;
+ }
}
// Create the state-action reward for the newly created choice.
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } );
-
+
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
}
@@ -467,11 +470,14 @@ namespace storm {
// If the new state was already found as a successor state, update the probability
// and otherwise insert it.
- auto targetStateIt = newTargetStates->find(newTargetState);
- if (targetStateIt != newTargetStates->end()) {
- targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
- } else {
- newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()));
+ auto probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
+ if (probability != storm::utility::zero<ValueType>()) {
+ auto targetStateIt = newTargetStates->find(newTargetState);
+ if (targetStateIt != newTargetStates->end()) {
+ targetStateIt->second += probability;
+ } else {
+ newTargetStates->emplace(newTargetState, probability);
+ }
}
}
@@ -500,7 +506,7 @@ namespace storm {
// Add the rewards to the choice.
choice.addRewards(std::move(stateActionRewards));
-
+
// Add the probabilities/rates to the newly created choice.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
@@ -510,7 +516,7 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
- STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
+ STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ").");
// Dispose of the temporary maps.
delete currentTargetStates;
@@ -689,7 +695,7 @@ namespace storm {
}
}
}
-
+
for (auto const& edge : automaton.getEdges()) {
auto rewardVariableIt = rewardVariables.begin();
auto rewardVariableIte = rewardVariables.end();
@@ -717,35 +723,35 @@ namespace storm {
#ifdef STORM_HAVE_CARL
if (!std::is_same<ValueType, storm::RationalFunction>::value && model.hasUndefinedConstants()) {
#else
- if (model.hasUndefinedConstants()) {
+ if (model.hasUndefinedConstants()) {
#endif
- std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
- std::stringstream stream;
- bool printComma = false;
- for (auto const& constant : undefinedConstants) {
- if (printComma) {
- stream << ", ";
- } else {
- printComma = true;
+ std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
+ std::stringstream stream;
+ bool printComma = false;
+ for (auto const& constant : undefinedConstants) {
+ if (printComma) {
+ stream << ", ";
+ } else {
+ printComma = true;
+ }
+ stream << constant.get().getName() << " (" << constant.get().getType() << ")";
}
- stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+ stream << ".";
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
}
- stream << ".";
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
- }
#ifdef STORM_HAVE_CARL
- else if (std::is_same<ValueType, storm::RationalFunction>::value && !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.");
- }
+ else if (std::is_same<ValueType, storm::RationalFunction>::value && !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
- }
-
- template class JaniNextStateGenerator<double>;
-
+ }
+
+ template class JaniNextStateGenerator<double>;
+
#ifdef STORM_HAVE_CARL
- template class JaniNextStateGenerator<storm::RationalNumber>;
- template class JaniNextStateGenerator<storm::RationalFunction>;
+ template class JaniNextStateGenerator<storm::RationalNumber>;
+ template class JaniNextStateGenerator<storm::RationalFunction>;
#endif
+ }
}
-}
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index e344ab13a..35dc1f7a2 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -395,15 +395,17 @@ namespace storm {
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::prism::Update const& update = command.getUpdate(k);
-
- // Obtain target state index and add it to the list of known states. If it has not yet been
- // seen, we also add it to the set of states that have yet to be explored.
- StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
-
- // Update the choice by adding the probability/target state to it.
+
ValueType probability = this->evaluator->asRational(update.getLikelihoodExpression());
- choice.addProbability(stateIndex, probability);
- probabilitySum += probability;
+ if (probability != storm::utility::zero<ValueType>()) {
+ // Obtain target state index and add it to the list of known states. If it has not yet been
+ // seen, we also add it to the set of states that have yet to be explored.
+ StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
+
+ // Update the choice by adding the probability/target state to it.
+ choice.addProbability(stateIndex, probability);
+ probabilitySum += probability;
+ }
}
// Create the state-action reward for the newly created choice.
@@ -458,16 +460,20 @@ namespace storm {
storm::prism::Update const& update = command.getUpdate(j);
for (auto const& stateProbabilityPair : *currentTargetStates) {
- // Compute the new state under the current update and add it to the set of new target states.
- CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
+ auto probability = stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
- // If the new state was already found as a successor state, update the probability
- // and otherwise insert it.
- auto targetStateIt = newTargetStates->find(newTargetState);
- if (targetStateIt != newTargetStates->end()) {
- targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
- } else {
- newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()));
+ if (probability != storm::utility::zero<ValueType>()) {
+ // Compute the new state under the current update and add it to the set of new target states.
+ CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update);
+
+ // If the new state was already found as a successor state, update the probability
+ // and otherwise insert it.
+ auto targetStateIt = newTargetStates->find(newTargetState);
+ if (targetStateIt != newTargetStates->end()) {
+ targetStateIt->second += probability;
+ } else {
+ newTargetStates->emplace(newTargetState, probability);
+ }
}
}
}
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 2aba99492..9a5afe650 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -34,6 +34,7 @@
#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
#include "src/settings/modules/ExplorationSettings.h"
#include "src/settings/modules/JaniExportSettings.h"
+#include "src/settings/modules/JitBuilderSettings.h"
#include "src/utility/macros.h"
#include "src/settings/Option.h"
@@ -526,6 +527,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::Smt2SmtSolverSettings>();
storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+ storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
}
}
diff --git a/src/settings/modules/JitBuilderSettings.cpp b/src/settings/modules/JitBuilderSettings.cpp
new file mode 100644
index 000000000..217ee61e0
--- /dev/null
+++ b/src/settings/modules/JitBuilderSettings.cpp
@@ -0,0 +1,42 @@
+#include "src/settings/modules/JitBuilderSettings.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+#include "src/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+ const std::string JitBuilderSettings::moduleName = "jitbuilder";
+
+ const std::string JitBuilderSettings::noJitOptionName = "nojit";
+ const std::string JitBuilderSettings::doctorOptionName = "doctor";
+
+ JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) {
+// this->addOption(storm::settings::OptionBuilder(moduleName, noJitOptionName, false, "Don't use the jit-based explicit model builder.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show information on why the jit-based explicit model builder is not usable on the current system.").build());
+ }
+
+// bool JitBuilderSettings::isNoJitSet() const {
+// return this->getOption(noJitOptionName).getHasOptionBeenSet();
+// }
+
+ bool JitBuilderSettings::isDoctorSet() const {
+ return this->getOption(doctorOptionName).getHasOptionBeenSet();
+ }
+
+ void JitBuilderSettings::finalize() {
+ // Intentionally left empty.
+ }
+
+ bool JitBuilderSettings::check() const {
+ return true;
+ }
+ }
+ }
+}
diff --git a/src/settings/modules/JitBuilderSettings.h b/src/settings/modules/JitBuilderSettings.h
new file mode 100644
index 000000000..1080e89b6
--- /dev/null
+++ b/src/settings/modules/JitBuilderSettings.h
@@ -0,0 +1,32 @@
+#pragma once
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ class JitBuilderSettings : public ModuleSettings {
+ public:
+ /*!
+ * Creates a new JitBuilder settings object.
+ */
+ JitBuilderSettings();
+
+// bool isNoJitSet() const;
+
+ bool isDoctorSet() const;
+
+ bool check() const override;
+ void finalize() override;
+
+ static const std::string moduleName;
+
+ private:
+ static const std::string noJitOptionName;
+ static const std::string doctorOptionName;
+ };
+
+ }
+ }
+}
diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp
index ddf65afe4..99f2a09b1 100644
--- a/src/storage/jani/Assignment.cpp
+++ b/src/storage/jani/Assignment.cpp
@@ -48,20 +48,20 @@ namespace storm {
return stream;
}
- bool AssignmentPartialOrderByVariable::operator()(Assignment const& left, Assignment const& right) const {
- return left.getExpressionVariable() < right.getExpressionVariable();
+ bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, Assignment const& right) const {
+ return left.getLevel() < right.getLevel() || (left.getLevel() == right.getLevel() && left.getExpressionVariable() < right.getExpressionVariable());
}
- bool AssignmentPartialOrderByVariable::operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const {
- return left.getExpressionVariable() < right->getExpressionVariable();
+ bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const {
+ return left.getLevel() < right->getLevel() || (left.getLevel() == right->getLevel() && left.getExpressionVariable() < right->getExpressionVariable());
}
- bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
- return left->getExpressionVariable() < right->getExpressionVariable();
+ bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
+ return left->getLevel() < right->getLevel() || (left->getLevel() == right->getLevel() && left->getExpressionVariable() < right->getExpressionVariable());
}
- bool AssignmentPartialOrderByVariable::operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const {
- return left->getExpressionVariable() < right.getExpressionVariable();
+ bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const {
+ return left->getLevel() < right.getLevel() || (left->getLevel() == right.getLevel() && left->getExpressionVariable() < right.getExpressionVariable());
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Assignment.h b/src/storage/jani/Assignment.h
index 030c1f68f..7886a5b5b 100644
--- a/src/storage/jani/Assignment.h
+++ b/src/storage/jani/Assignment.h
@@ -66,9 +66,10 @@ namespace storm {
};
/*!
- * This functor enables ordering the assignments by variable. Note that this is a partial order.
+ * This functor enables ordering the assignments first by the assignment level and then by variable.
+ * Note that this is a partial order.
*/
- struct AssignmentPartialOrderByVariable {
+ struct AssignmentPartialOrderByLevelAndVariable {
bool operator()(Assignment const& left, Assignment const& right) const;
bool operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const;
bool operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const;
@@ -76,4 +77,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/OrderedAssignments.cpp b/src/storage/jani/OrderedAssignments.cpp
index 933054100..b98d543c5 100644
--- a/src/storage/jani/OrderedAssignments.cpp
+++ b/src/storage/jani/OrderedAssignments.cpp
@@ -70,18 +70,26 @@ namespace storm {
}
bool OrderedAssignments::hasMultipleLevels() const {
- if(allAssignments.empty()) {
+ if (allAssignments.empty()) {
return false;
}
uint64_t firstLevel = allAssignments.front()->getLevel();
- for(auto const& assignment : allAssignments) {
- if(assignment->getLevel() != firstLevel) {
+ for (auto const& assignment : allAssignments) {
+ if (assignment->getLevel() != firstLevel) {
return true;
}
}
return false;
}
+ int_fast64_t OrderedAssignments::getLowestLevel() const {
+ return allAssignments.front()->getLevel();
+ }
+
+ int_fast64_t OrderedAssignments::getHighestLevel() const {
+ return allAssignments.back()->getLevel();
+ }
+
bool OrderedAssignments::contains(Assignment const& assignment) const {
auto it = lowerBound(assignment, allAssignments);
if (it != allAssignments.end() && assignment == **it) {
@@ -126,8 +134,8 @@ namespace storm {
}
std::vector<std::shared_ptr<Assignment>>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments) {
- return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByVariable());
+ return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable());
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/OrderedAssignments.h b/src/storage/jani/OrderedAssignments.h
index afbf66cad..f21b09fb8 100644
--- a/src/storage/jani/OrderedAssignments.h
+++ b/src/storage/jani/OrderedAssignments.h
@@ -42,6 +42,18 @@ namespace storm {
*/
bool hasMultipleLevels() const;
+ /*!
+ * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least
+ * one assignment.
+ */
+ int_fast64_t getLowestLevel() const;
+
+ /*!
+ * Retrieves the highest level among all assignments. Note that this may only be called if there is at least
+ * one assignment.
+ */
+ int_fast64_t getHighestLevel() const;
+
/*!
* Retrieves whether the given assignment is contained in this set of assignments.
*/
@@ -97,4 +109,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index 5cad634e7..09c59197f 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -73,14 +73,13 @@ namespace storm {
return true;
}
- Command Command::removeIdentityAssignmentsFromUpdates() const {
+ Command Command::simplify() const {
std::vector<Update> newUpdates;
newUpdates.reserve(this->getNumberOfUpdates());
for (auto const& update : this->getUpdates()) {
newUpdates.emplace_back(update.removeIdentityAssignments());
}
return copyWithNewUpdates(std::move(newUpdates));
-
}
Command Command::copyWithNewUpdates(std::vector<Update> && newUpdates) const {
diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h
index 658cce67d..473ca07a4 100644
--- a/src/storage/prism/Command.h
+++ b/src/storage/prism/Command.h
@@ -128,12 +128,11 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, Command const& command);
- /**
- * Removes identity assignments from the updates
- * @return The resulting command
+ /*!
+ * Simplifies this command.
*/
- Command removeIdentityAssignmentsFromUpdates() const;
-
+ Command simplify() const;
+
private:
// The index of the action associated with this command.
uint_fast64_t actionIndex;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index f187ecc08..095e54fee 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1231,7 +1231,7 @@ namespace storm {
std::vector<Command> newCommands;
for (auto const& command : module.getCommands()) {
if (!command.getGuardExpression().isFalse()) {
- newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
+ newCommands.emplace_back(command.simplify());
}
}
diff --git a/test/functional/builder/ExplicitJitJaniModelBuilderTest.cpp b/test/functional/builder/ExplicitJitJaniModelBuilderTest.cpp
index b2f06a905..0086008a6 100644
--- a/test/functional/builder/ExplicitJitJaniModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitJitJaniModelBuilderTest.cpp
@@ -2,11 +2,11 @@
#include "storm-config.h"
#include "src/parser/PrismParser.h"
#include "src/storage/jani/Model.h"
-#include "src/builder/ExplicitJitJaniModelBuilder.h"
+#include "src/builder/jit/ExplicitJitJaniModelBuilder.h"
TEST(ExplicitJitJaniModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = program.toJani();
- storm::builder::ExplicitJitJaniModelBuilder<double>(janiModel).build();
+ storm::builder::jit::ExplicitJitJaniModelBuilder<double>(janiModel).build();
}