diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index bf4725841..db0f5d91b 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -10,6 +10,7 @@ #include "src/storage/jani/RenameComposition.h" #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" +#include "src/storage/jani/CompositionActionInformationVisitor.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" @@ -172,7 +173,7 @@ namespace storm { template class CompositionVariableCreator : public storm::jani::CompositionVisitor { public: - CompositionVariableCreator(storm::jani::Model const& model) : model(model), automata() { + CompositionVariableCreator(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) { // Intentionally left empty. } @@ -180,7 +181,7 @@ namespace storm { // First, check whether every automaton appears exactly once in the system composition. Simultaneously, // we determine the set of non-silent actions used by the composition. automata.clear(); - nonSilentActions = boost::any_cast>(this->model.getSystemComposition().accept(*this, boost::none)); + this->model.getSystemComposition().accept(*this, boost::none); STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata."); // Then, check that the model does not contain unbounded integer or non-transient real variables. @@ -194,78 +195,38 @@ namespace storm { } // Based on this assumption, we create the variables. - return createVariables(nonSilentActions); + return createVariables(); } boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { auto it = automata.find(composition.getAutomatonName()); STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times."); automata.insert(it, composition.getAutomatonName()); - - // Compute the set of actions used by this automaton. - std::set actionIndices = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices(); - std::set result; - for (auto const& index : actionIndices) { - result.insert(this->model.getAction(index).getName()); - } - return result; + return boost::none; } boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - std::set usedActions = boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); - - std::set newUsedActions; - for (auto const& action : usedActions) { - auto it = composition.getRenaming().find(action); - if (it != composition.getRenaming().end()) { - if (it->second) { - newUsedActions.insert(it->second.get()); - } - } else { - newUsedActions.insert(action); - } - } - - return newUsedActions; + boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); + return boost::none; } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - std::vector> subresults; for (auto const& subcomposition : composition.getSubcompositions()) { - subresults.push_back(boost::any_cast>(subcomposition->accept(*this, boost::none))); - } - - // Determine all actions that do not take part in synchronization vectors. - std::set result; - for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) { - std::set actionsInSynch; - for (auto const& synchVector : composition.getSynchronizationVectors()) { - actionsInSynch.insert(synchVector.getInput()[subresultIndex]); - } - - std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin())); + subcomposition->accept(*this, boost::none); } - - // Now add all outputs of synchronization vectors. - for (auto const& synchVector : composition.getSynchronizationVectors()) { - result.insert(synchVector.getOutput()); - } - - return result; + return boost::none; } private: CompositionVariables createVariables() { CompositionVariables result; - for (auto const& action : this->model.getActions()) { - if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) { - std::pair variablePair = result.manager->addMetaVariable(action.getName()); - result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first; - result.allNondeterminismVariables.insert(variablePair.first); - } + for (auto const& nonSilentActionIndex : actionInformation.getNonSilentActionIndices()) { + std::pair variablePair = result.manager->addMetaVariable(actionInformation.getActionName(nonSilentActionIndex)); + result.actionVariablesMap[nonSilentActionIndex] = variablePair.first; + result.allNondeterminismVariables.insert(variablePair.first); } - + // FIXME: check how many nondeterminism variables we should actually allocate. uint64_t numberOfNondeterminismVariables = this->model.getNumberOfAutomata(); for (auto const& automaton : this->model.getAutomata()) { @@ -390,7 +351,7 @@ namespace storm { storm::jani::Model const& model; std::set automata; - std::set nonSilentActions; + storm::jani::ActionInformation actionInformation; }; template @@ -1055,29 +1016,29 @@ namespace storm { // The identity of the automaton's variables. storm::dd::Add identity; - // The local nondeterminism variables used by this action DD, given as the lowest + // The local nondeterminism variables used by this action DD, given as the lowest and highest variable index. std::pair localNondeterminismVariables; }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionToIndex(model.getActionToIndexMap()) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { // Intentionally left empty. } - std::unordered_map actionToIndex; + storm::jani::ActionInformation const& actionInformation; ComposerResult compose() override { - std::map actionIndexToLocalNondeterminismVariableOffset; - for (auto const& action : this->model.getActions()) { - actionIndexToLocalNondeterminismVariableOffset[this->model.getActionIndex(action.getName())] = 0; + std::map actionIndexToLocalNondeterminismVariableOffset; + for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { + actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; } - + AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); return buildSystemFromAutomaton(globalAutomaton); } boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset); } @@ -1085,12 +1046,12 @@ namespace storm { // Build a mapping from indices to indices for the renaming. std::map renamingIndexToIndex; for (auto const& entry : composition.getRenaming()) { - if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { + if (actionInformation.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { // Distinguish the cases where we hide the action or properly rename it. if (entry.second) { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get())); + renamingIndexToIndex.emplace(actionInformation.getActionIndex(entry.first), actionInformation.getActionIndex(entry.second.get())); } else { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); + renamingIndexToIndex.emplace(actionInformation.getActionIndex(entry.first), this->model.getSilentActionIndex()); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); @@ -1098,9 +1059,10 @@ namespace storm { } // Prepare the new offset mapping. - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); - std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; for (auto const& indexPair : renamingIndexToIndex) { + // FIXME: Check correct? Introduce zero if not contained? auto it = actionIndexToLocalNondeterminismVariableOffset.find(indexPair.second); STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << "."); newSynchronizingActionToOffsetMap[indexPair.first] = it->second; @@ -1114,38 +1076,52 @@ namespace storm { } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - // Build the set of synchronizing action indices. - std::set synchronizingActionIndices; - for (auto const& entry : composition.getSynchronizationAlphabet()) { - if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) { - synchronizingActionIndices.insert(this->model.getActionIndex(entry)); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action."); - } - } - - // Then translate the left subcomposition. - AutomatonDd left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); - - // Prepare the new offset mapping. std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); - std::map newActionIndexToLocalNondeterminismVariableOffset = actionIndexToLocalNondeterminismVariableOffset; - for (auto const& actionIndex : synchronizingActionIndices) { - auto it = left.actionIndexToAction.find(actionIndex); - if (it != left.actionIndexToAction.end()) { - newActionIndexToLocalNondeterminismVariableOffset[actionIndex] = it->second.getHighestLocalNondeterminismVariable(); + + std::vector subautomata; + for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) { + // Prepare the new offset mapping. + std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + if (subcompositionIndex == 0) { + for (auto const& synchVector : composition.getSynchronizationVectors()) { + auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput())); + STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << "."); + newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second; + } + } else { + AutomatonDd const& previousAutomatonDd = subautomata.back(); + + // Based on the previous results, we need to update the offsets. + for (auto const& synchVector : composition.getSynchronizationVectors()) { + auto it = previousAutomatonDd.actionIndexToAction.find(actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex - 1))); + if (it != previousAutomatonDd.actionIndexToAction.end()) { + newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex))] = it->second.getHighestLocalNondeterminismVariable(); + } else { + STORM_LOG_ASSERT(false, "Subcomposition does not have action that is mentioned in parallel composition."); + } + } } + + // Build the DD for the next element of the composition wrt. to the current offset mapping. + subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap))); } - // Then translate the right subcomposition. - AutomatonDd right = boost::any_cast(composition.getRightSubcomposition().accept(*this, newActionIndexToLocalNondeterminismVariableOffset)); - - return composeInParallel(left, right, synchronizingActionIndices); + return composeInParallel(subautomata, composition.getSynchronizationVectors()); } private: - AutomatonDd composeInParallel(AutomatonDd const& automaton1, AutomatonDd const& automaton2, std::set const& synchronizingActionIndices) { - AutomatonDd result(automaton1); + AutomatonDd composeInParallel(std::vector const& subautomata, std::vector const& synchronizationVectors) { + AutomatonDd result(this->variables.manager->template getAddOne()); + + for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { + AutomatonDd const& subautomaton = subautomata[automatonIndex]; + + // Construct combined identity. + result.identity *= subautomaton.identity; + + addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments); + } + result.transientLocationAssignments = joinTransientAssignmentMaps(automaton1.transientLocationAssignments, automaton2.transientLocationAssignments); // Treat all actions of the first automaton. @@ -1958,16 +1934,19 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << "."); } + // Determine the actions that will appear in the parallel composition. + storm::jani::CompositionActionInformationVisitor actionInformationVisitor(model); + storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation(); + // Create all necessary variables. - CompositionVariableCreator variableCreator(model); + CompositionVariableCreator variableCreator(model, actionInformation); CompositionVariables variables = variableCreator.create(); // Determine which transient assignments need to be considered in the building process. std::vector rewardVariables = selectRewardVariables(model, options); // Create a builder to compose and build the model. -// SeparateEdgesSystemComposer composer(model, variables); - CombinedEdgesSystemComposer composer(model, variables, rewardVariables); + CombinedEdgesSystemComposer composer(model, actionInformation, variables, rewardVariables); ComposerResult system = composer.compose(); // Postprocess the variables in place. @@ -2013,4 +1992,4 @@ namespace storm { template class DdJaniModelBuilder; template class DdJaniModelBuilder; } -} \ No newline at end of file +} diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp new file mode 100644 index 000000000..ad8812648 --- /dev/null +++ b/src/storage/jani/CompositionActionInformationVisitor.cpp @@ -0,0 +1,133 @@ +#include "src/storage/jani/CompositionActionInformationVisitor.h" + +#include "src/storage/jani/Model.h" +#include "src/storage/jani/Compositions.h" + +namespace storm { + namespace jani { + + ActionInformation::ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap) : nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) { + // Intentionally left empty. + } + + std::string const& ActionInformation::getActionName(uint64_t index) const { + return indexToNameMap.at(index); + } + + uint64_t ActionInformation::getActionIndex(std::string const& name) const { + return nameToIndexMap.at(name); + } + + std::set const& ActionInformation::getNonSilentActionIndices() const { + return nonsilentActionIndices; + } + + CompositionActionInformationVisitor::CompositionActionInformationVisitor(storm::jani::Model const& model) : model(model), nextFreeActionIndex(0), nameToIndexMap(), indexToNameMap() { + // Intentionally left empty. + } + + ActionInformation CompositionActionInformationVisitor::getActionInformation() { + indexToNameMap.clear(); + nameToIndexMap.clear(); + + // Determine the next free index we can give out to a new action. + for (auto const& action : model.getActions()) { + nextFreeActionIndex = std::max(nextFreeActionIndex, model.getActionIndex(action.getName())); + } + ++nextFreeActionIndex; + + std::set nonSilentActionIndices = boost::any_cast>(model.getSystemComposition().accept(*this, boost::none)); + + return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap); + } + + boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { + return model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices(); + } + + boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { + std::set usedActions = boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); + + std::set newUsedActions; + for (auto const& index : usedActions) { + auto renamingIt = composition.getRenaming().find(indexToNameMap.at(index)); + if (renamingIt != composition.getRenaming().end()) { + if (renamingIt->second) { + newUsedActions.insert(addOrGetActionIndex(renamingIt->second.get())); + + auto actionIndexIt = nameToIndexMap.find(renamingIt->second.get()); + if (actionIndexIt != nameToIndexMap.end()) { + newUsedActions.insert(actionIndexIt->second); + } else { + nameToIndexMap[renamingIt->second.get()] = nextFreeActionIndex; + indexToNameMap[nextFreeActionIndex] = renamingIt->second.get(); + ++nextFreeActionIndex; + } + } + } else { + newUsedActions.insert(index); + } + } + + return newUsedActions; + } + + boost::any CompositionActionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { + std::vector> subresults; + for (auto const& subcomposition : composition.getSubcompositions()) { + subresults.push_back(boost::any_cast>(subcomposition->accept(*this, boost::none))); + } + + std::set effectiveSynchronizationVectors; + for (uint64_t index = 0; index < composition.getNumberOfSynchronizationVectors(); ++index) { + effectiveSynchronizationVectors.insert(index); + } + + // Determine all actions that do not take part in synchronization vectors. + std::set result; + for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) { + + std::set actionsInSynch; + std::set localEffectiveSynchVectors; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); + uint64_t synchVectorActionIndex = nameToIndexMap.at(synchVector.getInput(subresultIndex)); + actionsInSynch.insert(synchVectorActionIndex); + + // If the action of they synchronization vector at this position is one that is actually contained + // in the corresponding subcomposition, the synchronization vector is effective. + if (subresults[subresultIndex].find(synchVectorActionIndex) != subresults[subresultIndex].end()) { + effectiveSynchronizationVectors.insert(synchVectorIndex); + } + } + + std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin())); + + // Intersect the previously effective synchronization vectors with the ones that were derived to be + // effective for the current subcomposition. + std::set newEffectiveSynchVectors; + std::set_intersection(effectiveSynchronizationVectors.begin(), effectiveSynchronizationVectors.end(), newEffectiveSynchVectors.begin(), newEffectiveSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); + effectiveSynchronizationVectors = std::move(newEffectiveSynchVectors); + } + + // Now add all outputs of synchronization vectors. + for (auto const& synchVector : composition.getSynchronizationVectors()) { + result.insert(addOrGetActionIndex(synchVector.getOutput())); + } + + return result; + } + + uint64_t CompositionActionInformationVisitor::addOrGetActionIndex(std::string const& name) { + auto it = nameToIndexMap.find(name); + if (it != nameToIndexMap.end()) { + return it->second; + } else { + nameToIndexMap[name] = nextFreeActionIndex; + indexToNameMap[nextFreeActionIndex] = name; + return nextFreeActionIndex++; + } + } + + } +} diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h new file mode 100644 index 000000000..93017b8a1 --- /dev/null +++ b/src/storage/jani/CompositionActionInformationVisitor.h @@ -0,0 +1,48 @@ +#pragma once + +#include +#include + +#include "src/storage/jani/CompositionVisitor.h" + +namespace storm { + namespace jani { + + class Model; + + class ActionInformation { + public: + ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap); + + std::string const& getActionName(uint64_t index) const; + uint64_t getActionIndex(std::string const& name) const; + std::set const& getNonSilentActionIndices() const; + + private: + std::set nonsilentActionIndices; + std::map indexToNameMap; + std::map nameToIndexMap; + }; + + class CompositionActionInformationVisitor : public CompositionVisitor { + public: + CompositionActionInformationVisitor(storm::jani::Model const& model); + + ActionInformation getActionInformation(); + + virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override; + virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override; + virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override; + + private: + uint64_t addOrGetActionIndex(std::string const& name); + + storm::jani::Model const& model; + uint64_t nextFreeActionIndex; + std::map nameToIndexMap; + std::map indexToNameMap; + }; + + + } +}