diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 1b759cfc5..5a7ecae4e 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1805,38 +1805,47 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << "."); } - STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support transient edge destination assignments."); + STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels."); + + storm::jani::Model preparedModel = model; + + // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway). + if (preparedModel.hasTransientEdgeDestinationAssignments()) { + preparedModel.liftTransientEdgeDestinationAssignments(); + } + + STORM_LOG_THROW(!preparedModel.hasTransientEdgeDestinationAssignments(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support transient edge destination assignments."); // Determine the actions that will appear in the parallel composition. - storm::jani::CompositionInformationVisitor visitor(model, model.getSystemComposition()); + storm::jani::CompositionInformationVisitor visitor(preparedModel, preparedModel.getSystemComposition()); storm::jani::CompositionInformation actionInformation = visitor.getInformation(); // Create all necessary variables. - CompositionVariableCreator<Type, ValueType> variableCreator(model, actionInformation); + CompositionVariableCreator<Type, ValueType> variableCreator(preparedModel, actionInformation); CompositionVariables<Type, ValueType> variables = variableCreator.create(); // Determine which transient assignments need to be considered in the building process. - std::vector<storm::expressions::Variable> rewardVariables = selectRewardVariables<Type, ValueType>(model, options); + std::vector<storm::expressions::Variable> rewardVariables = selectRewardVariables<Type, ValueType>(preparedModel, options); // Create a builder to compose and build the model. - CombinedEdgesSystemComposer<Type, ValueType> composer(model, actionInformation, variables, rewardVariables); + CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables); ComposerResult<Type, ValueType> system = composer.compose(); // Postprocess the variables in place. - postprocessVariables(model.getModelType(), system, variables); + postprocessVariables(preparedModel.getModelType(), system, variables); // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off). - storm::dd::Bdd<Type> terminalStates = postprocessSystem(model, system, variables, options); + storm::dd::Bdd<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options); // Start creating the model components. ModelComponents<Type, ValueType> modelComponents; // Build initial states. - modelComponents.initialStates = computeInitialStates(model, variables); + modelComponents.initialStates = computeInitialStates(preparedModel, variables); // Perform reachability analysis to obtain reachable states. storm::dd::Bdd<Type> transitionMatrixBdd = system.transitions.notZero(); - if (model.getModelType() == storm::jani::ModelType::MDP) { + if (preparedModel.getModelType() == storm::jani::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables); } modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); @@ -1850,7 +1859,7 @@ namespace storm { modelComponents.transitionMatrix = system.transitions * reachableStatesAdd; // Fix deadlocks if existing. - modelComponents.deadlockStates = fixDeadlocks(model.getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables); + modelComponents.deadlockStates = fixDeadlocks(preparedModel.getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables); // Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal. modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates; @@ -1859,10 +1868,10 @@ namespace storm { modelComponents.rewardModels = buildRewardModels(system, rewardVariables); // Build the label to expressions mapping. - modelComponents.labelToExpressionMap = buildLabelExpressions(model, variables, options); + modelComponents.labelToExpressionMap = buildLabelExpressions(preparedModel, variables, options); // Finally, create the model. - return createModel(model.getModelType(), variables, modelComponents); + return createModel(preparedModel.getModelType(), variables, modelComponents); } template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>; diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index a5abac90d..2623ee831 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -17,6 +17,7 @@ #include "src/utility/solver.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/UnexpectedException.h" @@ -41,12 +42,39 @@ namespace storm { transientVariables.insert(variable->getExpressionVariable()); } - for (auto const& automaton : this->model.getAutomata()) { + for (auto& automaton : this->model.getAutomata()) { + // FIXME: just for testing purposes. + automaton.pushEdgeAssignmentsToDestinations(); + automatonToLocationVariable.emplace(automaton.getName(), model.getManager().declareFreshIntegerVariable(false, automaton.getName() + "_")); - for (auto const& variable : automaton.getVariables().getTransientVariables()) { - transientVariables.insert(variable->getExpressionVariable()); - } } + + // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. +#ifdef STORM_HAVE_CARL + if (!std::is_same<ValueType, storm::RationalFunction>::value && model.hasUndefinedConstants()) { +#else + if (model.hasUndefinedConstants()) { +#endif + std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " + stream.str()); + } + +#ifdef STORM_HAVE_CARL + else if (std::is_same<ValueType, storm::RationalFunction>::value && !model.undefinedConstantsAreGraphPreserving()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); + } +#endif } template <typename ValueType, typename RewardModelType> @@ -112,7 +140,7 @@ namespace storm { std::ostream& operator<<(std::ostream& out, StateType const& in) { out << "<"; - {% for variable in nontransient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", "; + {% for variable in nontransient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", " << std::noboolalpha; {% endfor %} {% for variable in nontransient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; {% endfor %} @@ -126,9 +154,12 @@ namespace storm { return out; } - {% if transient_variables %} - struct TransientVariableType { - TransientVariableType() { + struct TransientVariables { + TransientVariables() { + reset(); + } + + void reset() { {% for variable in transient_variables.boolean %}{$variable.name} = {$variable.init}; {% endfor %} {% for variable in transient_variables.boundedInteger %}{$variable.name} = {$variable.init}; @@ -153,9 +184,9 @@ namespace storm { {% endfor %} }; - std::ostream& operator<<(std::ostream& out, TransientVariableType const& in) { + std::ostream& operator<<(std::ostream& out, TransientVariables const& in) { out << "<"; - {% for variable in transient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", "; + {% for variable in transient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", " << std::noboolalpha; {% endfor %} {% for variable in transient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; {% endfor %} @@ -166,7 +197,6 @@ namespace storm { out << ">"; return out; } - {% endif %} } } @@ -213,7 +243,21 @@ namespace storm { } {% for destination in edge.destinations %} - 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 %}) { + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% endfor %} + } + + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { + {% for level in destination.levels %} + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out); + {% endfor %} + } + + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { {% for level in destination.levels %}if (level == {$level.index}) { {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; {% endfor %} @@ -223,11 +267,9 @@ namespace storm { {% endfor %} } - static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { - {% if edge.referenced_transient_variables %}TransientVariableType transientIn; - TransientVariableType transientOut;{% endif %} + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { {% for level in destination.levels %} - destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out{% if edge.referenced_transient_variables %}, transientIn, transientOut{% endif %}); + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); {% endfor %} } {% endfor %} @@ -241,7 +283,21 @@ namespace storm { } {% for destination in edge.destinations %} - 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 %}) { + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% endfor %} + } + + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { + {% for level in destination.levels %} + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out); + {% endfor %} + } + + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { {% for level in destination.levels %}if (level == {$level.index}) { {% for assignment in level.nonTransientAssignments %}out.{$assignment.variable} = {$assignment.value}; {% endfor %} @@ -251,29 +307,27 @@ namespace storm { {% endfor %} } - static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out{% if edge.referenced_transient_variables %}, TransientVariableType const& transientIn, TransientVariableType& transientOut{% endif %}) { + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { {% for level in destination.levels %} - destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out{% if edge.referenced_transient_variables %}, transientIn, transientOut{% endif %}); + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); {% endfor %} } {% endfor %} {% endfor %} - 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 %} + typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&, TransientVariables const&, TransientVariables&); + typedef void (*DestinationFunctionPtr)(StateType const&, StateType&, TransientVariables const&, TransientVariables&); + typedef void (*DestinationWithoutTransientLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&); + typedef void (*DestinationWithoutTransientFunctionPtr)(StateType const&, StateType&); class Destination { public: - Destination() : mLowestLevel(0), mHighestLevel(0), mValue(), destinationLevelFunction(nullptr), destinationFunction(nullptr) { + Destination() : mLowestLevel(0), mHighestLevel(0), mValue(), destinationLevelFunction(nullptr), destinationFunction(nullptr), destinationWithoutTransientLevelFunction(nullptr), destinationWithoutTransientFunction(nullptr) { // Intentionally left empty. } - Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), mValue(value), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction) { + Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), mValue(value), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction), destinationWithoutTransientLevelFunction(destinationWithoutTransientLevelFunction), destinationWithoutTransientFunction(destinationWithoutTransientFunction) { // Intentionally left empty. } @@ -289,60 +343,31 @@ namespace storm { return mValue; } - void performLevel(int_fast64_t level, StateType const& in, StateType& out) const { - destinationLevelFunction(level, in, out); + void perform(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) const { + destinationLevelFunction(level, in, out, transientIn, transientOut); } - void perform(StateType const& in, StateType& out) const { - destinationFunction(in, out); + void perform(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) const { + destinationFunction(in, out, transientIn, transientOut); } - private: - int_fast64_t mLowestLevel; - int_fast64_t mHighestLevel; - ValueType mValue; - 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; + void perform(int_fast64_t level, StateType const& in, StateType& out) const { + destinationWithoutTransientLevelFunction(level, in, out); } - 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); + void perform(StateType const& in, StateType& out) const { + destinationWithoutTransientFunction(in, out); } - + private: int_fast64_t mLowestLevel; int_fast64_t mHighestLevel; ValueType mValue; - DestinationTransientLevelFunctionPtr destinationLevelFunction; - DestinationTransientFunctionPtr destinationFunction; + DestinationLevelFunctionPtr destinationLevelFunction; + DestinationFunctionPtr destinationFunction; + DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction; + DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction; }; - {% endif %} typedef bool (*EdgeEnabledFunctionPtr)(StateType const&); @@ -366,8 +391,8 @@ namespace storm { destinations.push_back(destination); } - void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction) { - destinations.emplace_back(lowestLevel, highestLevel, value, destinationLevelFunction, destinationFunction); + void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) { + destinations.emplace_back(lowestLevel, highestLevel, value, destinationLevelFunction, destinationFunction, destinationWithoutTransientLevelFunction, destinationWithoutTransientFunction); } std::vector<Destination> const& getDestinations() const { @@ -387,48 +412,6 @@ namespace storm { 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,13 +423,13 @@ namespace storm { }{% endfor %} {% for edge in nonsynch_edges %}{ edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}); - {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); {% endfor %} } {% endfor %} {% for edge in synch_edges %}{ edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}); - {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); {% endfor %} } {% endfor %} @@ -533,13 +516,18 @@ namespace storm { void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) { {% for edge in nonsynch_edges %}{ if ({$edge.guard}) { + {% if edge.referenced_transient_variables %} + TransientVariables transientIn; + TransientVariables transientOut; + {% endif %} Choice<IndexType, ValueType>& choice = behaviour.addChoice(); {% for destination in edge.destinations %}{ StateType out(in); - destination_perform_{$edge.name}_{$destination.name}(in, out); + destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.referenced_transient_variables %}, transientIn, transientOut{% endif %}); IndexType outStateIndex = getOrAddIndex(out, statesToExplore); choice.add(outStateIndex, {$destination.value}); - }{% endfor %} + } + {% endfor %} } } {% endfor %} @@ -596,9 +584,9 @@ namespace storm { std::vector<StateType> initialStates; std::vector<IndexType> deadlockStates; - {% for edge in nonsynch_edges %}{% if edge.referenced_transient_variables %}EdgeTransient {% endif %}{% if not edge.referenced_transient_variables %}Edge {% endif %} edge_{$edge.name}; + {% for edge in nonsynch_edges %}Edge edge_{$edge.name}; {% endfor %} - {% for edge in synch_edges %}{% if edge.referenced_transient_variables %}EdgeTransient {% endif %}{% if not edge.referenced_transient_variables %}Edge {% endif %} edge_{$edge.name}; + {% for edge in synch_edges %}Edge edge_{$edge.name}; {% endfor %} }; @@ -727,7 +715,7 @@ namespace storm { template <typename ValueType, typename RewardModelType> cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateBooleanVariable(storm::jani::BooleanVariable const& variable) { cpptempl::data_map result; - result["name"] = registerVariableName(variable.getExpressionVariable()); + result["name"] = registerVariable(variable.getExpressionVariable()); if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsBool()); } @@ -748,7 +736,7 @@ namespace storm { uint64_t range = static_cast<uint64_t>(upperBound - lowerBound + 1); uint64_t numberOfBits = static_cast<uint64_t>(std::ceil(std::log2(range))); - result["name"] = registerVariableName(variable.getExpressionVariable()); + result["name"] = registerVariable(variable.getExpressionVariable()); result["numberOfBits"] = std::to_string(numberOfBits); if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsInt() - lowerBound); @@ -761,7 +749,7 @@ namespace storm { cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateUnboundedIntegerVariable(storm::jani::UnboundedIntegerVariable const& variable) { cpptempl::data_map result; - result["name"] = registerVariableName(variable.getExpressionVariable()); + result["name"] = registerVariable(variable.getExpressionVariable()); if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsInt()); } @@ -773,7 +761,7 @@ namespace storm { cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateRealVariable(storm::jani::RealVariable const& variable) { cpptempl::data_map result; - result["name"] = registerVariableName(variable.getExpressionVariable()); + result["name"] = registerVariable(variable.getExpressionVariable()); if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsDouble()); } @@ -785,7 +773,7 @@ namespace storm { cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateLocationVariable(storm::jani::Automaton const& automaton) { cpptempl::data_map result; - result["name"] = registerVariableName(getLocationVariable(automaton)); + result["name"] = registerVariable(getLocationVariable(automaton)); result["numberOfBits"] = static_cast<uint64_t>(std::ceil(std::log2(automaton.getNumberOfLocations()))); return result; @@ -902,7 +890,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(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions("in.")); + label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable->asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); labels.push_back(label); } } @@ -911,7 +899,7 @@ namespace storm { for (auto const& expression : this->options.getExpressionLabels()) { cpptempl::data_map label; label["name"] = expression.toString(); - label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions("in.")); + label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); labels.push_back(label); } @@ -934,10 +922,10 @@ namespace storm { if (terminalEntry.second) { labelExpression = !labelExpression; } - terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions("in."))); + terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName))); } else { auto expression = terminalEntry.second ? labelOrExpression.getExpression() : !labelOrExpression.getExpression(); - terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions("in."))); + terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName))); } } @@ -958,8 +946,10 @@ namespace storm { // 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; + int_fast64_t lowestLevel; + int_fast64_t highestLevel; + bool firstDestination = true; + bool generateTransient = 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()); @@ -967,17 +957,26 @@ namespace storm { 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()) { - + if (!destination.getOrderedAssignments().empty()) { + if (firstDestination) { + lowestLevel = destination.getOrderedAssignments().getLowestLevel(); + highestLevel = destination.getOrderedAssignments().getHighestLevel(); + firstDestination = false; + } else { + lowestLevel = std::min(lowestLevel, destination.getOrderedAssignments().getLowestLevel()); + highestLevel = std::max(highestLevel, destination.getOrderedAssignments().getHighestLevel()); } - std::set<storm::expressions::Variable> usedVariables; - for (auto const& variable : usedVariables) { - if (transientVariables.find(variable) != transientVariables.end()) { - generateTransientVariableCode = true; + } + if (!generateTransient) { + for (auto const& assignment : destination.getOrderedAssignments()) { + if (assignment.isTransient()) { + generateTransient = true; + } + std::set<storm::expressions::Variable> usedVariables = assignment.getAssignedExpression().getVariables(); + for (auto const& variable : usedVariables) { + if (transientVariables.find(variable) != transientVariables.end()) { + generateTransient = true; + } } } } @@ -987,16 +986,35 @@ namespace storm { } ++position; } + bool generateLevelCode = lowestLevel != highestLevel; 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 << ", "; } + if (generateLevelCode) { + vectorSource << "int64_t lowestLevel, int64_t highestLevel, "; + } vectorSource << "Choice<IndexType, ValueType>& choice) {" << std::endl; indent(vectorSource, indentLevel + 1) << "StateType out(in);" << std::endl; + indent(vectorSource, indentLevel + 1) << "TransientVariables transientIn;" << std::endl; + indent(vectorSource, indentLevel + 1) << "TransientVariables transientOut;" << std::endl; + + if (generateLevelCode) { + indent(vectorSource, indentLevel + 1) << "for (int64_t level = lowestLevel; level <= highestLevel; ++level) {" << std::endl; + ++indentLevel; + } for (uint64_t index = 0; index < numberOfActionInputs; ++index) { - indent(vectorSource, indentLevel + 1) << "destination" << index << ".perform(in, out);" << std::endl; + indent(vectorSource, indentLevel + 1) << "destination" << index << ".perform("; + if (generateLevelCode) { + vectorSource << "level, "; + } + vectorSource << "in, out, transientIn, transientOut);" << std::endl; + } + if (generateLevelCode) { + --indentLevel; + indent(vectorSource, indentLevel + 1) << "}" << std::endl; } indent(vectorSource, indentLevel + 1) << "IndexType outStateIndex = getOrAddIndex(out, statesToExplore);" << std::endl; indent(vectorSource, indentLevel + 1) << "choice.add(outStateIndex, "; @@ -1014,13 +1032,28 @@ namespace storm { vectorSource << "Edge const& edge" << index << ", "; } vectorSource << "Choice<IndexType, ValueType>& choice) {" << std::endl; + if (generateLevelCode) { + indent(vectorSource, indentLevel + 1) << "int64_t lowestLevel; int64_t highestLevel;"; + } for (uint64_t index = 0; index < numberOfActionInputs; ++index) { indent(vectorSource, indentLevel + 1 + index) << "for (auto const& destination" << index << " : edge" << index << ") {" << std::endl; + if (generateLevelCode) { + if (index == 0) { + indent(vectorSource, indentLevel + 2 + index) << "lowestLevel = edge0.lowestLevel();" << std::endl; + indent(vectorSource, indentLevel + 2 + index) << "highestLevel = edge0.highestLevel();" << std::endl; + } else { + indent(vectorSource, indentLevel + 2 + index) << "lowestLevel = std::min(lowestLevel, edge0.lowestLevel());" << std::endl; + indent(vectorSource, indentLevel + 2 + index) << "highestLevel = std::max(highestLevel, edge0.highestLevel());" << std::endl; + } + } } indent(vectorSource, indentLevel + 1 + numberOfActionInputs) << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(in, behaviour, statesToExplore, "; for (uint64_t index = 0; index < numberOfActionInputs; ++index) { vectorSource << "destination" << index << ", "; } + if (generateLevelCode) { + vectorSource << "lowestLevel, highestLevel, "; + } vectorSource << "choice);" << std::endl; for (uint64_t index = 0; index < numberOfActionInputs; ++index) { indent(vectorSource, indentLevel + numberOfActionInputs - index) << "}" << std::endl; @@ -1224,7 +1257,7 @@ namespace storm { ++destinationIndex; } - edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions("in.")); + edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); edgeData["destinations"] = cpptempl::make_data(destinations); edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex); @@ -1243,7 +1276,7 @@ namespace storm { cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments()); destinationData["name"] = asString(destinationIndex); destinationData["levels"] = cpptempl::make_data(levels); - destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions("in.", "double")); + destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double")); if (destination.getOrderedAssignments().empty()) { destinationData["lowestLevel"] = "0"; destinationData["highestLevel"] = "0"; @@ -1279,9 +1312,9 @@ namespace storm { } if (assignment.isTransient()) { - transientAssignmentData.push_back(generateAssignment(assignment, "in.")); + transientAssignmentData.push_back(generateAssignment(assignment)); } else { - nonTransientAssignmentData.push_back(generateAssignment(assignment, "in.")); + nonTransientAssignmentData.push_back(generateAssignment(assignment)); } } @@ -1314,20 +1347,20 @@ namespace storm { } template <typename ValueType, typename RewardModelType> - cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateAssignment(storm::jani::Assignment const& assignment, std::string const& prefix) { + cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateAssignment(storm::jani::Assignment const& assignment) { cpptempl::data_map result; result["variable"] = getVariableName(assignment.getExpressionVariable()); auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable()); if (lowerBoundIt != lowerBounds.end()) { if (lowerBoundIt->second < 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), prefix); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); } else if (lowerBoundIt->second == 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), prefix); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), prefix); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); } } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), prefix); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); } return result; } @@ -1338,9 +1371,25 @@ namespace storm { } template <typename ValueType, typename RewardModelType> - std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::registerVariableName(storm::expressions::Variable const& variable) { - variableToName[variable] = variable.getName(); - return variable.getName(); + std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::registerVariable(storm::expressions::Variable const& variable, bool transient) { + std::string variableName; + + // Technically, we would need to catch all keywords here... + if (variable.getName() == "default") { + variableName = "__default"; + } else { + variableName = variable.getName(); + } + + variableToName[variable] = variableName; + if (transient) { + transientVariables.insert(variable); + variablePrefixes[variable] = "transientIn."; + } else { + nontransientVariables.insert(variable); + variablePrefixes[variable] = "in."; + } + return variableToName[variable] ; } template <typename ValueType, typename RewardModelType> diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h index bc38cb60b..552c1154f 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -74,11 +74,11 @@ namespace storm { cpptempl::data_map generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const; - cpptempl::data_map generateAssignment(storm::jani::Assignment const& assignment, std::string const& prefix = ""); + cpptempl::data_map generateAssignment(storm::jani::Assignment const& assignment); // Auxiliary functions that perform regularly needed steps. std::string const& getVariableName(storm::expressions::Variable const& variable) const; - std::string const& registerVariableName(storm::expressions::Variable const& variable); + std::string const& registerVariable(storm::expressions::Variable const& variable, bool transient = false); 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); @@ -100,6 +100,8 @@ namespace storm { std::map<storm::expressions::Variable, storm::expressions::Expression> lowerBoundShiftSubstitution; std::map<storm::expressions::Variable, int_fast64_t> lowerBounds; std::set<storm::expressions::Variable> transientVariables; + std::set<storm::expressions::Variable> nontransientVariables; + std::unordered_map<storm::expressions::Variable, std::string> variablePrefixes; }; } diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index a6407acdd..5b86fec6e 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -26,8 +26,14 @@ namespace storm { STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); + STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); + // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway). + if (this->model.hasTransientEdgeDestinationAssignments()) { + this->model.liftTransientEdgeDestinationAssignments(); + } + // Only after checking validity of the program, we initialize the variable information. this->checkValid(); this->variableInformation = VariableInformation(model); diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index 62440992d..3e1bbcf80 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -86,12 +86,6 @@ namespace storm { if (this->isJaniModel()) { std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString); storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants(); - if (preparedModel.hasTransientEdgeDestinationAssignments()) { - preparedModel.liftTransientEdgeDestinationAssignments(); - if (preparedModel.hasTransientEdgeDestinationAssignments()) { - STORM_LOG_WARN("JANI model has non-liftable transient edge-destinations assignments, which are currently not supported. Trying to lift these assignments to edges rather than destinations failed."); - } - } return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString); diff --git a/src/storage/expressions/ToCppVisitor.cpp b/src/storage/expressions/ToCppVisitor.cpp index 6bf0b6d53..108d95fe8 100644 --- a/src/storage/expressions/ToCppVisitor.cpp +++ b/src/storage/expressions/ToCppVisitor.cpp @@ -5,24 +5,16 @@ namespace storm { namespace expressions { - ToCppTranslationOptions::ToCppTranslationOptions(std::string const& prefix, std::string const& valueTypeCast) : valueTypeCast(valueTypeCast), prefix(prefix) { + ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast) : prefixes(prefixes), names(names), valueTypeCast(valueTypeCast) { // Intentionally left empty. } - std::string const& ToCppTranslationOptions::getPrefix() const { - return prefix; + std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getPrefixes() const { + return prefixes; } - 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(); + std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getNames() const { + return names; } bool ToCppTranslationOptions::hasValueTypeCast() const { @@ -213,11 +205,21 @@ namespace storm { stream << "static_cast<" << options.getValueTypeCast() << ">("; } - auto prefixIt = options.getSpecificPrefixes().find(expression.getVariable()); - if (prefixIt != options.getSpecificPrefixes().end()) { - stream << prefixIt->second << expression.getVariableName(); + auto prefixIt = options.getPrefixes().find(expression.getVariable()); + if (prefixIt != options.getPrefixes().end()) { + auto nameIt = options.getNames().find(expression.getVariable()); + if (nameIt != options.getNames().end()) { + stream << prefixIt->second << nameIt->second; + } else { + stream << prefixIt->second << expression.getVariableName(); + } } else { - stream << options.getPrefix() << expression.getVariableName(); + auto nameIt = options.getNames().find(expression.getVariable()); + if (nameIt != options.getNames().end()) { + stream << nameIt->second; + } else { + stream << expression.getVariableName(); + } } if (options.hasValueTypeCast()) { diff --git a/src/storage/expressions/ToCppVisitor.h b/src/storage/expressions/ToCppVisitor.h index 98d13e750..a94af32de 100644 --- a/src/storage/expressions/ToCppVisitor.h +++ b/src/storage/expressions/ToCppVisitor.h @@ -12,27 +12,24 @@ namespace storm { class ToCppTranslationOptions { public: - ToCppTranslationOptions(std::string const& prefix = "", std::string const& valueTypeCast = ""); + ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast = ""); - 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(); + std::unordered_map<storm::expressions::Variable, std::string> const& getPrefixes() const; + std::unordered_map<storm::expressions::Variable, std::string> const& getNames() const; bool hasValueTypeCast() const; std::string const& getValueTypeCast() const; void clearValueTypeCast(); private: + std::unordered_map<storm::expressions::Variable, std::string> const& prefixes; + std::unordered_map<storm::expressions::Variable, std::string> const& names; std::string valueTypeCast; - std::string prefix; - std::unordered_map<storm::expressions::Variable, std::string> specificPrefixes; }; class ToCppVisitor : public ExpressionVisitor { public: - std::string translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options = ToCppTranslationOptions()); + std::string translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options); virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; diff --git a/src/storage/jani/Assignment.cpp b/src/storage/jani/Assignment.cpp index 99f2a09b1..cbbd45ba7 100644 --- a/src/storage/jani/Assignment.cpp +++ b/src/storage/jani/Assignment.cpp @@ -11,8 +11,7 @@ namespace storm { } bool Assignment::operator==(Assignment const& other) const { - // FIXME: the level is currently ignored as we do not support it - return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()); + return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel(); } storm::jani::Variable const& Assignment::getVariable() const { diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 8ed71acbc..7f511d251 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -461,5 +461,15 @@ namespace storm { edge.liftTransientDestinationAssignments(); } } + + bool Automaton::usesAssignmentLevels() const { + for (auto const& edge : this->getEdges()) { + if (edge.usesAssignmentLevels()) { + return true; + } + } + return false; + } + } } diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 5ae609853..71a61b4fe 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -327,6 +327,11 @@ namespace storm { */ void liftTransientEdgeDestinationAssignments(); + /*! + * Retrieves whether the automaton uses an assignment level other than zero. + */ + bool usesAssignmentLevels() const; + private: /// The name of the automaton. std::string name; diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index 69c85db59..5a30ec00e 100644 --- a/src/storage/jani/Edge.cpp +++ b/src/storage/jani/Edge.cpp @@ -146,5 +146,14 @@ namespace storm { } return false; } + + bool Edge::usesAssignmentLevels() const { + for (auto const& destination : this->getDestinations()) { + if (destination.usesAssignmentLevels()) { + return true; + } + } + return false; + } } } diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h index de4becb3e..60d202cd2 100644 --- a/src/storage/jani/Edge.h +++ b/src/storage/jani/Edge.h @@ -102,7 +102,8 @@ namespace storm { /*! * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these - * assignments are no longer contained in the destination. + * assignments are no longer contained in the destination. Note that this may modify the semantics of the + * model if assignment levels are being used somewhere in the model. */ void liftTransientDestinationAssignments(); @@ -121,6 +122,11 @@ namespace storm { */ bool hasTransientEdgeDestinationAssignments() const; + /*! + * Retrieves whether the edge uses an assignment level other than zero. + */ + bool usesAssignmentLevels() const; + private: /// The index of the source location. uint64_t sourceLocationIndex; diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp index b5c785c05..f1b30fe0e 100644 --- a/src/storage/jani/EdgeDestination.cpp +++ b/src/storage/jani/EdgeDestination.cpp @@ -55,5 +55,12 @@ namespace storm { return !assignments.getTransientAssignments().empty(); } + bool EdgeDestination::usesAssignmentLevels() const { + if (this->getOrderedAssignments().empty()) { + return false; + } + return this->getOrderedAssignments().getLowestLevel() != 0 || this->getOrderedAssignments().getHighestLevel() != 0; + } + } } diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h index c9e5e5e64..b119ac80d 100644 --- a/src/storage/jani/EdgeDestination.h +++ b/src/storage/jani/EdgeDestination.h @@ -58,6 +58,11 @@ namespace storm { */ bool hasTransientAssignment() const; + /*! + * Retrieves whether the edge uses an assignment level other than zero. + */ + bool usesAssignmentLevels() const; + private: // The index of the destination location. uint64_t locationIndex; diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 0203a2279..5da8a4e62 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -577,5 +577,14 @@ namespace storm { } return false; } + + bool Model::usesAssignmentLevels() const { + for (auto const& automaton : this->getAutomata()) { + if (automaton.usesAssignmentLevels()) { + return true; + } + } + return false; + } } } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 8a69901e4..8cc33341d 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -355,6 +355,11 @@ namespace storm { */ bool hasTransientEdgeDestinationAssignments() const; + /*! + * Retrieves whether the model uses an assignment level other than zero. + */ + bool usesAssignmentLevels() const; + void makeStandardJaniCompliant(); /// The name of the silent action.