From 141316943cd6ccda9a7787c2524967c37841a579 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Feb 2020 09:06:12 +0100 Subject: [PATCH] DdJaniModelBuilder: Also apply max. progress if the system consists of just a single automaton. --- src/storm/builder/DdJaniModelBuilder.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 2175dd2e1..0df1fa029 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -887,7 +887,7 @@ namespace storm { inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName)); } - return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast(data), inputEnabledActionIndices); + return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast(data), inputEnabledActionIndices, data.empty()); } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { @@ -1707,10 +1707,13 @@ namespace storm { } } - AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set const& inputEnabledActionIndices) { + AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set const& inputEnabledActionIndices, bool isTopLevelAutomaton) { STORM_LOG_TRACE("Building DD for automaton '" << automatonName << "'."); AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); + // Disjunction of all guards of non-markovian actions (only required for maximum progress assumption). + storm::dd::Bdd nonMarkovianActionGuards = this->variables.manager->getBddZero(); + storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); for (auto const& actionInstantiation : actionInstantiations) { uint64_t actionIndex = actionInstantiation.first; @@ -1727,12 +1730,20 @@ namespace storm { if (inputEnabled) { actionDd.setIsInputEnabled(); } + if (applyMaximumProgress && isTopLevelAutomaton && !instantiation.isMarkovian()) { + nonMarkovianActionGuards |= actionDd.guard; + } STORM_LOG_TRACE("Used local nondeterminism variables are " << actionDd.getLowestLocalNondeterminismVariable() << " to " << actionDd.getHighestLocalNondeterminismVariable() << "."); result.actions[ActionIdentification(actionIndex, instantiation.synchronizationVectorIndex, instantiation.isMarkovian())] = actionDd; result.extendLocalNondeterminismVariables(actionDd.getLocalNondeterminismVariables()); } } + if (applyMaximumProgress && isTopLevelAutomaton) { + ActionIdentification silentMarkovianActionIdentification(storm::jani::Model::SILENT_ACTION_INDEX, true); + result.actions[silentMarkovianActionIdentification].conjunctGuardWith(!nonMarkovianActionGuards); + } + for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) { auto const& location = automaton.getLocation(locationIndex); performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) {