From acfb8d28c0ae98c1d4360e5c43fa753a9f0fa062 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 6 Oct 2018 15:22:32 +0200 Subject: [PATCH] fixing issues related to rewards in JIT-based model builder --- src/storm-conv/api/storm-conv.cpp | 8 +- src/storm/builder/BuilderOptions.cpp | 6 +- src/storm/builder/BuilderOptions.h | 7 +- .../jit/ExplicitJitJaniModelBuilder.cpp | 111 +++++++++++------- .../builder/jit/ExplicitJitJaniModelBuilder.h | 2 +- .../modelchecker/CtmcCslModelCheckerTest.cpp | 2 +- .../DtmcPrctlModelCheckerTest.cpp | 2 +- .../MarkovAutomatonCslModelCheckerTest.cpp | 3 +- 8 files changed, 84 insertions(+), 57 deletions(-) diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index 0ed03a071..d9aa2212b 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -52,11 +52,11 @@ namespace storm { // Perform conversion auto res = program.toJani(properties, options.allVariablesGlobal); if (res.second.empty()) { - std::vector clondedProperties; + std::vector clonedProperties; for (auto const& p : properties) { - clondedProperties.push_back(p.clone()); + clonedProperties.push_back(p.clone()); } - res.second = std::move(clondedProperties); + res.second = std::move(clonedProperties); } // Postprocess Jani model based on the options @@ -75,4 +75,4 @@ namespace storm { } -} \ No newline at end of file +} diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 24753ec91..791bc661a 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -74,7 +74,7 @@ namespace storm { // Determine the reward models we need to build. std::set referencedRewardModels = formula.getReferencedRewardModels(); for (auto const& rewardModelName : referencedRewardModels) { - rewardModelNames.push_back(rewardModelName); + rewardModelNames.emplace(rewardModelName); } // Extract all the labels used in the formula. @@ -123,7 +123,7 @@ namespace storm { } } - std::vector const& BuilderOptions::getRewardModelNames() const { + std::set const& BuilderOptions::getRewardModelNames() const { return rewardModelNames; } @@ -211,7 +211,7 @@ namespace storm { BuilderOptions& BuilderOptions::addRewardModel(std::string const& rewardModelName) { STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway."); - rewardModelNames.emplace_back(rewardModelName); + rewardModelNames.emplace(rewardModelName); return *this; } diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index b718a7f82..d0982fa85 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -82,17 +82,18 @@ namespace storm { */ void setTerminalStatesFromFormula(storm::logic::Formula const& formula); - /*! * Which reward models are built * @return */ - std::vector const& getRewardModelNames() const; + std::set const& getRewardModelNames() const; + /*! * Which labels are built * @return */ std::set const& getLabelNames() const; + /*! * Which expression labels are built * @return @@ -203,7 +204,7 @@ namespace storm { bool buildAllRewardModels; /// The names of the reward models to generate. - std::vector rewardModelNames; + std::set rewardModelNames; /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored. bool buildAllLabels; diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index f1e6ba3e8..a3eaf8b35 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -35,7 +35,6 @@ #include "storm/settings/modules/CoreSettings.h" - #include "storm/utility/OsDetection.h" #include "storm-config.h" @@ -1044,7 +1043,7 @@ namespace storm { if (generateLevelCode) { vectorSource << "int64_t lowestLevel, int64_t highestLevel, "; } - vectorSource << "Choice& choice) {" << std::endl; + vectorSource << "ValueType const& rate, Choice& choice) {" << std::endl; if (options.isExplorationChecksSet()) { indent(vectorSource, indentLevel + 1) << "VariableWrites variableWrites;" << std::endl; } @@ -1074,13 +1073,14 @@ namespace storm { indent(vectorSource, indentLevel + 1) << "IndexType outStateIndex = getOrAddIndex(out, statesToExplore);" << std::endl; indent(vectorSource, indentLevel + 1) << "ValueType probability = "; for (uint64_t index = 0; index < numberOfActionInputs; ++index) { - vectorSource << "destination" << index << ".value(in)"; + vectorSource << "destination" << index << ".probability(in)"; if (index + 1 < numberOfActionInputs) { vectorSource << " * "; } } vectorSource << ";" << std::endl; - indent(vectorSource, indentLevel + 1) << "choice.add(outStateIndex, probability);" << std::endl; + indent(vectorSource, indentLevel + 1) << "ValueType value = rate * probability;" << std::endl; + indent(vectorSource, indentLevel + 1) << "choice.add(outStateIndex, value);" << std::endl; std::stringstream tmp; indent(tmp, indentLevel + 1) << "{% for reward in destination_rewards %}choice.addReward({$reward.index}, probability * transientOut.{$reward.variable});" << std::endl; @@ -1092,7 +1092,7 @@ namespace storm { for (uint64_t index = 0; index < numberOfActionInputs; ++index) { vectorSource << "Edge const& edge" << index << ", "; } - vectorSource << "Choice& choice) {" << std::endl; + vectorSource << "ValueType const& rate, Choice& choice) {" << std::endl; if (generateLevelCode) { indent(vectorSource, indentLevel + 1) << "int64_t lowestLevel; int64_t highestLevel;"; } @@ -1115,7 +1115,7 @@ namespace storm { if (generateLevelCode) { vectorSource << "lowestLevel, highestLevel, "; } - vectorSource << "choice);" << std::endl; + vectorSource << "rate, choice);" << std::endl; for (uint64_t index = 0; index < numberOfActionInputs; ++index) { indent(vectorSource, indentLevel + numberOfActionInputs - index) << "}" << std::endl; } @@ -1138,7 +1138,7 @@ namespace storm { vectorSource << ", VariableWrites& variableWrites"; } } - vectorSource << ") {" << std::endl; + vectorSource << ", ValueType const& rate) {" << std::endl; if (index == 0) { if (options.isExplorationChecksSet()) { indent(vectorSource, indentLevel + 1) << "VariableWrites variableWrites;" << std::endl; @@ -1157,11 +1157,11 @@ namespace storm { for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) { vectorSource << "edge" << innerIndex << ", "; } - vectorSource << "transientIn, transientOut"; + vectorSource << "transientIn, transientOut, "; if (options.isExplorationChecksSet()) { - vectorSource << ", variableWrites"; + vectorSource << "variableWrites, "; } - vectorSource << ");" << std::endl; + vectorSource << "rate * edge" << index << ".get().rate(in));" << std::endl; } else { indent(vectorSource, indentLevel + 2) << "Choice& choice = behaviour.addChoice();" << std::endl; @@ -1176,7 +1176,7 @@ namespace storm { for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) { vectorSource << "edge" << innerIndex << ", "; } - vectorSource << " choice);" << std::endl; + vectorSource << "rate * edge" << index << ".get().rate(in), choice);" << std::endl; } indent(vectorSource, indentLevel + 1) << "}" << std::endl; @@ -1212,7 +1212,7 @@ namespace storm { indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; indent(vectorSource, indentLevel + 1) << "#ifndef NDEBUG" << std::endl; - indent(vectorSource, indentLevel + 1) << "std::cout << \"exploring synchronization vector " << synchronizationVectorIndex << "\" << std::endl;" << std::endl; + indent(vectorSource, indentLevel + 1) << "std::cout << \"Exploring synchronization vector " << synchronizationVectorIndex << ".\" << std::endl;" << std::endl; indent(vectorSource, indentLevel + 1) << "#endif" << std::endl; indent(vectorSource, indentLevel + 1) << "std::vector>> edges(" << synchronizationVector.getNumberOfActionInputs() << ");" << std::endl; @@ -1226,7 +1226,7 @@ namespace storm { ++participatingPosition; } } - indent(vectorSource, indentLevel + 1) << "performSynchronizedEdges_" << synchronizationVectorIndex << "_0(state, edges, behaviour, statesToExplore);" << std::endl; + indent(vectorSource, indentLevel + 1) << "performSynchronizedEdges_" << synchronizationVectorIndex << "_0(state, edges, behaviour, statesToExplore, storm::utility::one());" << std::endl; indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; cpptempl::data_map vector; @@ -1338,7 +1338,7 @@ namespace storm { uint64_t destinationIndex = 0; std::set transientVariablesInDestinations; for (auto const& destination : edge.getDestinations()) { - destinations.push_back(generateDestination(automaton, destinationIndex, destination, edge.getOptionalRate())); + destinations.push_back(generateDestination(automaton, destinationIndex, destination)); for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) { if (assignment.isTransient()) { @@ -1364,6 +1364,17 @@ namespace storm { edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex); edgeData["transient_assignments"] = cpptempl::make_data(edgeAssignments); edgeData["markovian"] = asString(edge.hasRate()); + if (edge.hasRate()) { + if (std::is_same::value) { + edgeData["rate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getRate()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble)); + } else if (std::is_same::value) { + edgeData["rate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getRate()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber)); + } else if (std::is_same::value) { + edgeData["rate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getRate()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction)); + } + } else { + edgeData["rate"] = std::string("storm::utility::one()"); + } cpptempl::data_list transientVariablesInDestinationsData; for (auto const& variable : transientVariablesInDestinations) { @@ -1379,19 +1390,19 @@ namespace storm { } template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(storm::jani::Automaton const& automaton, uint64_t destinationIndex, storm::jani::EdgeDestination const& destination, boost::optional const& rate) { + cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(storm::jani::Automaton const& automaton, uint64_t destinationIndex, storm::jani::EdgeDestination const& destination) { cpptempl::data_map destinationData; cpptempl::data_list levels = generateLevels(automaton, destination.getLocationIndex(), destination.getOrderedAssignments()); destinationData["name"] = asString(destinationIndex); destinationData["levels"] = cpptempl::make_data(levels); - storm::expressions::Expression expressionToTranslate = rate ? shiftVariablesWrtLowerBound(rate.get() * destination.getProbability()) : shiftVariablesWrtLowerBound(destination.getProbability()); + storm::expressions::Expression shiftedProbabilityExpression = shiftVariablesWrtLowerBound(destination.getProbability()); if (std::is_same::value) { - destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble)); + destinationData["probability"] = expressionTranslator.translate(shiftedProbabilityExpression, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble)); } else if (std::is_same::value) { - destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber)); + destinationData["probability"] = expressionTranslator.translate(shiftedProbabilityExpression, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber)); } else if (std::is_same::value) { - destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction)); + destinationData["probability"] = expressionTranslator.translate(shiftedProbabilityExpression, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction)); } if (destination.getOrderedAssignments().empty()) { destinationData["lowestLevel"] = "0"; @@ -1927,6 +1938,10 @@ namespace storm { return false; } + static ValueType edge_rate_{$edge.name}(StateType const& in) { + return {$edge.rate}; + } + static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}) { {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; {% if exploration_checks %} @@ -1991,8 +2006,8 @@ namespace storm { {% endfor %} } - static ValueType destination_value_{$edge.name}_{$destination.name}(StateType const& in) { - return {$destination.value}; + static ValueType destination_probability_{$edge.name}_{$destination.name}(StateType const& in) { + return {$destination.probability}; } {% endfor %}{% endfor %} @@ -2004,6 +2019,10 @@ namespace storm { return false; } + static ValueType edge_rate_{$edge.name}(StateType const& in) { + return {$edge.rate}; + } + static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}) { {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; {% if exploration_checks %} @@ -2068,12 +2087,12 @@ namespace storm { {% endfor %} } - static ValueType destination_value_{$edge.name}_{$destination.name}(StateType const& in) { - return {$destination.value}; + static ValueType destination_probability_{$edge.name}_{$destination.name}(StateType const& in) { + return {$destination.probability}; } {% endfor %}{% endfor %} - typedef ValueType (*DestinationValueFunctionPtr)(StateType const&); + typedef ValueType (*DestinationProbabilityFunctionPtr)(StateType const&); typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&, TransientVariables const&, TransientVariables& {% if exploration_checks %}, VariableWrites& {% endif %}); typedef void (*DestinationFunctionPtr)(StateType const&, StateType&, TransientVariables const&, TransientVariables& {% if exploration_checks %}, VariableWrites& {% endif %}); typedef void (*DestinationWithoutTransientLevelFunctionPtr)(int_fast64_t, StateType const&, StateType& {% if exploration_checks %}, VariableWrites& {% endif %}); @@ -2081,11 +2100,11 @@ namespace storm { class Destination { public: - Destination() : mLowestLevel(0), mHighestLevel(0), destinationValueFunction(nullptr), destinationLevelFunction(nullptr), destinationFunction(nullptr), destinationWithoutTransientLevelFunction(nullptr), destinationWithoutTransientFunction(nullptr) { + Destination() : mLowestLevel(0), mHighestLevel(0), destinationProbabilityFunction(nullptr), destinationLevelFunction(nullptr), destinationFunction(nullptr), destinationWithoutTransientLevelFunction(nullptr), destinationWithoutTransientFunction(nullptr) { // Intentionally left empty. } - Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, DestinationValueFunctionPtr destinationValueFunction, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), destinationValueFunction(destinationValueFunction), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction), destinationWithoutTransientLevelFunction(destinationWithoutTransientLevelFunction), destinationWithoutTransientFunction(destinationWithoutTransientFunction) { + Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, DestinationProbabilityFunctionPtr destinationProbabilityFunction, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), destinationProbabilityFunction(destinationProbabilityFunction), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction), destinationWithoutTransientLevelFunction(destinationWithoutTransientLevelFunction), destinationWithoutTransientFunction(destinationWithoutTransientFunction) { // Intentionally left empty. } @@ -2097,8 +2116,8 @@ namespace storm { return mHighestLevel; } - ValueType value(StateType const& in) const { - return destinationValueFunction(in); + ValueType probability(StateType const& in) const { + return destinationProbabilityFunction(in); } void perform(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}) const { @@ -2120,7 +2139,7 @@ namespace storm { private: int_fast64_t mLowestLevel; int_fast64_t mHighestLevel; - DestinationValueFunctionPtr destinationValueFunction; + DestinationProbabilityFunctionPtr destinationProbabilityFunction; DestinationLevelFunctionPtr destinationLevelFunction; DestinationFunctionPtr destinationFunction; DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction; @@ -2128,17 +2147,18 @@ namespace storm { }; typedef bool (*EdgeEnabledFunctionPtr)(StateType const&, TransientVariables const& transientIn); + typedef ValueType (*EdgeRateFunctionPtr)(StateType const&); typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}); class Edge { public: typedef std::vector ContainerType; - Edge() : edgeEnabledFunction(nullptr), edgeTransientFunction(nullptr) { + Edge() : edgeEnabledFunction(nullptr), edgeRateFunction(nullptr), edgeTransientFunction(nullptr) { // Intentionally left empty. } - Edge(EdgeEnabledFunctionPtr edgeEnabledFunction, EdgeTransientFunctionPtr edgeTransientFunction = nullptr) : edgeEnabledFunction(edgeEnabledFunction), edgeTransientFunction(edgeTransientFunction) { + Edge(EdgeEnabledFunctionPtr edgeEnabledFunction, EdgeRateFunctionPtr edgeRateFunction, EdgeTransientFunctionPtr edgeTransientFunction = nullptr) : edgeEnabledFunction(edgeEnabledFunction), edgeRateFunction(edgeRateFunction), edgeTransientFunction(edgeTransientFunction) { // Intentionally left empty. } @@ -2150,8 +2170,8 @@ namespace storm { destinations.push_back(destination); } - void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, DestinationValueFunctionPtr destinationValueFunction, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) { - destinations.emplace_back(lowestLevel, highestLevel, destinationValueFunction, destinationLevelFunction, destinationFunction, destinationWithoutTransientLevelFunction, destinationWithoutTransientFunction); + void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, DestinationProbabilityFunctionPtr destinationProbabilityFunction, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) { + destinations.emplace_back(lowestLevel, highestLevel, destinationProbabilityFunction, destinationLevelFunction, destinationFunction, destinationWithoutTransientLevelFunction, destinationWithoutTransientFunction); } std::vector const& getDestinations() const { @@ -2166,12 +2186,17 @@ namespace storm { return destinations.end(); } + ValueType rate(StateType const& in) const { + return edgeRateFunction(in); + } + void perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}) const { edgeTransientFunction(in, transientIn, transientOut {% if exploration_checks %}, variableWrites {% endif %}); } private: EdgeEnabledFunctionPtr edgeEnabledFunction; + EdgeRateFunctionPtr edgeRateFunction; EdgeTransientFunctionPtr edgeTransientFunction; ContainerType destinations; }; @@ -2201,14 +2226,14 @@ namespace storm { initialStates.push_back(state); }{% endfor %} {% for edge in nonsynch_edges %}{ - edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name}); - {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, &destination_value_{$edge.name}_{$destination.name}, &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}); + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, &edge_rate_{$edge.name}, edge_perform_{$edge.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, &destination_probability_{$edge.name}_{$destination.name}, &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}, edge_perform_{$edge.name}); - {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, &destination_value_{$edge.name}_{$destination.name}, &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}); + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, &edge_rate_{$edge.name}, edge_perform_{$edge.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, &destination_probability_{$edge.name}_{$destination.name}, &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 %} @@ -2343,6 +2368,9 @@ namespace storm { void exploreNonSynchronizingEdges(StateType const& in, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for edge in nonsynch_edges %}{ +#ifndef NDEBUG + std::cout << "Exploring non-synchronizing edge {$edge.name}." << std::endl; +#endif if ({$edge.guard}) { Choice& choice = behaviour.addChoice(!model_is_deterministic() && !model_is_discrete_time() && {$edge.markovian}); choice.resizeRewards({$edge_destination_rewards_count}); @@ -2358,6 +2386,7 @@ namespace storm { choice.addReward({$reward.index}, transient.{$reward.variable}); {% endfor %} } + auto rate = edge_rate_{$edge.name}(in); {% for destination in edge.destinations %}{ {% if exploration_checks %}VariableWrites variableWrites; {% endif %} @@ -2367,9 +2396,10 @@ namespace storm { TransientVariables transientOut; destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.transient_variables_in_destinations %}, transientIn, transientOut{% endif %}{% if exploration_checks %}, variableWrites{% endif %}); IndexType outStateIndex = getOrAddIndex(out, statesToExplore); - choice.add(outStateIndex, destination_value_{$edge.name}_{$destination.name}(in)); + auto probability = destination_probability_{$edge.name}_{$destination.name}(in); + choice.add(outStateIndex, rate * probability); {% for reward in destination_rewards %} - choice.addReward({$reward.index}, transientOut.{$reward.variable}); + choice.addReward({$reward.index}, probability * transientOut.{$reward.variable}); {% endfor %} } {% endfor %} @@ -2395,9 +2425,6 @@ namespace storm { } else { IndexType newIndex = static_cast(stateIds.size()); stateIds.insert(std::make_pair(state, newIndex)); -#ifndef NDEBUG - std::cout << "inserting state " << state << std::endl; -#endif statesToExplore.add(state); return newIndex; } diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index 7d4f1365a..63509aa44 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -110,7 +110,7 @@ namespace storm { cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex); cpptempl::data_list generateLevels(storm::jani::Automaton const& automaton, uint64_t destinationLocationIndex, storm::jani::OrderedAssignments const& assignments); cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge); - cpptempl::data_map generateDestination(storm::jani::Automaton const& automaton, uint64_t destinationIndex, storm::jani::EdgeDestination const& destination, boost::optional const& rate = boost::none); + cpptempl::data_map generateDestination(storm::jani::Automaton const& automaton, uint64_t destinationIndex, storm::jani::EdgeDestination const& destination); template cpptempl::data_map generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const; cpptempl::data_map generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const; diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index b0bf313be..fc906da6c 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -458,4 +458,4 @@ namespace { } } -} \ No newline at end of file +} diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index f29c88859..ff0e4630d 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -462,10 +462,10 @@ namespace { result.first = storm::api::buildSparseModel(program, result.second)->template as(); } else if (TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) { auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - janiData.first.substituteFunctions(); result.second = storm::api::extractFormulasFromProperties(janiData.second); result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as(); } + return result; } diff --git a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp index db6ca04f9..b04a7cf06 100644 --- a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp @@ -138,7 +138,6 @@ namespace { result.first = storm::api::buildSparseModel(program, result.second)->template as(); } else if (TestType::engine == MaEngine::JaniSparse || TestType::engine == MaEngine::JitSparse) { auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - janiData.first.substituteFunctions(); result.second = storm::api::extractFormulasFromProperties(janiData.second); result.first = storm::api::buildSparseModel(janiData.first, result.second, TestType::engine == MaEngine::JitSparse)->template as(); } @@ -308,4 +307,4 @@ namespace { EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); } -} \ No newline at end of file +}