From 8f096e9475ceba80cdcc62ac616294cf19f98a2f Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 1 Nov 2016 16:48:46 +0100 Subject: [PATCH] more work on transient variables Former-commit-id: e046bbe8a20003b5eed7cddffbc4c9aec8f6b4a4 [formerly f4a866f0eff128097307a3f3e221ebf1c238d279] Former-commit-id: a6e6dbfee6dbeea4a1bd6079b9c5a6eac828bb68 --- .../jit/ExplicitJitJaniModelBuilder.cpp | 568 +++++++++++++----- src/builder/jit/ExplicitJitJaniModelBuilder.h | 19 +- src/cli/cli.cpp | 16 +- src/cli/cli.h | 2 +- src/settings/modules/GeneralSettings.cpp | 10 +- src/settings/modules/GeneralSettings.h | 9 +- src/settings/modules/IOSettings.h | 4 +- src/storage/expressions/ToCppVisitor.cpp | 21 +- src/storage/expressions/ToCppVisitor.h | 7 + src/storage/jani/OrderedAssignments.cpp | 8 +- src/storm.cpp | 7 +- src/utility/ErrorHandling.h | 4 +- 12 files changed, 498 insertions(+), 177 deletions(-) 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 ExplicitJitJaniModelBuilder::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 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 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 { public: JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) { @@ -440,9 +596,9 @@ namespace storm { std::vector initialStates; std::vector 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 - cpptempl::data_map ExplicitJitJaniModelBuilder::generateStateVariables() { - cpptempl::data_list booleanVariables; - cpptempl::data_list boundedIntegerVariables; + cpptempl::data_map ExplicitJitJaniModelBuilder::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 + cpptempl::data_map ExplicitJitJaniModelBuilder::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(upperBound - lowerBound + 1); + uint64_t numberOfBits = static_cast(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 + cpptempl::data_map ExplicitJitJaniModelBuilder::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 + cpptempl::data_map ExplicitJitJaniModelBuilder::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 + cpptempl::data_map ExplicitJitJaniModelBuilder::generateLocationVariable(storm::jani::Automaton const& automaton) { + cpptempl::data_map result; + + result["name"] = registerVariableName(getLocationVariable(automaton)); + result["numberOfBits"] = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); + + return result; + } + + template + void ExplicitJitJaniModelBuilder::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(upperBound - lowerBound + 1); - uint64_t numberOfBits = static_cast(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(upperBound - lowerBound); - uint64_t numberOfBits = static_cast(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(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 @@ -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 cpptempl::data_map ExplicitJitJaniModelBuilder::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& behaviour, StateSet& 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 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& behaviour, StateSet& statesToExplore, "; for (uint64_t index = 0; index < numberOfActionInputs; ++index) { vectorSource << "Destination const& destination" << index << ", "; } vectorSource << "Choice& 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& behaviour, StateSet& statesToExplore, "; + indent(vectorSource, indentLevel) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore, "; for (uint64_t index = 0; index < numberOfActionInputs; ++index) { vectorSource << "Edge const& edge" << index << ", "; } vectorSource << "Choice& 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>> const& edges, StateBehaviour& behaviour, StateSet& statesToExplore"; + indent(vectorSource, indentLevel) << "void performSynchronizedEdges_" << synchronizationVectorIndex << "_" << index << "(StateType const& in, std::vector>> const& edges, StateBehaviour& behaviour, StateSet& 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& choice = behaviour.addChoice();" << std::endl; - vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, "; + indent(vectorSource, indentLevel + 2) << "Choice& 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>& edges, uint64_t position) {" << std::endl; - uint64_t position = 0; + indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector>& 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& behaviour, StateSet& statesToExplore) {" << std::endl; - vectorSource << "std::vector>> edges(" << synchronizationVector.getNumberOfActionInputs() << ");" << std::endl; + indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; + indent(vectorSource, indentLevel + 1) << "std::vector>> 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> synchronizingActions(parallelComposition.getNumberOfSubcompositions()); uint64_t synchronizationVectorIndex = 0; @@ -916,14 +1205,34 @@ namespace storm { cpptempl::data_list destinations; uint64_t destinationIndex = 0; + std::set 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 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 cpptempl::data_map ExplicitJitJaniModelBuilder::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::getVariableName(storm::expressions::Variable const& variable) const { return variableToName.at(variable); } - - template - std::string ExplicitJitJaniModelBuilder::getQualifiedVariableName(storm::jani::Variable const& variable) const { - return variable.getName(); - } - - template - std::string ExplicitJitJaniModelBuilder::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const { - return variable.getExpressionVariable().getName(); - } template - std::string ExplicitJitJaniModelBuilder::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::Variable const& variable) const { + std::string const& ExplicitJitJaniModelBuilder::registerVariableName(storm::expressions::Variable const& variable) { + variableToName[variable] = variable.getName(); return variable.getName(); } - + template - std::string ExplicitJitJaniModelBuilder::getLocationVariableName(storm::jani::Automaton const& automaton) const { - return automaton.getName() + "_location"; + storm::expressions::Variable const& ExplicitJitJaniModelBuilder::getLocationVariable(storm::jani::Automaton const& automaton) const { + return automatonToLocationVariable.at(automaton.getName()); } template 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 locationVariables; ModelComponentsBuilder modelComponentsBuilder; typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderGetFunction; std::unique_ptr> builder; std::unordered_map variableToName; + std::map automatonToLocationVariable; + storm::expressions::ToCppVisitor expressionTranslator; std::map lowerBoundShiftSubstitution; std::map lowerBounds; + std::set 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().isParametricSet()) { #ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(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 const& prefixes) { + specificPrefixes = prefixes; + } + + std::unordered_map 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 +#include +#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 const& prefixes); + std::unordered_map 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 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(end - start); - auto durationSec = std::chrono::duration_cast(end - start); - if(storm::settings::getModule().isPrintTimingsSet()) { - std::cout << "Overal runtime: " << duration.count() << " ms. (approximately " << durationSec.count() << " seconds)." << std::endl; + + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::showTimeAndMemoryStatistics(std::chrono::duration_cast(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];