more precise analysis of whether commands will synchronize

src/storm/generator/PrismNextStateGenerator.cpp

@@ -482,6 +482,9 @@ namespace storm {
                 bool hasOneEnabledCommand = false;
                 for (auto commandIndexIt = commandIndices.begin(), commandIndexIte = commandIndices.end(); commandIndexIt != commandIndexIte; ++commandIndexIt) {
                     storm::prism::Command const& command = module.getCommand(*commandIndexIt);
+                    if (!isCommandPotentiallySynchronizing(command)) {
+                        continue;
+                    }
                     if (commandFilter != CommandFilter::All) {
                         STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter.");
                         if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) {
@@ -546,8 +549,8 @@ namespace storm {
                 for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
                     storm::prism::Command const& command = module.getCommand(j);
 
-                    // Only consider unlabeled commands.
-                    if (command.isLabeled()) continue;
+                    // Only consider commands that are not possibly synchronizing.
+                    if (isCommandPotentiallySynchronizing(command)) continue;
 
                     if (commandFilter != CommandFilter::All) {
                         STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter.");
@@ -607,6 +610,10 @@ namespace storm {
                         choice.addReward(stateActionRewardValue);
                     }
 
+                    if (this->options.isBuildChoiceLabelsSet() && command.isLabeled()) {
+                        choice.addLabel(program.getActionName(command.getActionIndex()));
+                    }
+
                     if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
                         storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i);
                         STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command.");
@@ -838,6 +845,11 @@ namespace storm {
             return std::make_shared<storm::storage::sparse::PrismChoiceOrigins>(std::make_shared<storm::prism::Program>(program), std::move(identifiers), std::move(identifierToCommandSetMapping));
         }
 
+        template<typename ValueType, typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::isCommandPotentiallySynchronizing(const prism::Command &command) const {
+            return program.getPossiblySynchronizingCommands().get(command.getGlobalIndex());
+        }
+
 
         template class PrismNextStateGenerator<double>;
 

src/storm/generator/PrismNextStateGenerator.h

@@ -117,6 +117,8 @@ namespace storm {
              */
             void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> const& iteratorList, storm::builder::jit::Distribution<StateType, ValueType>& distribution, StateToIdCallback stateToIdCallback);
 
+            bool isCommandPotentiallySynchronizing(prism::Command const& command) const;
+
             // The program used for the generation of next states.
             storm::prism::Program program;
 

src/storm/storage/prism/Program.cpp

@@ -146,7 +146,7 @@ namespace storm {
         formulas(formulas), formulaToIndexMap(), players(players), modules(modules), moduleToIndexMap(),
         rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
         labels(labels), labelToIndexMap(), observationLabels(observationLabels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
-        synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility)
+        synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), possiblySynchronizingCommands(), prismCompatibility(prismCompatibility)
         {
 
             // Start by creating the necessary mappings from the given ones.
@@ -163,6 +163,24 @@ namespace storm {
                 }
             }
 
+            possiblySynchronizingCommands = storage::BitVector(this->getNumberOfCommands());
+            std::set<uint64_t> possiblySynchronizingActionIndices;
+            for(uint64_t syncAction : synchronizingActionIndices) {
+                if (getModuleIndicesByActionIndex(syncAction).size() > 1) {
+                    std::cout << "syncAction " << syncAction << std::endl;
+                    possiblySynchronizingActionIndices.insert(syncAction);
+                }
+            }
+            for (auto const& module : getModules()) {
+                for (auto const& command : module.getCommands()) {
+                    if (command.isLabeled()) {
+                        if (possiblySynchronizingActionIndices.count(command.getActionIndex())) {
+                            possiblySynchronizingCommands.set(command.getGlobalIndex());
+                        }
+                    }
+                }
+            }
+
             if (finalModel) {
                 // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
                 // commands and issue a warning.
@@ -816,6 +834,10 @@ namespace storm {
             return this->observationLabels.size();
         }
 
+        storm::storage::BitVector const& Program::getPossiblySynchronizingCommands() const {
+            return possiblySynchronizingCommands;
+        }
+
         Program Program::restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const {
             std::vector<storm::prism::Module> newModules;
             newModules.reserve(this->getNumberOfModules());

src/storm/storage/prism/Program.h

@@ -6,6 +6,7 @@
 #include <vector>
 #include <set>
 #include <boost/optional.hpp>
+#include <storm/storage/BitVector.h>
 
 #include "storm/storage/prism/Constant.h"
 #include "storm/storage/prism/Formula.h"
@@ -729,6 +730,8 @@ namespace storm {
              */
             std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal = true, std::string suffix = "") const;
 
+            storm::storage::BitVector const& getPossiblySynchronizingCommands() const;
+
         private:
             /*!
              * This function builds a command that corresponds to the synchronization of the given list of commands.
@@ -831,6 +834,8 @@ namespace storm {
             // A mapping from variable names to the modules in which they were declared.
             std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
 
+            storage::BitVector possiblySynchronizingCommands;
+
             bool prismCompatibility;
         };