diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 2addcba41..9f700c9ef 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 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 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>(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 createVariables() { CompositionVariables result; - for (auto const& action : this->model.getActions()) { - if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) { - std::pair variablePair = result.manager->addMetaVariable(action.getName()); - result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first; - result.allNondeterminismVariables.insert(variablePair.first); - } + for (auto const& nonSilentActionIndex : actionInformation.getNonSilentActionIndices()) { + std::pair variablePair = result.manager->addMetaVariable(actionInformation.getActionName(nonSilentActionIndex)); + result.actionVariablesMap[nonSilentActionIndex] = variablePair.first; + result.allNondeterminismVariables.insert(variablePair.first); } - + // FIXME: check how many nondeterminism variables we should actually allocate. uint64_t numberOfNondeterminismVariables = this->model.getNumberOfAutomata(); for (auto const& automaton : this->model.getAutomata()) { @@ -350,6 +351,7 @@ namespace storm { storm::jani::Model const& model; std::set automata; + storm::jani::ActionInformation actionInformation; }; template @@ -488,434 +490,434 @@ namespace storm { return result; } - template - class SeparateEdgesSystemComposer : public SystemComposer { - public: - // This structure represents an edge. - struct EdgeDd { - EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { - // Intentionally left empty. - } - - EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { - // Intentionally left empty. - } - - EdgeDd& operator=(EdgeDd const& other) { - if (this != &other) { - globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes; - writtenGlobalVariables = other.writtenGlobalVariables; - guard = other.guard; - transitions = other.transitions; - } - return *this; - } - - storm::dd::Add guard; - storm::dd::Add transitions; - std::set writtenGlobalVariables; - std::set globalVariablesWrittenMultipleTimes; - }; - - // This structure represents a subcomponent of a composition. - struct AutomatonDd { - AutomatonDd(storm::dd::Add const& identity) : identity(identity) { - // Intentionally left empty. - } - - std::map> actionIndexToEdges; - storm::dd::Add identity; - }; - - SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { - // Intentionally left empty. - } - - ComposerResult compose() override { - AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); - return buildSystemFromAutomaton(globalAutomaton); - } - - boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - return buildAutomatonDd(composition.getAutomatonName()); - } - - boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); - - // Build a mapping from indices to indices for the renaming. - std::map renamingIndexToIndex; - for (auto const& entry : composition.getRenaming()) { - if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { - // Distinguish the cases where we hide the action or properly rename it. - if (entry.second) { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get())); - } else { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); - } - } - - // Finally, apply the renaming. - AutomatonDd result(subautomaton.identity); - for (auto const& actionEdges : subautomaton.actionIndexToEdges) { - auto it = renamingIndexToIndex.find(actionEdges.first); - if (it != renamingIndexToIndex.end()) { - // If we are to rename the action, do so. - result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end()); - } else { - // Otherwise copy over the edges. - result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end()); - } - } - return result; - } - - boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - AutomatonDd leftSubautomaton = boost::any_cast(composition.getLeftSubcomposition().accept(*this, boost::none)); - AutomatonDd rightSubautomaton = boost::any_cast(composition.getRightSubcomposition().accept(*this, boost::none)); - - // Build the set of synchronizing action indices. - std::set synchronizingActionIndices; - for (auto const& entry : composition.getSynchronizationAlphabet()) { - if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) { - synchronizingActionIndices.insert(this->model.getActionIndex(entry)); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action."); - } - } - - // Perform the composition. - - // First, consider all actions in the left subcomposition. - AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); - uint64_t index = 0; - for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { - // If we need to synchronize over this action, do so now. - if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { - auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first); - if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { - for (auto const& edge1 : actionEdges.second) { - for (auto const& edge2 : rightIt->second) { - EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); - if (!edgeDd.guard.isZero()) { - result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); - } - index++; - } - } - } - } else { - // Extend all edges by the missing identity (unsynchronizing) and copy them over. - for (auto const& edge : actionEdges.second) { - result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity)); - } - } - } - - // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because - // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none, - // such transitions can not be taken and we can drop them. - for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) { - if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) { - for (auto const& edge : actionEdges.second) { - result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity)); - } - } - } - - return result; - } - - private: - storm::dd::Add combineEdgesBySummation(std::vector const& edges, CompositionVariables const& variables) { - storm::dd::Add result = variables.manager->template getAddZero(); - for (auto const& edge : edges) { - // Simply add all actions, but make sure to include the missing global variable identities. - result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables); - } - return result; - } - - std::pair> combineEdgesByNondeterministicChoice(std::vector& edges) { - // Complete all edges by adding the missing global variable identities. - for (auto& edge : edges) { - edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables); - } - - // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); - for (auto const& edge : edges) { - sumOfGuards += edge.guard; - } - uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); - STORM_LOG_TRACE("Found " << maxChoices << " local choices."); - - // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. - if (maxChoices == 0) { - return std::make_pair(0, this->variables.manager->template getAddZero()); - } else if (maxChoices == 1) { - return std::make_pair(0, combineEdgesBySummation(edges, this->variables)); - } else { - // Calculate number of required variables to encode the nondeterminism. - uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - - storm::dd::Add allEdges = this->variables.manager->template getAddZero(); - - storm::dd::Bdd equalsNumberOfChoicesDd; - std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); - std::vector> remainingDds(maxChoices, this->variables.manager->getBddZero()); - - for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { - // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast(currentChoices))); - - // If there is no such state, continue with the next possible number of choices. - if (equalsNumberOfChoicesDd.isZero()) { - continue; - } - - // Reset the previously used intermediate storage. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - choiceDds[j] = this->variables.manager->template getAddZero(); - remainingDds[j] = equalsNumberOfChoicesDd; - } - - for (std::size_t j = 0; j < edges.size(); ++j) { - // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices - // choices such that one outgoing choice is given by the j-th edge. - storm::dd::Bdd guardChoicesIntersection = edges[j].guard.toBdd() && equalsNumberOfChoicesDd; - - // If there is no such state, continue with the next command. - if (guardChoicesIntersection.isZero()) { - continue; - } - - // Split the currentChoices nondeterministic choices. - for (uint_fast64_t k = 0; k < currentChoices; ++k) { - // Calculate the overlapping part of command guard and the remaining DD. - storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; - - // Check if we can add some overlapping parts to the current index. - if (!remainingGuardChoicesIntersection.isZero()) { - // Remove overlapping parts from the remaining DD. - remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; - - // Combine the overlapping part of the guard with command updates and add it to the resulting DD. - choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * edges[j].transitions; - } - - // Remove overlapping parts from the command guard DD - guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; - - // If the guard DD has become equivalent to false, we can stop here. - if (guardChoicesIntersection.isZero()) { - break; - } - } - } - - // Add the meta variables that encode the nondeterminisim to the different choices. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j]; - } - - // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); - } - - return std::make_pair(numberOfBinaryVariables, allEdges); - } - } - - storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { - // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. - storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); - for (auto const& action : actionIndexToEdges) { - for (auto const& edge : action.second) { - if (!edge.globalVariablesWrittenMultipleTimes.empty()) { - for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { - STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); - illegalFragment |= edge.guard.toBdd(); - } - } - } - } - return illegalFragment; - } - - ComposerResult buildSystemFromAutomaton(AutomatonDd& automatonDd) { - // If the model is an MDP, we need to encode the nondeterminism using additional variables. - if (this->model.getModelType() == storm::jani::ModelType::MDP) { - std::map>> actionIndexToUsedVariablesAndDd; - - // Combine the edges of each action individually and keep track of how many local nondeterminism variables - // were used. - uint64_t highestNumberOfUsedNondeterminismVariables = 0; - for (auto& action : automatonDd.actionIndexToEdges) { - std::pair> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second); - actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); - highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); - } - - storm::dd::Add result = this->variables.manager->template getAddZero(); - for (auto const& element : actionIndexToUsedVariablesAndDd) { - result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); - } - - return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables); - } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { - storm::dd::Add result = this->variables.manager->template getAddZero(); - for (auto const& action : automatonDd.actionIndexToEdges) { - result += combineEdgesBySummation(action.second, this->variables); - } - return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); - } - - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); - } - - storm::dd::Add computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables const& variables) { - std::set missingIdentities; - std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - storm::dd::Add identityEncoding = variables.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - identityEncoding *= variables.variableToIdentityMap.at(variable); - } - return identityEncoding; - } - - EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add const& identity) { - EdgeDd result(edge); - result.transitions *= identity; - return result; - } - - EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { - EdgeDd result; - - // Compose the guards. - result.guard = edge1.guard * edge2.guard; - - // If the composed guard is already zero, we can immediately return an empty result. - if (result.guard.isZero()) { - result.transitions = edge1.transitions.getDdManager().template getAddZero(); - return result; - } - - // Compute the set of variables written multiple times by the composition. - std::set oldVariablesWrittenMultipleTimes; - std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); - - std::set newVariablesWrittenMultipleTimes; - std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin())); - - std::set variablesWrittenMultipleTimes; - std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin())); - - result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes); - - // Compute the set of variables written by the composition. - std::set variablesWritten; - std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin())); - - result.writtenGlobalVariables = variablesWritten; - - // Compose the guards. - result.guard = edge1.guard * edge2.guard; - - // Compose the transitions. - result.transitions = edge1.transitions * edge2.transitions; - - return result; - } - - /*! - * Builds the DD for the given edge. - */ - EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { - STORM_LOG_TRACE("Translating guard " << edge.getGuard()); - storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName()); - STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); - - if (!guard.isZero()) { - // Create the DDs representing the individual updates. - std::vector> destinationDds; - for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { - destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables)); - - STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); - } - - // Start by gathering all variables that were written in at least one update. - std::set globalVariablesInSomeUpdate; - - // If the edge is not labeled with the silent action, we have to analyze which portion of the global - // variables was written by any of the updates and make all update results equal w.r.t. this set. If - // the edge is labeled with the silent action, we can already multiply the identities of all global variables. - if (edge.getActionIndex() != this->model.getSilentActionIndex()) { - for (auto const& edgeDestinationDd : destinationDds) { - globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); - } - } else { - globalVariablesInSomeUpdate = this->variables.allGlobalVariables; - } - - // Then, multiply the missing identities. - for (auto& destinationDd : destinationDds) { - std::set missingIdentities; - std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - - for (auto const& variable : missingIdentities) { - STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD."); - destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable); - } - } - - // Now combine the destination DDs to the edge DD. - storm::dd::Add transitions = this->variables.manager->template getAddZero(); - for (auto const& destinationDd : destinationDds) { - transitions += destinationDd.transitions; - } - - // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; - - // If we multiply the ranges of global variables, make sure everything stays within its bounds. - if (!globalVariablesInSomeUpdate.empty()) { - transitions *= this->variables.globalVariableRanges; - } - - // If the edge has a rate, we multiply it to the DD. - if (edge.hasRate()) { - transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); - } - return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); - } else { - return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); - } - } - - /*! - * Builds the DD for the automaton with the given name. - */ - AutomatonDd buildAutomatonDd(std::string const& automatonName) { - AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); - - storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); - for (auto const& edge : automaton.getEdges()) { - // Build the edge and add it if it adds transitions. - EdgeDd edgeDd = buildEdgeDd(automaton, edge); - if (!edgeDd.guard.isZero()) { - result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd); - } - } - - return result; - } - }; +// template +// class SeparateEdgesSystemComposer : public SystemComposer { +// public: +// // This structure represents an edge. +// struct EdgeDd { +// EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { +// // Intentionally left empty. +// } +// +// EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { +// // Intentionally left empty. +// } +// +// EdgeDd& operator=(EdgeDd const& other) { +// if (this != &other) { +// globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes; +// writtenGlobalVariables = other.writtenGlobalVariables; +// guard = other.guard; +// transitions = other.transitions; +// } +// return *this; +// } +// +// storm::dd::Add guard; +// storm::dd::Add transitions; +// std::set writtenGlobalVariables; +// std::set globalVariablesWrittenMultipleTimes; +// }; +// +// // This structure represents a subcomponent of a composition. +// struct AutomatonDd { +// AutomatonDd(storm::dd::Add const& identity) : identity(identity) { +// // Intentionally left empty. +// } +// +// std::map> actionIndexToEdges; +// storm::dd::Add identity; +// }; +// +// SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { +// // Intentionally left empty. +// } +// +// ComposerResult compose() override { +// AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); +// return buildSystemFromAutomaton(globalAutomaton); +// } +// +// boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { +// return buildAutomatonDd(composition.getAutomatonName()); +// } +// +// boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { +// AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); +// +// // Build a mapping from indices to indices for the renaming. +// std::map renamingIndexToIndex; +// for (auto const& entry : composition.getRenaming()) { +// if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { +// // Distinguish the cases where we hide the action or properly rename it. +// if (entry.second) { +// renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get())); +// } else { +// renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); +// } +// } else { +// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); +// } +// } +// +// // Finally, apply the renaming. +// AutomatonDd result(subautomaton.identity); +// for (auto const& actionEdges : subautomaton.actionIndexToEdges) { +// auto it = renamingIndexToIndex.find(actionEdges.first); +// if (it != renamingIndexToIndex.end()) { +// // If we are to rename the action, do so. +// result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end()); +// } else { +// // Otherwise copy over the edges. +// result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end()); +// } +// } +// return result; +// } +// +// boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { +// AutomatonDd leftSubautomaton = boost::any_cast(composition.getLeftSubcomposition().accept(*this, boost::none)); +// AutomatonDd rightSubautomaton = boost::any_cast(composition.getRightSubcomposition().accept(*this, boost::none)); +// +// // Build the set of synchronizing action indices. +// std::set synchronizingActionIndices; +// for (auto const& entry : composition.getSynchronizationAlphabet()) { +// if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) { +// synchronizingActionIndices.insert(this->model.getActionIndex(entry)); +// } else { +// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action."); +// } +// } +// +// // Perform the composition. +// +// // First, consider all actions in the left subcomposition. +// AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); +// uint64_t index = 0; +// for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { +// // If we need to synchronize over this action, do so now. +// if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { +// auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first); +// if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { +// for (auto const& edge1 : actionEdges.second) { +// for (auto const& edge2 : rightIt->second) { +// EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); +// if (!edgeDd.guard.isZero()) { +// result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); +// } +// index++; +// } +// } +// } +// } else { +// // Extend all edges by the missing identity (unsynchronizing) and copy them over. +// for (auto const& edge : actionEdges.second) { +// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity)); +// } +// } +// } +// +// // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because +// // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none, +// // such transitions can not be taken and we can drop them. +// for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) { +// if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) { +// for (auto const& edge : actionEdges.second) { +// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity)); +// } +// } +// } +// +// return result; +// } +// +// private: +// storm::dd::Add combineEdgesBySummation(std::vector const& edges, CompositionVariables const& variables) { +// storm::dd::Add result = variables.manager->template getAddZero(); +// for (auto const& edge : edges) { +// // Simply add all actions, but make sure to include the missing global variable identities. +// result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables); +// } +// return result; +// } +// +// std::pair> combineEdgesByNondeterministicChoice(std::vector& edges) { +// // Complete all edges by adding the missing global variable identities. +// for (auto& edge : edges) { +// edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables); +// } +// +// // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. +// storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); +// for (auto const& edge : edges) { +// sumOfGuards += edge.guard; +// } +// uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); +// STORM_LOG_TRACE("Found " << maxChoices << " local choices."); +// +// // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. +// if (maxChoices == 0) { +// return std::make_pair(0, this->variables.manager->template getAddZero()); +// } else if (maxChoices == 1) { +// return std::make_pair(0, combineEdgesBySummation(edges, this->variables)); +// } else { +// // Calculate number of required variables to encode the nondeterminism. +// uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); +// +// storm::dd::Add allEdges = this->variables.manager->template getAddZero(); +// +// storm::dd::Bdd equalsNumberOfChoicesDd; +// std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); +// std::vector> remainingDds(maxChoices, this->variables.manager->getBddZero()); +// +// for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { +// // Determine the set of states with exactly currentChoices choices. +// equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast(currentChoices))); +// +// // If there is no such state, continue with the next possible number of choices. +// if (equalsNumberOfChoicesDd.isZero()) { +// continue; +// } +// +// // Reset the previously used intermediate storage. +// for (uint_fast64_t j = 0; j < currentChoices; ++j) { +// choiceDds[j] = this->variables.manager->template getAddZero(); +// remainingDds[j] = equalsNumberOfChoicesDd; +// } +// +// for (std::size_t j = 0; j < edges.size(); ++j) { +// // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices +// // choices such that one outgoing choice is given by the j-th edge. +// storm::dd::Bdd guardChoicesIntersection = edges[j].guard.toBdd() && equalsNumberOfChoicesDd; +// +// // If there is no such state, continue with the next command. +// if (guardChoicesIntersection.isZero()) { +// continue; +// } +// +// // Split the currentChoices nondeterministic choices. +// for (uint_fast64_t k = 0; k < currentChoices; ++k) { +// // Calculate the overlapping part of command guard and the remaining DD. +// storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; +// +// // Check if we can add some overlapping parts to the current index. +// if (!remainingGuardChoicesIntersection.isZero()) { +// // Remove overlapping parts from the remaining DD. +// remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; +// +// // Combine the overlapping part of the guard with command updates and add it to the resulting DD. +// choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * edges[j].transitions; +// } +// +// // Remove overlapping parts from the command guard DD +// guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; +// +// // If the guard DD has become equivalent to false, we can stop here. +// if (guardChoicesIntersection.isZero()) { +// break; +// } +// } +// } +// +// // Add the meta variables that encode the nondeterminisim to the different choices. +// for (uint_fast64_t j = 0; j < currentChoices; ++j) { +// allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j]; +// } +// +// // Delete currentChoices out of overlapping DD +// sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); +// } +// +// return std::make_pair(numberOfBinaryVariables, allEdges); +// } +// } +// +// storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { +// // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. +// storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); +// for (auto const& action : actionIndexToEdges) { +// for (auto const& edge : action.second) { +// if (!edge.globalVariablesWrittenMultipleTimes.empty()) { +// for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { +// STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); +// illegalFragment |= edge.guard.toBdd(); +// } +// } +// } +// } +// return illegalFragment; +// } +// +// ComposerResult buildSystemFromAutomaton(AutomatonDd& automatonDd) { +// // If the model is an MDP, we need to encode the nondeterminism using additional variables. +// if (this->model.getModelType() == storm::jani::ModelType::MDP) { +// std::map>> actionIndexToUsedVariablesAndDd; +// +// // Combine the edges of each action individually and keep track of how many local nondeterminism variables +// // were used. +// uint64_t highestNumberOfUsedNondeterminismVariables = 0; +// for (auto& action : automatonDd.actionIndexToEdges) { +// std::pair> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second); +// actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); +// highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); +// } +// +// storm::dd::Add result = this->variables.manager->template getAddZero(); +// for (auto const& element : actionIndexToUsedVariablesAndDd) { +// result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); +// } +// +// return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables); +// } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { +// storm::dd::Add result = this->variables.manager->template getAddZero(); +// for (auto const& action : automatonDd.actionIndexToEdges) { +// result += combineEdgesBySummation(action.second, this->variables); +// } +// return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); +// } +// +// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); +// } +// +// storm::dd::Add computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables const& variables) { +// std::set missingIdentities; +// std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); +// storm::dd::Add identityEncoding = variables.manager->template getAddOne(); +// for (auto const& variable : missingIdentities) { +// identityEncoding *= variables.variableToIdentityMap.at(variable); +// } +// return identityEncoding; +// } +// +// EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add const& identity) { +// EdgeDd result(edge); +// result.transitions *= identity; +// return result; +// } +// +// EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { +// EdgeDd result; +// +// // Compose the guards. +// result.guard = edge1.guard * edge2.guard; +// +// // If the composed guard is already zero, we can immediately return an empty result. +// if (result.guard.isZero()) { +// result.transitions = edge1.transitions.getDdManager().template getAddZero(); +// return result; +// } +// +// // Compute the set of variables written multiple times by the composition. +// std::set oldVariablesWrittenMultipleTimes; +// std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); +// +// std::set newVariablesWrittenMultipleTimes; +// std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin())); +// +// std::set variablesWrittenMultipleTimes; +// std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin())); +// +// result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes); +// +// // Compute the set of variables written by the composition. +// std::set variablesWritten; +// std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin())); +// +// result.writtenGlobalVariables = variablesWritten; +// +// // Compose the guards. +// result.guard = edge1.guard * edge2.guard; +// +// // Compose the transitions. +// result.transitions = edge1.transitions * edge2.transitions; +// +// return result; +// } +// +// /*! +// * Builds the DD for the given edge. +// */ +// EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { +// STORM_LOG_TRACE("Translating guard " << edge.getGuard()); +// storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName()); +// STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); +// +// if (!guard.isZero()) { +// // Create the DDs representing the individual updates. +// std::vector> destinationDds; +// for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { +// destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables)); +// +// STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); +// } +// +// // Start by gathering all variables that were written in at least one update. +// std::set globalVariablesInSomeUpdate; +// +// // If the edge is not labeled with the silent action, we have to analyze which portion of the global +// // variables was written by any of the updates and make all update results equal w.r.t. this set. If +// // the edge is labeled with the silent action, we can already multiply the identities of all global variables. +// if (edge.getActionIndex() != this->model.getSilentActionIndex()) { +// for (auto const& edgeDestinationDd : destinationDds) { +// globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); +// } +// } else { +// globalVariablesInSomeUpdate = this->variables.allGlobalVariables; +// } +// +// // Then, multiply the missing identities. +// for (auto& destinationDd : destinationDds) { +// std::set missingIdentities; +// std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); +// +// for (auto const& variable : missingIdentities) { +// STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD."); +// destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable); +// } +// } +// +// // Now combine the destination DDs to the edge DD. +// storm::dd::Add transitions = this->variables.manager->template getAddZero(); +// for (auto const& destinationDd : destinationDds) { +// transitions += destinationDd.transitions; +// } +// +// // Add the source location and the guard. +// transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; +// +// // If we multiply the ranges of global variables, make sure everything stays within its bounds. +// if (!globalVariablesInSomeUpdate.empty()) { +// transitions *= this->variables.globalVariableRanges; +// } +// +// // If the edge has a rate, we multiply it to the DD. +// if (edge.hasRate()) { +// transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); +// } +// return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); +// } else { +// return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); +// } +// } +// +// /*! +// * Builds the DD for the automaton with the given name. +// */ +// AutomatonDd buildAutomatonDd(std::string const& automatonName) { +// AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); +// +// storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); +// for (auto const& edge : automaton.getEdges()) { +// // Build the edge and add it if it adds transitions. +// EdgeDd edgeDd = buildEdgeDd(automaton, edge); +// if (!edgeDd.guard.isZero()) { +// result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd); +// } +// } +// +// return result; +// } +// }; template class CombinedEdgesSystemComposer : public SystemComposer { @@ -956,6 +958,10 @@ namespace storm { std::pair const& getLocalNondeterminismVariables() const { return localNondeterminismVariables; } + + ActionDd multiplyTransitions(storm::dd::Add const& factor) const { + return ActionDd(guard, transitions * factor, transientEdgeAssignments, localNondeterminismVariables, variableToWritingFragment, illegalFragment); + } // A DD that represents all states that have this edge enabled. storm::dd::Add guard; @@ -1014,27 +1020,30 @@ namespace storm { // The identity of the automaton's variables. storm::dd::Add identity; - // The local nondeterminism variables used by this action DD, given as the lowest + // The local nondeterminism variables used by this action DD, given as the lowest and highest variable index. std::pair localNondeterminismVariables; }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { // Intentionally left empty. } + + storm::jani::ActionInformation const& actionInformation; ComposerResult compose() override { - std::map actionIndexToLocalNondeterminismVariableOffset; - for (auto const& action : this->model.getActions()) { - actionIndexToLocalNondeterminismVariableOffset[this->model.getActionIndex(action.getName())] = 0; + std::map actionIndexToLocalNondeterminismVariableOffset; + for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { + actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; } - + actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0; + AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); return buildSystemFromAutomaton(globalAutomaton); } boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset); } @@ -1042,12 +1051,12 @@ namespace storm { // Build a mapping from indices to indices for the renaming. std::map renamingIndexToIndex; for (auto const& entry : composition.getRenaming()) { - if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { + if (actionInformation.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { // Distinguish the cases where we hide the action or properly rename it. if (entry.second) { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get())); + renamingIndexToIndex.emplace(actionInformation.getActionIndex(entry.first), actionInformation.getActionIndex(entry.second.get())); } else { - renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); + renamingIndexToIndex.emplace(actionInformation.getActionIndex(entry.first), this->model.getSilentActionIndex()); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); @@ -1055,9 +1064,10 @@ namespace storm { } // Prepare the new offset mapping. - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); - std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; for (auto const& indexPair : renamingIndexToIndex) { + // FIXME: Check correct? Introduce zero if not contained? auto it = actionIndexToLocalNondeterminismVariableOffset.find(indexPair.second); STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << "."); newSynchronizingActionToOffsetMap[indexPair.first] = it->second; @@ -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 synchronizingActionIndices; - for (auto const& entry : composition.getSynchronizationAlphabet()) { - if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) { - synchronizingActionIndices.insert(this->model.getActionIndex(entry)); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action."); - } - } - - // Then translate the left subcomposition. - AutomatonDd left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); - - // Prepare the new offset mapping. std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); - std::map newActionIndexToLocalNondeterminismVariableOffset = actionIndexToLocalNondeterminismVariableOffset; - for (auto const& actionIndex : synchronizingActionIndices) { - auto it = left.actionIndexToAction.find(actionIndex); - if (it != left.actionIndexToAction.end()) { - newActionIndexToLocalNondeterminismVariableOffset[actionIndex] = it->second.getHighestLocalNondeterminismVariable(); + + std::vector subautomata; + for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) { + // Prepare the new offset mapping. + std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + if (subcompositionIndex == 0) { + for (auto const& synchVector : composition.getSynchronizationVectors()) { + auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput())); + STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << "."); + newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second; + } + } else { + AutomatonDd const& previousAutomatonDd = subautomata.back(); + + // Based on the previous results, we need to update the offsets. + for (auto const& synchVector : composition.getSynchronizationVectors()) { + auto it = previousAutomatonDd.actionIndexToAction.find(actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex - 1))); + if (it != previousAutomatonDd.actionIndexToAction.end()) { + newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex))] = it->second.getHighestLocalNondeterminismVariable(); + } else { + STORM_LOG_ASSERT(false, "Subcomposition does not have action that is mentioned in parallel composition."); + } + } } + + // Build the DD for the next element of the composition wrt. to the current offset mapping. + subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap))); } - // Then translate the right subcomposition. - AutomatonDd right = boost::any_cast(composition.getRightSubcomposition().accept(*this, newActionIndexToLocalNondeterminismVariableOffset)); - - return composeInParallel(left, right, synchronizingActionIndices); + return composeInParallel(subautomata, composition.getSynchronizationVectors()); } private: - AutomatonDd composeInParallel(AutomatonDd const& automaton1, AutomatonDd const& automaton2, std::set const& synchronizingActionIndices) { - AutomatonDd result(automaton1); - 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 const& subautomata, std::vector const& synchronizationVectors) { + AutomatonDd result(this->variables.manager->template getAddOne()); + + std::map> nonSynchronizingActions; + std::vector> synchronizationVectorActions(synchronizationVectors.size(), boost::none); + for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { + AutomatonDd const& subautomaton = subautomata[automatonIndex]; + + // Add the transient assignments from the new subautomaton. + addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments); + + // 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 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 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 actions) { STORM_LOG_TRACE("Combining unsynchronized actions."); if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { - return ActionDd(action1.guard + action2.guard, action1.transitions + action2.transitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), this->variables.manager->getBddZero()); + auto actionIt = actions.begin(); + ActionDd result(*actionIt); + + for (++actionIt; actionIt != actions.end(); ++actionIt) { + result = ActionDd(result.guard + actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment); + } + return result; } else if (this->model.getModelType() == storm::jani::ModelType::MDP) { - if (action1.transitions.isZero()) { - return action2; - } else if (action2.transitions.isZero()) { - return action1; + // Ensure that all actions start at the same local nondeterminism variable. + uint_fast64_t lowestLocalNondeterminismVariable = actions.front().getLowestLocalNondeterminismVariable(); + uint_fast64_t highestLocalNondeterminismVariable = actions.front().getHighestLocalNondeterminismVariable(); + for (auto const& action : actions) { + STORM_LOG_ASSERT(action.getLowestLocalNondeterminismVariable() == lowestLocalNondeterminismVariable, "Mismatching lowest nondeterminism variable indices."); } - // Bring both choices to the same number of variables that encode the nondeterminism. - STORM_LOG_ASSERT(action1.getLowestLocalNondeterminismVariable() == action2.getLowestLocalNondeterminismVariable(), "Mismatching lowest nondeterminism variable indices."); - uint_fast64_t highestLocalNondeterminismVariable = std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable()); - if (action1.getHighestLocalNondeterminismVariable() > action2.getHighestLocalNondeterminismVariable()) { + // Bring all actions to the same number of variables that encode the nondeterminism. + for (auto& action : actions) { storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); - - for (uint_fast64_t i = action2.getHighestLocalNondeterminismVariable(); i < action1.getHighestLocalNondeterminismVariable(); ++i) { + for (uint_fast64_t i = action.getHighestLocalNondeterminismVariable(); i < highestLocalNondeterminismVariable; ++i) { nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); } - action2.transitions *= nondeterminismEncoding; - - for (auto& transientAssignment : action2.transientEdgeAssignments) { - transientAssignment.second *= nondeterminismEncoding; - } - } else if (action2.getHighestLocalNondeterminismVariable() > action1.getHighestLocalNondeterminismVariable()) { - storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); + 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(); - } - action1.transitions *= nondeterminismEncoding; - - for (auto& transientAssignment : action1.transientEdgeAssignments) { + for (auto& transientAssignment : action.transientEdgeAssignments) { transientAssignment.second *= nondeterminismEncoding; } } - // Add a new variable that resolves the nondeterminism between the two choices. - storm::dd::Add combinedTransitions = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1).ite(action2.transitions, action1.transitions); - - // Add the new variable to the writing fragments of each global variable before joining them. - for (auto& entry : action1.variableToWritingFragment) { - entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 0) && entry.second; - } - for (auto& entry : action2.variableToWritingFragment) { - entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1) && entry.second; + uint64_t numberOfLocalNondeterminismVariables = static_cast(std::ceil(std::log2(actions.size()))); + storm::dd::Bdd guard = this->variables.manager->getBddZero(); + storm::dd::Add transitions = this->variables.manager->template getAddZero(); + std::map> transientEdgeAssignments; + std::map> variableToWritingFragment; + storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); + + for (uint64_t actionIndex = 0; actionIndex < actions.size(); ++actionIndex) { + ActionDd& action = actions[actionIndex]; + + guard |= action.guard.toBdd(); + + storm::dd::Add nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables); + transitions += nondeterminismEncoding * action.transitions; + + joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments); + + storm::dd::Bdd nondeterminismEncodingBdd = nondeterminismEncoding.toBdd(); + for (auto& entry : action.variableToWritingFragment) { + entry.second &= nondeterminismEncodingBdd; + } + addToVariableWritingFragmentMap(variableToWritingFragment, action.variableToWritingFragment); + illegalFragment |= action.illegalFragment; } - return ActionDd((action1.guard.toBdd() || action2.guard.toBdd()).template toAdd(), combinedTransitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(action1.getLowestLocalNondeterminismVariable(), highestLocalNondeterminismVariable + 1), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), action1.illegalFragment || action2.illegalFragment); + return ActionDd(guard.template toAdd(), transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } @@ -1476,7 +1558,13 @@ namespace storm { globalVariableToWritingFragment.emplace(variable, partToAdd); } } - + + void addToVariableWritingFragmentMap(std::map>& globalVariableToWritingFragment, std::map> const& partToAdd) const { + for (auto const& entry : partToAdd) { + addToVariableWritingFragmentMap(globalVariableToWritingFragment, entry.first, entry.second); + } + } + std::map> joinVariableWritingFragmentMaps(std::map> const& globalVariableToWritingFragment1, std::map> const& globalVariableToWritingFragment2) { std::map> result = globalVariableToWritingFragment1; @@ -1752,7 +1840,13 @@ namespace storm { storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { - system.transitions = system.transitions / system.transitions.sumAbstract(variables.columnMetaVariables); + storm::dd::Add stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables); + system.transitions = system.transitions / stateToNumberOfChoices; + + // Scale all state-action rewards. + for (auto& entry : system.transientEdgeAssignments) { + entry.second = entry.second / stateToNumberOfChoices; + } } // If we were asked to treat some states as terminal states, we cut away their transitions now. @@ -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 variableCreator(model); + CompositionVariableCreator variableCreator(model, actionInformation); CompositionVariables variables = variableCreator.create(); // Determine which transient assignments need to be considered in the building process. std::vector rewardVariables = selectRewardVariables(model, options); // Create a builder to compose and build the model. -// SeparateEdgesSystemComposer composer(model, variables); - CombinedEdgesSystemComposer composer(model, variables, rewardVariables); + CombinedEdgesSystemComposer composer(model, actionInformation, variables, rewardVariables); ComposerResult system = composer.compose(); // Postprocess the variables in place. @@ -1964,4 +2061,4 @@ namespace storm { template class DdJaniModelBuilder; template class DdJaniModelBuilder; } -} \ 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(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 - Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), choiceRewards() { + Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), rewards(), labels() { // Intentionally left empty. } @@ -33,24 +33,24 @@ namespace storm { } template - void Choice::addChoiceLabel(uint_fast64_t label) { - if (!choiceLabels) { - choiceLabels = LabelSet(); + void Choice::addLabel(uint_fast64_t label) { + if (!labels) { + labels = LabelSet(); } - choiceLabels->insert(label); + labels->insert(label); } template - void Choice::addChoiceLabels(LabelSet const& labelSet) { - if (!choiceLabels) { - choiceLabels = LabelSet(); + void Choice::addLabels(LabelSet const& labelSet) { + if (!labels) { + labels = LabelSet(); } - choiceLabels->insert(labelSet.begin(), labelSet.end()); + labels->insert(labelSet.begin(), labelSet.end()); } template - boost::container::flat_set const& Choice::getChoiceLabels() const { - return *choiceLabels; + boost::container::flat_set const& Choice::getLabels() const { + return *labels; } template @@ -70,13 +70,18 @@ namespace storm { } template - void Choice::addChoiceReward(ValueType const& value) { - choiceRewards.push_back(value); + void Choice::addReward(ValueType const& value) { + rewards.push_back(value); } template - std::vector const& Choice::getChoiceRewards() const { - return choiceRewards; + void Choice::addRewards(std::vector&& values) { + this->rewards = std::move(values); + } + + template + std::vector const& Choice::getRewards() const { + return rewards; } template diff --git a/src/generator/Choice.h b/src/generator/Choice.h index 76b6c8d16..bd20af0f0 100644 --- a/src/generator/Choice.h +++ b/src/generator/Choice.h @@ -66,21 +66,21 @@ namespace storm { * * @param label The label to associate with this choice. */ - void addChoiceLabel(uint_fast64_t label); + void addLabel(uint_fast64_t label); /*! * Adds the given label set to the labels associated with this choice. * * @param labelSet The label set to associate with this choice. */ - void addChoiceLabels(LabelSet const& labelSet); + void addLabels(LabelSet const& labelSet); /*! * Retrieves the set of labels associated with this choice. * * @return The set of labels associated with this choice. */ - LabelSet const& getChoiceLabels() const; + LabelSet const& getLabels() const; /*! * Retrieves the index of the action of this choice. @@ -104,12 +104,17 @@ namespace storm { /*! * Adds the given value to the reward associated with this choice. */ - void addChoiceReward(ValueType const& value); + void addReward(ValueType const& value); + + /*! + * Adds the given choices rewards to this choice. + */ + void addRewards(std::vector&& values); /*! * Retrieves the rewards for this choice under selected reward models. */ - std::vector const& getChoiceRewards() const; + std::vector const& getRewards() const; /*! * Retrieves whether the choice is Markovian. @@ -135,10 +140,10 @@ namespace storm { ValueType totalMass; // The reward values associated with this choice. - std::vector choiceRewards; + std::vector rewards; // The labels that are associated with this choice. - boost::optional choiceLabels; + boost::optional labels; }; template diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 5d03578fe..c0aae624a 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -22,7 +22,7 @@ namespace storm { } template - JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables() { + JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables(), hasStateActionRewards(false) { STORM_LOG_THROW(model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); @@ -282,6 +282,10 @@ namespace storm { if (this->isDeterministicModel() && totalNumberOfChoices > 1) { Choice globalChoice; + // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs + // this is equal to the number of choices, which is why we initialize it like this here. + ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast(totalNumberOfChoices) : storm::utility::zero(); + // Iterate over all choices and combine the probabilities/rates into one choice. for (auto const& choice : allChoices) { for (auto const& stateProbabilityPair : choice) { @@ -292,11 +296,23 @@ namespace storm { } } + if (hasStateActionRewards && !this->isDiscreteTimeModel()) { + totalExitRate += choice.getTotalMass(); + } + if (this->options.isBuildChoiceLabelsSet()) { - globalChoice.addChoiceLabels(choice.getChoiceLabels()); + globalChoice.addLabels(choice.getLabels()); } } - + + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); + for (auto const& choice : allChoices) { + for (uint_fast64_t rewardVariableIndex = 0; rewardVariableIndex < rewardVariables.size(); ++rewardVariableIndex) { + stateActionRewards[rewardVariableIndex] += choice.getRewards()[rewardVariableIndex] * choice.getTotalMass() / totalExitRate; + } + } + globalChoice.addRewards(std::move(stateActionRewards)); + // Move the newly fused choice in place. allChoices.clear(); allChoices.push_back(std::move(globalChoice)); @@ -349,7 +365,7 @@ namespace storm { } // Create the state-action reward for the newly created choice. - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addChoiceReward(value); } ); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } ); // Check that the resulting distribution is in fact a distribution. STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); @@ -385,6 +401,7 @@ namespace storm { while (!done) { boost::container::flat_map* currentTargetStates = new boost::container::flat_map(); boost::container::flat_map* newTargetStates = new boost::container::flat_map(); + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); currentTargetStates->emplace(state, storm::utility::one()); @@ -405,6 +422,10 @@ namespace storm { newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability())); } } + + // Create the state-action reward for the newly created choice. + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } // If there is one more command to come, shift the target states one time step back. @@ -423,6 +444,9 @@ namespace storm { // Now create the actual distribution. Choice& choice = result.back(); + // Add the rewards to the choice. + choice.addRewards(std::move(stateActionRewards)); + // Add the probabilities/rates to the newly created choice. ValueType probabilitySum = storm::utility::zero(); for (auto const& stateProbabilityPair : *newTargetStates) { @@ -601,6 +625,7 @@ namespace storm { } if (*rewardVariableIt == assignment.getExpressionVariable()) { rewardModelInformation[std::distance(rewardVariables.begin(), rewardVariableIt)].setHasStateActionRewards(); + hasStateActionRewards = true; ++rewardVariableIt; } } diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index d9932f60a..d0b5707a6 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -108,6 +108,9 @@ namespace storm { /// A vector storing information about the corresponding reward models (variables). std::vector rewardModelInformation; + + // A flag that stores whether at least one of the selected reward models has state-action rewards. + bool hasStateActionRewards; }; } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 1ecbec2ab..6c24cd00b 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -242,7 +242,7 @@ namespace storm { } if (this->options.isBuildChoiceLabelsSet()) { - globalChoice.addChoiceLabels(choice.getChoiceLabels()); + globalChoice.addLabels(choice.getLabels()); } } @@ -259,7 +259,7 @@ namespace storm { } } - globalChoice.addChoiceReward(stateActionRewardValue); + globalChoice.addReward(stateActionRewardValue); } // Move the newly fused choice in place. @@ -382,7 +382,7 @@ namespace storm { // Remember the command labels only if we were asked to. if (this->options.isBuildChoiceLabelsSet()) { - choice.addChoiceLabel(command.getGlobalIndex()); + choice.addLabel(command.getGlobalIndex()); } // Iterate over all updates of the current command. @@ -410,7 +410,7 @@ namespace storm { } } } - choice.addChoiceReward(stateActionRewardValue); + choice.addReward(stateActionRewardValue); } // Check that the resulting distribution is in fact a distribution. @@ -486,7 +486,7 @@ namespace storm { if (this->options.isBuildChoiceLabelsSet()) { // Add the labels of all commands to this choice. for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); + choice.addLabel(iteratorList[i]->get().getGlobalIndex()); } } @@ -511,7 +511,7 @@ namespace storm { } } } - choice.addChoiceReward(stateActionRewardValue); + choice.addReward(stateActionRewardValue); } // Dispose of the temporary maps. 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; template class Dd; } -} \ No newline at end of file +} diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h index 18605c259..ae9728263 100644 --- a/src/storage/dd/Dd.h +++ b/src/storage/dd/Dd.h @@ -30,6 +30,8 @@ namespace storm { Dd(Dd&& other) = default; Dd& operator=(Dd&& other) = default; + virtual ~Dd() = 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 83ed56172..aeb59e4b3 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -406,6 +406,14 @@ namespace storm { edge.finalize(containingModel); } } + + std::set Automaton::getUsedActionIndices() const { + std::set result; + for (auto const& edge : edges) { + result.insert(edge.getActionIndex()); + } + return result; + } } } \ No newline at end of file diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 6e9f945e8..83d31db83 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -304,6 +304,11 @@ namespace storm { */ void finalize(Model const& containingModel); + /*! + * Retrieves the action indices appearing at some edge of the automaton. + */ + std::set getUsedActionIndices() const; + private: /// The name of the automaton. std::string name; @@ -335,4 +340,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 const& nonsilentActionIndices, std::map const& indexToNameMap, std::map 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 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 nonSilentActionIndices = boost::any_cast>(model.getSystemComposition().accept(*this, boost::none)); + + return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap); + } + + boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { + std::set result = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices(); + result.erase(model.getSilentActionIndex()); + return result; + } + + boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { + std::set usedActions = boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); + + std::set newUsedActions; + for (auto const& index : usedActions) { + auto renamingIt = composition.getRenaming().find(indexToNameMap.at(index)); + if (renamingIt != composition.getRenaming().end()) { + if (renamingIt->second) { + newUsedActions.insert(addOrGetActionIndex(renamingIt->second.get())); + + auto actionIndexIt = nameToIndexMap.find(renamingIt->second.get()); + if (actionIndexIt != nameToIndexMap.end()) { + newUsedActions.insert(actionIndexIt->second); + } else { + nameToIndexMap[renamingIt->second.get()] = nextFreeActionIndex; + indexToNameMap[nextFreeActionIndex] = renamingIt->second.get(); + ++nextFreeActionIndex; + } + } + } else { + newUsedActions.insert(index); + } + } + + return newUsedActions; + } + + boost::any CompositionActionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { + std::vector> subresults; + for (auto const& subcomposition : composition.getSubcompositions()) { + subresults.push_back(boost::any_cast>(subcomposition->accept(*this, boost::none))); + } + + std::set effectiveSynchronizationVectors; + for (uint64_t index = 0; index < composition.getNumberOfSynchronizationVectors(); ++index) { + effectiveSynchronizationVectors.insert(index); + } + + // Determine all actions that do not take part in synchronization vectors. + std::set result; + for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) { + + std::set actionsInSynch; + std::set localEffectiveSynchVectors; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); + uint64_t synchVectorActionIndex = nameToIndexMap.at(synchVector.getInput(subresultIndex)); + actionsInSynch.insert(synchVectorActionIndex); + + // If the action of they synchronization vector at this position is one that is actually contained + // in the corresponding subcomposition, the synchronization vector is effective. + if (subresults[subresultIndex].find(synchVectorActionIndex) != subresults[subresultIndex].end()) { + effectiveSynchronizationVectors.insert(synchVectorIndex); + } + } + + std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin())); + + // Intersect the previously effective synchronization vectors with the ones that were derived to be + // effective for the current subcomposition. + std::set newEffectiveSynchVectors; + std::set_intersection(effectiveSynchronizationVectors.begin(), effectiveSynchronizationVectors.end(), newEffectiveSynchVectors.begin(), newEffectiveSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); + effectiveSynchronizationVectors = std::move(newEffectiveSynchVectors); + } + + // Now add all outputs of synchronization vectors. + for (auto const& synchVector : composition.getSynchronizationVectors()) { + result.insert(addOrGetActionIndex(synchVector.getOutput())); + } + + return result; + } + + uint64_t CompositionActionInformationVisitor::addOrGetActionIndex(std::string const& name) { + auto it = nameToIndexMap.find(name); + if (it != nameToIndexMap.end()) { + return it->second; + } else { + nameToIndexMap[name] = nextFreeActionIndex; + indexToNameMap[nextFreeActionIndex] = name; + return nextFreeActionIndex++; + } + } + + } +} diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h new file mode 100644 index 000000000..705773c27 --- /dev/null +++ b/src/storage/jani/CompositionActionInformationVisitor.h @@ -0,0 +1,50 @@ +#pragma once + +#include +#include + +#include "src/storage/jani/CompositionVisitor.h" + +namespace storm { + namespace jani { + + class Model; + + class ActionInformation { + public: + ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap, uint64_t silentActionIndex = 0); + + std::string const& getActionName(uint64_t index) const; + uint64_t getActionIndex(std::string const& name) const; + std::set const& getNonSilentActionIndices() const; + uint64_t getSilentActionIndex() const; + + private: + uint64_t silentActionIndex; + std::set nonsilentActionIndices; + std::map indexToNameMap; + std::map nameToIndexMap; + }; + + class CompositionActionInformationVisitor : public CompositionVisitor { + public: + CompositionActionInformationVisitor(storm::jani::Model const& model); + + ActionInformation getActionInformation(); + + virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override; + virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override; + virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override; + + private: + uint64_t addOrGetActionIndex(std::string const& name); + + storm::jani::Model const& model; + uint64_t nextFreeActionIndex; + std::map nameToIndexMap; + std::map indexToNameMap; + }; + + + } +} diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index d6b661b53..b07911ca6 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -6,11 +6,11 @@ namespace storm { namespace jani { - CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), restrictedParallelComposition(false) { + CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), nonStandardParallelComposition(false) { // Intentionally left empty. } - CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) { + CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), nonStandardParallelComposition(nonStandardParallelComposition) { // Intentionally left empty. } @@ -49,12 +49,12 @@ namespace storm { return renameComposition; } - void CompositionInformation::setContainsRestrictedParallelComposition() { - restrictedParallelComposition = true; + void CompositionInformation::setContainsNonStandardParallelComposition() { + nonStandardParallelComposition = true; } - bool CompositionInformation::containsRestrictedParallelComposition() const { - return restrictedParallelComposition; + bool CompositionInformation::containsNonStandardParallelComposition() const { + return nonStandardParallelComposition; } std::map CompositionInformation::joinMultiplicityMaps(std::map const& first, std::map const& second) { @@ -90,30 +90,61 @@ namespace storm { boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { CompositionInformation subresult = boost::any_cast(composition.getSubcomposition().accept(*this, data)); std::set nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming()); - return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsRestrictedParallelComposition()); + return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsNonStandardParallelComposition()); } boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { - CompositionInformation left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); - CompositionInformation right = boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); - - // Join the information from both sides. - bool containsRenameComposition = left.containsRenameComposition() || right.containsRenameComposition(); - bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition(); - std::map joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap()); + std::vector subinformation; - std::set nonsilentActions; - std::set_union(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(nonsilentActions, nonsilentActions.begin())); + for (auto const& subcomposition : composition.getSubcompositions()) { + subinformation.push_back(boost::any_cast(subcomposition->accept(*this, data))); + } + + std::map joinedAutomatonToMultiplicityMap; + bool containsRenameComposition = false; + bool containsNonStandardParallelComposition = false; + + for (auto const& subinfo : subinformation) { + containsRenameComposition |= subinfo.containsRenameComposition(); + containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition(); + joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap()); + + } - // If there was no restricted parallel composition yet, maybe the current composition is one, so check it. - if (!containsRestrictedParallelComposition) { - std::set commonNonsilentActions; - std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin())); - bool allCommonActionsIncluded = std::includes(commonNonsilentActions.begin(), commonNonsilentActions.end(), composition.getSynchronizationAlphabet().begin(), composition.getSynchronizationAlphabet().end()); - containsRestrictedParallelComposition = !allCommonActionsIncluded; + // Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have + // the non-silent actions that are referred to. + std::set effectiveSynchVectors; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + effectiveSynchVectors.insert(synchVectorIndex); } - return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition); + // Now compute non-silent actions. + std::set nonsilentActions; + for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) { + auto const& subinfo = subinformation[infoIndex]; + + std::set enabledSynchVectors; + for (auto const& nonsilentAction : subinfo.getNonsilentActions()) { + bool appearsInSomeSynchVector = false; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); + if (synchVector.getInput(infoIndex) == nonsilentAction) { + appearsInSomeSynchVector = true; + enabledSynchVectors.insert(synchVectorIndex); + } + } + + if (!appearsInSomeSynchVector) { + nonsilentActions.insert(nonsilentAction); + } + } + + std::set newEffectiveSynchVectors; + std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); + effectiveSynchVectors = std::move(newEffectiveSynchVectors); + } + + return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsRenameComposition, containsNonStandardParallelComposition); } } diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h index 59a422a41..786078e2e 100644 --- a/src/storage/jani/CompositionInformationVisitor.h +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -16,7 +16,7 @@ namespace storm { class CompositionInformation { public: CompositionInformation(); - CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition); + CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool nonStandardParallelComposition); void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1); @@ -27,8 +27,8 @@ namespace storm { void setContainsRenameComposition(); bool containsRenameComposition() const; - void setContainsRestrictedParallelComposition(); - bool containsRestrictedParallelComposition() const; + void setContainsNonStandardParallelComposition(); + bool containsNonStandardParallelComposition() const; static std::map joinMultiplicityMaps(std::map const& first, std::map const& second); std::map const& getAutomatonToMultiplicityMap() const; @@ -43,8 +43,8 @@ namespace storm { /// A flag indicating whether the composition contains a renaming composition. bool renameComposition; - /// A flag indicating whether the composition contains - bool restrictedParallelComposition; + /// A flag indicating whether the composition contains any non-standard parallel composition. + bool nonStandardParallelComposition; }; class CompositionInformationVisitor : public CompositionVisitor { diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 5a528b631..19d8bb1d5 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -77,6 +77,10 @@ namespace storm { return it->second; } + std::unordered_map const& Model::getActionToIndexMap() const { + return actionToIndex; + } + std::vector const& Model::getActions() const { return actions; } @@ -450,7 +454,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 eaf0f9d0f..7d9431d0a 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -69,6 +69,11 @@ namespace storm { */ uint64_t getActionIndex(std::string const& name) const; + /*! + * Retrieves the mapping from action names to their indices. + */ + std::unordered_map const& getActionToIndexMap() const; + /** * Adds an action to the model. * diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index f767e32cc..fac8e2ad7 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -1,33 +1,131 @@ #include "src/storage/jani/ParallelComposition.h" +#include + #include +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace jani { - ParallelComposition::ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) { + SynchronizationVector::SynchronizationVector(std::vector const& input, std::string const& output) : input(input), output(output) { // Intentionally left empty. } - Composition const& ParallelComposition::getLeftSubcomposition() const { - return *leftSubcomposition; + std::size_t SynchronizationVector::size() const { + return input.size(); + } + + std::vector const& SynchronizationVector::getInput() const { + return input; + } + + std::string const& SynchronizationVector::getInput(uint64_t index) const { + return input[index]; + } + + std::string const& SynchronizationVector::getOutput() const { + return output; } - Composition const& ParallelComposition::getRightSubcomposition() const { - return *rightSubcomposition; + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector) { + bool first = true; + stream << "("; + for (auto const& element : synchronizationVector.getInput()) { + if (!first) { + stream << ", "; + } + stream << element; + } + stream << ") -> " << synchronizationVector.getOutput(); + return stream; } - std::set const& ParallelComposition::getSynchronizationAlphabet() const { - return alphabet; + ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) { + STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); + this->checkSynchronizationVectors(); } + + ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() { + STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); + // Manually construct the synchronization vectors for all elements of the synchronization alphabet. + for (auto const& action : synchronizationAlphabet) { + synchronizationVectors.emplace_back(std::vector(this->subcompositions.size(), action), action); + } + } + + ParallelComposition::ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet) { + subcompositions.push_back(leftSubcomposition); + subcompositions.push_back(rightSubcomposition); + + // Manually construct the synchronization vectors for all elements of the synchronization alphabet. + for (auto const& action : synchronizationAlphabet) { + synchronizationVectors.emplace_back(std::vector(this->subcompositions.size(), action), action); + } + } + + Composition const& ParallelComposition::getSubcomposition(uint64_t index) const { + return *subcompositions[index]; + } + + std::vector> const& ParallelComposition::getSubcompositions() const { + return subcompositions; + } + + uint64_t ParallelComposition::getNumberOfSubcompositions() const { + return subcompositions.size(); + } + + SynchronizationVector const& ParallelComposition::getSynchronizationVector(uint64_t index) const { + return synchronizationVectors[index]; + } + + std::vector const& ParallelComposition::getSynchronizationVectors() const { + return synchronizationVectors; + } + + std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const { + return synchronizationVectors.size(); + } + + void ParallelComposition::checkSynchronizationVectors() const { + for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { + std::set actions; + for (auto const& vector : synchronizationVectors) { + STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); + std::string const& action = vector.getInput(inputIndex); + STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vectors."); + actions.insert(action); + } + } + } + boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } void ParallelComposition::write(std::ostream& stream) const { - stream << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(alphabet, ", ") << "]| " << this->getRightSubcomposition(); + std::vector synchronizationVectorsAsStrings; + for (auto const& synchronizationVector : synchronizationVectors) { + std::stringstream tmpStream; + tmpStream << synchronizationVector; + synchronizationVectorsAsStrings.push_back(tmpStream.str()); + } + + bool first = true; + stream << "("; + for (auto const& subcomposition : subcompositions) { + if (!first) { + stream << " || "; + first = false; + } + stream << *subcomposition; + } + stream << ")[" << boost::algorithm::join(synchronizationVectorsAsStrings, ", ") << "]"; } } -} \ No newline at end of file +} 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 #include +#include +#include #include "src/storage/jani/Composition.h" namespace storm { namespace jani { + class SynchronizationVector { + public: + SynchronizationVector(std::vector const& input, std::string const& output); + + std::size_t size() const; + std::vector const& getInput() const; + std::string const& getInput(uint64_t index) const; + std::string const& getOutput() const; + + private: + /// The input to the synchronization. + std::vector input; + + /// The output of the synchronization. + std::string output; + }; + + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector); + class ParallelComposition : public Composition { public: /*! - * Creates a parallel composition of the two subcompositions. + * Creates a parallel composition of the subcompositions and the provided synchronization vectors. */ - ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& alphabet = {}); - + ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors); + /*! - * Retrieves the left subcomposition. + * Creates a parallel composition of the subcompositions over the provided synchronization alphabet. */ - Composition const& getLeftSubcomposition() const; + ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet); /*! - * Retrieves the right subcomposition. + * Creates a parallel composition of the subcompositions over the provided synchronization alphabet. */ - Composition const& getRightSubcomposition() const; + ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet); /*! - * Retrieves the alphabet of actions over which to synchronize the automata. + * Retrieves the subcomposition with the given index. */ - std::set const& getSynchronizationAlphabet() const; + Composition const& getSubcomposition(uint64_t index) const; + + /*! + * Retrieves the subcompositions of the parallel composition. + */ + std::vector> const& getSubcompositions() const; + + /*! + * Retrieves the number of subcompositions of this parallel composition. + */ + uint64_t getNumberOfSubcompositions() const; + + /*! + * Retrieves the synchronization vector with the given index. + */ + SynchronizationVector const& getSynchronizationVector(uint64_t index) const; + + /*! + * Retrieves the synchronization vectors of the parallel composition. + */ + std::vector const& getSynchronizationVectors() const; + + /*! + * Retrieves the number of synchronization vectors. + */ + std::size_t getNumberOfSynchronizationVectors() const; virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; virtual void write(std::ostream& stream) const override; private: - // The left subcomposition. - std::shared_ptr leftSubcomposition; + /*! + * Checks the synchronization vectors for validity. + */ + void checkSynchronizationVectors() const; - // The right subcomposition. - std::shared_ptr rightSubcomposition; + /// The subcompositions. + std::vector> subcompositions; - // The alphabet of actions over which to synchronize. - std::set alphabet; + /// The synchronization vectors of the parallel composition. + std::vector synchronizationVectors; }; } diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 33ad88fef..08819964a 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -137,7 +137,7 @@ namespace storm { } STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented."); } - STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); + STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // previously built mapping to make variables global that are read by more than one module. 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 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..1b0248ce5 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,67 @@ TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) { storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder builder; EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); -} \ No newline at end of file +} + +TEST(DdJaniModelBuilderTest_Sylvan, IllegalSynchronizingWrites) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + storm::builder::DdJaniModelBuilder builder; + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); +} + +TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + + // Start by checking the original composition. + std::shared_ptr> model = builder.build(janiModel); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + + // Now we tweak it's system composition to check whether synchronization vectors work. + std::vector> automataCompositions; + automataCompositions.push_back(std::make_shared("one")); + automataCompositions.push_back(std::make_shared("two")); + automataCompositions.push_back(std::make_shared("three")); + + // First, make all actions non-synchronizing. + std::vector synchronizationVectors; + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(24ul, model->getNumberOfStates()); + EXPECT_EQ(48ul, model->getNumberOfTransitions()); + + // Then, make only a, b and c synchronize. + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back("c"); + inputVector.push_back("a"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(3ul, model->getNumberOfStates()); + EXPECT_EQ(3ul, model->getNumberOfTransitions()); + + inputVector.clear(); + inputVector.push_back("b"); + inputVector.push_back("c"); + inputVector.push_back("b"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); + EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); +} diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index a6b73779a..fa05bf3e0 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -3,6 +3,7 @@ #include "src/settings/SettingMemento.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/IOSettings.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" @@ -11,56 +12,66 @@ #include "src/builder/DdPrismModelBuilder.h" TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); @@ -70,28 +81,33 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); @@ -101,35 +117,41 @@ TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -139,9 +161,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -149,9 +171,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -159,9 +181,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); EXPECT_EQ(400ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -169,9 +191,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -179,9 +201,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -191,9 +213,10 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { } TEST(DdPrismModelBuilderTest_Cudd, Mdp) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); @@ -201,9 +224,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -211,9 +234,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -221,9 +244,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); EXPECT_EQ(400ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -231,9 +254,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -241,9 +264,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -253,7 +276,8 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { } TEST(DdPrismModelBuilderTest_Sylvan, Composition) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); @@ -264,10 +288,9 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); @@ -277,7 +300,8 @@ TEST(DdPrismModelBuilderTest_Sylvan, Composition) { } TEST(DdPrismModelBuilderTest_Cudd, Composition) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); @@ -288,10 +312,9 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); - + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); mdp = model->as>(); diff --git a/test/functional/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 enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -123,7 +125,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -220,7 +223,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -299,7 +303,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -378,7 +383,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -414,7 +420,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -457,7 +464,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -545,7 +553,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index ac2c7dcb7..53e992fd3 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -12,6 +12,7 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/StandardRewardModel.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" @@ -19,8 +20,9 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -80,8 +82,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -141,8 +144,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -185,8 +189,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -229,8 +234,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -281,8 +287,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { } TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 1733fa40f..eb00b67cd 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "src/parser/PrismParser.h" #include "src/parser/FormulaParser.h" #include "src/builder/DdPrismModelBuilder.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -21,8 +22,9 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -118,8 +120,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -215,8 +218,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -294,8 +298,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); - + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 5f744cc68..5d8391f5c 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -6,6 +6,7 @@ #include "src/logic/Formulas.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/storage/dd/DdType.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -25,7 +26,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -122,7 +124,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -219,7 +222,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -298,7 +302,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -377,7 +382,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -413,7 +419,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -456,7 +463,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); @@ -546,7 +554,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index cd6d87afb..ac419c04b 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/solver/NativeLinearEquationSolver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -14,13 +15,12 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - #include "src/settings/modules/GmmxxEquationSolverSettings.h" - #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -81,7 +81,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -142,7 +143,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -186,7 +188,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -230,7 +233,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -282,7 +286,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) { } TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 1762c098f..1fe89c609 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/parser/FormulaParser.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" @@ -19,7 +20,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -115,7 +117,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -211,7 +214,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -290,7 +294,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 3d1f3621f..c5ff7e1d1 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -4,6 +4,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" @@ -18,7 +19,8 @@ #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -79,7 +81,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -141,7 +144,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -185,7 +189,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -232,7 +237,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { } TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -284,7 +290,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { } TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index efe1b3283..ea024ccb7 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -3,6 +3,7 @@ #include "src/logic/Formulas.h" #include "src/utility/solver.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" @@ -18,7 +19,8 @@ #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -115,7 +117,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { } TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -212,7 +215,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -291,7 +295,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 2813e1a9b..e8c2e26fc 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/parser/PrismParser.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" @@ -16,7 +17,8 @@ #include "src/storage/dd/DdManager.h" TEST(GraphTest, SymbolicProb01_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -37,7 +39,8 @@ TEST(GraphTest, SymbolicProb01_Cudd) { } TEST(GraphTest, SymbolicProb01_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -58,7 +61,8 @@ TEST(GraphTest, SymbolicProb01_Sylvan) { } TEST(GraphTest, SymbolicProb01MinMax_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -75,7 +79,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -100,7 +105,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -119,7 +125,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { } TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -136,7 +143,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -161,7 +169,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); } - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::DdPrismModelBuilder().build(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -180,7 +189,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { } TEST(GraphTest, ExplicitProb01) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -201,7 +211,8 @@ TEST(GraphTest, ExplicitProb01) { } TEST(GraphTest, ExplicitProb01MinMax) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -216,7 +227,8 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -237,7 +249,8 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + program = modelDescription.preprocess().asPrismProgram(); model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(false, true)).build(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -249,4 +262,4 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); -} \ No newline at end of file +}