From ce5ca9d1ced4ecfdc5b77ce00ecc05c914c81164 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 13 Sep 2016 11:44:08 +0200 Subject: [PATCH 01/11] added proper action reward handling to JANI next-state generator Former-commit-id: cd554d6e127faf12c368dea1e5e2a2999bba5f51 [formerly 47dfb5a7967fb88c345851604e8a8974f0b1e09e] Former-commit-id: 67a31637c5b2d1c36afec11b017bd46a2794b38c --- src/builder/ExplicitModelBuilder.cpp | 4 +-- src/generator/Choice.cpp | 35 +++++++++++++---------- src/generator/Choice.h | 19 +++++++----- src/generator/JaniNextStateGenerator.cpp | 33 ++++++++++++++++++--- src/generator/JaniNextStateGenerator.h | 3 ++ src/generator/PrismNextStateGenerator.cpp | 12 ++++---- 6 files changed, 72 insertions(+), 34 deletions(-) diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index 5faf386e5..8d2164f9f 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -274,7 +274,7 @@ namespace storm { for (auto const& choice : behavior) { // Add command labels if requested. if (generator->getOptions().isBuildChoiceLabelsSet()) { - choiceLabels.get().push_back(choice.getChoiceLabels()); + choiceLabels.get().push_back(choice.getLabels()); } // If we keep track of the Markovian choices, store whether the current one is Markovian. @@ -289,7 +289,7 @@ namespace storm { } // Add the rewards to the reward models. - auto choiceRewardIt = choice.getChoiceRewards().begin(); + auto choiceRewardIt = choice.getRewards().begin(); for (auto& rewardModelBuilder : rewardModelBuilders) { if (rewardModelBuilder.hasStateActionRewards()) { rewardModelBuilder.addStateActionReward(*choiceRewardIt); diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp index 7f91a4b4d..4337fffd4 100644 --- a/src/generator/Choice.cpp +++ b/src/generator/Choice.cpp @@ -8,7 +8,7 @@ namespace storm { namespace generator { template - Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), choiceRewards() { + Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), rewards(), labels() { // Intentionally left empty. } @@ -33,24 +33,24 @@ namespace storm { } template - void Choice::addChoiceLabel(uint_fast64_t label) { - if (!choiceLabels) { - choiceLabels = LabelSet(); + void Choice::addLabel(uint_fast64_t label) { + if (!labels) { + labels = LabelSet(); } - choiceLabels->insert(label); + labels->insert(label); } template - void Choice::addChoiceLabels(LabelSet const& labelSet) { - if (!choiceLabels) { - choiceLabels = LabelSet(); + void Choice::addLabels(LabelSet const& labelSet) { + if (!labels) { + labels = LabelSet(); } - choiceLabels->insert(labelSet.begin(), labelSet.end()); + labels->insert(labelSet.begin(), labelSet.end()); } template - boost::container::flat_set const& Choice::getChoiceLabels() const { - return *choiceLabels; + boost::container::flat_set const& Choice::getLabels() const { + return *labels; } template @@ -70,13 +70,18 @@ namespace storm { } template - void Choice::addChoiceReward(ValueType const& value) { - choiceRewards.push_back(value); + void Choice::addReward(ValueType const& value) { + rewards.push_back(value); } template - std::vector const& Choice::getChoiceRewards() const { - return choiceRewards; + void Choice::addRewards(std::vector&& values) { + this->rewards = std::move(values); + } + + template + std::vector const& Choice::getRewards() const { + return rewards; } template diff --git a/src/generator/Choice.h b/src/generator/Choice.h index 76b6c8d16..bd20af0f0 100644 --- a/src/generator/Choice.h +++ b/src/generator/Choice.h @@ -66,21 +66,21 @@ namespace storm { * * @param label The label to associate with this choice. */ - void addChoiceLabel(uint_fast64_t label); + void addLabel(uint_fast64_t label); /*! * Adds the given label set to the labels associated with this choice. * * @param labelSet The label set to associate with this choice. */ - void addChoiceLabels(LabelSet const& labelSet); + void addLabels(LabelSet const& labelSet); /*! * Retrieves the set of labels associated with this choice. * * @return The set of labels associated with this choice. */ - LabelSet const& getChoiceLabels() const; + LabelSet const& getLabels() const; /*! * Retrieves the index of the action of this choice. @@ -104,12 +104,17 @@ namespace storm { /*! * Adds the given value to the reward associated with this choice. */ - void addChoiceReward(ValueType const& value); + void addReward(ValueType const& value); + + /*! + * Adds the given choices rewards to this choice. + */ + void addRewards(std::vector&& values); /*! * Retrieves the rewards for this choice under selected reward models. */ - std::vector const& getChoiceRewards() const; + std::vector const& getRewards() const; /*! * Retrieves whether the choice is Markovian. @@ -135,10 +140,10 @@ namespace storm { ValueType totalMass; // The reward values associated with this choice. - std::vector choiceRewards; + std::vector rewards; // The labels that are associated with this choice. - boost::optional choiceLabels; + boost::optional labels; }; template diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 5b5f54151..0df974f3b 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -22,7 +22,7 @@ namespace storm { } template - JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables() { + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables(), hasStateActionRewards(false) { STORM_LOG_THROW(model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); @@ -282,6 +282,10 @@ namespace storm { if (this->isDeterministicModel() && totalNumberOfChoices > 1) { Choice globalChoice; + // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs + // this is equal to the number of choices, which is why we initialize it like this here. + ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast(totalNumberOfChoices) : storm::utility::zero(); + // Iterate over all choices and combine the probabilities/rates into one choice. for (auto const& choice : allChoices) { for (auto const& stateProbabilityPair : choice) { @@ -292,11 +296,23 @@ namespace storm { } } + if (hasStateActionRewards && !this->isDiscreteTimeModel()) { + totalExitRate += choice.getTotalMass(); + } + if (this->options.isBuildChoiceLabelsSet()) { - globalChoice.addChoiceLabels(choice.getChoiceLabels()); + globalChoice.addLabels(choice.getLabels()); } } - + + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); + for (auto const& choice : allChoices) { + for (uint_fast64_t rewardVariableIndex = 0; rewardVariableIndex < rewardVariables.size(); ++rewardVariableIndex) { + stateActionRewards[rewardVariableIndex] += choice.getRewards()[rewardVariableIndex] * choice.getTotalMass() / totalExitRate; + } + } + globalChoice.addRewards(std::move(stateActionRewards)); + // Move the newly fused choice in place. allChoices.clear(); allChoices.push_back(std::move(globalChoice)); @@ -349,7 +365,7 @@ namespace storm { } // Create the state-action reward for the newly created choice. - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addChoiceReward(value); } ); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } ); // Check that the resulting distribution is in fact a distribution. STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); @@ -385,6 +401,7 @@ namespace storm { while (!done) { boost::container::flat_map* currentTargetStates = new boost::container::flat_map(); boost::container::flat_map* newTargetStates = new boost::container::flat_map(); + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); currentTargetStates->emplace(state, storm::utility::one()); @@ -405,6 +422,10 @@ namespace storm { newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability())); } } + + // Create the state-action reward for the newly created choice. + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } // If there is one more command to come, shift the target states one time step back. @@ -423,6 +444,9 @@ namespace storm { // Now create the actual distribution. Choice& choice = result.back(); + // Add the rewards to the choice. + choice.addRewards(std::move(stateActionRewards)); + // Add the probabilities/rates to the newly created choice. ValueType probabilitySum = storm::utility::zero(); for (auto const& stateProbabilityPair : *newTargetStates) { @@ -601,6 +625,7 @@ namespace storm { } if (*rewardVariableIt == assignment.getExpressionVariable()) { rewardModelInformation[std::distance(rewardVariables.begin(), rewardVariableIt)].setHasStateActionRewards(); + hasStateActionRewards = true; ++rewardVariableIt; } } diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index d9932f60a..d0b5707a6 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -108,6 +108,9 @@ namespace storm { /// A vector storing information about the corresponding reward models (variables). std::vector rewardModelInformation; + + // A flag that stores whether at least one of the selected reward models has state-action rewards. + bool hasStateActionRewards; }; } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 1ecbec2ab..6c24cd00b 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -242,7 +242,7 @@ namespace storm { } if (this->options.isBuildChoiceLabelsSet()) { - globalChoice.addChoiceLabels(choice.getChoiceLabels()); + globalChoice.addLabels(choice.getLabels()); } } @@ -259,7 +259,7 @@ namespace storm { } } - globalChoice.addChoiceReward(stateActionRewardValue); + globalChoice.addReward(stateActionRewardValue); } // Move the newly fused choice in place. @@ -382,7 +382,7 @@ namespace storm { // Remember the command labels only if we were asked to. if (this->options.isBuildChoiceLabelsSet()) { - choice.addChoiceLabel(command.getGlobalIndex()); + choice.addLabel(command.getGlobalIndex()); } // Iterate over all updates of the current command. @@ -410,7 +410,7 @@ namespace storm { } } } - choice.addChoiceReward(stateActionRewardValue); + choice.addReward(stateActionRewardValue); } // Check that the resulting distribution is in fact a distribution. @@ -486,7 +486,7 @@ namespace storm { if (this->options.isBuildChoiceLabelsSet()) { // Add the labels of all commands to this choice. for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); + choice.addLabel(iteratorList[i]->get().getGlobalIndex()); } } @@ -511,7 +511,7 @@ namespace storm { } } } - choice.addChoiceReward(stateActionRewardValue); + choice.addReward(stateActionRewardValue); } // Dispose of the temporary maps. From 24e89ecce6cd5b3003a47ef7e762b157f62d7530 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 13 Sep 2016 11:48:18 +0200 Subject: [PATCH 02/11] properly scaling state-action rewards for DTMCs in JANI model now Former-commit-id: a70c5c3c6e458243396887dc0073a071f2e9ed40 [formerly 8d2a346735a5d0a7a4e5679dad54205d4cea9bfa] Former-commit-id: cad11b1b3f60945b7c636ed298d273460d63ed61 --- src/builder/DdJaniModelBuilder.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 5ab18683b..94df8a2f9 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1752,7 +1752,13 @@ namespace storm { storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { - system.transitions = system.transitions / system.transitions.sumAbstract(variables.columnMetaVariables); + storm::dd::Add stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables); + system.transitions = system.transitions / stateToNumberOfChoices; + + // Scale all state-action rewards. + for (auto& entry : system.transientEdgeAssignments) { + entry.second = entry.second / stateToNumberOfChoices; + } } // If we were asked to treat some states as terminal states, we cut away their transitions now. From f616bf606b4cd800216b1a2c16398c9db7f9cdbf Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 13 Sep 2016 22:35:39 +0200 Subject: [PATCH 03/11] adapted JANI parallel composition class to synchronization vector usage Former-commit-id: 71322c70f0ae525ff3fc11e28b6f692f70b1c1bc [formerly ec71a5adc543cb46f6f9f8b881610e2c7f4f248f] Former-commit-id: ccdb40b1f3758c82c2cec6ae033ade357c04215d --- src/builder/DdJaniModelBuilder.cpp | 921 +++++++++--------- src/storage/jani/Automaton.cpp | 8 + src/storage/jani/Automaton.h | 5 + .../jani/CompositionInformationVisitor.cpp | 77 +- .../jani/CompositionInformationVisitor.h | 10 +- src/storage/jani/Model.cpp | 6 +- src/storage/jani/Model.h | 5 + src/storage/jani/ParallelComposition.cpp | 116 ++- src/storage/jani/ParallelComposition.h | 78 +- src/storage/prism/ToJaniConverter.cpp | 2 +- 10 files changed, 736 insertions(+), 492 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 94df8a2f9..bf4725841 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -172,14 +172,15 @@ namespace storm { template class CompositionVariableCreator : public storm::jani::CompositionVisitor { public: - CompositionVariableCreator(storm::jani::Model const& model) : model(model) { + CompositionVariableCreator(storm::jani::Model const& model) : model(model), automata() { // Intentionally left empty. } CompositionVariables create() { - // First, check whether every automaton appears exactly once in the system composition. + // 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(); - this->model.getSystemComposition().accept(*this, boost::none); + nonSilentActions = boost::any_cast>(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. @@ -193,25 +194,64 @@ namespace storm { } // Based on this assumption, we create the variables. - return createVariables(); + return createVariables(nonSilentActions); } 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()); - return boost::none; + + // 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; } boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - composition.getSubcomposition().accept(*this, boost::none); - return boost::none; + 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 visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - composition.getLeftSubcomposition().accept(*this, boost::none); - composition.getRightSubcomposition().accept(*this, boost::none); - return boost::none; + 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())); + } + + // Now add all outputs of synchronization vectors. + for (auto const& synchVector : composition.getSynchronizationVectors()) { + result.insert(synchVector.getOutput()); + } + + return result; } private: @@ -350,6 +390,7 @@ namespace storm { storm::jani::Model const& model; std::set automata; + std::set nonSilentActions; }; template @@ -488,434 +529,434 @@ namespace storm { return result; } - template - class SeparateEdgesSystemComposer : public SystemComposer { - public: - // This structure represents an edge. - struct EdgeDd { - EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { - // Intentionally left empty. - } - - EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { - // Intentionally left empty. - } - - EdgeDd& operator=(EdgeDd const& other) { - if (this != &other) { - globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes; - writtenGlobalVariables = other.writtenGlobalVariables; - guard = other.guard; - transitions = other.transitions; - } - return *this; - } - - storm::dd::Add guard; - storm::dd::Add transitions; - std::set writtenGlobalVariables; - std::set globalVariablesWrittenMultipleTimes; - }; - - // This structure represents a subcomponent of a composition. - struct AutomatonDd { - AutomatonDd(storm::dd::Add const& identity) : identity(identity) { - // Intentionally left empty. - } - - std::map> actionIndexToEdges; - storm::dd::Add identity; - }; - - SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { - // Intentionally left empty. - } - - ComposerResult compose() override { - AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); - return buildSystemFromAutomaton(globalAutomaton); - } - - boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - return buildAutomatonDd(composition.getAutomatonName()); - } - - boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); - - // 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()) { - // 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())); - } else { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); - } - } - - // Finally, apply the renaming. - AutomatonDd result(subautomaton.identity); - for (auto const& actionEdges : subautomaton.actionIndexToEdges) { - auto it = renamingIndexToIndex.find(actionEdges.first); - if (it != renamingIndexToIndex.end()) { - // If we are to rename the action, do so. - result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end()); - } else { - // Otherwise copy over the edges. - result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end()); - } - } - return result; - } - - boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - AutomatonDd leftSubautomaton = boost::any_cast(composition.getLeftSubcomposition().accept(*this, boost::none)); - AutomatonDd rightSubautomaton = boost::any_cast(composition.getRightSubcomposition().accept(*this, boost::none)); - - // 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."); - } - } - - // Perform the composition. - - // First, consider all actions in the left subcomposition. - AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); - uint64_t index = 0; - for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { - // If we need to synchronize over this action, do so now. - if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { - auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first); - if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { - for (auto const& edge1 : actionEdges.second) { - for (auto const& edge2 : rightIt->second) { - EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); - if (!edgeDd.guard.isZero()) { - result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); - } - index++; - } - } - } - } else { - // Extend all edges by the missing identity (unsynchronizing) and copy them over. - for (auto const& edge : actionEdges.second) { - result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity)); - } - } - } - - // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because - // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none, - // such transitions can not be taken and we can drop them. - for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) { - if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) { - for (auto const& edge : actionEdges.second) { - result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity)); - } - } - } - - return result; - } - - private: - storm::dd::Add combineEdgesBySummation(std::vector const& edges, CompositionVariables const& variables) { - storm::dd::Add result = variables.manager->template getAddZero(); - for (auto const& edge : edges) { - // Simply add all actions, but make sure to include the missing global variable identities. - result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables); - } - return result; - } - - std::pair> combineEdgesByNondeterministicChoice(std::vector& edges) { - // Complete all edges by adding the missing global variable identities. - for (auto& edge : edges) { - edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables); - } - - // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); - for (auto const& edge : edges) { - sumOfGuards += edge.guard; - } - uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); - STORM_LOG_TRACE("Found " << maxChoices << " local choices."); - - // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. - if (maxChoices == 0) { - return std::make_pair(0, this->variables.manager->template getAddZero()); - } else if (maxChoices == 1) { - return std::make_pair(0, combineEdgesBySummation(edges, this->variables)); - } else { - // Calculate number of required variables to encode the nondeterminism. - uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - - storm::dd::Add allEdges = this->variables.manager->template getAddZero(); - - storm::dd::Bdd equalsNumberOfChoicesDd; - std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); - std::vector> remainingDds(maxChoices, this->variables.manager->getBddZero()); - - for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { - // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast(currentChoices))); - - // If there is no such state, continue with the next possible number of choices. - if (equalsNumberOfChoicesDd.isZero()) { - continue; - } - - // Reset the previously used intermediate storage. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - choiceDds[j] = this->variables.manager->template getAddZero(); - remainingDds[j] = equalsNumberOfChoicesDd; - } - - for (std::size_t j = 0; j < edges.size(); ++j) { - // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices - // choices such that one outgoing choice is given by the j-th edge. - storm::dd::Bdd guardChoicesIntersection = edges[j].guard.toBdd() && equalsNumberOfChoicesDd; - - // If there is no such state, continue with the next command. - if (guardChoicesIntersection.isZero()) { - continue; - } - - // Split the currentChoices nondeterministic choices. - for (uint_fast64_t k = 0; k < currentChoices; ++k) { - // Calculate the overlapping part of command guard and the remaining DD. - storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; - - // Check if we can add some overlapping parts to the current index. - if (!remainingGuardChoicesIntersection.isZero()) { - // Remove overlapping parts from the remaining DD. - remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; - - // Combine the overlapping part of the guard with command updates and add it to the resulting DD. - choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * edges[j].transitions; - } - - // Remove overlapping parts from the command guard DD - guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; - - // If the guard DD has become equivalent to false, we can stop here. - if (guardChoicesIntersection.isZero()) { - break; - } - } - } - - // Add the meta variables that encode the nondeterminisim to the different choices. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j]; - } - - // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); - } - - return std::make_pair(numberOfBinaryVariables, allEdges); - } - } - - storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { - // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. - storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); - for (auto const& action : actionIndexToEdges) { - for (auto const& edge : action.second) { - if (!edge.globalVariablesWrittenMultipleTimes.empty()) { - for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { - STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); - illegalFragment |= edge.guard.toBdd(); - } - } - } - } - return illegalFragment; - } - - ComposerResult buildSystemFromAutomaton(AutomatonDd& automatonDd) { - // If the model is an MDP, we need to encode the nondeterminism using additional variables. - if (this->model.getModelType() == storm::jani::ModelType::MDP) { - std::map>> actionIndexToUsedVariablesAndDd; - - // Combine the edges of each action individually and keep track of how many local nondeterminism variables - // were used. - uint64_t highestNumberOfUsedNondeterminismVariables = 0; - for (auto& action : automatonDd.actionIndexToEdges) { - std::pair> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second); - actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); - highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); - } - - storm::dd::Add result = this->variables.manager->template getAddZero(); - for (auto const& element : actionIndexToUsedVariablesAndDd) { - result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); - } - - return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables); - } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { - storm::dd::Add result = this->variables.manager->template getAddZero(); - for (auto const& action : automatonDd.actionIndexToEdges) { - result += combineEdgesBySummation(action.second, this->variables); - } - return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); - } - - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); - } - - storm::dd::Add computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables const& variables) { - std::set missingIdentities; - std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - storm::dd::Add identityEncoding = variables.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - identityEncoding *= variables.variableToIdentityMap.at(variable); - } - return identityEncoding; - } - - EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add const& identity) { - EdgeDd result(edge); - result.transitions *= identity; - return result; - } - - EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { - EdgeDd result; - - // Compose the guards. - result.guard = edge1.guard * edge2.guard; - - // If the composed guard is already zero, we can immediately return an empty result. - if (result.guard.isZero()) { - result.transitions = edge1.transitions.getDdManager().template getAddZero(); - return result; - } - - // Compute the set of variables written multiple times by the composition. - std::set oldVariablesWrittenMultipleTimes; - std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); - - std::set newVariablesWrittenMultipleTimes; - std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin())); - - std::set variablesWrittenMultipleTimes; - std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin())); - - result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes); - - // Compute the set of variables written by the composition. - std::set variablesWritten; - std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin())); - - result.writtenGlobalVariables = variablesWritten; - - // Compose the guards. - result.guard = edge1.guard * edge2.guard; - - // Compose the transitions. - result.transitions = edge1.transitions * edge2.transitions; - - return result; - } - - /*! - * Builds the DD for the given edge. - */ - EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { - STORM_LOG_TRACE("Translating guard " << edge.getGuard()); - storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName()); - STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); - - if (!guard.isZero()) { - // Create the DDs representing the individual updates. - std::vector> destinationDds; - for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { - destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables)); - - STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); - } - - // Start by gathering all variables that were written in at least one update. - std::set globalVariablesInSomeUpdate; - - // If the edge is not labeled with the silent action, we have to analyze which portion of the global - // variables was written by any of the updates and make all update results equal w.r.t. this set. If - // the edge is labeled with the silent action, we can already multiply the identities of all global variables. - if (edge.getActionIndex() != this->model.getSilentActionIndex()) { - for (auto const& edgeDestinationDd : destinationDds) { - globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); - } - } else { - globalVariablesInSomeUpdate = this->variables.allGlobalVariables; - } - - // Then, multiply the missing identities. - for (auto& destinationDd : destinationDds) { - std::set missingIdentities; - std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD."); - destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable); - } - } - - // Now combine the destination DDs to the edge DD. - storm::dd::Add transitions = this->variables.manager->template getAddZero(); - for (auto const& destinationDd : destinationDds) { - transitions += destinationDd.transitions; - } - - // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; - - // If we multiply the ranges of global variables, make sure everything stays within its bounds. - if (!globalVariablesInSomeUpdate.empty()) { - transitions *= this->variables.globalVariableRanges; - } - - // If the edge has a rate, we multiply it to the DD. - if (edge.hasRate()) { - transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); - } - return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); - } else { - return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); - } - } - - /*! - * Builds the DD for the automaton with the given name. - */ - AutomatonDd buildAutomatonDd(std::string const& automatonName) { - AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); - - storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); - for (auto const& edge : automaton.getEdges()) { - // Build the edge and add it if it adds transitions. - EdgeDd edgeDd = buildEdgeDd(automaton, edge); - if (!edgeDd.guard.isZero()) { - result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd); - } - } - - return result; - } - }; +// template +// class SeparateEdgesSystemComposer : public SystemComposer { +// public: +// // This structure represents an edge. +// struct EdgeDd { +// EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { +// // Intentionally left empty. +// } +// +// EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { +// // Intentionally left empty. +// } +// +// EdgeDd& operator=(EdgeDd const& other) { +// if (this != &other) { +// globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes; +// writtenGlobalVariables = other.writtenGlobalVariables; +// guard = other.guard; +// transitions = other.transitions; +// } +// return *this; +// } +// +// storm::dd::Add guard; +// storm::dd::Add transitions; +// std::set writtenGlobalVariables; +// std::set globalVariablesWrittenMultipleTimes; +// }; +// +// // This structure represents a subcomponent of a composition. +// struct AutomatonDd { +// AutomatonDd(storm::dd::Add const& identity) : identity(identity) { +// // Intentionally left empty. +// } +// +// std::map> actionIndexToEdges; +// storm::dd::Add identity; +// }; +// +// SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { +// // Intentionally left empty. +// } +// +// ComposerResult compose() override { +// AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); +// return buildSystemFromAutomaton(globalAutomaton); +// } +// +// boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { +// return buildAutomatonDd(composition.getAutomatonName()); +// } +// +// boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { +// AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); +// +// // 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()) { +// // 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())); +// } else { +// renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); +// } +// } else { +// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); +// } +// } +// +// // Finally, apply the renaming. +// AutomatonDd result(subautomaton.identity); +// for (auto const& actionEdges : subautomaton.actionIndexToEdges) { +// auto it = renamingIndexToIndex.find(actionEdges.first); +// if (it != renamingIndexToIndex.end()) { +// // If we are to rename the action, do so. +// result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end()); +// } else { +// // Otherwise copy over the edges. +// result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end()); +// } +// } +// return result; +// } +// +// boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { +// AutomatonDd leftSubautomaton = boost::any_cast(composition.getLeftSubcomposition().accept(*this, boost::none)); +// AutomatonDd rightSubautomaton = boost::any_cast(composition.getRightSubcomposition().accept(*this, boost::none)); +// +// // 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."); +// } +// } +// +// // Perform the composition. +// +// // First, consider all actions in the left subcomposition. +// AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); +// uint64_t index = 0; +// for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { +// // If we need to synchronize over this action, do so now. +// if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { +// auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first); +// if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { +// for (auto const& edge1 : actionEdges.second) { +// for (auto const& edge2 : rightIt->second) { +// EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); +// if (!edgeDd.guard.isZero()) { +// result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); +// } +// index++; +// } +// } +// } +// } else { +// // Extend all edges by the missing identity (unsynchronizing) and copy them over. +// for (auto const& edge : actionEdges.second) { +// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity)); +// } +// } +// } +// +// // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because +// // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none, +// // such transitions can not be taken and we can drop them. +// for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) { +// if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) { +// for (auto const& edge : actionEdges.second) { +// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity)); +// } +// } +// } +// +// return result; +// } +// +// private: +// storm::dd::Add combineEdgesBySummation(std::vector const& edges, CompositionVariables const& variables) { +// storm::dd::Add result = variables.manager->template getAddZero(); +// for (auto const& edge : edges) { +// // Simply add all actions, but make sure to include the missing global variable identities. +// result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables); +// } +// return result; +// } +// +// std::pair> combineEdgesByNondeterministicChoice(std::vector& edges) { +// // Complete all edges by adding the missing global variable identities. +// for (auto& edge : edges) { +// edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables); +// } +// +// // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. +// storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); +// for (auto const& edge : edges) { +// sumOfGuards += edge.guard; +// } +// uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); +// STORM_LOG_TRACE("Found " << maxChoices << " local choices."); +// +// // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. +// if (maxChoices == 0) { +// return std::make_pair(0, this->variables.manager->template getAddZero()); +// } else if (maxChoices == 1) { +// return std::make_pair(0, combineEdgesBySummation(edges, this->variables)); +// } else { +// // Calculate number of required variables to encode the nondeterminism. +// uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); +// +// storm::dd::Add allEdges = this->variables.manager->template getAddZero(); +// +// storm::dd::Bdd equalsNumberOfChoicesDd; +// std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); +// std::vector> remainingDds(maxChoices, this->variables.manager->getBddZero()); +// +// for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { +// // Determine the set of states with exactly currentChoices choices. +// equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast(currentChoices))); +// +// // If there is no such state, continue with the next possible number of choices. +// if (equalsNumberOfChoicesDd.isZero()) { +// continue; +// } +// +// // Reset the previously used intermediate storage. +// for (uint_fast64_t j = 0; j < currentChoices; ++j) { +// choiceDds[j] = this->variables.manager->template getAddZero(); +// remainingDds[j] = equalsNumberOfChoicesDd; +// } +// +// for (std::size_t j = 0; j < edges.size(); ++j) { +// // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices +// // choices such that one outgoing choice is given by the j-th edge. +// storm::dd::Bdd guardChoicesIntersection = edges[j].guard.toBdd() && equalsNumberOfChoicesDd; +// +// // If there is no such state, continue with the next command. +// if (guardChoicesIntersection.isZero()) { +// continue; +// } +// +// // Split the currentChoices nondeterministic choices. +// for (uint_fast64_t k = 0; k < currentChoices; ++k) { +// // Calculate the overlapping part of command guard and the remaining DD. +// storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; +// +// // Check if we can add some overlapping parts to the current index. +// if (!remainingGuardChoicesIntersection.isZero()) { +// // Remove overlapping parts from the remaining DD. +// remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; +// +// // Combine the overlapping part of the guard with command updates and add it to the resulting DD. +// choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * edges[j].transitions; +// } +// +// // Remove overlapping parts from the command guard DD +// guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; +// +// // If the guard DD has become equivalent to false, we can stop here. +// if (guardChoicesIntersection.isZero()) { +// break; +// } +// } +// } +// +// // Add the meta variables that encode the nondeterminisim to the different choices. +// for (uint_fast64_t j = 0; j < currentChoices; ++j) { +// allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j]; +// } +// +// // Delete currentChoices out of overlapping DD +// sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); +// } +// +// return std::make_pair(numberOfBinaryVariables, allEdges); +// } +// } +// +// storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { +// // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. +// storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); +// for (auto const& action : actionIndexToEdges) { +// for (auto const& edge : action.second) { +// if (!edge.globalVariablesWrittenMultipleTimes.empty()) { +// for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { +// STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); +// illegalFragment |= edge.guard.toBdd(); +// } +// } +// } +// } +// return illegalFragment; +// } +// +// ComposerResult buildSystemFromAutomaton(AutomatonDd& automatonDd) { +// // If the model is an MDP, we need to encode the nondeterminism using additional variables. +// if (this->model.getModelType() == storm::jani::ModelType::MDP) { +// std::map>> actionIndexToUsedVariablesAndDd; +// +// // Combine the edges of each action individually and keep track of how many local nondeterminism variables +// // were used. +// uint64_t highestNumberOfUsedNondeterminismVariables = 0; +// for (auto& action : automatonDd.actionIndexToEdges) { +// std::pair> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second); +// actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); +// highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); +// } +// +// storm::dd::Add result = this->variables.manager->template getAddZero(); +// for (auto const& element : actionIndexToUsedVariablesAndDd) { +// result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); +// } +// +// return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables); +// } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { +// storm::dd::Add result = this->variables.manager->template getAddZero(); +// for (auto const& action : automatonDd.actionIndexToEdges) { +// result += combineEdgesBySummation(action.second, this->variables); +// } +// return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); +// } +// +// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); +// } +// +// storm::dd::Add computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables const& variables) { +// std::set missingIdentities; +// std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); +// storm::dd::Add identityEncoding = variables.manager->template getAddOne(); +// for (auto const& variable : missingIdentities) { +// identityEncoding *= variables.variableToIdentityMap.at(variable); +// } +// return identityEncoding; +// } +// +// EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add const& identity) { +// EdgeDd result(edge); +// result.transitions *= identity; +// return result; +// } +// +// EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { +// EdgeDd result; +// +// // Compose the guards. +// result.guard = edge1.guard * edge2.guard; +// +// // If the composed guard is already zero, we can immediately return an empty result. +// if (result.guard.isZero()) { +// result.transitions = edge1.transitions.getDdManager().template getAddZero(); +// return result; +// } +// +// // Compute the set of variables written multiple times by the composition. +// std::set oldVariablesWrittenMultipleTimes; +// std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); +// +// std::set newVariablesWrittenMultipleTimes; +// std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin())); +// +// std::set variablesWrittenMultipleTimes; +// std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin())); +// +// result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes); +// +// // Compute the set of variables written by the composition. +// std::set variablesWritten; +// std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin())); +// +// result.writtenGlobalVariables = variablesWritten; +// +// // Compose the guards. +// result.guard = edge1.guard * edge2.guard; +// +// // Compose the transitions. +// result.transitions = edge1.transitions * edge2.transitions; +// +// return result; +// } +// +// /*! +// * Builds the DD for the given edge. +// */ +// EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { +// STORM_LOG_TRACE("Translating guard " << edge.getGuard()); +// storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName()); +// STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); +// +// if (!guard.isZero()) { +// // Create the DDs representing the individual updates. +// std::vector> destinationDds; +// for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { +// destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables)); +// +// STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); +// } +// +// // Start by gathering all variables that were written in at least one update. +// std::set globalVariablesInSomeUpdate; +// +// // If the edge is not labeled with the silent action, we have to analyze which portion of the global +// // variables was written by any of the updates and make all update results equal w.r.t. this set. If +// // the edge is labeled with the silent action, we can already multiply the identities of all global variables. +// if (edge.getActionIndex() != this->model.getSilentActionIndex()) { +// for (auto const& edgeDestinationDd : destinationDds) { +// globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); +// } +// } else { +// globalVariablesInSomeUpdate = this->variables.allGlobalVariables; +// } +// +// // Then, multiply the missing identities. +// for (auto& destinationDd : destinationDds) { +// std::set missingIdentities; +// std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); +// +// for (auto const& variable : missingIdentities) { +// STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD."); +// destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable); +// } +// } +// +// // Now combine the destination DDs to the edge DD. +// storm::dd::Add transitions = this->variables.manager->template getAddZero(); +// for (auto const& destinationDd : destinationDds) { +// transitions += destinationDd.transitions; +// } +// +// // Add the source location and the guard. +// transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; +// +// // If we multiply the ranges of global variables, make sure everything stays within its bounds. +// if (!globalVariablesInSomeUpdate.empty()) { +// transitions *= this->variables.globalVariableRanges; +// } +// +// // If the edge has a rate, we multiply it to the DD. +// if (edge.hasRate()) { +// transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); +// } +// return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); +// } else { +// return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); +// } +// } +// +// /*! +// * Builds the DD for the automaton with the given name. +// */ +// AutomatonDd buildAutomatonDd(std::string const& automatonName) { +// AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); +// +// storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); +// for (auto const& edge : automaton.getEdges()) { +// // Build the edge and add it if it adds transitions. +// EdgeDd edgeDd = buildEdgeDd(automaton, edge); +// if (!edgeDd.guard.isZero()) { +// result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd); +// } +// } +// +// return result; +// } +// }; template class CombinedEdgesSystemComposer : public SystemComposer { @@ -1019,9 +1060,11 @@ namespace storm { }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionToIndex(model.getActionToIndexMap()) { // Intentionally left empty. } + + std::unordered_map actionToIndex; ComposerResult compose() override { std::map actionIndexToLocalNondeterminismVariableOffset; diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 9c618a838..d3c68cd39 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -391,6 +391,14 @@ namespace storm { edge.finalize(containingModel); } } + + std::set Automaton::getUsedActionIndices() const { + std::set result; + for (auto const& edge : edges) { + result.insert(edge.getActionIndex()); + } + return result; + } } } \ No newline at end of file diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index c6219aa1e..f2c784084 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -294,6 +294,11 @@ namespace storm { */ void finalize(Model const& containingModel); + /*! + * Retrieves the action indices appearing at some edge of the automaton. + */ + std::set getUsedActionIndices() const; + private: /// The name of the automaton. std::string name; diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index d6b661b53..b07911ca6 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -6,11 +6,11 @@ namespace storm { namespace jani { - CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), restrictedParallelComposition(false) { + CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), nonStandardParallelComposition(false) { // Intentionally left empty. } - CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) { + CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), nonStandardParallelComposition(nonStandardParallelComposition) { // Intentionally left empty. } @@ -49,12 +49,12 @@ namespace storm { return renameComposition; } - void CompositionInformation::setContainsRestrictedParallelComposition() { - restrictedParallelComposition = true; + void CompositionInformation::setContainsNonStandardParallelComposition() { + nonStandardParallelComposition = true; } - bool CompositionInformation::containsRestrictedParallelComposition() const { - return restrictedParallelComposition; + bool CompositionInformation::containsNonStandardParallelComposition() const { + return nonStandardParallelComposition; } std::map CompositionInformation::joinMultiplicityMaps(std::map const& first, std::map const& second) { @@ -90,30 +90,61 @@ namespace storm { boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { CompositionInformation subresult = boost::any_cast(composition.getSubcomposition().accept(*this, data)); std::set nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming()); - return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsRestrictedParallelComposition()); + return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsNonStandardParallelComposition()); } boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { - CompositionInformation left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); - CompositionInformation right = boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); - - // Join the information from both sides. - bool containsRenameComposition = left.containsRenameComposition() || right.containsRenameComposition(); - bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition(); - std::map joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap()); + std::vector subinformation; - std::set nonsilentActions; - std::set_union(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(nonsilentActions, nonsilentActions.begin())); + for (auto const& subcomposition : composition.getSubcompositions()) { + subinformation.push_back(boost::any_cast(subcomposition->accept(*this, data))); + } + + std::map joinedAutomatonToMultiplicityMap; + bool containsRenameComposition = false; + bool containsNonStandardParallelComposition = false; + + for (auto const& subinfo : subinformation) { + containsRenameComposition |= subinfo.containsRenameComposition(); + containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition(); + joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap()); + + } - // If there was no restricted parallel composition yet, maybe the current composition is one, so check it. - if (!containsRestrictedParallelComposition) { - std::set commonNonsilentActions; - std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin())); - bool allCommonActionsIncluded = std::includes(commonNonsilentActions.begin(), commonNonsilentActions.end(), composition.getSynchronizationAlphabet().begin(), composition.getSynchronizationAlphabet().end()); - containsRestrictedParallelComposition = !allCommonActionsIncluded; + // Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have + // the non-silent actions that are referred to. + std::set effectiveSynchVectors; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + effectiveSynchVectors.insert(synchVectorIndex); } - return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition); + // Now compute non-silent actions. + std::set nonsilentActions; + for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) { + auto const& subinfo = subinformation[infoIndex]; + + std::set enabledSynchVectors; + for (auto const& nonsilentAction : subinfo.getNonsilentActions()) { + bool appearsInSomeSynchVector = false; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); + if (synchVector.getInput(infoIndex) == nonsilentAction) { + appearsInSomeSynchVector = true; + enabledSynchVectors.insert(synchVectorIndex); + } + } + + if (!appearsInSomeSynchVector) { + nonsilentActions.insert(nonsilentAction); + } + } + + std::set newEffectiveSynchVectors; + std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); + effectiveSynchVectors = std::move(newEffectiveSynchVectors); + } + + return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsRenameComposition, containsNonStandardParallelComposition); } } diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h index 59a422a41..786078e2e 100644 --- a/src/storage/jani/CompositionInformationVisitor.h +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -16,7 +16,7 @@ namespace storm { class CompositionInformation { public: CompositionInformation(); - CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition); + CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool nonStandardParallelComposition); void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1); @@ -27,8 +27,8 @@ namespace storm { void setContainsRenameComposition(); bool containsRenameComposition() const; - void setContainsRestrictedParallelComposition(); - bool containsRestrictedParallelComposition() const; + void setContainsNonStandardParallelComposition(); + bool containsNonStandardParallelComposition() const; static std::map joinMultiplicityMaps(std::map const& first, std::map const& second); std::map const& getAutomatonToMultiplicityMap() const; @@ -43,8 +43,8 @@ namespace storm { /// A flag indicating whether the composition contains a renaming composition. bool renameComposition; - /// A flag indicating whether the composition contains - bool restrictedParallelComposition; + /// A flag indicating whether the composition contains any non-standard parallel composition. + bool nonStandardParallelComposition; }; class CompositionInformationVisitor : public CompositionVisitor { diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index fc170ac58..5f6d3e6eb 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -75,6 +75,10 @@ namespace storm { return it->second; } + std::unordered_map const& Model::getActionToIndexMap() const { + return actionToIndex; + } + std::vector const& Model::getActions() const { return actions; } @@ -448,7 +452,7 @@ namespace storm { bool Model::hasDefaultComposition() const { CompositionInformationVisitor visitor; CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this); - if (info.containsRestrictedParallelComposition() || info.containsRenameComposition()) { + if (info.containsNonStandardParallelComposition() || info.containsRenameComposition()) { return false; } for (auto const& multiplicity : info.getAutomatonToMultiplicityMap()) { diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 2fc06b18f..d955bb0e7 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -65,6 +65,11 @@ namespace storm { */ uint64_t getActionIndex(std::string const& name) const; + /*! + * Retrieves the mapping from action names to their indices. + */ + std::unordered_map const& getActionToIndexMap() const; + /** * Adds an action to the model. * diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index f767e32cc..0f8a41d63 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -1,32 +1,132 @@ #include "src/storage/jani/ParallelComposition.h" +#include + #include +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace jani { - ParallelComposition::ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) { + SynchronizationVector::SynchronizationVector(std::vector const& input, std::string const& output) : input(input), output(output) { // Intentionally left empty. } - Composition const& ParallelComposition::getLeftSubcomposition() const { - return *leftSubcomposition; + std::size_t SynchronizationVector::size() const { + return input.size(); + } + + std::vector const& SynchronizationVector::getInput() const { + return input; + } + + std::string const& SynchronizationVector::getInput(uint64_t index) const { + return input[index]; + } + + std::string const& SynchronizationVector::getOutput() const { + return output; } - Composition const& ParallelComposition::getRightSubcomposition() const { - return *rightSubcomposition; + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector) { + bool first = true; + stream << "("; + for (auto const& element : synchronizationVector.getInput()) { + if (!first) { + stream << ", "; + } + stream << element; + } + stream << ") -> " << synchronizationVector.getOutput(); + return stream; } - std::set const& ParallelComposition::getSynchronizationAlphabet() const { - return alphabet; + ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) { + STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); + + for (auto const& vector : this->synchronizationVectors) { + STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); + } } + + ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() { + STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); + // Manually construct the synchronization vectors for all elements of the synchronization alphabet. + for (auto const& action : synchronizationAlphabet) { + synchronizationVectors.emplace_back(std::vector(this->subcompositions.size(), action), action); + } + } + + ParallelComposition::ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet) { + subcompositions.push_back(leftSubcomposition); + subcompositions.push_back(rightSubcomposition); + + // Manually construct the synchronization vectors for all elements of the synchronization alphabet. + for (auto const& action : synchronizationAlphabet) { + synchronizationVectors.emplace_back(std::vector(this->subcompositions.size(), action), action); + } + } + + Composition const& ParallelComposition::getSubcomposition(uint64_t index) const { + return *subcompositions[index]; + } + + std::vector> const& ParallelComposition::getSubcompositions() const { + return subcompositions; + } + + uint64_t ParallelComposition::getNumberOfSubcompositions() const { + return subcompositions.size(); + } + + SynchronizationVector const& ParallelComposition::getSynchronizationVector(uint64_t index) const { + return synchronizationVectors[index]; + } + + std::vector const& ParallelComposition::getSynchronizationVectors() const { + return synchronizationVectors; + } + + std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const { + return synchronizationVectors.size(); + } + + bool ParallelComposition::checkSynchronizationVectors() const { + for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { + std::set actions; + for (auto const& vector : synchronizationVectors) { + std::string const& action = vector.getInput(inputIndex); + STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vector."); + actions.insert(action); + } + } + } + boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } void ParallelComposition::write(std::ostream& stream) const { - stream << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(alphabet, ", ") << "]| " << this->getRightSubcomposition(); + std::vector synchronizationVectorsAsStrings; + for (auto const& synchronizationVector : synchronizationVectors) { + std::stringstream tmpStream; + tmpStream << synchronizationVector; + synchronizationVectorsAsStrings.push_back(tmpStream.str()); + } + + bool first = true; + stream << "("; + for (auto const& subcomposition : subcompositions) { + if (!first) { + stream << " || "; + first = false; + } + stream << *subcomposition; + } + stream << ")[" << boost::algorithm::join(synchronizationVectorsAsStrings, ", ") << "]"; } } diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h index 4b7ff69be..0ae525714 100644 --- a/src/storage/jani/ParallelComposition.h +++ b/src/storage/jani/ParallelComposition.h @@ -2,47 +2,95 @@ #include #include +#include +#include #include "src/storage/jani/Composition.h" namespace storm { namespace jani { + class SynchronizationVector { + public: + SynchronizationVector(std::vector const& input, std::string const& output); + + std::size_t size() const; + std::vector const& getInput() const; + std::string const& getInput(uint64_t index) const; + std::string const& getOutput() const; + + private: + /// The input to the synchronization. + std::vector input; + + /// The output of the synchronization. + std::string output; + }; + + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector); + class ParallelComposition : public Composition { public: /*! - * Creates a parallel composition of the two subcompositions. + * Creates a parallel composition of the subcompositions and the provided synchronization vectors. */ - ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& alphabet = {}); - + ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors); + /*! - * Retrieves the left subcomposition. + * Creates a parallel composition of the subcompositions over the provided synchronization alphabet. */ - Composition const& getLeftSubcomposition() const; + ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet); /*! - * Retrieves the right subcomposition. + * Creates a parallel composition of the subcompositions over the provided synchronization alphabet. */ - Composition const& getRightSubcomposition() const; + ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet); /*! - * Retrieves the alphabet of actions over which to synchronize the automata. + * Retrieves the subcomposition with the given index. */ - std::set const& getSynchronizationAlphabet() const; + Composition const& getSubcomposition(uint64_t index) const; + + /*! + * Retrieves the subcompositions of the parallel composition. + */ + std::vector> const& getSubcompositions() const; + + /*! + * Retrieves the number of subcompositions of this parallel composition. + */ + uint64_t getNumberOfSubcompositions() const; + + /*! + * Retrieves the synchronization vector with the given index. + */ + SynchronizationVector const& getSynchronizationVector(uint64_t index) const; + + /*! + * Retrieves the synchronization vectors of the parallel composition. + */ + std::vector const& getSynchronizationVectors() const; + + /*! + * Retrieves the number of synchronization vectors. + */ + std::size_t getNumberOfSynchronizationVectors() const; virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; virtual void write(std::ostream& stream) const override; private: - // The left subcomposition. - std::shared_ptr leftSubcomposition; + /*! + * Checks the synchronization vectors for validity. + */ + bool checkSynchronizationVectors() const; - // The right subcomposition. - std::shared_ptr rightSubcomposition; + /// The subcompositions. + std::vector> subcompositions; - // The alphabet of actions over which to synchronize. - std::set alphabet; + /// The synchronization vectors of the parallel composition. + std::vector synchronizationVectors; }; } diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 33ad88fef..08819964a 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -137,7 +137,7 @@ namespace storm { } STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented."); } - STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); + STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // previously built mapping to make variables global that are read by more than one module. From de6d03b2b6edfcbffc45d1e8838ed6ddfacdaad0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Sep 2016 16:59:10 +0200 Subject: [PATCH 04/11] even closer to make synchronization vectors work with DD-based builder Former-commit-id: befbb623dee4871ec81ce72e38f2b8dc02d03748 [formerly cdf63caac6dd8fc896a63d2df1ced12e555039d6] Former-commit-id: 7645ece87038849e7f59e63bc5f6c4f399146d1a --- src/builder/DdJaniModelBuilder.cpp | 171 ++++++++---------- .../CompositionActionInformationVisitor.cpp | 133 ++++++++++++++ .../CompositionActionInformationVisitor.h | 48 +++++ 3 files changed, 256 insertions(+), 96 deletions(-) create mode 100644 src/storage/jani/CompositionActionInformationVisitor.cpp create mode 100644 src/storage/jani/CompositionActionInformationVisitor.h 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; + }; + + + } +} From a14ee4f2c34aea919218863ed62f56a64de0b083 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Sep 2016 21:55:23 +0200 Subject: [PATCH 05/11] DD-based JANI model builder compiling again after change to synchronization vectors Former-commit-id: b2a113b16051926bf3eca8e26737287225c44916 [formerly 6347ac5b3c650337ce896ea32e679a5999b00c72] Former-commit-id: f1bf3b063cf3d852af0996d7d5343899a6814581 --- src/builder/DdJaniModelBuilder.cpp | 107 ++++++++++++++--------- src/storage/jani/ParallelComposition.cpp | 10 ++- src/storage/jani/ParallelComposition.h | 2 +- 3 files changed, 76 insertions(+), 43 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index db0f5d91b..2f65a58b0 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1116,56 +1116,83 @@ namespace storm { for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { AutomatonDd const& subautomaton = subautomata[automatonIndex]; - // Construct combined identity. - result.identity *= subautomaton.identity; - + // Add the transient assignments from the new subautomaton. addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments); - } - - result.transientLocationAssignments = joinTransientAssignmentMaps(automaton1.transientLocationAssignments, automaton2.transientLocationAssignments); - - // Treat all actions of the first automaton. - for (auto const& action1 : automaton1.actionIndexToAction) { - // If we need to synchronize over this action index, we try to do so now. - if (synchronizingActionIndices.find(action1.first) != synchronizingActionIndices.end()) { - auto action2It = automaton2.actionIndexToAction.find(action1.first); - if (action2It != automaton2.actionIndexToAction.end()) { - ActionDd newAction = combineSynchronizingActions(action1.second, action2It->second); - result.actionIndexToAction[action1.first] = newAction; - result.extendLocalNondeterminismVariables(newAction.getLocalNondeterminismVariables()); - } + + // Set the used local nondeterminism variables appropriately. + if (automatonIndex == 0) { + result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable()); + result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable()); } else { - // If we don't synchronize over this action, we need to construct the interleaving. + result.extendLocalNondeterminismVariables(subautomaton.localNondeterminismVariables); + } + + // Keep track of all actions of the current result that were combined with another action of the current + // automaton so we can extend the missing actions with the current automaton's identity later. + std::set combinedActions; + + // Compose the actions according to the synchronization vectors. + std::set actionsInSynch; + for (auto const& synchVector : synchronizationVectors) { + uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput()); + uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex)); + actionsInSynch.insert(inputActionIndex); - // If both automata contain the action, we need to combine the actions in an unsynchronized way. - auto action2It = automaton2.actionIndexToAction.find(action1.first); - if (action2It != automaton2.actionIndexToAction.end()) { - ActionDd newAction = combineUnsynchronizedActions(action1.second, action2It->second, automaton1.identity, automaton2.identity); - result.actionIndexToAction[action1.first] = newAction; - result.extendLocalNondeterminismVariables(newAction.getLocalNondeterminismVariables()); + // Either set the action (if it's the first of the ones to compose) or compose the actions directly. + if (automatonIndex == 0) { + // If the action cannot be found, the particular spot in the output will be left empty. + auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); + if (inputActionIt != subautomaton.actionIndexToAction.end()) { + result.actionIndexToAction[actionInformation.getActionIndex(synchVector.getOutput())] = inputActionIt->second; + } } else { - // If only the first automaton has this action, we only need to apply the identity of the - // second automaton. - result.actionIndexToAction[action1.first] = ActionDd(action1.second.guard, action1.second.transitions * automaton2.identity, action1.second.transientEdgeAssignments, action1.second.localNondeterminismVariables, action1.second.variableToWritingFragment, action1.second.illegalFragment); + // If there is no action in the output spot, this means that some other subcomposition did + // not provide the action necessary for the synchronization vector to resolve. + auto outputActionIt = result.actionIndexToAction.find(outputActionIndex); + if (outputActionIt != result.actionIndexToAction.end()) { + auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); + if (inputActionIt != subautomaton.actionIndexToAction.end()) { + combinedActions.insert(outputActionIt->first); + outputActionIt->second = combineSynchronizingActions(outputActionIt->second, inputActionIt->second); + result.extendLocalNondeterminismVariables(outputActionIt->second.getLocalNondeterminismVariables()); + } else { + // If the current subcomposition does not provide the required action for the synchronization + // vector, we clear the action. + result.actionIndexToAction.erase(outputActionIt); + } + } } } - } - - // Treat the actions of the second automaton. - for (auto const& action2 : automaton2.actionIndexToAction) { - // Here, we only need to treat actions that the first automaton does not have, because we have handled - // this case earlier. Likewise, we have to consider non-synchronizing actions only. - if (automaton1.actionIndexToAction.find(action2.first) == automaton1.actionIndexToAction.end()) { - if (synchronizingActionIndices.find(action2.first) == synchronizingActionIndices.end()) { - // If only the second automaton has this action, we only need to apply the identity of the - // first automaton. - result.actionIndexToAction[action2.first] = ActionDd(action2.second.guard, action2.second.transitions * automaton1.identity, action2.second.transientEdgeAssignments, action2.second.localNondeterminismVariables, action2.second.variableToWritingFragment, action2.second.illegalFragment); + + // Now treat all unsynchronizing actions. + for (auto const& action : subautomaton.actionIndexToAction) { + if (actionsInSynch.find(action.first) == actionsInSynch.end()) { + auto oldActionIt = result.actionIndexToAction.find(action.first); + combinedActions.insert(action.first); + if (oldActionIt != result.actionIndexToAction.end()) { + oldActionIt->second = combineUnsynchronizedActions(oldActionIt->second, action.second, result.identity, subautomaton.identity); + result.extendLocalNondeterminismVariables(oldActionIt->second.getLocalNondeterminismVariables()); + } else { + // Extend the action with the identity of the previous composition. + result.actionIndexToAction[action.first] = ActionDd(action.second.guard, action.second.transitions * result.identity, action.second.transientEdgeAssignments, action.second.localNondeterminismVariables, action.second.variableToWritingFragment, action.second.illegalFragment); + } + } + } + + // If it's not the first automaton we are treating, then we need to add the current automaton's + // identity to all actions that were not yet combined with another action. + if (automatonIndex == 0) { + for (auto& action : result.actionIndexToAction) { + if (combinedActions.find(action.first) == combinedActions.end()) { + result.actionIndexToAction[action.first] = ActionDd(action.second.guard, action.second.transitions * subautomaton.identity, action.second.transientEdgeAssignments, action.second.localNondeterminismVariables, action.second.variableToWritingFragment, action.second.illegalFragment); + } } } + + // Finally, construct combined identity. + result.identity *= subautomaton.identity; } - result.identity = automaton1.identity * automaton2.identity; - return result; } diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index 0f8a41d63..7e453eb0f 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -94,15 +94,21 @@ namespace storm { return synchronizationVectors.size(); } - bool ParallelComposition::checkSynchronizationVectors() const { + void ParallelComposition::checkSynchronizationVectors() const { for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { std::set actions; for (auto const& vector : synchronizationVectors) { std::string const& action = vector.getInput(inputIndex); - STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vector."); + STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vectors."); actions.insert(action); } } + + std::set actions; + for (auto const& vector : synchronizationVectors) { + STORM_LOG_THROW(actions.find(vector.getOutput()) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same output action multiple times in synchronization vectors."); + actions.insert(vector.getOutput()); + } } boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h index 0ae525714..3138261a8 100644 --- a/src/storage/jani/ParallelComposition.h +++ b/src/storage/jani/ParallelComposition.h @@ -84,7 +84,7 @@ namespace storm { /*! * Checks the synchronization vectors for validity. */ - bool checkSynchronizationVectors() const; + void checkSynchronizationVectors() const; /// The subcompositions. std::vector> subcompositions; From d2af83a98a39a99832e9b9352ddad07051bcccb2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Sep 2016 22:21:11 +0200 Subject: [PATCH 06/11] fixed some bugs here and there Former-commit-id: 0dbedbb01152cdaa9ac9d4b9617b957155600edd [formerly 5a4bce00e870223ae2d843200fd9acaa2462c1d8] Former-commit-id: 7dd87b11556968dfdc9970e81b74b17a185d7658 --- src/builder/DdJaniModelBuilder.cpp | 1 + src/storage/dd/Dd.cpp | 7 ++++++- src/storage/dd/Dd.h | 4 +++- src/storage/jani/Automaton.h | 4 ++-- .../jani/CompositionActionInformationVisitor.cpp | 15 +++++++++++++-- .../jani/CompositionActionInformationVisitor.h | 4 +++- src/storage/sparse/StateValuations.cpp | 6 +++++- src/storage/sparse/StateValuations.h | 4 +++- 8 files changed, 36 insertions(+), 9 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 2f65a58b0..9a6a2681d 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1032,6 +1032,7 @@ namespace storm { for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; } + actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0; AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); return buildSystemFromAutomaton(globalAutomaton); diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp index bae32c108..ec6b8b2aa 100644 --- a/src/storage/dd/Dd.cpp +++ b/src/storage/dd/Dd.cpp @@ -14,6 +14,11 @@ namespace storm { // Intentionally left empty. } + template + Dd::~Dd() { + // Intentionally left empty. + } + template bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); @@ -87,4 +92,4 @@ namespace storm { template class Dd; template class Dd; } -} \ No newline at end of file +} diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h index 18605c259..71f392dea 100644 --- a/src/storage/dd/Dd.h +++ b/src/storage/dd/Dd.h @@ -30,6 +30,8 @@ namespace storm { Dd(Dd&& other) = default; Dd& operator=(Dd&& other) = default; + virtual ~Dd(); + /*! * Retrieves the support of the current DD. * @@ -181,4 +183,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_DD_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_DD_H_ */ diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index f2c784084..9df752612 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -298,7 +298,7 @@ namespace storm { * Retrieves the action indices appearing at some edge of the automaton. */ std::set getUsedActionIndices() const; - + private: /// The name of the automaton. std::string name; @@ -330,4 +330,4 @@ namespace storm { }; } -} \ No newline at end of file +} diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp index ad8812648..683995d07 100644 --- a/src/storage/jani/CompositionActionInformationVisitor.cpp +++ b/src/storage/jani/CompositionActionInformationVisitor.cpp @@ -6,7 +6,7 @@ namespace storm { namespace jani { - ActionInformation::ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap) : nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) { + ActionInformation::ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap, uint64_t silentActionIndex) : silentActionIndex(silentActionIndex), nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) { // Intentionally left empty. } @@ -21,6 +21,10 @@ namespace storm { std::set const& ActionInformation::getNonSilentActionIndices() const { return nonsilentActionIndices; } + + uint64_t ActionInformation::getSilentActionIndex() const { + return silentActionIndex; + } CompositionActionInformationVisitor::CompositionActionInformationVisitor(storm::jani::Model const& model) : model(model), nextFreeActionIndex(0), nameToIndexMap(), indexToNameMap() { // Intentionally left empty. @@ -32,6 +36,11 @@ namespace storm { // Determine the next free index we can give out to a new action. for (auto const& action : model.getActions()) { + uint64_t actionIndex = model.getActionIndex(action.getName()); + + nameToIndexMap[action.getName()] = model.getActionIndex(action.getName()); + indexToNameMap[actionIndex] = action.getName(); + nextFreeActionIndex = std::max(nextFreeActionIndex, model.getActionIndex(action.getName())); } ++nextFreeActionIndex; @@ -42,7 +51,9 @@ namespace storm { } boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { - return model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices(); + std::set result = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices(); + result.erase(model.getSilentActionIndex()); + return result; } boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h index 93017b8a1..705773c27 100644 --- a/src/storage/jani/CompositionActionInformationVisitor.h +++ b/src/storage/jani/CompositionActionInformationVisitor.h @@ -12,13 +12,15 @@ namespace storm { class ActionInformation { public: - ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap); + ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap, uint64_t silentActionIndex = 0); std::string const& getActionName(uint64_t index) const; uint64_t getActionIndex(std::string const& name) const; std::set const& getNonSilentActionIndices() const; + uint64_t getSilentActionIndex() const; private: + uint64_t silentActionIndex; std::set nonsilentActionIndices; std::map indexToNameMap; std::map nameToIndexMap; diff --git a/src/storage/sparse/StateValuations.cpp b/src/storage/sparse/StateValuations.cpp index f3f98818f..a574d7a10 100644 --- a/src/storage/sparse/StateValuations.cpp +++ b/src/storage/sparse/StateValuations.cpp @@ -8,10 +8,14 @@ namespace storm { // Intentionally left empty. } + StateValuations::~StateValuations() { + // Intentionally left empty. + } + std::string StateValuations::stateInfo(state_type const& state) const { return valuations[state].toString(); } } } -} \ No newline at end of file +} diff --git a/src/storage/sparse/StateValuations.h b/src/storage/sparse/StateValuations.h index b64620efd..a378dcaf8 100644 --- a/src/storage/sparse/StateValuations.h +++ b/src/storage/sparse/StateValuations.h @@ -20,6 +20,8 @@ namespace storm { */ StateValuations(state_type const& numberOfStates); + virtual ~StateValuations(); + // A mapping from state indices to their variable valuations. std::vector valuations; @@ -30,4 +32,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */ From 1dc4af0e289b43f595bbc8c2b6c600bc545b1ae5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Sep 2016 22:25:30 +0200 Subject: [PATCH 07/11] switched from empty virtual destructors to default destructors. Also: apparently no swimming for me, Mr. B! Former-commit-id: 31340d1502a6caa2259e366a4b411c4b02efeab1 [formerly 5229b67e7d4ecd215a93983ce8816515f5f81388] Former-commit-id: dfb77cf34621abf1fc0b69d6d1e62ed41a5c6b61 --- src/storage/dd/Dd.cpp | 5 ----- src/storage/dd/Dd.h | 2 +- src/storage/sparse/StateValuations.cpp | 6 +----- src/storage/sparse/StateValuations.h | 2 +- 4 files changed, 3 insertions(+), 12 deletions(-) diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp index ec6b8b2aa..ded8bb457 100644 --- a/src/storage/dd/Dd.cpp +++ b/src/storage/dd/Dd.cpp @@ -14,11 +14,6 @@ namespace storm { // Intentionally left empty. } - template - Dd::~Dd() { - // Intentionally left empty. - } - template bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h index 71f392dea..ae9728263 100644 --- a/src/storage/dd/Dd.h +++ b/src/storage/dd/Dd.h @@ -30,7 +30,7 @@ namespace storm { Dd(Dd&& other) = default; Dd& operator=(Dd&& other) = default; - virtual ~Dd(); + virtual ~Dd() = default; /*! * Retrieves the support of the current DD. diff --git a/src/storage/sparse/StateValuations.cpp b/src/storage/sparse/StateValuations.cpp index a574d7a10..522d09f27 100644 --- a/src/storage/sparse/StateValuations.cpp +++ b/src/storage/sparse/StateValuations.cpp @@ -7,11 +7,7 @@ namespace storm { StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) { // Intentionally left empty. } - - StateValuations::~StateValuations() { - // Intentionally left empty. - } - + std::string StateValuations::stateInfo(state_type const& state) const { return valuations[state].toString(); } diff --git a/src/storage/sparse/StateValuations.h b/src/storage/sparse/StateValuations.h index a378dcaf8..aa7d2c30e 100644 --- a/src/storage/sparse/StateValuations.h +++ b/src/storage/sparse/StateValuations.h @@ -20,7 +20,7 @@ namespace storm { */ StateValuations(state_type const& numberOfStates); - virtual ~StateValuations(); + virtual ~StateValuations() = default; // A mapping from state indices to their variable valuations. std::vector valuations; From 62ca16b20a3628a9295b0b7d222e47a7c1e61ebf Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Sep 2016 17:37:59 +0200 Subject: [PATCH 08/11] alpha-draft of synchronization vectors in JANI Former-commit-id: 31eec25d2e6e7c2ed03a9b347112c4bf84d3a76b [formerly ecd02f99e6492c160681336e61d1a7b4305b8d96] Former-commit-id: 43c14e1dac6eb8a9d8aec13e9a742c3053345eb4 --- src/builder/DdJaniModelBuilder.cpp | 179 +++++++++++------- .../builder/DdJaniModelBuilderTest.cpp | 59 +++++- test/functional/builder/SmallPrismTest.nm | 27 +++ 3 files changed, 195 insertions(+), 70 deletions(-) create mode 100644 test/functional/builder/SmallPrismTest.nm diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 9a6a2681d..c0a6ae09f 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -958,6 +958,10 @@ namespace storm { std::pair const& getLocalNondeterminismVariables() const { return localNondeterminismVariables; } + + ActionDd multiplyTransitions(storm::dd::Add const& factor) const { + return ActionDd(guard, transitions * factor, transientEdgeAssignments, localNondeterminismVariables, variableToWritingFragment, illegalFragment); + } // A DD that represents all states that have this edge enabled. storm::dd::Add guard; @@ -1114,28 +1118,26 @@ namespace storm { AutomatonDd composeInParallel(std::vector const& subautomata, std::vector const& synchronizationVectors) { AutomatonDd result(this->variables.manager->template getAddOne()); + std::map> nonSynchronizingActions; + std::vector> synchronizationVectorActions(synchronizationVectors.size(), boost::none); for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { AutomatonDd const& subautomaton = subautomata[automatonIndex]; // Add the transient assignments from the new subautomaton. addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments); - // Set the used local nondeterminism variables appropriately. + // Initilize the used local nondeterminism variables appropriately. if (automatonIndex == 0) { result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable()); result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable()); - } else { - result.extendLocalNondeterminismVariables(subautomaton.localNondeterminismVariables); } - // Keep track of all actions of the current result that were combined with another action of the current - // automaton so we can extend the missing actions with the current automaton's identity later. - std::set combinedActions; - // Compose the actions according to the synchronization vectors. std::set actionsInSynch; - for (auto const& synchVector : synchronizationVectors) { - uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput()); + for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { + auto const& synchVector = synchronizationVectors[synchVectorIndex]; + + // Determine the indices of input (at the current automaton position) and the output. uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex)); actionsInSynch.insert(inputActionIndex); @@ -1144,48 +1146,45 @@ namespace storm { // If the action cannot be found, the particular spot in the output will be left empty. auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); if (inputActionIt != subautomaton.actionIndexToAction.end()) { - result.actionIndexToAction[actionInformation.getActionIndex(synchVector.getOutput())] = inputActionIt->second; + synchronizationVectorActions[synchVectorIndex] = inputActionIt->second; } } else { // If there is no action in the output spot, this means that some other subcomposition did // not provide the action necessary for the synchronization vector to resolve. - auto outputActionIt = result.actionIndexToAction.find(outputActionIndex); - if (outputActionIt != result.actionIndexToAction.end()) { + if (synchronizationVectorActions[synchVectorIndex]) { auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); if (inputActionIt != subautomaton.actionIndexToAction.end()) { - combinedActions.insert(outputActionIt->first); - outputActionIt->second = combineSynchronizingActions(outputActionIt->second, inputActionIt->second); - result.extendLocalNondeterminismVariables(outputActionIt->second.getLocalNondeterminismVariables()); + synchronizationVectorActions[synchVectorIndex] = combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get(), inputActionIt->second); } else { // If the current subcomposition does not provide the required action for the synchronization // vector, we clear the action. - result.actionIndexToAction.erase(outputActionIt); + synchronizationVectorActions[synchVectorIndex] = boost::none; } } } } // Now treat all unsynchronizing actions. - for (auto const& action : subautomaton.actionIndexToAction) { - if (actionsInSynch.find(action.first) == actionsInSynch.end()) { - auto oldActionIt = result.actionIndexToAction.find(action.first); - combinedActions.insert(action.first); - if (oldActionIt != result.actionIndexToAction.end()) { - oldActionIt->second = combineUnsynchronizedActions(oldActionIt->second, action.second, result.identity, subautomaton.identity); - result.extendLocalNondeterminismVariables(oldActionIt->second.getLocalNondeterminismVariables()); - } else { - // Extend the action with the identity of the previous composition. - result.actionIndexToAction[action.first] = ActionDd(action.second.guard, action.second.transitions * result.identity, action.second.transientEdgeAssignments, action.second.localNondeterminismVariables, action.second.variableToWritingFragment, action.second.illegalFragment); + if (automatonIndex == 0) { + // Since it's the first automaton, there is nothing to combine. + for (auto const& action : subautomaton.actionIndexToAction) { + if (actionsInSynch.find(action.first) == actionsInSynch.end()) { + nonSynchronizingActions[action.first].push_back(action.second); } } - } - - // If it's not the first automaton we are treating, then we need to add the current automaton's - // identity to all actions that were not yet combined with another action. - if (automatonIndex == 0) { - for (auto& action : result.actionIndexToAction) { - if (combinedActions.find(action.first) == combinedActions.end()) { - result.actionIndexToAction[action.first] = ActionDd(action.second.guard, action.second.transitions * subautomaton.identity, action.second.transientEdgeAssignments, action.second.localNondeterminismVariables, action.second.variableToWritingFragment, action.second.illegalFragment); + } else { + // Extend all other non-synchronizing actions with the identity of the current subautomaton. + for (auto& actions : nonSynchronizingActions) { + for (auto& action : actions.second) { + action.transitions *= subautomaton.identity; + } + } + + // Extend the actions of the current subautomaton with the identity of the previous system and + // add it to the overall non-synchronizing action result. + for (auto const& action : subautomaton.actionIndexToAction) { + if (actionsInSynch.find(action.first) == actionsInSynch.end()) { + nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity)); } } } @@ -1194,6 +1193,31 @@ namespace storm { result.identity *= subautomaton.identity; } + // Add the results of the synchronization vectors to that of the non-synchronizing actions. + for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { + auto const& synchVector = synchronizationVectors[synchVectorIndex]; + + // If there is an action resulting from this combination of actions, add it to the output action. + if (synchronizationVectorActions[synchVectorIndex]) { + uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput()); + nonSynchronizingActions[outputActionIndex].push_back(synchronizationVectorActions[synchVectorIndex].get()); + } + } + + // Now that we have built the individual action DDs for all resulting actions, we need to combine them + // in an unsynchronizing way. + for (auto const& nonSynchronizingActionDds : nonSynchronizingActions) { + std::vector const& actionDds = nonSynchronizingActionDds.second; + if (actionDds.size() > 1) { + ActionDd combinedAction = combineUnsynchronizedActions(actionDds); + result.actionIndexToAction[nonSynchronizingActionDds.first] = combinedAction; + result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables()); + } else { + result.actionIndexToAction[nonSynchronizingActionDds.first] = actionDds.front(); + result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables()); + } + } + return result; } @@ -1237,56 +1261,67 @@ namespace storm { } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2) { + return combineUnsynchronizedActions({action1, action2}); + } + + ActionDd combineUnsynchronizedActions(std::vector actions) { STORM_LOG_TRACE("Combining unsynchronized actions."); if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { - return ActionDd(action1.guard + action2.guard, action1.transitions + action2.transitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), this->variables.manager->getBddZero()); + auto actionIt = actions.begin(); + ActionDd result(*actionIt); + + for (++actionIt; actionIt != actions.end(); ++actionIt) { + result = ActionDd(result.guard + actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment); + } + return result; } else if (this->model.getModelType() == storm::jani::ModelType::MDP) { - if (action1.transitions.isZero()) { - return action2; - } else if (action2.transitions.isZero()) { - return action1; + // Ensure that all actions start at the same local nondeterminism variable. + uint_fast64_t lowestLocalNondeterminismVariable = actions.front().getLowestLocalNondeterminismVariable(); + uint_fast64_t highestLocalNondeterminismVariable = actions.front().getHighestLocalNondeterminismVariable(); + for (auto const& action : actions) { + STORM_LOG_ASSERT(action.getLowestLocalNondeterminismVariable() == lowestLocalNondeterminismVariable, "Mismatching lowest nondeterminism variable indices."); } - // Bring both choices to the same number of variables that encode the nondeterminism. - STORM_LOG_ASSERT(action1.getLowestLocalNondeterminismVariable() == action2.getLowestLocalNondeterminismVariable(), "Mismatching lowest nondeterminism variable indices."); - uint_fast64_t highestLocalNondeterminismVariable = std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable()); - if (action1.getHighestLocalNondeterminismVariable() > action2.getHighestLocalNondeterminismVariable()) { + // Bring all actions to the same number of variables that encode the nondeterminism. + for (auto& action : actions) { storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); - - for (uint_fast64_t i = action2.getHighestLocalNondeterminismVariable(); i < action1.getHighestLocalNondeterminismVariable(); ++i) { + for (uint_fast64_t i = action.getHighestLocalNondeterminismVariable(); i < highestLocalNondeterminismVariable; ++i) { nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); } - action2.transitions *= nondeterminismEncoding; + action.transitions *= nondeterminismEncoding; - for (auto& transientAssignment : action2.transientEdgeAssignments) { - transientAssignment.second *= nondeterminismEncoding; - } - } else if (action2.getHighestLocalNondeterminismVariable() > action1.getHighestLocalNondeterminismVariable()) { - storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); - - for (uint_fast64_t i = action1.getHighestLocalNondeterminismVariable(); i < action2.getHighestLocalNondeterminismVariable(); ++i) { - nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); - } - action1.transitions *= nondeterminismEncoding; - - for (auto& transientAssignment : action1.transientEdgeAssignments) { + for (auto& transientAssignment : action.transientEdgeAssignments) { transientAssignment.second *= nondeterminismEncoding; } } - // Add a new variable that resolves the nondeterminism between the two choices. - storm::dd::Add combinedTransitions = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1).ite(action2.transitions, action1.transitions); - - // Add the new variable to the writing fragments of each global variable before joining them. - for (auto& entry : action1.variableToWritingFragment) { - entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 0) && entry.second; - } - for (auto& entry : action2.variableToWritingFragment) { - entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1) && entry.second; + uint64_t numberOfLocalNondeterminismVariables = static_cast(std::ceil(std::log2(actions.size()))); + storm::dd::Bdd guard = this->variables.manager->getBddZero(); + storm::dd::Add transitions = this->variables.manager->template getAddZero(); + std::map> transientEdgeAssignments; + std::map> variableToWritingFragment; + storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); + + for (uint64_t actionIndex = 0; actionIndex < actions.size(); ++actionIndex) { + ActionDd& action = actions[actionIndex]; + + guard |= action.guard.toBdd(); + + storm::dd::Add nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables); + transitions += nondeterminismEncoding * action.transitions; + + joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments); + + storm::dd::Bdd nondeterminismEncodingBdd = nondeterminismEncoding.toBdd(); + for (auto& entry : action.variableToWritingFragment) { + entry.second &= nondeterminismEncodingBdd; + } + addToVariableWritingFragmentMap(variableToWritingFragment, action.variableToWritingFragment); + illegalFragment |= action.illegalFragment; } - return ActionDd((action1.guard.toBdd() || action2.guard.toBdd()).template toAdd(), combinedTransitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(action1.getLowestLocalNondeterminismVariable(), highestLocalNondeterminismVariable + 1), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), action1.illegalFragment || action2.illegalFragment); + return ActionDd(guard.template toAdd(), transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } @@ -1523,7 +1558,13 @@ namespace storm { globalVariableToWritingFragment.emplace(variable, partToAdd); } } - + + void addToVariableWritingFragmentMap(std::map>& globalVariableToWritingFragment, std::map> const& partToAdd) const { + for (auto const& entry : partToAdd) { + addToVariableWritingFragmentMap(globalVariableToWritingFragment, entry.first, entry.second); + } + } + std::map> joinVariableWritingFragmentMaps(std::map> const& globalVariableToWritingFragment1, std::map> const& globalVariableToWritingFragment2) { std::map> result = globalVariableToWritingFragment1; diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 3fc00e217..2d01bb209 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -7,6 +7,7 @@ #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" #include "src/storage/SymbolicModelDescription.h" +#include "src/storage/jani/Compositions.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/parser/PrismParser.h" @@ -300,4 +301,60 @@ TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) { storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder builder; EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); -} \ No newline at end of file +} + +TEST(DdJaniModelBuilderTest_Sylvan, IllegalSynchronizingWrites) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); +} + +TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + + // Start by checking the original composition. + std::shared_ptr> model = builder.build(janiModel); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + + // Now we tweak it's system composition to check whether synchronization vectors work. + std::vector> automataCompositions; + automataCompositions.push_back(std::make_shared("one")); + automataCompositions.push_back(std::make_shared("two")); + automataCompositions.push_back(std::make_shared("three")); + + // First, make all actions non-synchronizing. + std::vector synchronizationVectors; + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(24ul, model->getNumberOfStates()); + EXPECT_EQ(48ul, model->getNumberOfTransitions()); + + // Then, make only a, b and c synchronize. + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back("c"); + inputVector.push_back("a"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(3ul, model->getNumberOfStates()); + EXPECT_EQ(3ul, model->getNumberOfTransitions()); +} diff --git a/test/functional/builder/SmallPrismTest.nm b/test/functional/builder/SmallPrismTest.nm new file mode 100644 index 000000000..9d33b5c89 --- /dev/null +++ b/test/functional/builder/SmallPrismTest.nm @@ -0,0 +1,27 @@ +mdp + +module one + s1 : [0 .. 3]; + + [a] s1=0 -> (s1'=1); + + [c] s1=1 -> (s1'=2); + + [d] s1=1 -> (s1'=3); +endmodule + +module two + s2 : [0 .. 2]; + + [b] s2=0 -> (s2'=1); + + [c] s2=1 -> (s2'=2); +endmodule + +module three + s3 : [0 .. 1]; + + [c] s3=0 -> (s3'=1); +endmodule + +// (one || two || three)[(a, b, c) -> d, (c, c, a) -> a] From ba35120683893c0b873dafd11263b16e564efe92 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Sep 2016 18:00:04 +0200 Subject: [PATCH 09/11] fixing problems as a consequence of moving from PRISM programs to SymbolicModelDescription Former-commit-id: 01c8004a32af3b9d638fe034e80c82ce05151547 [formerly 824ae0342841bef956d186275b4dc07fffcc1d82] Former-commit-id: 028527340f0f05deb79acb0c4c8e2ed2de2d0f2b --- src/builder/DdPrismModelBuilder.cpp | 4 +- .../builder/DdPrismModelBuilderTest.cpp | 127 +++++++++++------- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 25 ++-- 3 files changed, 93 insertions(+), 63 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index b45269dc4..5a1a38b98 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1218,9 +1218,7 @@ namespace storm { transitionRewards.get() /= stateActionDd; } } - - stateActionRewards.get().exportToDot("prismrew.dot"); - + return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); } diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index a6b73779a..fa05bf3e0 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -3,6 +3,7 @@ #include "src/settings/SettingMemento.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/IOSettings.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" @@ -11,56 +12,66 @@ #include "src/builder/DdPrismModelBuilder.h" TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); @@ -70,28 +81,33 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); @@ -101,35 +117,41 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -139,9 +161,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -149,9 +171,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -159,9 +181,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); EXPECT_EQ(400ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -169,9 +191,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -179,9 +201,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -191,9 +213,10 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { } TEST(DdPrismModelBuilderTest_Cudd, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -201,9 +224,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -211,9 +234,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -221,9 +244,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); EXPECT_EQ(400ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -231,9 +254,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -241,9 +264,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -253,7 +276,8 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { } TEST(DdPrismModelBuilderTest_Sylvan, Composition) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); @@ -264,10 +288,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -277,7 +300,8 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { } TEST(DdPrismModelBuilderTest_Cudd, Composition) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); @@ -288,10 +312,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index c8ec4d75c..96450fa35 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "src/logic/Formulas.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -26,7 +27,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -123,7 +125,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -220,7 +223,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -299,7 +303,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -378,7 +383,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -414,7 +420,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -457,7 +464,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -545,7 +553,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); From d22d1daaa6d583ae57372d62c59c62521f0142c9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Sep 2016 19:35:03 +0200 Subject: [PATCH 10/11] adapted more tests Former-commit-id: 4d75a4fe5009fcd3b64abed2c55bce6e8fa987a5 [formerly ad1ad61873261e1442a037567f2180ba3678289d] Former-commit-id: d359f2c9c14f7ffa6c32537cdd67f9ac338a9e9c --- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 31 +++++++++------ .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 21 ++++++---- .../NativeHybridCtmcCslModelCheckerTest.cpp | 25 ++++++++---- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 21 ++++++---- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 13 +++++-- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 19 ++++++--- .../SymbolicMdpPrctlModelCheckerTest.cpp | 13 +++++-- test/functional/utility/GraphTest.cpp | 39 ++++++++++++------- 8 files changed, 119 insertions(+), 63 deletions(-) diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index ac2c7dcb7..53e992fd3 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -12,6 +12,7 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/StandardRewardModel.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" @@ -19,8 +20,9 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -80,8 +82,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -141,8 +144,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -185,8 +189,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -229,8 +234,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -281,8 +287,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 1733fa40f..eb00b67cd 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "src/parser/PrismParser.h" #include "src/parser/FormulaParser.h" #include "src/builder/DdPrismModelBuilder.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -21,8 +22,9 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -118,8 +120,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -215,8 +218,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -294,8 +298,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 5f744cc68..5d8391f5c 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "src/logic/Formulas.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -25,7 +26,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -122,7 +124,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -219,7 +222,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -298,7 +302,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -377,7 +382,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -413,7 +419,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -456,7 +463,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -546,7 +554,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index cd6d87afb..ac419c04b 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/solver/NativeLinearEquationSolver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -14,13 +15,12 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - #include "src/settings/modules/GmmxxEquationSolverSettings.h" - #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -81,7 +81,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -142,7 +143,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -186,7 +188,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -230,7 +233,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -282,7 +286,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 1762c098f..1fe89c609 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/parser/FormulaParser.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" @@ -19,7 +20,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -115,7 +117,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -211,7 +214,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -290,7 +294,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 3d1f3621f..c5ff7e1d1 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" @@ -18,7 +19,8 @@ #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -79,7 +81,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -141,7 +144,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -185,7 +189,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -232,7 +237,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -284,7 +290,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index efe1b3283..ea024ccb7 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -3,6 +3,7 @@ #include "src/logic/Formulas.h" #include "src/utility/solver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" @@ -18,7 +19,8 @@ #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -115,7 +117,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -212,7 +215,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -291,7 +295,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 2813e1a9b..e8c2e26fc 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/parser/PrismParser.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" @@ -16,7 +17,8 @@ #include "src/storage/dd/DdManager.h" TEST(GraphTest, SymbolicProb01_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -37,7 +39,8 @@ TEST(GraphTest, SymbolicProb01_Cudd) { } TEST(GraphTest, SymbolicProb01_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -58,7 +61,8 @@ TEST(GraphTest, SymbolicProb01_Sylvan) { } TEST(GraphTest, SymbolicProb01MinMax_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -75,7 +79,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -100,7 +105,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -119,7 +125,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { } TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -136,7 +143,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -161,7 +169,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -180,7 +189,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { } TEST(GraphTest, ExplicitProb01) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -201,7 +211,8 @@ TEST(GraphTest, ExplicitProb01) { } TEST(GraphTest, ExplicitProb01MinMax) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -216,7 +227,8 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -237,7 +249,8 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -249,4 +262,4 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); -} \ No newline at end of file +} From 36e07006f98c0cd055b6102a018dcbdfe4a5f67d Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Sep 2016 21:26:03 +0200 Subject: [PATCH 11/11] added test for legality check of synch vectors Former-commit-id: 6bef2f5a987e5fc32883b2432ac0501bee338b5f [formerly df607c9c1ab9028f8fd9dbaa19b2a031dd85c282] Former-commit-id: 78cc502eb2678fc29a568038e00cf24bc928d23d --- src/storage/jani/ParallelComposition.cpp | 14 +++----------- test/functional/builder/DdJaniModelBuilderTest.cpp | 7 +++++++ 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index 7e453eb0f..fac8e2ad7 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -45,10 +45,7 @@ namespace storm { ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) { STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); - - for (auto const& vector : this->synchronizationVectors) { - STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); - } + this->checkSynchronizationVectors(); } ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() { @@ -98,17 +95,12 @@ namespace storm { for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { std::set actions; for (auto const& vector : synchronizationVectors) { + STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); std::string const& action = vector.getInput(inputIndex); STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vectors."); actions.insert(action); } } - - std::set actions; - for (auto const& vector : synchronizationVectors) { - STORM_LOG_THROW(actions.find(vector.getOutput()) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same output action multiple times in synchronization vectors."); - actions.insert(vector.getOutput()); - } } boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { @@ -136,4 +128,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 2d01bb209..1b0248ce5 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -357,4 +357,11 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { model = builder.build(janiModel); EXPECT_EQ(3ul, model->getNumberOfStates()); EXPECT_EQ(3ul, model->getNumberOfTransitions()); + + inputVector.clear(); + inputVector.push_back("b"); + inputVector.push_back("c"); + inputVector.push_back("b"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); + EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); }