diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 9d7dede85..a5abac90d 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -37,9 +37,15 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model), modelComponentsBuilder(model.getModelType()) {
-
+ for (auto const& variable : this->model.getGlobalVariables().getTransientVariables()) {
+ transientVariables.insert(variable->getExpressionVariable());
+ }
+
for (auto const& automaton : this->model.getAutomata()) {
- locationVariables.emplace(automaton.getName(), model.getManager().declareFreshIntegerVariable(false, automaton.getName() + "_"));
+ automatonToLocationVariable.emplace(automaton.getName(), model.getManager().declareFreshIntegerVariable(false, automaton.getName() + "_"));
+ for (auto const& variable : automaton.getVariables().getTransientVariables()) {
+ transientVariables.insert(variable->getExpressionVariable());
+ }
}
}
@@ -73,38 +79,95 @@ namespace storm {
struct StateType {
// Boolean variables.
- {% for variable in stateVariables.boolean %}bool {$variable.name} : 1;
+ {% for variable in nontransient_variables.boolean %}bool {$variable.name} : 1;
{% endfor %}
// Bounded integer variables.
- {% for variable in stateVariables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits};
+ {% for variable in nontransient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits};
+ {% endfor %}
+ // Unbounded integer variables.
+ {% for variable in nontransient_variables.unboundedInteger %}int64_t {$variable.name};
+ {% endfor %}
+ // Real variables.
+ {% for variable in nontransient_variables.real %}double {$variable.name};
{% endfor %}
// Location variables.
- {% for variable in stateVariables.locations %}uint64_t {$variable.name} : {$variable.numberOfBits};
+ {% for variable in nontransient_variables.locations %}uint64_t {$variable.name} : {$variable.numberOfBits};
{% endfor %}
};
bool operator==(StateType const& first, StateType const& second) {
bool result = true;
- {% for variable in stateVariables.boolean %}result &= !(first.{$variable.name} ^ second.{$variable.name});
+ {% for variable in nontransient_variables.boolean %}result &= !(first.{$variable.name} ^ second.{$variable.name});
+ {% endfor %}
+ {% for variable in nontransient_variables.boundedInteger %}result &= first.{$variable.name} == second.{$variable.name};
{% endfor %}
- {% for variable in stateVariables.boundedInteger %}result &= first.{$variable.name} == second.{$variable.name};
+ {% for variable in nontransient_variables.unboundedInteger %}result &= first.{$variable.name} == second.{$variable.name};
{% endfor %}
- {% for variable in stateVariables.locations %}result &= first.{$variable.name} == second.{$variable.name};
+ {% for variable in nontransient_variables.real %}result &= first.{$variable.name} == second.{$variable.name};
+ {% endfor %}
+ {% for variable in nontransient_variables.locations %}result &= first.{$variable.name} == second.{$variable.name};
{% endfor %}
return result;
}
std::ostream& operator<<(std::ostream& out, StateType const& in) {
out << "<";
- {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", ";
+ {% for variable in nontransient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", ";
+ {% endfor %}
+ {% for variable in nontransient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
+ {% endfor %}
+ {% for variable in nontransient_variables.unboundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
+ {% endfor %}
+ {% for variable in nontransient_variables.real %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
+ {% endfor %}
+ {% for variable in nontransient_variables.locations %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
+ {% endfor %}
+ out << ">";
+ return out;
+ }
+
+ {% if transient_variables %}
+ struct TransientVariableType {
+ TransientVariableType() {
+ {% for variable in transient_variables.boolean %}{$variable.name} = {$variable.init};
+ {% endfor %}
+ {% for variable in transient_variables.boundedInteger %}{$variable.name} = {$variable.init};
+ {% endfor %}
+ {% for variable in transient_variables.unboundedInteger %}{$variable.name} = {$variable.init};
+ {% endfor %}
+ {% for variable in transient_variables.real %}{$variable.name} = {$variable.init};
+ {% endfor %}
+ }
+
+ // Boolean variables.
+ {% for variable in transient_variables.boolean %}bool {$variable.name} : 1;
+ {% endfor %}
+ // Bounded integer variables.
+ {% for variable in transient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits};
+ {% endfor %}
+ // Unbounded integer variables.
+ {% for variable in transient_variables.unboundedInteger %}int64_t {$variable.name};
+ {% endfor %}
+ // Real variables.
+ {% for variable in transient_variables.real %}double {$variable.name};
+ {% endfor %}
+ };
+
+ std::ostream& operator<<(std::ostream& out, TransientVariableType const& in) {
+ out << "<";
+ {% for variable in transient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", ";
+ {% endfor %}
+ {% for variable in transient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
{% endfor %}
- {% for variable in stateVariables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
+ {% for variable in transient_variables.unboundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
{% endfor %}
- {% for variable in stateVariables.locations %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
+ {% for variable in transient_variables.real %}out << "{$variable.name}=" << in.{$variable.name} << ", ";
{% endfor %}
out << ">";
return out;
}
+ {% endif %}
+
}
}
}
@@ -115,11 +178,15 @@ namespace storm {
std::size_t operator()(storm::builder::jit::StateType const& in) const {
// Note: this is faster than viewing the struct as a bit field and taking hash_combine of the bytes.
std::size_t seed = 0;
- {% for variable in stateVariables.boolean %}spp::hash_combine(seed, in.{$variable.name});
+ {% for variable in nontransient_variables.boolean %}spp::hash_combine(seed, in.{$variable.name});
{% endfor %}
- {% for variable in stateVariables.boundedInteger %}spp::hash_combine(seed, in.{$variable.name});
+ {% for variable in nontransient_variables.boundedInteger %}spp::hash_combine(seed, in.{$variable.name});
{% endfor %}
- {% for variable in stateVariables.locations %}spp::hash_combine(seed, in.{$variable.name});
+ {% for variable in nontransient_variables.unboundedInteger %}spp::hash_combine(seed, in.{$variable.name});
+ {% endfor %}
+ {% for variable in nontransient_variables.real %}spp::hash_combine(seed, in.{$variable.name});
+ {% endfor %}
+ {% for variable in nontransient_variables.locations %}spp::hash_combine(seed, in.{$variable.name});
{% endfor %}
return seed;
}
@@ -130,11 +197,11 @@ namespace storm {
namespace builder {
namespace jit {
- bool model_is_deterministic() {
+ static bool model_is_deterministic() {
return {$deterministic_model};
}
- bool model_is_discrete_time() {
+ static bool model_is_discrete_time() {
return {$discrete_time_model};
}
@@ -146,18 +213,21 @@ namespace storm {
}
{% for destination in edge.destinations %}
- void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) {
+ static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out{% if edge.referenced_transient_variables %}, TransientVariableType const& transientIn, TransientVariableType& transientOut{% endif %}) {
{% for level in destination.levels %}if (level == {$level.index}) {
{% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value};
{% endfor %}
+ {% for assignment in level.transientAssignments %}transientOut.{$assignment.variable} = {$assignment.value};
+ {% endfor %}
}
{% endfor %}
}
- void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) {
+ static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) {
+ {% if edge.referenced_transient_variables %}TransientVariableType transientIn;
+ TransientVariableType transientOut;{% endif %}
{% for level in destination.levels %}
- {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value};
- {% endfor %}
+ destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out{% if edge.referenced_transient_variables %}, transientIn, transientOut{% endif %});
{% endfor %}
}
{% endfor %}
@@ -171,18 +241,19 @@ namespace storm {
}
{% for destination in edge.destinations %}
- void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) {
+ static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out{% if edge.referenced_transient_variables %}, TransientVariableType const& transientIn, TransientVariableType& transientOut{% endif %}) {
{% for level in destination.levels %}if (level == {$level.index}) {
{% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value};
{% endfor %}
+ {% for assignment in level.transientAssignments %}transientOut.{$assignment.variable} = {$assignment.value};
+ {% endfor %}
}
{% endfor %}
}
- void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) {
+ static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out{% if edge.referenced_transient_variables %}, TransientVariableType const& transientIn, TransientVariableType& transientOut{% endif %}) {
{% for level in destination.levels %}
- {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value};
- {% endfor %}
+ destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out{% if edge.referenced_transient_variables %}, transientIn, transientOut{% endif %});
{% endfor %}
}
{% endfor %}
@@ -191,6 +262,10 @@ namespace storm {
typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&);
typedef void (*DestinationFunctionPtr)(StateType const&, StateType&);
+
+ {% if transient_variables %}typedef void (*DestinationTransientLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&, TransientVariableType const&, TransientVariableType&);
+ typedef void (*DestinationTransientFunctionPtr)(StateType const&, StateType&, TransientVariableType const&, TransientVariableType&);
+ {% endif %}
class Destination {
public:
@@ -229,7 +304,46 @@ namespace storm {
DestinationLevelFunctionPtr destinationLevelFunction;
DestinationFunctionPtr destinationFunction;
};
-
+
+ {% if transient_variables %}class DestinationTransient {
+ public:
+ DestinationTransient() : mLowestLevel(0), mHighestLevel(0), mValue(), destinationLevelFunction(nullptr), destinationFunction(nullptr) {
+ // Intentionally left empty.
+ }
+
+ DestinationTransient(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationTransientLevelFunctionPtr destinationLevelFunction, DestinationTransientFunctionPtr destinationFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), mValue(value), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction) {
+ // Intentionally left empty.
+ }
+
+ int_fast64_t lowestLevel() const {
+ return mLowestLevel;
+ }
+
+ int_fast64_t highestLevel() const {
+ return mHighestLevel;
+ }
+
+ ValueType const& value() const {
+ return mValue;
+ }
+
+ void performLevel(int_fast64_t level, StateType const& in, StateType& out, TransientVariableType const& transientIn, TransientVariableType& transientOut) const {
+ destinationLevelFunction(level, in, out, transientIn, transientOut);
+ }
+
+ void perform(StateType const& in, StateType& out, TransientVariableType const& transientIn, TransientVariableType& transientOut) const {
+ destinationFunction(in, out, transientIn, transientOut);
+ }
+
+ private:
+ int_fast64_t mLowestLevel;
+ int_fast64_t mHighestLevel;
+ ValueType mValue;
+ DestinationTransientLevelFunctionPtr destinationLevelFunction;
+ DestinationTransientFunctionPtr destinationFunction;
+ };
+ {% endif %}
+
typedef bool (*EdgeEnabledFunctionPtr)(StateType const&);
class Edge {
@@ -272,7 +386,49 @@ namespace storm {
EdgeEnabledFunctionPtr edgeEnabledFunction;
ContainerType destinations;
};
-
+
+ {% if transient_variables %}class EdgeTransient {
+ public:
+ typedef std::vector<DestinationTransient> ContainerType;
+
+ EdgeTransient() : edgeEnabledFunction(nullptr) {
+ // Intentionally left empty.
+ }
+
+ EdgeTransient(EdgeEnabledFunctionPtr edgeEnabledFunction) : edgeEnabledFunction(edgeEnabledFunction) {
+ // Intentionally left empty.
+ }
+
+ bool isEnabled(StateType const& in) const {
+ return edgeEnabledFunction(in);
+ }
+
+ void addDestination(DestinationTransient const& destination) {
+ destinations.push_back(destination);
+ }
+
+ void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationTransientLevelFunctionPtr destinationLevelFunction, DestinationTransientFunctionPtr destinationFunction) {
+ destinations.emplace_back(lowestLevel, highestLevel, value, destinationLevelFunction, destinationFunction);
+ }
+
+ std::vector<DestinationTransient> const& getDestinations() const {
+ return destinations;
+ }
+
+ ContainerType::const_iterator begin() const {
+ return destinations.begin();
+ }
+
+ ContainerType::const_iterator end() const {
+ return destinations.end();
+ }
+
+ private:
+ EdgeEnabledFunctionPtr edgeEnabledFunction;
+ ContainerType destinations;
+ };
+ {% endif %}
+
class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> {
public:
JitBuilder(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) {
@@ -440,9 +596,9 @@ namespace storm {
std::vector<StateType> initialStates;
std::vector<IndexType> deadlockStates;
- {% for edge in nonsynch_edges %}Edge edge_{$edge.name};
+ {% for edge in nonsynch_edges %}{% if edge.referenced_transient_variables %}EdgeTransient {% endif %}{% if not edge.referenced_transient_variables %}Edge {% endif %} edge_{$edge.name};
{% endfor %}
- {% for edge in synch_edges %}Edge edge_{$edge.name};
+ {% for edge in synch_edges %}{% if edge.referenced_transient_variables %}EdgeTransient {% endif %}{% if not edge.referenced_transient_variables %}Edge {% endif %} edge_{$edge.name};
{% endfor %}
};
@@ -453,7 +609,7 @@ namespace storm {
)";
cpptempl::data_map modelData;
- modelData["stateVariables"] = generateStateVariables();
+ generateVariables(modelData);
cpptempl::data_list initialStates = generateInitialStates();
modelData["initialStates"] = cpptempl::make_data(initialStates);
generateEdges(modelData);
@@ -569,79 +725,170 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
- cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateStateVariables() {
- cpptempl::data_list booleanVariables;
- cpptempl::data_list boundedIntegerVariables;
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateBooleanVariable(storm::jani::BooleanVariable const& variable) {
+ cpptempl::data_map result;
+ result["name"] = registerVariableName(variable.getExpressionVariable());
+ if (variable.hasInitExpression()) {
+ result["init"] = asString(variable.getInitExpression().evaluateAsBool());
+ }
+ return result;
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateBoundedIntegerVariable(storm::jani::BoundedIntegerVariable const& variable) {
+ cpptempl::data_map result;
+
+ 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)));
+
+ result["name"] = registerVariableName(variable.getExpressionVariable());
+ result["numberOfBits"] = std::to_string(numberOfBits);
+ if (variable.hasInitExpression()) {
+ result["init"] = asString(variable.getInitExpression().evaluateAsInt() - lowerBound);
+ }
+
+ return result;
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateUnboundedIntegerVariable(storm::jani::UnboundedIntegerVariable const& variable) {
+ cpptempl::data_map result;
+
+ result["name"] = registerVariableName(variable.getExpressionVariable());
+ if (variable.hasInitExpression()) {
+ result["init"] = asString(variable.getInitExpression().evaluateAsInt());
+ }
+
+ return result;
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateRealVariable(storm::jani::RealVariable const& variable) {
+ cpptempl::data_map result;
+
+ result["name"] = registerVariableName(variable.getExpressionVariable());
+ if (variable.hasInitExpression()) {
+ result["init"] = asString(variable.getInitExpression().evaluateAsDouble());
+ }
+
+ return result;
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLocationVariable(storm::jani::Automaton const& automaton) {
+ cpptempl::data_map result;
+
+ result["name"] = registerVariableName(getLocationVariable(automaton));
+ result["numberOfBits"] = static_cast<uint64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
+
+ return result;
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateVariables(cpptempl::data_map& modelData) {
+ cpptempl::data_list nonTransientBooleanVariables;
+ cpptempl::data_list transientBooleanVariables;
+ cpptempl::data_list nonTransientBoundedIntegerVariables;
+ cpptempl::data_list transientBoundedIntegerVariables;
+ cpptempl::data_list nonTransientUnboundedIntegerVariables;
+ cpptempl::data_list transientUnboundedIntegerVariables;
+ cpptempl::data_list nonTransientRealVariables;
+ cpptempl::data_list transientRealVariables;
cpptempl::data_list locationVariables;
for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
- cpptempl::data_map booleanVariable;
- std::string variableName = getQualifiedVariableName(variable);
- variableToName[variable.getExpressionVariable()] = variableName;
- booleanVariable["name"] = variableName;
- booleanVariables.push_back(booleanVariable);
+ cpptempl::data_map newBooleanVariable = generateBooleanVariable(variable.asBooleanVariable());
+ if (variable.isTransient()) {
+ transientBooleanVariables.push_back(newBooleanVariable);
+ } else {
+ nonTransientBooleanVariables.push_back(newBooleanVariable);
+ }
}
for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
- cpptempl::data_map boundedIntegerVariable;
- std::string variableName = getQualifiedVariableName(variable);
- variableToName[variable.getExpressionVariable()] = variableName;
-
- 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);
+ cpptempl::data_map newBoundedIntegerVariable = generateBoundedIntegerVariable(variable.asBoundedIntegerVariable());
+ if (variable.isTransient()) {
+ transientBoundedIntegerVariables.push_back(newBoundedIntegerVariable);
+ } else {
+ nonTransientBoundedIntegerVariables.push_back(newBoundedIntegerVariable);
+ }
+ }
+ for (auto const& variable : model.getGlobalVariables().getUnboundedIntegerVariables()) {
+ cpptempl::data_map newUnboundedIntegerVariable = generateUnboundedIntegerVariable(variable.asUnboundedIntegerVariable());
+ if (variable.isTransient()) {
+ transientUnboundedIntegerVariables.push_back(newUnboundedIntegerVariable);
+ } else {
+ nonTransientUnboundedIntegerVariables.push_back(newUnboundedIntegerVariable);
+ }
+ }
+ for (auto const& variable : model.getGlobalVariables().getRealVariables()) {
+ cpptempl::data_map newRealVariable = generateRealVariable(variable.asRealVariable());
+ if (variable.isTransient()) {
+ transientRealVariables.push_back(newRealVariable);
+ } else {
+ nonTransientRealVariables.push_back(newRealVariable);
}
- 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;
- boundedIntegerVariable["numberOfBits"] = std::to_string(numberOfBits);
- boundedIntegerVariables.push_back(boundedIntegerVariable);
}
for (auto const& automaton : model.getAutomata()) {
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
- cpptempl::data_map booleanVariable;
- std::string variableName = getQualifiedVariableName(automaton, variable);
- variableToName[variable.getExpressionVariable()] = variableName;
- booleanVariable["name"] = variableName;
- booleanVariables.push_back(booleanVariable);
+ cpptempl::data_map newBooleanVariable = generateBooleanVariable(variable.asBooleanVariable());
+ if (variable.isTransient()) {
+ transientBooleanVariables.push_back(newBooleanVariable);
+ } else {
+ nonTransientBooleanVariables.push_back(newBooleanVariable);
+ }
}
for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
- cpptempl::data_map boundedIntegerVariable;
- std::string variableName = getQualifiedVariableName(automaton, variable);
- variableToName[variable.getExpressionVariable()] = variableName;
-
- 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);
+ cpptempl::data_map newBoundedIntegerVariable = generateBoundedIntegerVariable(variable.asBoundedIntegerVariable());
+ if (variable.isTransient()) {
+ transientBoundedIntegerVariables.push_back(newBoundedIntegerVariable);
+ } else {
+ nonTransientBoundedIntegerVariables.push_back(newBoundedIntegerVariable);
+ }
+ }
+ for (auto const& variable : automaton.getVariables().getUnboundedIntegerVariables()) {
+ cpptempl::data_map newUnboundedIntegerVariable = generateUnboundedIntegerVariable(variable.asUnboundedIntegerVariable());
+ if (variable.isTransient()) {
+ transientUnboundedIntegerVariables.push_back(newUnboundedIntegerVariable);
+ } else {
+ nonTransientUnboundedIntegerVariables.push_back(newUnboundedIntegerVariable);
+ }
+ }
+ for (auto const& variable : automaton.getVariables().getRealVariables()) {
+ cpptempl::data_map newRealVariable = generateRealVariable(variable.asRealVariable());
+ if (variable.isTransient()) {
+ transientRealVariables.push_back(newRealVariable);
+ } else {
+ nonTransientRealVariables.push_back(newRealVariable);
}
- uint64_t range = static_cast<uint64_t>(upperBound - lowerBound);
- uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range)));
-
- boundedIntegerVariable["name"] = variableName;
- boundedIntegerVariable["numberOfBits"] = std::to_string(numberOfBits);
- boundedIntegerVariables.push_back(boundedIntegerVariable);
}
// Only generate a location variable if there is more than one location for the automaton.
if (automaton.getNumberOfLocations() > 1) {
- cpptempl::data_map locationVariable;
- locationVariable["name"] = getQualifiedVariableName(automaton, this->locationVariables.at(automaton.getName()));
- locationVariable["numberOfBits"] = static_cast<uint64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
- locationVariables.push_back(locationVariable);
+ locationVariables.push_back(generateLocationVariable(automaton));
}
}
- cpptempl::data_map stateVariables;
- stateVariables["boolean"] = cpptempl::make_data(booleanVariables);
- stateVariables["boundedInteger"] = cpptempl::make_data(boundedIntegerVariables);
- stateVariables["locations"] = cpptempl::make_data(locationVariables);
- return stateVariables;
+ cpptempl::data_map nonTransientVariables;
+ nonTransientVariables["boolean"] = cpptempl::make_data(nonTransientBooleanVariables);
+ nonTransientVariables["boundedInteger"] = cpptempl::make_data(nonTransientBoundedIntegerVariables);
+ nonTransientVariables["unboundedInteger"] = cpptempl::make_data(nonTransientUnboundedIntegerVariables);
+ nonTransientVariables["real"] = cpptempl::make_data(nonTransientRealVariables);
+ nonTransientVariables["locations"] = cpptempl::make_data(locationVariables);
+ modelData["nontransient_variables"] = nonTransientVariables;
+
+ cpptempl::data_map transientVariables;
+ transientVariables["boolean"] = cpptempl::make_data(transientBooleanVariables);
+ transientVariables["boundedInteger"] = cpptempl::make_data(transientBoundedIntegerVariables);
+ transientVariables["unboundedInteger"] = cpptempl::make_data(transientUnboundedIntegerVariables);
+ transientVariables["real"] = cpptempl::make_data(transientRealVariables);
+ modelData["transient_variables"] = transientVariables;
}
template <typename ValueType, typename RewardModelType>
@@ -655,7 +902,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(shiftVariablesWrtLowerBound(model.getLabelExpression(variable->asBooleanVariable(), locationVariables)), storm::expressions::ToCppTranslationOptions("in."));
+ label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable->asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions("in."));
labels.push_back(label);
}
}
@@ -683,7 +930,7 @@ namespace storm {
auto const& variable = variables.getVariable(labelOrExpression.getLabel());
STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << ".");
STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << ".");
- auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), locationVariables);
+ auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable);
if (terminalEntry.second) {
labelExpression = !labelExpression;
}
@@ -697,22 +944,62 @@ namespace storm {
return terminalExpressions;
}
+ std::ostream& indent(std::ostream& out, uint64_t indentLevel) {
+ for (uint64_t i = 0; i < indentLevel; ++i) {
+ out << "\t";
+ }
+ return out;
+ }
+
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) {
std::stringstream vectorSource;
uint64_t numberOfActionInputs = synchronizationVector.getNumberOfActionInputs();
- vectorSource << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
+ // First, we check whether we need to generate code for a) different assignment levels and b) transient variables.
+ uint64_t position = 0;
+ bool generateLevelCode = false;
+ bool generateTransientVariableCode = false;
+ for (auto const& inputActionName : synchronizationVector.getInput()) {
+ if (!storm::jani::SynchronizationVector::isNoActionInput(inputActionName)) {
+ storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName());
+ uint64_t actionIndex = model.getActionIndex(inputActionName);
+ for (auto const& edge : automaton.getEdges()) {
+ if (edge.getActionIndex() == actionIndex) {
+ for (auto const& destination : edge.getDestinations()) {
+ if (destination.getOrderedAssignments().hasMultipleLevels()) {
+ generateLevelCode = true;
+ }
+ for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
+ if (assignment.isTransient()) {
+
+ }
+ std::set<storm::expressions::Variable> usedVariables;
+ for (auto const& variable : usedVariables) {
+ if (transientVariables.find(variable) != transientVariables.end()) {
+ generateTransientVariableCode = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ ++position;
+ }
+
+ uint64_t indentLevel = 4;
+ indent(vectorSource, indentLevel - 4) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
vectorSource << "Destination const& destination" << index << ", ";
}
vectorSource << "Choice<IndexType, ValueType>& choice) {" << std::endl;
- vectorSource << "StateType out(in);" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "StateType out(in);" << std::endl;
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
- vectorSource << "destination" << index << ".perform(in, out);" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "destination" << index << ".perform(in, out);" << std::endl;
}
- vectorSource << "IndexType outStateIndex = getOrAddIndex(out, statesToExplore);" << std::endl;
- vectorSource << "choice.add(outStateIndex, ";
+ indent(vectorSource, indentLevel + 1) << "IndexType outStateIndex = getOrAddIndex(out, statesToExplore);" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "choice.add(outStateIndex, ";
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
vectorSource << "destination" << index << ".value()";
if (index + 1 < numberOfActionInputs) {
@@ -720,28 +1007,28 @@ namespace storm {
}
}
vectorSource << ");" << std::endl;
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
- vectorSource << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
+ indent(vectorSource, indentLevel) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
vectorSource << "Edge const& edge" << index << ", ";
}
vectorSource << "Choice<IndexType, ValueType>& choice) {" << std::endl;
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
- vectorSource << "for (auto const& destination" << index << " : edge" << index << ") {" << std::endl;
+ indent(vectorSource, indentLevel + 1 + index) << "for (auto const& destination" << index << " : edge" << index << ") {" << std::endl;
}
- vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, ";
+ indent(vectorSource, indentLevel + 1 + numberOfActionInputs) << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, ";
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
vectorSource << "destination" << index << ", ";
}
vectorSource << "choice);" << std::endl;
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel + numberOfActionInputs - index) << "}" << std::endl;
}
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
- vectorSource << "void performSynchronizedEdges_" << synchronizationVectorIndex << "_" << index << "(StateType const& in, std::vector<std::vector<std::reference_wrapper<Edge const>>> const& edges, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore";
+ indent(vectorSource, indentLevel) << "void performSynchronizedEdges_" << synchronizationVectorIndex << "_" << index << "(StateType const& in, std::vector<std::vector<std::reference_wrapper<Edge const>>> const& edges, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore";
if (index > 0) {
vectorSource << ", ";
}
@@ -752,9 +1039,9 @@ namespace storm {
}
}
vectorSource << ") {" << std::endl;
- vectorSource << "for (auto const& edge" << index << " : edges[" << index << "]) {" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "for (auto const& edge" << index << " : edges[" << index << "]) {" << std::endl;
if (index + 1 < numberOfActionInputs) {
- vectorSource << "performSynchronizedEdges_" << synchronizationVectorIndex << "_" << (index + 1) << "(in, edges, behaviour, statesToExplore, ";
+ 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) {
@@ -763,24 +1050,24 @@ namespace storm {
}
vectorSource << ");" << std::endl;
} else {
- vectorSource << "Choice<IndexType, ValueType>& choice = behaviour.addChoice();" << std::endl;
- vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, ";
+ indent(vectorSource, indentLevel + 2) << "Choice<IndexType, ValueType>& choice = behaviour.addChoice();" << std::endl;
+ indent(vectorSource, indentLevel + 2) << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, ";
for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) {
vectorSource << "edge" << innerIndex << ", ";
}
vectorSource << " choice);" << std::endl;
}
- vectorSource << "}" << std::endl;
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "}" << std::endl;
+ indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
}
- vectorSource << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector<std::reference_wrapper<Edge const>>& edges, uint64_t position) {" << std::endl;
- uint64_t position = 0;
+ indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector<std::reference_wrapper<Edge const>>& edges, uint64_t position) {" << std::endl;
+ position = 0;
uint64_t participatingPosition = 0;
for (auto const& inputActionName : synchronizationVector.getInput()) {
if (!storm::jani::SynchronizationVector::isNoActionInput(inputActionName)) {
- vectorSource << "if (position == " << participatingPosition << ") {" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "if (position == " << participatingPosition << ") {" << std::endl;
storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName());
uint64_t actionIndex = model.getActionIndex(inputActionName);
@@ -788,35 +1075,35 @@ namespace storm {
for (auto const& edge : automaton.getEdges()) {
if (edge.getActionIndex() == actionIndex) {
std::string edgeName = automaton.getName() + "_" + std::to_string(edgeIndex);
- vectorSource << "if (edge_enabled_" << edgeName << "(state)) {" << std::endl;
- vectorSource << "edges.emplace_back(edge_" << edgeName << ");" << std::endl;
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName << "(state)) {" << std::endl;
+ indent(vectorSource, indentLevel + 3) << "edges.emplace_back(edge_" << edgeName << ");" << std::endl;
+ indent(vectorSource, indentLevel + 2) << "}" << std::endl;
}
++edgeIndex;
}
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "}" << std::endl;
++participatingPosition;
}
++position;
}
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
- vectorSource << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {" << std::endl;
- vectorSource << "std::vector<std::vector<std::reference_wrapper<Edge const>>> edges(" << synchronizationVector.getNumberOfActionInputs() << ");" << std::endl;
+ indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "std::vector<std::vector<std::reference_wrapper<Edge const>>> edges(" << synchronizationVector.getNumberOfActionInputs() << ");" << std::endl;
participatingPosition = 0;
for (auto const& input : synchronizationVector.getInput()) {
if (!storm::jani::SynchronizationVector::isNoActionInput(input)) {
- vectorSource << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl;
- vectorSource << "if (edges[" << participatingPosition << "].empty()) {" << std::endl;
- vectorSource << "return;" << std::endl;
- vectorSource << "};" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "if (edges[" << participatingPosition << "].empty()) {" << std::endl;
+ indent(vectorSource, indentLevel + 2) << "return;" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "}" << std::endl;
++participatingPosition;
}
}
- vectorSource << "performSynchronizedEdges_" << synchronizationVectorIndex << "_0(state, edges, behaviour, statesToExplore);" << std::endl;
- vectorSource << "}" << std::endl;
+ indent(vectorSource, indentLevel + 1) << "performSynchronizedEdges_" << synchronizationVectorIndex << "_0(state, edges, behaviour, statesToExplore);" << std::endl;
+ indent(vectorSource, indentLevel) << "}" << std::endl << std::endl;
cpptempl::data_map vector;
vector["functions"] = vectorSource.str();
@@ -843,9 +1130,11 @@ namespace storm {
} else {
STORM_LOG_ASSERT(topLevelComposition.isParallelComposition(), "Expected parallel composition.");
storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition();
+#ifndef NDEBUG
for (auto const& composition : parallelComposition.getSubcompositions()) {
STORM_LOG_ASSERT(composition->isAutomatonComposition(), "Expected flat parallel composition.");
}
+#endif
std::vector<std::set<uint64_t>> synchronizingActions(parallelComposition.getNumberOfSubcompositions());
uint64_t synchronizationVectorIndex = 0;
@@ -916,14 +1205,34 @@ namespace storm {
cpptempl::data_list destinations;
uint64_t destinationIndex = 0;
+ std::set<storm::expressions::Variable> referencedTransientVariables;
for (auto const& destination : edge.getDestinations()) {
destinations.push_back(generateDestination(destinationIndex, destination));
+
+ for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
+ if (assignment.isTransient()) {
+ referencedTransientVariables.insert(assignment.getExpressionVariable());
+ }
+ std::set<storm::expressions::Variable> usedVariables = assignment.getAssignedExpression().getVariables();
+ for (auto const& variable : usedVariables) {
+ if (transientVariables.find(variable) != transientVariables.end()) {
+ referencedTransientVariables.insert(variable);
+ }
+ }
+ }
+
++destinationIndex;
}
edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions("in."));
edgeData["destinations"] = cpptempl::make_data(destinations);
edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex);
+
+ cpptempl::data_list referencedTransientVariableData;
+ for (auto const& variable : referencedTransientVariables) {
+ referencedTransientVariableData.push_back(getVariableName(variable));
+ }
+ edgeData["referenced_transient_variables"] = cpptempl::make_data(referencedTransientVariableData);
return edgeData;
}
@@ -999,7 +1308,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const {
cpptempl::data_map result;
- result["variable"] = getLocationVariableName(automaton);
+ result["variable"] = getVariableName(getLocationVariable(automaton));
result["value"] = asString(value);
return result;
}
@@ -1027,25 +1336,16 @@ namespace storm {
std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getVariableName(storm::expressions::Variable const& variable) const {
return variableToName.at(variable);
}
-
- template <typename ValueType, typename RewardModelType>
- std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Variable const& variable) const {
- return variable.getName();
- }
-
- template <typename ValueType, typename RewardModelType>
- std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const {
- return variable.getExpressionVariable().getName();
- }
template <typename ValueType, typename RewardModelType>
- std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::Variable const& variable) const {
+ std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::registerVariableName(storm::expressions::Variable const& variable) {
+ variableToName[variable] = variable.getName();
return variable.getName();
}
-
+
template <typename ValueType, typename RewardModelType>
- std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getLocationVariableName(storm::jani::Automaton const& automaton) const {
- return automaton.getName() + "_location";
+ storm::expressions::Variable const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getLocationVariable(storm::jani::Automaton const& automaton) const {
+ return automatonToLocationVariable.at(automaton.getName());
}
template <typename ValueType, typename RewardModelType>
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h
index c6a5a7c2f..bc38cb60b 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.h
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h
@@ -52,7 +52,14 @@ namespace storm {
// Functions that generate data maps or data templates.
cpptempl::data_list generateInitialStates();
- cpptempl::data_map generateStateVariables();
+
+ cpptempl::data_map generateBooleanVariable(storm::jani::BooleanVariable const& variable);
+ cpptempl::data_map generateBoundedIntegerVariable(storm::jani::BoundedIntegerVariable const& variable);
+ cpptempl::data_map generateUnboundedIntegerVariable(storm::jani::UnboundedIntegerVariable const& variable);
+ cpptempl::data_map generateRealVariable(storm::jani::RealVariable const& variable);
+ cpptempl::data_map generateLocationVariable(storm::jani::Automaton const& automaton);
+ void generateVariables(cpptempl::data_map& modelData);
+
cpptempl::data_list generateLabels();
cpptempl::data_list generateTerminalExpressions();
void generateEdges(cpptempl::data_map& modelData);
@@ -71,10 +78,8 @@ namespace storm {
// Auxiliary functions that perform regularly needed steps.
std::string const& getVariableName(storm::expressions::Variable const& variable) const;
- std::string getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const;
- std::string getQualifiedVariableName(storm::jani::Variable const& variable) const;
- 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 const& registerVariableName(storm::expressions::Variable const& variable);
+ storm::expressions::Variable const& getLocationVariable(storm::jani::Automaton const& automaton) const;
std::string asString(bool value) const;
storm::expressions::Expression shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression);
@@ -83,16 +88,18 @@ namespace storm {
storm::builder::BuilderOptions options;
storm::jani::Model model;
- std::map<std::string, storm::expressions::Variable> locationVariables;
ModelComponentsBuilder<IndexType, ValueType> modelComponentsBuilder;
typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportFunctionType jitBuilderGetFunction;
std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>> builder;
std::unordered_map<storm::expressions::Variable, std::string> variableToName;
+ std::map<std::string, storm::expressions::Variable> automatonToLocationVariable;
+
storm::expressions::ToCppVisitor expressionTranslator;
std::map<storm::expressions::Variable, storm::expressions::Expression> lowerBoundShiftSubstitution;
std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;
+ std::set<storm::expressions::Variable> transientVariables;
};
}
diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 2d0b467aa..3c4cbf535 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -128,16 +128,17 @@ namespace storm {
std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
}
-
- void printUsage() {
+ void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) {
#ifndef WINDOWS
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
- std::cout << "===== Statistics ==============================" << std::endl;
- std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
- std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
- std::cout << "===============================================" << std::endl;
+ std::cout << "Performance statistics:" << std::endl;
+ std::cout << " * peak memory usage: " << ru.ru_maxrss/1024/1024 << " mb" << std::endl;
+ std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
+ if (wallclockMilliseconds != 0) {
+ std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl;
+ }
#else
HANDLE hProcess = GetCurrentProcess ();
FILETIME ftCreation, ftExit, ftUser, ftKernel;
@@ -265,9 +266,7 @@ namespace storm {
// Get the string that assigns values to the unknown currently undefined constants in the model.
std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
model = model.preprocess(constantDefinitionString);
-
-
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalFunction>(model, properties, true);
@@ -302,7 +301,6 @@ namespace storm {
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
-
}
}
diff --git a/src/cli/cli.h b/src/cli/cli.h
index db2ab11bf..f48d53f23 100644
--- a/src/cli/cli.h
+++ b/src/cli/cli.h
@@ -10,7 +10,7 @@ namespace storm {
void printHeader(std::string name, const int argc, const char* argv[]);
- void printUsage();
+ void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds = 0);
/*!
* Parses the given command line arguments.
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 0a1cd849d..63bf0155f 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -19,8 +19,8 @@ namespace storm {
const std::string GeneralSettings::moduleName = "general";
const std::string GeneralSettings::helpOptionName = "help";
const std::string GeneralSettings::helpOptionShortName = "h";
- const std::string GeneralSettings::printTimingsOptionName = "printTime";
- const std::string GeneralSettings::printTimingsOptionShortName = "pt";
+ const std::string GeneralSettings::printTimeAndMemoryOptionName = "timemem";
+ const std::string GeneralSettings::printTimeAndMemoryOptionShortName = "tm";
const std::string GeneralSettings::versionOptionName = "version";
const std::string GeneralSettings::verboseOptionName = "verbose";
const std::string GeneralSettings::verboseOptionShortName = "v";
@@ -43,7 +43,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, printTimingsOptionName, false, "Prints the timing at the end").setShortName(printTimingsOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, printTimeAndMemoryOptionName, false, "Prints CPU time and memory consumption at the end.").setShortName(printTimeAndMemoryOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
@@ -117,8 +117,8 @@ namespace storm {
return this->getOption(parametricRegionOptionName).getHasOptionBeenSet();
}
- bool GeneralSettings::isPrintTimingsSet() const {
- return this->getOption(printTimingsOptionName).getHasOptionBeenSet();
+ bool GeneralSettings::isPrintTimeAndMemorySet() const {
+ return this->getOption(printTimeAndMemoryOptionName).getHasOptionBeenSet();
}
bool GeneralSettings::isExactSet() const {
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index b19573852..dda25a6ba 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -129,12 +129,11 @@ namespace storm {
bool isMinMaxEquationSolvingTechniqueSet() const;
/*!
- * Retrieves whether timings should be printed after running
+ * Retrieves whether time and memory consumption shall be printed at the end of a run.
*
* @return True iff the option was set.
*/
- bool isPrintTimingsSet() const;
-
+ bool isPrintTimeAndMemorySet() const;
/*!
* Retrieves whether the option enabling exact model checking is set.
@@ -153,8 +152,8 @@ namespace storm {
// Define the string names of the options as constants.
static const std::string helpOptionName;
static const std::string helpOptionShortName;
- static const std::string printTimingsOptionName;
- static const std::string printTimingsOptionShortName;
+ static const std::string printTimeAndMemoryOptionName;
+ static const std::string printTimeAndMemoryOptionShortName;
static const std::string versionOptionName;
static const std::string verboseOptionName;
static const std::string verboseOptionShortName;
diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h
index a560757d7..cf804f1b9 100644
--- a/src/settings/modules/IOSettings.h
+++ b/src/settings/modules/IOSettings.h
@@ -35,7 +35,6 @@ namespace storm {
*/
std::string getExportDotFilename() const;
-
/*!
* Retrieves whether the export-to-explicit option was set
*
@@ -43,7 +42,6 @@ namespace storm {
*/
bool isExportExplicitSet() const;
-
/*!
* Retrieves thename in which to write the model in explicit format, if the option was set.
*
@@ -219,7 +217,7 @@ namespace storm {
bool isPrismCompatibilityEnabled() const;
/**
- * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file
+ * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file.
*/
bool isNoBuildModelSet() const;
diff --git a/src/storage/expressions/ToCppVisitor.cpp b/src/storage/expressions/ToCppVisitor.cpp
index 08043120c..6bf0b6d53 100644
--- a/src/storage/expressions/ToCppVisitor.cpp
+++ b/src/storage/expressions/ToCppVisitor.cpp
@@ -13,6 +13,18 @@ namespace storm {
return prefix;
}
+ void ToCppTranslationOptions::setSpecificPrefixes(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes) {
+ specificPrefixes = prefixes;
+ }
+
+ std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getSpecificPrefixes() const {
+ return specificPrefixes;
+ }
+
+ void ToCppTranslationOptions::clearSpecificPrefixes() {
+ specificPrefixes.clear();
+ }
+
bool ToCppTranslationOptions::hasValueTypeCast() const {
return !valueTypeCast.empty();
}
@@ -200,7 +212,14 @@ namespace storm {
if (options.hasValueTypeCast()) {
stream << "static_cast<" << options.getValueTypeCast() << ">(";
}
- stream << options.getPrefix() << expression.getVariableName();
+
+ auto prefixIt = options.getSpecificPrefixes().find(expression.getVariable());
+ if (prefixIt != options.getSpecificPrefixes().end()) {
+ stream << prefixIt->second << expression.getVariableName();
+ } else {
+ stream << options.getPrefix() << expression.getVariableName();
+ }
+
if (options.hasValueTypeCast()) {
stream << ")";
}
diff --git a/src/storage/expressions/ToCppVisitor.h b/src/storage/expressions/ToCppVisitor.h
index 7b65c6af4..98d13e750 100644
--- a/src/storage/expressions/ToCppVisitor.h
+++ b/src/storage/expressions/ToCppVisitor.h
@@ -1,7 +1,9 @@
#pragma once
#include <sstream>
+#include <unordered_map>
+#include "src/storage/expressions/Variable.h"
#include "src/storage/expressions/ExpressionVisitor.h"
namespace storm {
@@ -14,6 +16,10 @@ namespace storm {
std::string const& getPrefix() const;
+ void setSpecificPrefixes(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes);
+ std::unordered_map<storm::expressions::Variable, std::string> const& getSpecificPrefixes() const;
+ void clearSpecificPrefixes();
+
bool hasValueTypeCast() const;
std::string const& getValueTypeCast() const;
void clearValueTypeCast();
@@ -21,6 +27,7 @@ namespace storm {
private:
std::string valueTypeCast;
std::string prefix;
+ std::unordered_map<storm::expressions::Variable, std::string> specificPrefixes;
};
class ToCppVisitor : public ExpressionVisitor {
diff --git a/src/storage/jani/OrderedAssignments.cpp b/src/storage/jani/OrderedAssignments.cpp
index e38b93918..e8b994a59 100644
--- a/src/storage/jani/OrderedAssignments.cpp
+++ b/src/storage/jani/OrderedAssignments.cpp
@@ -73,13 +73,7 @@ namespace storm {
if (allAssignments.empty()) {
return false;
}
- uint64_t firstLevel = allAssignments.front()->getLevel();
- for (auto const& assignment : allAssignments) {
- if (assignment->getLevel() != firstLevel) {
- return true;
- }
- }
- return false;
+ return getLowestLevel() == getHighestLevel();
}
bool OrderedAssignments::empty() const {
diff --git a/src/storm.cpp b/src/storm.cpp
index 236d15a7b..e8b6f8c49 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -29,10 +29,9 @@ int main(const int argc, const char** argv) {
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
auto end = std::chrono::high_resolution_clock::now();
- auto duration = std::chrono::duration_cast<std::chrono::milliseconds>(end - start);
- auto durationSec = std::chrono::duration_cast<std::chrono::seconds>(end - start);
- if(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPrintTimingsSet()) {
- std::cout << "Overal runtime: " << duration.count() << " ms. (approximately " << durationSec.count() << " seconds)." << std::endl;
+
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPrintTimeAndMemorySet()) {
+ storm::cli::showTimeAndMemoryStatistics(std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count());
}
return 0;
} catch (storm::exceptions::BaseException const& exception) {
diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h
index 9bc228d6e..dc46b063d 100644
--- a/src/utility/ErrorHandling.h
+++ b/src/utility/ErrorHandling.h
@@ -79,7 +79,7 @@ std::string demangle(char const* symbol) {
return symbol;
}
-void printUsage();
+void showPerformanceStatistics(uint64_t wallclockMilliseconds);
/*
* Handles the given signal. This will display the received signal and a backtrace.
@@ -88,7 +88,7 @@ void printUsage();
*/
void signalHandler(int sig) {
STORM_LOG_ERROR("The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal.");
- printUsage();
+ showPerformanceStatistics(0);
#ifndef WINDOWS
# define SIZE 128
void *buffer[SIZE];