From d144a1776c182df3170958093bcde789ce5a9bf2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 11 Jun 2021 13:53:42 -0700 Subject: [PATCH] prism next state generator, rename actions to reflect labeled choices vs unlabeled choices are sync vs async --- src/storm/generator/PrismNextStateGenerator.cpp | 16 ++++++++-------- src/storm/generator/PrismNextStateGenerator.h | 13 +++++++------ src/storm/storage/prism/Program.h | 10 ++++++++-- 3 files changed, 23 insertions(+), 16 deletions(-) diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 26c9bf673..a9c845d32 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -296,16 +296,16 @@ namespace storm { std::vector> allChoices; if (this->getOptions().isApplyMaximalProgressAssumptionSet()) { // First explore only edges without a rate - allChoices = getUnlabeledChoices(*this->state, stateToIdCallback, CommandFilter::Probabilistic); - addLabeledChoices(allChoices, *this->state, stateToIdCallback, CommandFilter::Probabilistic); + allChoices = getAsynchronousChoices(*this->state, stateToIdCallback, CommandFilter::Probabilistic); + addSynchronousChoices(allChoices, *this->state, stateToIdCallback, CommandFilter::Probabilistic); if (allChoices.empty()) { // Expand the Markovian edges if there are no probabilistic ones. - allChoices = getUnlabeledChoices(*this->state, stateToIdCallback, CommandFilter::Markovian); - addLabeledChoices(allChoices, *this->state, stateToIdCallback, CommandFilter::Markovian); + allChoices = getAsynchronousChoices(*this->state, stateToIdCallback, CommandFilter::Markovian); + addSynchronousChoices(allChoices, *this->state, stateToIdCallback, CommandFilter::Markovian); } } else { - allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); - addLabeledChoices(allChoices, *this->state, stateToIdCallback); + allChoices = getAsynchronousChoices(*this->state, stateToIdCallback); + addSynchronousChoices(allChoices, *this->state, stateToIdCallback); } std::size_t totalNumberOfChoices = allChoices.size(); @@ -538,7 +538,7 @@ namespace storm { } template - std::vector> PrismNextStateGenerator::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { + std::vector> PrismNextStateGenerator::getAsynchronousChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { std::vector> result; // Iterate over all modules. @@ -650,7 +650,7 @@ namespace storm { } template - void PrismNextStateGenerator::addLabeledChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { + void PrismNextStateGenerator::addSynchronousChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { if (this->actionMask != nullptr) { diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index a053e4488..a83d0bc31 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -86,21 +86,22 @@ namespace storm { boost::optional>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter = CommandFilter::All); /*! - * Retrieves all unlabeled choices possible from the given state. + * Retrieves all choices that are definitively asynchronous, possible from the given state. * * @param state The state for which to retrieve the unlabeled choices. - * @return The unlabeled choices of the state. + * @return The asynchronous choices of the state. */ - std::vector> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); + std::vector> getAsynchronousChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); /*! - * Retrieves all labeled choices possible from the given state. + * Retrieves all (potentially) synchronous choices possible from the given state. + * Note that these may include choices that run asynchronously for this state. * * @param choices The new choices are inserted in this vector * @param state The state for which to retrieve the unlabeled choices. - * @return The labeled choices of the state. + * @return The synchronous choices of the state. */ - void addLabeledChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); + void addSynchronousChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); /*! * Extend the Json struct with additional information about the state. diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index afca86cb4..1c090107b 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -708,8 +708,14 @@ namespace storm { */ Program flattenModules(std::shared_ptr const& smtSolverFactory = std::shared_ptr(new storm::utility::solver::SmtSolverFactory())) const; - - Program labelUnlabelledCommands(std::map const& nameSuggestions) const; + /*! + * Give commands that do not have an action name an action, + * which can be helpful for debugging and understanding traces. + * + * @param nameSuggestions Optional suggestions that map command indices to names + * @return + */ + Program labelUnlabelledCommands(std::map const& nameSuggestions = {}) const; friend std::ostream& operator<<(std::ostream& stream, Program const& program);