diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 5ab18683b..c0a6ae09f 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,12 +173,13 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
class CompositionVariableCreator : public storm::jani::CompositionVisitor {
public:
- CompositionVariableCreator(storm::jani::Model const& model) : model(model) {
+ CompositionVariableCreator(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) {
// Intentionally left empty.
}
CompositionVariables<Type, ValueType> 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);
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.");
@@ -204,13 +206,14 @@ namespace storm {
}
boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
- composition.getSubcomposition().accept(*this, boost::none);
+ boost::any_cast<std::set<std::string>>(composition.getSubcomposition().accept(*this, boost::none));
return boost::none;
}
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);
+ for (auto const& subcomposition : composition.getSubcompositions()) {
+ subcomposition->accept(*this, boost::none);
+ }
return boost::none;
}
@@ -218,14 +221,12 @@ namespace storm {
CompositionVariables<Type, ValueType> createVariables() {
CompositionVariables<Type, ValueType> result;
- for (auto const& action : this->model.getActions()) {
- if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) {
- std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Variable> 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()) {
@@ -350,6 +351,7 @@ namespace storm {
storm::jani::Model const& model;
std::set<std::string> automata;
+ storm::jani::ActionInformation actionInformation;
};
template <storm::dd::DdType Type, typename ValueType>
@@ -488,434 +490,434 @@ namespace storm {
return result;
}
- template <storm::dd::DdType Type, typename ValueType>
- class SeparateEdgesSystemComposer : public SystemComposer<Type, ValueType> {
- public:
- // This structure represents an edge.
- struct EdgeDd {
- EdgeDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> 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<Type, ValueType> guard;
- storm::dd::Add<Type, ValueType> transitions;
- std::set<storm::expressions::Variable> writtenGlobalVariables;
- std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
- };
-
- // This structure represents a subcomponent of a composition.
- struct AutomatonDd {
- AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
- // Intentionally left empty.
- }
-
- std::map<uint64_t, std::vector<EdgeDd>> actionIndexToEdges;
- storm::dd::Add<Type, ValueType> identity;
- };
-
- SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : SystemComposer<Type, ValueType>(model, variables) {
- // Intentionally left empty.
- }
-
- ComposerResult<Type, ValueType> compose() override {
- AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(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<AutomatonDd>(composition.getSubcomposition().accept(*this, boost::none));
-
- // Build a mapping from indices to indices for the renaming.
- std::map<uint64_t, uint64_t> 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<AutomatonDd>(composition.getLeftSubcomposition().accept(*this, boost::none));
- AutomatonDd rightSubautomaton = boost::any_cast<AutomatonDd>(composition.getRightSubcomposition().accept(*this, boost::none));
-
- // Build the set of synchronizing action indices.
- std::set<uint64_t> 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<Type, ValueType> combineEdgesBySummation(std::vector<EdgeDd> const& edges, CompositionVariables<Type, ValueType> const& variables) {
- storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
- 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<uint64_t, storm::dd::Add<Type, ValueType>> combineEdgesByNondeterministicChoice(std::vector<EdgeDd>& 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<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
- for (auto const& edge : edges) {
- sumOfGuards += edge.guard;
- }
- uint_fast64_t maxChoices = static_cast<uint_fast64_t>(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<ValueType>());
- } 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<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
-
- storm::dd::Add<Type, ValueType> allEdges = this->variables.manager->template getAddZero<ValueType>();
-
- storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
- std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, this->variables.manager->template getAddZero<ValueType>());
- std::vector<storm::dd::Bdd<Type>> 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<double>(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<ValueType>();
- 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<Type> 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<Type> 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<ValueType>() * 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<ValueType>();
- }
-
- return std::make_pair(numberOfBinaryVariables, allEdges);
- }
- }
-
- storm::dd::Bdd<Type> computeIllegalFragmentFromEdges(std::map<uint64_t, std::vector<EdgeDd>> const& actionIndexToEdges) {
- // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times.
- storm::dd::Bdd<Type> 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<Type, ValueType> 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<uint64_t, std::pair<uint64_t, storm::dd::Add<Type, ValueType>>> 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<uint64_t, storm::dd::Add<Type, ValueType>> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second);
- actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd);
- highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first);
- }
-
- storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
- for (auto const& element : actionIndexToUsedVariablesAndDd) {
- result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables);
- }
-
- return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables);
- } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
- storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
- for (auto const& action : automatonDd.actionIndexToEdges) {
- result += combineEdgesBySummation(action.second, this->variables);
- }
- return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0);
- }
-
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
- }
-
- storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables<Type, ValueType> const& variables) {
- std::set<storm::expressions::Variable> missingIdentities;
- std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
- storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
- for (auto const& variable : missingIdentities) {
- identityEncoding *= variables.variableToIdentityMap.at(variable);
- }
- return identityEncoding;
- }
-
- EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add<Type, ValueType> 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<ValueType>();
- return result;
- }
-
- // Compute the set of variables written multiple times by the composition.
- std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
- std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
-
- std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
- std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
-
- std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<Type, ValueType> 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<EdgeDestinationDd<Type, ValueType>> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
- 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<ValueType>() * 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<ValueType>(), this->variables.manager->template getAddZero<ValueType>());
- }
- }
-
- /*!
- * 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 <storm::dd::DdType Type, typename ValueType>
+// class SeparateEdgesSystemComposer : public SystemComposer<Type, ValueType> {
+// public:
+// // This structure represents an edge.
+// struct EdgeDd {
+// EdgeDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> 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<Type, ValueType> guard;
+// storm::dd::Add<Type, ValueType> transitions;
+// std::set<storm::expressions::Variable> writtenGlobalVariables;
+// std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
+// };
+//
+// // This structure represents a subcomponent of a composition.
+// struct AutomatonDd {
+// AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
+// // Intentionally left empty.
+// }
+//
+// std::map<uint64_t, std::vector<EdgeDd>> actionIndexToEdges;
+// storm::dd::Add<Type, ValueType> identity;
+// };
+//
+// SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : SystemComposer<Type, ValueType>(model, variables) {
+// // Intentionally left empty.
+// }
+//
+// ComposerResult<Type, ValueType> compose() override {
+// AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(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<AutomatonDd>(composition.getSubcomposition().accept(*this, boost::none));
+//
+// // Build a mapping from indices to indices for the renaming.
+// std::map<uint64_t, uint64_t> 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<AutomatonDd>(composition.getLeftSubcomposition().accept(*this, boost::none));
+// AutomatonDd rightSubautomaton = boost::any_cast<AutomatonDd>(composition.getRightSubcomposition().accept(*this, boost::none));
+//
+// // Build the set of synchronizing action indices.
+// std::set<uint64_t> 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<Type, ValueType> combineEdgesBySummation(std::vector<EdgeDd> const& edges, CompositionVariables<Type, ValueType> const& variables) {
+// storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+// 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<uint64_t, storm::dd::Add<Type, ValueType>> combineEdgesByNondeterministicChoice(std::vector<EdgeDd>& 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<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
+// for (auto const& edge : edges) {
+// sumOfGuards += edge.guard;
+// }
+// uint_fast64_t maxChoices = static_cast<uint_fast64_t>(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<ValueType>());
+// } 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<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
+//
+// storm::dd::Add<Type, ValueType> allEdges = this->variables.manager->template getAddZero<ValueType>();
+//
+// storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
+// std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, this->variables.manager->template getAddZero<ValueType>());
+// std::vector<storm::dd::Bdd<Type>> 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<double>(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<ValueType>();
+// 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<Type> 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<Type> 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<ValueType>() * 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<ValueType>();
+// }
+//
+// return std::make_pair(numberOfBinaryVariables, allEdges);
+// }
+// }
+//
+// storm::dd::Bdd<Type> computeIllegalFragmentFromEdges(std::map<uint64_t, std::vector<EdgeDd>> const& actionIndexToEdges) {
+// // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times.
+// storm::dd::Bdd<Type> 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<Type, ValueType> 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<uint64_t, std::pair<uint64_t, storm::dd::Add<Type, ValueType>>> 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<uint64_t, storm::dd::Add<Type, ValueType>> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second);
+// actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd);
+// highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first);
+// }
+//
+// storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
+// for (auto const& element : actionIndexToUsedVariablesAndDd) {
+// result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables);
+// }
+//
+// return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables);
+// } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
+// storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
+// for (auto const& action : automatonDd.actionIndexToEdges) {
+// result += combineEdgesBySummation(action.second, this->variables);
+// }
+// return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0);
+// }
+//
+// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+// }
+//
+// storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables<Type, ValueType> const& variables) {
+// std::set<storm::expressions::Variable> missingIdentities;
+// std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+// storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
+// for (auto const& variable : missingIdentities) {
+// identityEncoding *= variables.variableToIdentityMap.at(variable);
+// }
+// return identityEncoding;
+// }
+//
+// EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add<Type, ValueType> 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<ValueType>();
+// return result;
+// }
+//
+// // Compute the set of variables written multiple times by the composition.
+// std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
+// std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
+//
+// std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
+// std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
+//
+// std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<Type, ValueType> 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<EdgeDestinationDd<Type, ValueType>> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
+// 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<ValueType>() * 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<ValueType>(), this->variables.manager->template getAddZero<ValueType>());
+// }
+// }
+//
+// /*!
+// * 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 <storm::dd::DdType Type, typename ValueType>
class CombinedEdgesSystemComposer : public SystemComposer<Type, ValueType> {
@@ -956,6 +958,10 @@ namespace storm {
std::pair<uint64_t, uint64_t> const& getLocalNondeterminismVariables() const {
return localNondeterminismVariables;
}
+
+ ActionDd multiplyTransitions(storm::dd::Add<Type, ValueType> 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<Type, ValueType> guard;
@@ -1014,27 +1020,30 @@ namespace storm {
// The identity of the automaton's variables.
storm::dd::Add<Type, ValueType> 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<uint64_t, uint64_t> localNondeterminismVariables;
};
- CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables) {
+ CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) {
// Intentionally left empty.
}
+
+ storm::jani::ActionInformation const& actionInformation;
ComposerResult<Type, ValueType> compose() override {
- std::map<uint_fast64_t, uint_fast64_t> actionIndexToLocalNondeterminismVariableOffset;
- for (auto const& action : this->model.getActions()) {
- actionIndexToLocalNondeterminismVariableOffset[this->model.getActionIndex(action.getName())] = 0;
+ std::map<uint64_t, uint64_t> actionIndexToLocalNondeterminismVariableOffset;
+ for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
+ actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
}
-
+ actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0;
+
AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
return buildSystemFromAutomaton(globalAutomaton);
}
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
- std::map<uint_fast64_t, uint_fast64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+ std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset);
}
@@ -1042,12 +1051,12 @@ namespace storm {
// Build a mapping from indices to indices for the renaming.
std::map<uint64_t, uint64_t> 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.");
@@ -1055,9 +1064,10 @@ namespace storm {
}
// Prepare the new offset mapping.
- std::map<uint_fast64_t, uint_fast64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
- std::map<uint_fast64_t, uint_fast64_t> newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset;
+ std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint64_t, uint64_t> const&>(data);
+ std::map<uint64_t, uint64_t> 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;
@@ -1071,81 +1081,142 @@ namespace storm {
}
boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
- // Build the set of synchronizing action indices.
- std::set<uint64_t> 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<AutomatonDd>(composition.getLeftSubcomposition().accept(*this, data));
-
- // Prepare the new offset mapping.
std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint64_t, uint64_t> const&>(data);
- std::map<uint64_t, uint64_t> 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<AutomatonDd> subautomata;
+ for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) {
+ // Prepare the new offset mapping.
+ std::map<uint64_t, uint64_t> 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<AutomatonDd>(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap)));
}
- // Then translate the right subcomposition.
- AutomatonDd right = boost::any_cast<AutomatonDd>(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<uint64_t> const& synchronizingActionIndices) {
- AutomatonDd result(automaton1);
- 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());
+ AutomatonDd composeInParallel(std::vector<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) {
+ AutomatonDd result(this->variables.manager->template getAddOne<ValueType>());
+
+ std::map<uint64_t, std::vector<ActionDd>> nonSynchronizingActions;
+ std::vector<boost::optional<ActionDd>> 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);
+
+ // Initilize the used local nondeterminism variables appropriately.
+ if (automatonIndex == 0) {
+ result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable());
+ result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable());
+ }
+
+ // Compose the actions according to the synchronization vectors.
+ std::set<uint64_t> actionsInSynch;
+ 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);
+
+ // 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()) {
+ 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.
+ if (synchronizationVectorActions[synchVectorIndex]) {
+ auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
+ if (inputActionIt != subautomaton.actionIndexToAction.end()) {
+ 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.
+ synchronizationVectorActions[synchVectorIndex] = boost::none;
+ }
+ }
+ }
+ }
+
+ // Now treat all unsynchronizing actions.
+ 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);
+ }
}
} else {
- // If we don't synchronize over this action, we need to construct the interleaving.
+ // 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;
+ }
+ }
- // 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());
- } 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);
+ // 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));
+ }
}
}
+
+ // Finally, construct combined identity.
+ result.identity *= subautomaton.identity;
}
- // 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);
- }
+ // 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());
}
}
- result.identity = automaton1.identity * automaton2.identity;
+ // 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<ActionDd> 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;
}
@@ -1190,56 +1261,67 @@ namespace storm {
}
ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2) {
+ return combineUnsynchronizedActions({action1, action2});
+ }
+
+ ActionDd combineUnsynchronizedActions(std::vector<ActionDd> 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<uint64_t, uint64_t>(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<uint64_t, uint64_t>(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<Type, ValueType> nondeterminismEncoding = this->variables.manager->template getAddOne<ValueType>();
-
- 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<ValueType>();
}
- action2.transitions *= nondeterminismEncoding;
-
- for (auto& transientAssignment : action2.transientEdgeAssignments) {
- transientAssignment.second *= nondeterminismEncoding;
- }
- } else if (action2.getHighestLocalNondeterminismVariable() > action1.getHighestLocalNondeterminismVariable()) {
- storm::dd::Add<Type, ValueType> nondeterminismEncoding = this->variables.manager->template getAddOne<ValueType>();
+ action.transitions *= nondeterminismEncoding;
- for (uint_fast64_t i = action1.getHighestLocalNondeterminismVariable(); i < action2.getHighestLocalNondeterminismVariable(); ++i) {
- nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd<ValueType>();
- }
- 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<Type, ValueType> 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<uint64_t>(std::ceil(std::log2(actions.size())));
+ storm::dd::Bdd<Type> guard = this->variables.manager->getBddZero();
+ storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
+ std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
+ std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> variableToWritingFragment;
+ storm::dd::Bdd<Type> 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<Type, ValueType> nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables);
+ transitions += nondeterminismEncoding * action.transitions;
+
+ joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments);
+
+ storm::dd::Bdd<Type> 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<ValueType>(), 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<ValueType>(), transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type.");
}
@@ -1476,7 +1558,13 @@ namespace storm {
globalVariableToWritingFragment.emplace(variable, partToAdd);
}
}
-
+
+ void addToVariableWritingFragmentMap(std::map<storm::expressions::Variable, storm::dd::Bdd<Type>>& globalVariableToWritingFragment, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& partToAdd) const {
+ for (auto const& entry : partToAdd) {
+ addToVariableWritingFragmentMap(globalVariableToWritingFragment, entry.first, entry.second);
+ }
+ }
+
std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> joinVariableWritingFragmentMaps(std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& globalVariableToWritingFragment1, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& globalVariableToWritingFragment2) {
std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> result = globalVariableToWritingFragment1;
@@ -1752,7 +1840,13 @@ namespace storm {
storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::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<Type, ValueType> 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.
@@ -1909,16 +2003,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<Type, ValueType> variableCreator(model);
+ CompositionVariableCreator<Type, ValueType> variableCreator(model, actionInformation);
CompositionVariables<Type, ValueType> variables = variableCreator.create();
// Determine which transient assignments need to be considered in the building process.
std::vector<storm::expressions::Variable> rewardVariables = selectRewardVariables<Type, ValueType>(model, options);
// Create a builder to compose and build the model.
-// SeparateEdgesSystemComposer<Type, ValueType> composer(model, variables);
- CombinedEdgesSystemComposer<Type, ValueType> composer(model, variables, rewardVariables);
+ CombinedEdgesSystemComposer<Type, ValueType> composer(model, actionInformation, variables, rewardVariables);
ComposerResult<Type, ValueType> system = composer.compose();
// Postprocess the variables in place.
@@ -1964,4 +2061,4 @@ namespace storm {
template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
}
-}
\ No newline at end of file
+}
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<Type, ValueType>(stateRewards, stateActionRewards, transitionRewards);
}
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<typename ValueType, typename StateType>
- Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), choiceRewards() {
+ Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), rewards(), labels() {
// Intentionally left empty.
}
@@ -33,24 +33,24 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void Choice<ValueType, StateType>::addChoiceLabel(uint_fast64_t label) {
- if (!choiceLabels) {
- choiceLabels = LabelSet();
+ void Choice<ValueType, StateType>::addLabel(uint_fast64_t label) {
+ if (!labels) {
+ labels = LabelSet();
}
- choiceLabels->insert(label);
+ labels->insert(label);
}
template<typename ValueType, typename StateType>
- void Choice<ValueType, StateType>::addChoiceLabels(LabelSet const& labelSet) {
- if (!choiceLabels) {
- choiceLabels = LabelSet();
+ void Choice<ValueType, StateType>::addLabels(LabelSet const& labelSet) {
+ if (!labels) {
+ labels = LabelSet();
}
- choiceLabels->insert(labelSet.begin(), labelSet.end());
+ labels->insert(labelSet.begin(), labelSet.end());
}
template<typename ValueType, typename StateType>
- boost::container::flat_set<uint_fast64_t> const& Choice<ValueType, StateType>::getChoiceLabels() const {
- return *choiceLabels;
+ boost::container::flat_set<uint_fast64_t> const& Choice<ValueType, StateType>::getLabels() const {
+ return *labels;
}
template<typename ValueType, typename StateType>
@@ -70,13 +70,18 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void Choice<ValueType, StateType>::addChoiceReward(ValueType const& value) {
- choiceRewards.push_back(value);
+ void Choice<ValueType, StateType>::addReward(ValueType const& value) {
+ rewards.push_back(value);
}
template<typename ValueType, typename StateType>
- std::vector<ValueType> const& Choice<ValueType, StateType>::getChoiceRewards() const {
- return choiceRewards;
+ void Choice<ValueType, StateType>::addRewards(std::vector<ValueType>&& values) {
+ this->rewards = std::move(values);
+ }
+
+ template<typename ValueType, typename StateType>
+ std::vector<ValueType> const& Choice<ValueType, StateType>::getRewards() const {
+ return rewards;
}
template<typename ValueType, typename StateType>
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<ValueType>&& values);
/*!
* Retrieves the rewards for this choice under selected reward models.
*/
- std::vector<ValueType> const& getChoiceRewards() const;
+ std::vector<ValueType> 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<ValueType> choiceRewards;
+ std::vector<ValueType> rewards;
// The labels that are associated with this choice.
- boost::optional<LabelSet> choiceLabels;
+ boost::optional<LabelSet> labels;
};
template<typename ValueType, typename StateType>
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<typename ValueType, typename StateType>
- JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables() {
+ JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(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<ValueType> 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<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
+
// 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<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
+ 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<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+ std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
currentTargetStates->emplace(state, storm::utility::one<ValueType>());
@@ -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<ValueType>& 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<ValueType>();
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> 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.
diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp
index bae32c108..ded8bb457 100644
--- a/src/storage/dd/Dd.cpp
+++ b/src/storage/dd/Dd.cpp
@@ -87,4 +87,4 @@ namespace storm {
template class Dd<storm::dd::DdType::CUDD>;
template class Dd<storm::dd::DdType::Sylvan>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h
index 18605c259..ae9728263 100644
--- a/src/storage/dd/Dd.h
+++ b/src/storage/dd/Dd.h
@@ -30,6 +30,8 @@ namespace storm {
Dd(Dd<LibraryType>&& other) = default;
Dd& operator=(Dd<LibraryType>&& other) = default;
+ virtual ~Dd() = default;
+
/*!
* 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.cpp b/src/storage/jani/Automaton.cpp
index 6b11d29a0..9bb469693 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -402,6 +402,14 @@ namespace storm {
edge.finalize(containingModel);
}
}
+
+ std::set<uint64_t> Automaton::getUsedActionIndices() const {
+ std::set<uint64_t> 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 539e7df5e..ad61a1b69 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -299,6 +299,11 @@ namespace storm {
*/
void finalize(Model const& containingModel);
+ /*!
+ * Retrieves the action indices appearing at some edge of the automaton.
+ */
+ std::set<uint64_t> getUsedActionIndices() const;
+
private:
/// The name of the automaton.
std::string name;
@@ -330,4 +335,4 @@ namespace storm {
};
}
-}
\ 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..683995d07
--- /dev/null
+++ b/src/storage/jani/CompositionActionInformationVisitor.cpp
@@ -0,0 +1,144 @@
+#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<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap, uint64_t silentActionIndex) : silentActionIndex(silentActionIndex), 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<uint64_t> 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.
+ }
+
+ 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()) {
+ 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;
+
+ std::set<uint64_t> nonSilentActionIndices = boost::any_cast<std::set<uint64_t>>(model.getSystemComposition().accept(*this, boost::none));
+
+ return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap);
+ }
+
+ boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
+ std::set<uint64_t> result = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices();
+ result.erase(model.getSilentActionIndex());
+ return result;
+ }
+
+ boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
+ std::set<uint64_t> usedActions = boost::any_cast<std::set<uint64_t>>(composition.getSubcomposition().accept(*this, boost::none));
+
+ std::set<uint64_t> 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<std::set<uint64_t>> subresults;
+ for (auto const& subcomposition : composition.getSubcompositions()) {
+ subresults.push_back(boost::any_cast<std::set<uint64_t>>(subcomposition->accept(*this, boost::none)));
+ }
+
+ std::set<uint64_t> 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<uint64_t> result;
+ for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) {
+
+ std::set<uint64_t> actionsInSynch;
+ std::set<uint64_t> 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<uint64_t> 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..705773c27
--- /dev/null
+++ b/src/storage/jani/CompositionActionInformationVisitor.h
@@ -0,0 +1,50 @@
+#pragma once
+
+#include <set>
+#include <map>
+
+#include "src/storage/jani/CompositionVisitor.h"
+
+namespace storm {
+ namespace jani {
+
+ class Model;
+
+ class ActionInformation {
+ public:
+ ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap, uint64_t silentActionIndex = 0);
+
+ std::string const& getActionName(uint64_t index) const;
+ uint64_t getActionIndex(std::string const& name) const;
+ std::set<uint64_t> const& getNonSilentActionIndices() const;
+ uint64_t getSilentActionIndex() const;
+
+ private:
+ uint64_t silentActionIndex;
+ std::set<uint64_t> nonsilentActionIndices;
+ std::map<uint64_t, std::string> indexToNameMap;
+ std::map<std::string, uint64_t> 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<std::string, uint64_t> nameToIndexMap;
+ std::map<uint64_t, std::string> indexToNameMap;
+ };
+
+
+ }
+}
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<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) {
+ CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> 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<std::string, uint64_t> CompositionInformation::joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second) {
@@ -90,30 +90,61 @@ namespace storm {
boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
CompositionInformation subresult = boost::any_cast<CompositionInformation>(composition.getSubcomposition().accept(*this, data));
std::set<std::string> 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<CompositionInformation>(composition.getLeftSubcomposition().accept(*this, data));
- CompositionInformation right = boost::any_cast<CompositionInformation>(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<std::string, uint64_t> joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap());
+ std::vector<CompositionInformation> subinformation;
- std::set<std::string> 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<CompositionInformation>(subcomposition->accept(*this, data)));
+ }
+
+ std::map<std::string, uint64_t> 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<std::string> 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<uint64_t> 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<std::string> nonsilentActions;
+ for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) {
+ auto const& subinfo = subinformation[infoIndex];
+
+ std::set<uint64_t> 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<uint64_t> 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<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition);
+ CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> 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<std::string, uint64_t> joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second);
std::map<std::string, uint64_t> 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 619324ae7..5242a7d88 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<std::string, uint64_t> const& Model::getActionToIndexMap() const {
+ return actionToIndex;
+ }
+
std::vector<Action> const& Model::getActions() const {
return actions;
}
@@ -458,7 +462,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 bade96875..32bd1fa2b 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<std::string, uint64_t> 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..7e453eb0f 100644
--- a/src/storage/jani/ParallelComposition.cpp
+++ b/src/storage/jani/ParallelComposition.cpp
@@ -1,32 +1,138 @@
#include "src/storage/jani/ParallelComposition.h"
+#include <sstream>
+
#include <boost/algorithm/string/join.hpp>
+#include "src/utility/macros.h"
+#include "src/exceptions/WrongFormatException.h"
+
namespace storm {
namespace jani {
- ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) {
+ SynchronizationVector::SynchronizationVector(std::vector<std::string> 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<std::string> 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<std::string> const& ParallelComposition::getSynchronizationAlphabet() const {
- return alphabet;
+ ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> 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<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> 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<std::string>(this->subcompositions.size(), action), action);
+ }
+ }
+
+ ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> 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<std::string>(this->subcompositions.size(), action), action);
+ }
+ }
+
+ Composition const& ParallelComposition::getSubcomposition(uint64_t index) const {
+ return *subcompositions[index];
+ }
+
+ std::vector<std::shared_ptr<Composition>> 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<SynchronizationVector> const& ParallelComposition::getSynchronizationVectors() const {
+ return synchronizationVectors;
+ }
+
+ std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const {
+ return synchronizationVectors.size();
+ }
+
+ void ParallelComposition::checkSynchronizationVectors() const {
+ for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) {
+ std::set<std::string> 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 vectors.");
+ actions.insert(action);
+ }
+ }
+
+ std::set<std::string> 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 {
return visitor.visit(*this, data);
}
void ParallelComposition::write(std::ostream& stream) const {
- stream << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(alphabet, ", ") << "]| " << this->getRightSubcomposition();
+ std::vector<std::string> 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..3138261a8 100644
--- a/src/storage/jani/ParallelComposition.h
+++ b/src/storage/jani/ParallelComposition.h
@@ -2,47 +2,95 @@
#include <set>
#include <memory>
+#include <vector>
+#include <string>
#include "src/storage/jani/Composition.h"
namespace storm {
namespace jani {
+ class SynchronizationVector {
+ public:
+ SynchronizationVector(std::vector<std::string> const& input, std::string const& output);
+
+ std::size_t size() const;
+ std::vector<std::string> const& getInput() const;
+ std::string const& getInput(uint64_t index) const;
+ std::string const& getOutput() const;
+
+ private:
+ /// The input to the synchronization.
+ std::vector<std::string> 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<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet = {});
-
+ ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> 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<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> 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<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& synchronizationAlphabet);
/*!
- * Retrieves the alphabet of actions over which to synchronize the automata.
+ * Retrieves the subcomposition with the given index.
*/
- std::set<std::string> const& getSynchronizationAlphabet() const;
+ Composition const& getSubcomposition(uint64_t index) const;
+
+ /*!
+ * Retrieves the subcompositions of the parallel composition.
+ */
+ std::vector<std::shared_ptr<Composition>> 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<SynchronizationVector> 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<Composition> leftSubcomposition;
+ /*!
+ * Checks the synchronization vectors for validity.
+ */
+ void checkSynchronizationVectors() const;
- // The right subcomposition.
- std::shared_ptr<Composition> rightSubcomposition;
+ /// The subcompositions.
+ std::vector<std::shared_ptr<Composition>> subcompositions;
- // The alphabet of actions over which to synchronize.
- std::set<std::string> alphabet;
+ /// The synchronization vectors of the parallel composition.
+ std::vector<SynchronizationVector> 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.
diff --git a/src/storage/sparse/StateValuations.cpp b/src/storage/sparse/StateValuations.cpp
index f3f98818f..522d09f27 100644
--- a/src/storage/sparse/StateValuations.cpp
+++ b/src/storage/sparse/StateValuations.cpp
@@ -7,11 +7,11 @@ namespace storm {
StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) {
// 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..aa7d2c30e 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() = default;
+
// A mapping from state indices to their variable valuations.
std::vector<storm::expressions::SimpleValuation> 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_ */
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<storm::dd::DdType::CUDD, double> builder;
EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> 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<storm::dd::DdType::Sylvan, double> builder;
+ EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> 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<storm::dd::DdType::CUDD, double> builder;
+
+ // Start by checking the original composition.
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> 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<std::shared_ptr<storm::jani::Composition>> automataCompositions;
+ automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
+ automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
+ automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three"));
+
+ // First, make all actions non-synchronizing.
+ std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
+ std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(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<std::string> 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<storm::jani::ParallelComposition>(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<storm::jani::ParallelComposition>(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/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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::settings::SettingMemento> 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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::settings::SettingMemento> 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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -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<storm::dd::DdType::Sylvan>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -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<storm::dd::DdType::Sylvan>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -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<storm::dd::DdType::Sylvan>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -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<storm::dd::DdType::Sylvan>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
-
+
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -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<storm::dd::DdType::CUDD>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -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<storm::dd::DdType::CUDD>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -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<storm::dd::DdType::CUDD>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -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<storm::dd::DdType::CUDD>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -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<storm::dd::DdType::CUDD>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().build(program);
-
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
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]
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<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -123,7 +125,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -220,7 +223,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -299,7 +303,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -378,7 +383,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -414,7 +420,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -457,7 +464,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -545,7 +553,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
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<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -122,7 +124,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -219,7 +222,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -298,7 +302,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -377,7 +382,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -413,7 +419,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -456,7 +463,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> formula(nullptr);
@@ -546,7 +554,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
std::unique_ptr<storm::settings::SettingMemento> 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<storm::logic::Formula const> 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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::dd::DdType::Sylvan>().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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(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<double>(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<double>(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::models::sparse::Mdp<double>>(), 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
+}