sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

more work on transient variables 

Former-commit-id: e046bbe8a2 [formerly f4a866f0ef]
Former-commit-id: a6e6dbfee6
main
dehnert 9 years ago
parent
4728674a4a
commit
8f096e9475
12 changed files with 498 additions and 177 deletions
Split View
  1. 568
      src/builder/jit/ExplicitJitJaniModelBuilder.cpp
  2. 19
      src/builder/jit/ExplicitJitJaniModelBuilder.h
  3. 16
      src/cli/cli.cpp
  4. 2
      src/cli/cli.h
  5. 10
      src/settings/modules/GeneralSettings.cpp
  6. 9
      src/settings/modules/GeneralSettings.h
  7. 4
      src/settings/modules/IOSettings.h
  8. 21
      src/storage/expressions/ToCppVisitor.cpp
  9. 7
      src/storage/expressions/ToCppVisitor.h
  10. 8
      src/storage/jani/OrderedAssignments.cpp
  11. 7
      src/storm.cpp
  12. 4
      src/utility/ErrorHandling.h

568
src/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -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>

19
src/builder/jit/ExplicitJitJaniModelBuilder.h
View File

@ -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;
};
}

16
src/cli/cli.cpp
View File

@ -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.");
}
}
}

2
src/cli/cli.h
View File

@ -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.

10
src/settings/modules/GeneralSettings.cpp
View File

@ -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 {

9
src/settings/modules/GeneralSettings.h
View File

@ -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;

4
src/settings/modules/IOSettings.h
View File

@ -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;

21
src/storage/expressions/ToCppVisitor.cpp
View File

@ -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 << ")";
}

7
src/storage/expressions/ToCppVisitor.h
View File

@ -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 {

8
src/storage/jani/OrderedAssignments.cpp
View File

@ -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 {

7
src/storm.cpp
View File

@ -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) {

4
src/utility/ErrorHandling.h
View File

@ -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];

Write Preview
|||||||
100:0
Loading…
Cancel
Save