From df7da86bd7be0f05938a4ce2d83abdd95c3c96d2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 12 Dec 2016 17:10:47 +0100 Subject: [PATCH] flattening JANI models appears to be working, started adding tests --- src/storm/cli/cli.cpp | 2 +- src/storm/storage/jani/Automaton.cpp | 9 + src/storm/storage/jani/Automaton.h | 5 + src/storm/storage/jani/Location.cpp | 4 + src/storm/storage/jani/Location.h | 7 +- src/storm/storage/jani/Model.cpp | 255 ++++++++++++++++-- src/storm/storage/jani/Model.h | 13 + src/storm/storage/jani/OrderedAssignments.cpp | 8 + src/storm/storage/jani/OrderedAssignments.h | 5 + src/storm/storage/jani/TemplateEdge.cpp | 7 + src/storm/storage/jani/TemplateEdge.h | 5 + .../storage/jani/TemplateEdgeDestination.cpp | 4 + .../storage/jani/TemplateEdgeDestination.h | 7 +- src/storm/storage/jani/VariableSet.cpp | 9 + src/storm/storage/jani/VariableSet.h | 5 + src/storm/utility/storm.h | 2 + src/test/storage/JaniModelTest.cpp | 155 +++++++++++ 17 files changed, 470 insertions(+), 32 deletions(-) create mode 100644 src/test/storage/JaniModelTest.cpp diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 4f1ad61c3..7d43e0d8b 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -279,7 +279,7 @@ namespace storm { // Get the string that assigns values to the unknown currently undefined constants in the model. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); - + STORM_LOG_TRACE("Building and checking symbolic model."); if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index c9f163d57..563b08f25 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -427,6 +427,15 @@ namespace storm { } } + void Automaton::changeAssignmentVariables(std::map> const& remapping) { + for (auto& location : locations) { + location.changeAssignmentVariables(remapping); + } + for (auto& templateEdge : templateEdges) { + templateEdge->changeAssignmentVariables(remapping); + } + } + void Automaton::finalize(Model const& containingModel) { for (auto& templateEdge : templateEdges) { templateEdge->finalize(containingModel); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 9cec07519..ad7a46542 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -312,6 +312,11 @@ namespace storm { */ void substitute(std::map const& substitution); + /*! + * Changes all variables in assignments based on the given mapping. + */ + void changeAssignmentVariables(std::map> const& remapping); + /*! * Finalizes the building of this automaton. Subsequent changes to the automaton require another call to this * method. Note that this method is invoked by a call to finalize to the containing model. diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp index fa5d3198b..9922ffe4f 100644 --- a/src/storm/storage/jani/Location.cpp +++ b/src/storm/storage/jani/Location.cpp @@ -30,6 +30,10 @@ namespace storm { } } + void Location::changeAssignmentVariables(std::map> const& remapping) { + assignments.changeAssignmentVariables(remapping); + } + void Location::checkValid() const { // Intentionally left empty. } diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h index a0eed42af..9d6f409da 100644 --- a/src/storm/storage/jani/Location.h +++ b/src/storm/storage/jani/Location.h @@ -38,7 +38,12 @@ namespace storm { * Substitutes all variables in all expressions according to the given substitution. */ void substitute(std::map const& substitution); - + + /*! + * Changes all variables in assignments based on the given mapping. + */ + void changeAssignmentVariables(std::map> const& remapping); + /*! * Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments. */ diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index a37679c14..0fca85982 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -41,6 +41,47 @@ namespace storm { STORM_LOG_ASSERT(actionIndex == SILENT_ACTION_INDEX, "Illegal silent action index."); } + Model::Model(Model const& other) { + *this = other; + } + + Model& Model::operator=(Model const& other) { + if (this != &other) { + this->name = other.name; + this->modelType = other.modelType; + this->version = other.version; + this->expressionManager = other.expressionManager; + this->actions = other.actions; + this->actionToIndex = other.actionToIndex; + this->nonsilentActionIndices = other.nonsilentActionIndices; + this->constants = other.constants; + this->constantToIndex = other.constantToIndex; + this->globalVariables = other.globalVariables; + this->automata = other.automata; + this->automatonToIndex = other.automatonToIndex; + this->composition = other.composition; + this->initialStatesRestriction = other.initialStatesRestriction; + + // Now that we have copied all the data, we need to fix all assignments as they contain references to the old model. + std::map> remapping; + for (auto const& variable : other.getGlobalVariables()) { + remapping.emplace(&variable, this->getGlobalVariables().getVariable(variable.getName())); + } + auto otherAutomatonIt = other.automata.begin(); + auto thisAutomatonIt = this->automata.begin(); + + for (; otherAutomatonIt != other.automata.end(); ++otherAutomatonIt, ++thisAutomatonIt) { + for (auto const& variable : otherAutomatonIt->getVariables()) { + remapping.emplace(&variable, thisAutomatonIt->getVariables().getVariable(variable.getName())); + } + + thisAutomatonIt->changeAssignmentVariables(remapping); + } + } + + return *this; + } + storm::expressions::ExpressionManager& Model::getManager() const { return *expressionManager; } @@ -71,14 +112,85 @@ namespace storm { std::shared_ptr templateEdge; }; - std::vector createSynchronizingMetaEdges(Model const& oldModel, Model& newModel, std::vector>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector> const& composedAutomata, storm::solver::SmtSolver& solver) { + storm::expressions::Expression createSynchronizedGuard(std::vector> const& chosenEdges) { + STORM_LOG_ASSERT(!chosenEdges.empty(), "Expected non-empty set of edges."); + auto it = chosenEdges.begin(); + storm::expressions::Expression result = it->get().getGuard(); + ++it; + for (; it != chosenEdges.end(); ++it) { + result = result && it->get().getGuard(); + } + return result; + } + + ConditionalMetaEdge createSynchronizedMetaEdge(Automaton& automaton, std::vector> const& edgesToSynchronize) { + ConditionalMetaEdge result; + result.templateEdge = automaton.createTemplateEdge(createSynchronizedGuard(edgesToSynchronize)); + + for (auto const& edge : edgesToSynchronize) { + result.condition.push_back(edge.get().getSourceLocationIndex()); + } + + // Initialize all update iterators. + std::vector::const_iterator> destinationIterators; + for (uint_fast64_t i = 0; i < edgesToSynchronize.size(); ++i) { + destinationIterators.push_back(edgesToSynchronize[i].get().getDestinations().cbegin()); + } + + bool doneDestinations = false; + do { + // We create the new likelihood expression by multiplying the particapting destination probability expressions. + result.probabilities.emplace_back(destinationIterators[0]->getProbability()); + for (uint_fast64_t i = 1; i < destinationIterators.size(); ++i) { + result.probabilities.back() = result.probabilities.back() * destinationIterators[i]->getProbability(); + } + + // Now concatenate all assignments of all participating destinations. + TemplateEdgeDestination templateDestination; + for (uint_fast64_t i = 0; i < destinationIterators.size(); ++i) { + for (auto const& assignment : destinationIterators[i]->getOrderedAssignments().getAllAssignments()) { + templateDestination.addAssignment(assignment); + } + } + + // Then we are ready to add the new destination. + result.templateEdge->addDestination(templateDestination); + + // Finally, add the location effects. + result.effects.emplace_back(); + for (uint_fast64_t i = 0; i < destinationIterators.size(); ++i) { + result.effects.back().push_back(destinationIterators[i]->getLocationIndex()); + } + + // Now check whether there is some update combination we have not yet explored. + bool movedIterator = false; + for (int_fast64_t j = destinationIterators.size() - 1; j >= 0; --j) { + ++destinationIterators[j]; + if (destinationIterators[j] != edgesToSynchronize[j].get().getDestinations().cend()) { + movedIterator = true; + break; + } else { + // Reset the iterator to the beginning of the list. + destinationIterators[j] = edgesToSynchronize[j].get().getDestinations().cbegin(); + } + } + + doneDestinations = !movedIterator; + } while (!doneDestinations); + + return result; + } + + std::vector createSynchronizingMetaEdges(Model const& oldModel, Model& newModel, Automaton& newAutomaton, std::vector>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector> const& composedAutomata, storm::solver::SmtSolver& solver) { std::vector result; // Gather all participating automata and the corresponding input symbols. + std::vector components; std::vector, uint64_t>> participatingAutomataAndActions; for (uint64_t i = 0; i < composedAutomata.size(); ++i) { std::string const& actionName = vector.getInput(i); if (!SynchronizationVector::isNoActionInput(actionName)) { + components.push_back(i); uint64_t actionIndex = oldModel.getActionIndex(actionName); participatingAutomataAndActions.push_back(std::make_pair(composedAutomata[i], actionIndex)); synchronizingActionIndices[i].insert(actionIndex); @@ -114,11 +226,100 @@ namespace storm { } } + // If there are no valid combinations for the action, we need to skip the generation of synchronizing edges. + if (!noCombinations) { + // Save state of solver so that we can always restore the point where we have exactly the constant values + // and variables bounds on the assertion stack. + solver.push(); + + // Start by creating a fresh auxiliary variable for each edge and link it with the guard. + std::vector> edgeVariables(possibleEdges.size()); + std::vector allEdgeVariables; + for (uint_fast64_t outerIndex = 0; outerIndex < possibleEdges.size(); ++outerIndex) { + // Create auxiliary variables and link them with the guards. + for (uint_fast64_t innerIndex = 0; innerIndex < possibleEdges[outerIndex].size(); ++innerIndex) { + edgeVariables[outerIndex].push_back(newModel.getManager().declareFreshBooleanVariable()); + allEdgeVariables.push_back(edgeVariables[outerIndex].back()); + solver.add(implies(edgeVariables[outerIndex].back(), possibleEdges[outerIndex][innerIndex].get().getGuard())); + } + + storm::expressions::Expression atLeastOneEdgeFromAutomaton = newModel.getManager().boolean(false); + for (auto const& edgeVariable : edgeVariables[outerIndex]) { + atLeastOneEdgeFromAutomaton = atLeastOneEdgeFromAutomaton || edgeVariable; + } + solver.add(atLeastOneEdgeFromAutomaton); + + storm::expressions::Expression atMostOneEdgeFromAutomaton = newModel.getManager().boolean(true); + for (uint64_t first = 0; first < possibleEdges[outerIndex].size(); ++first) { + for (uint64_t second = first + 1; second < possibleEdges[outerIndex].size(); ++second) { + atMostOneEdgeFromAutomaton = atMostOneEdgeFromAutomaton && !(edgeVariables[outerIndex][first] && edgeVariables[outerIndex][second]); + } + } + solver.add(atMostOneEdgeFromAutomaton); + } + + // Now enumerate all possible combinations. + solver.allSat(allEdgeVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool { + // Now we need to reconstruct the chosen edges from the valuation of the edge variables. + std::vector> chosenEdges; + + for (uint_fast64_t outerIndex = 0; outerIndex < edgeVariables.size(); ++outerIndex) { + for (uint_fast64_t innerIndex = 0; innerIndex < edgeVariables[outerIndex].size(); ++innerIndex) { + if (modelReference.getBooleanValue(edgeVariables[outerIndex][innerIndex])) { + chosenEdges.emplace_back(possibleEdges[outerIndex][innerIndex]); + break; + } + } + } + + // Get a basic conditional meta edge that represents the synchronization of the provided edges. + // Note that there is still information missing, which we need to add (like the action index etc.). + ConditionalMetaEdge conditionalMetaEdge = createSynchronizedMetaEdge(newAutomaton, chosenEdges); + + // Set the participating components. + conditionalMetaEdge.components = components; + + // Set the action index. + conditionalMetaEdge.actionIndex = Model::SILENT_ACTION_INDEX; + if (vector.getOutput() != Model::SILENT_ACTION_NAME) { + if (newModel.hasAction(vector.getOutput())) { + conditionalMetaEdge.actionIndex = newModel.getActionIndex(vector.getOutput()); + } else { + conditionalMetaEdge.actionIndex = newModel.addAction(Action(vector.getOutput())); + } + } + + result.push_back(conditionalMetaEdge); + + return true; + }); + + solver.pop(); + } return result; } - std::unordered_map, uint64_t, storm::utility::vector::VectorHash> addEdgesToReachableLocations(Model const& model, std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& conditionalMetaEdges) { + void createCombinedLocation(std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& locations, bool initial = false) { + std::stringstream locationNameBuilder; + for (uint64_t i = 0; i < locations.size(); ++i) { + locationNameBuilder << composedAutomata[i].get().getLocation(locations[i]).getName() << "_"; + } + + uint64_t locationIndex = newAutomaton.addLocation(Location(locationNameBuilder.str())); + Location& location = newAutomaton.getLocation(locationIndex); + for (uint64_t i = 0; i < locations.size(); ++i) { + for (auto const& assignment : composedAutomata[i].get().getLocation(locations[i]).getAssignments()) { + location.addTransientAssignment(assignment); + } + } + + if (initial) { + newAutomaton.addInitialLocation(locationIndex); + } + } + + void addEdgesToReachableLocations(Model const& model, std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& conditionalMetaEdges) { // Maintain a stack of locations that still need to be to explored. std::vector> locationsToExplore; @@ -143,6 +344,7 @@ namespace storm { for (auto const& location : locationsToExplore) { uint64_t id = newLocationMapping.size(); newLocationMapping[location] = id; + createCombinedLocation(composedAutomata, newAutomaton, location, true); } // As long as there are locations to explore, do so. @@ -177,6 +379,7 @@ namespace storm { newLocationMapping[targetLocationCombination] = id; locationsToExplore.emplace_back(std::move(targetLocationCombination)); newLocations.emplace_back(id); + createCombinedLocation(composedAutomata, newAutomaton, newLocations); } } @@ -184,8 +387,6 @@ namespace storm { } } } - - return newLocationMapping; } Model Model::flattenComposition(std::shared_ptr const& smtSolverFactory) const { @@ -215,12 +416,14 @@ namespace storm { // Ensure that we have a parallel composition from now on. STORM_LOG_THROW(systemComposition.isParallelComposition(), storm::exceptions::WrongFormatException, "Unknown system composition cannot be flattened."); ParallelComposition const& parallelComposition = systemComposition.asParallelComposition(); - + + // Create the new automaton that will hold the flattened system. Automaton newAutomaton(this->getName() + "_flattening"); - for (auto const & variable : getGlobalVariables()) { + + std::map> variableRemapping; + for (auto const& variable : getGlobalVariables()) { std::unique_ptr renamedVariable = variable.clone(); - renamedVariable->setName("global_" + renamedVariable->getName()); - newAutomaton.addVariable(*renamedVariable); + variableRemapping.emplace(&variable, flattenedModel.addVariable(*renamedVariable)); } std::vector> composedAutomata; @@ -235,7 +438,7 @@ namespace storm { for (auto const& variable : oldAutomaton.getVariables()) { std::unique_ptr renamedVariable = variable.clone(); renamedVariable->setName(oldAutomaton.getName() + "_" + renamedVariable->getName()); - newAutomaton.addVariable(*renamedVariable); + variableRemapping.emplace(&variable, newAutomaton.addVariable(*renamedVariable)); } } @@ -253,7 +456,7 @@ namespace storm { } // Perform all necessary synchronizations and keep track which action indices participate in synchronization. - std::vector> synchronizingActionIndices; + std::vector> synchronizingActionIndices(composedAutomata.size()); std::vector conditionalMetaEdges; for (auto const& vector : parallelComposition.getSynchronizationVectors()) { // If less then 2 automata participate, there is no need to perform a synchronization. @@ -262,7 +465,7 @@ namespace storm { } // Create all conditional template edges corresponding to this synchronization vector. - std::vector newConditionalMetaEdges = createSynchronizingMetaEdges(*this, flattenedModel, synchronizingActionIndices, vector, composedAutomata, *solver); + std::vector newConditionalMetaEdges = createSynchronizingMetaEdges(*this, flattenedModel, newAutomaton, synchronizingActionIndices, vector, composedAutomata, *solver); conditionalMetaEdges.insert(conditionalMetaEdges.end(), newConditionalMetaEdges.begin(), newConditionalMetaEdges.end()); } @@ -281,43 +484,37 @@ namespace storm { } } - std::shared_ptr templateEdge = newAutomaton.createTemplateEdge(edge.getGuard()); conditionalMetaEdges.emplace_back(); ConditionalMetaEdge& conditionalMetaEdge = conditionalMetaEdges.back(); + conditionalMetaEdge.templateEdge = newAutomaton.createTemplateEdge(edge.getGuard()); conditionalMetaEdge.actionIndex = edge.getActionIndex(); conditionalMetaEdge.components.emplace_back(static_cast(i)); conditionalMetaEdge.condition.emplace_back(edge.getSourceLocationIndex()); conditionalMetaEdge.rate = edge.getOptionalRate(); for (auto const& destination : edge.getDestinations()) { + conditionalMetaEdge.templateEdge->addDestination(destination.getOrderedAssignments()); conditionalMetaEdge.effects.emplace_back(); conditionalMetaEdge.effects.back().emplace_back(destination.getLocationIndex()); conditionalMetaEdge.probabilities.emplace_back(destination.getProbability()); } - conditionalMetaEdge.templateEdge = templateEdge; } } } - std::unordered_map, uint64_t, storm::utility::vector::VectorHash> newLocationMapping = addEdgesToReachableLocations(*this, composedAutomata, newAutomaton, conditionalMetaEdges); - - for (auto const& newLocation : newLocationMapping) { - std::stringstream locationNameBuilder; - for (uint64_t i = 0; i < newLocation.first.size(); ++i) { - locationNameBuilder << composedAutomata[i].get().getLocation(newLocation.first[i]).getName() << "_"; - } - - uint64_t locationIndex = newAutomaton.addLocation(Location(locationNameBuilder.str())); - Location& location = newAutomaton.getLocation(locationIndex); - for (uint64_t i = 0; i < newLocation.first.size(); ++i) { - for (auto const& assignment : composedAutomata[i].get().getLocation(newLocation.first[i]).getAssignments()) { - location.addTransientAssignment(assignment); - } - } - } + // Now that all meta edges have been built, we can explore the location space and add all edges based + // on the templates. + addEdgesToReachableLocations(*this, composedAutomata, newAutomaton, conditionalMetaEdges); + + // Fix all variables mentioned in assignments by applying the constructed remapping. + newAutomaton.changeAssignmentVariables(variableRemapping); + // Finalize the flattened model. + newAutomaton.setInitialStatesRestriction(this->getInitialStatesExpression(composedAutomata)); flattenedModel.addAutomaton(newAutomaton); + flattenedModel.setStandardSystemComposition(); + flattenedModel.finalize(); return flattenedModel; } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 093df98c4..607d03452 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -35,6 +35,19 @@ namespace storm { */ Model(std::string const& name, ModelType const& modelType, uint64_t version = 1, boost::optional> const& expressionManager = boost::none); + /*! + * Copies the given model. + */ + Model(Model const& other); + + /*! + * Copy-assigns the given model + */ + Model& operator=(Model const& other); + + Model(Model&& other) = default; + Model& operator=(Model&& other) = default; + /*! * Retrieves the expression manager responsible for the expressions in the model. */ diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index b8e664751..00358b417 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -141,6 +141,14 @@ namespace storm { } } + void OrderedAssignments::changeAssignmentVariables(std::map> const& remapping) { + std::vector newAssignments; + for (auto& assignment : allAssignments) { + newAssignments.emplace_back(remapping.at(&assignment->getVariable()), assignment->getAssignedExpression(), assignment->getLevel()); + } + *this = OrderedAssignments(newAssignments); + } + std::vector>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector> const& assignments) { return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable()); } diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 210d5f2db..5c2dd36f8 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -113,6 +113,11 @@ namespace storm { * Substitutes all variables in all expressions according to the given substitution. */ void substitute(std::map const& substitution); + + /*! + * Changes all variables in assignments based on the given mapping. + */ + void changeAssignmentVariables(std::map> const& remapping); private: static std::vector>::const_iterator lowerBound(Assignment const& assignment, std::vector> const& assignments); diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 05e05c250..4446d7e10 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -62,6 +62,13 @@ namespace storm { destination.substitute(substitution); } } + + void TemplateEdge::changeAssignmentVariables(std::map> const& remapping) { + for (auto& destination : destinations) { + destination.changeAssignmentVariables(remapping); + } + assignments.changeAssignmentVariables(remapping); + } void TemplateEdge::liftTransientDestinationAssignments() { if (!destinations.empty()) { diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index be9a1ae95..5839f3daa 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/src/storm/storage/jani/TemplateEdge.h @@ -52,6 +52,11 @@ namespace storm { */ void substitute(std::map const& substitution); + /*! + * Changes all variables in assignments based on the given mapping. + */ + void changeAssignmentVariables(std::map> const& remapping); + /*! * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these * assignments are no longer contained in the destination. Note that this may modify the semantics of the diff --git a/src/storm/storage/jani/TemplateEdgeDestination.cpp b/src/storm/storage/jani/TemplateEdgeDestination.cpp index 10660e4fd..0330d61f3 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.cpp +++ b/src/storm/storage/jani/TemplateEdgeDestination.cpp @@ -19,6 +19,10 @@ namespace storm { assignments.substitute(substitution); } + void TemplateEdgeDestination::changeAssignmentVariables(std::map> const& remapping) { + assignments.changeAssignmentVariables(remapping); + } + OrderedAssignments const& TemplateEdgeDestination::getOrderedAssignments() const { return assignments; } diff --git a/src/storm/storage/jani/TemplateEdgeDestination.h b/src/storm/storage/jani/TemplateEdgeDestination.h index 6967f0aef..8398f8717 100644 --- a/src/storm/storage/jani/TemplateEdgeDestination.h +++ b/src/storm/storage/jani/TemplateEdgeDestination.h @@ -10,13 +10,18 @@ namespace storm { TemplateEdgeDestination() = default; TemplateEdgeDestination(OrderedAssignments const& assignments); TemplateEdgeDestination(Assignment const& assignment); - TemplateEdgeDestination(std::vector const& assignments = {}); + TemplateEdgeDestination(std::vector const& assignments); /*! * Substitutes all variables in all expressions according to the given substitution. */ void substitute(std::map const& substitution); + /*! + * Changes all variables in assignments based on the given mapping. + */ + void changeAssignmentVariables(std::map> const& remapping); + OrderedAssignments const& getOrderedAssignments() const; // Convenience methods to access the assignments. diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index 0fa697b9c..4c8b86591 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -250,5 +250,14 @@ namespace storm { return false; } + std::map> VariableSet::getNameToVariableMap() const { + std::map> result; + + for (auto const& variable : variables) { + result.emplace(variable->getName(), *variable); + } + + return result; + } } } diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h index 1da930022..200489116 100644 --- a/src/storm/storage/jani/VariableSet.h +++ b/src/storm/storage/jani/VariableSet.h @@ -199,6 +199,11 @@ namespace storm { */ bool containsVariablesInBoundExpressionsOrInitialValues(std::set const& variables) const; + /*! + * Retrieves a mapping from variable names to (references of) the variable objects. + */ + std::map> getNameToVariableMap() const; + private: /// The vector of all variables. std::vector> variables; diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index e13ec574e..d5be5ed9c 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -94,6 +94,8 @@ #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/storage/jani/JSONExporter.h" + namespace storm { template diff --git a/src/test/storage/JaniModelTest.cpp b/src/test/storage/JaniModelTest.cpp new file mode 100644 index 000000000..8b13f179c --- /dev/null +++ b/src/test/storage/JaniModelTest.cpp @@ -0,0 +1,155 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "storm/parser/PrismParser.h" + +#include "storm/utility/solver.h" + +#include "storm/storage/jani/Model.h" + +#ifdef STORM_HAVE_MSAT +TEST(JaniModelTest, FlattenModules) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(179, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(70, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(5024, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); +} +#endif + +#ifdef STORM_HAVE_Z3 +TEST(JaniModelTest, FlattenModules_Leader_Z3) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Wlan_Z3) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(179, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Csma_Z3) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(70, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Firewire_Z3) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(5024, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Coin_Z3) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); +} + +TEST(JaniModelTest, FlattenModules_Dice_Z3) { + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); + storm::jani::Model janiModel = program.toJani(); + + std::shared_ptr smtSolverFactory = std::make_shared(); + + ASSERT_NO_THROW(model = model.flattenComposition(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); +} +#endif