diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index 805f4d8a5..4075e6e8d 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -7,6 +7,8 @@ #include "src/adapters/CarlAdapter.h" #include "src/solver/SmtSolver.h" +#include "src/storage/jani/AutomatonComposition.h" +#include "src/storage/jani/ParallelComposition.h" #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/StandardRewardModel.h" @@ -57,6 +59,7 @@ namespace storm { #include "resources/3rdparty/sparsepp/sparsepp.h" +#include "src/builder/jit/StateSet.h" #include "src/builder/jit/JitModelBuilderInterface.h" #include "src/builder/jit/StateBehaviour.h" #include "src/builder/jit/ModelComponentsBuilder.h" @@ -93,7 +96,7 @@ namespace storm { std::ostream& operator<<(std::ostream& out, StateType const& state) { out << "<"; - {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << state.{$variable.name} << ", "; + {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << std::boolalpha << state.{$variable.name} << ", "; {% endfor %} {% for variable in stateVariables.boundedInteger %}out << "{$variable.name}=" << state.{$variable.name} << ", "; {% endfor %} @@ -127,39 +130,40 @@ namespace storm { namespace builder { namespace jit { - static bool model_is_deterministic() { + bool model_is_deterministic() { return {$deterministic_model}; } - static bool model_is_discrete_time() { + bool model_is_discrete_time() { return {$discrete_time_model}; } - - class StateSet { - public: - StateType const& peek() const { - return storage.front(); - } - - StateType get() { - StateType result = std::move(storage.front()); - storage.pop(); - return result; - } - - void add(StateType const& state) { - storage.push(state); + + {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& state) { + if ({$edge.guard}) { + return true; } - - bool empty() const { - return storage.empty(); + return false; + } + + {% for destination in edge.destinations %} + void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value}; + {% endfor %} } - - private: - std::queue storage; - }; + {% endfor %} + } + + void destination_perform_{$edge.name}_{$destination.name}(StateType& state) { + {% for level in destination.levels %} + {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value}; + {% endfor %} + {% endfor %} + } + {% endfor %} + {% endfor %} - {% for edge in nonSynchronizingEdges %}static bool edge_enabled_{$edge.name}(StateType const& state) { + {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& state) { if ({$edge.guard}) { return true; } @@ -167,14 +171,14 @@ namespace storm { } {% for destination in edge.destinations %} - static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) { + void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) { {% for level in destination.levels %}if (level == {$level.index}) { {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};{% endfor %} } {% endfor %} } - static void destination_perform_{$edge.name}_{$destination.name}(StateType& state) { + void destination_perform_{$edge.name}_{$destination.name}(StateType& state) { {% for level in destination.levels %} {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value}; {% endfor %} @@ -182,6 +186,7 @@ namespace storm { } {% endfor %} {% endfor %} + typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType&); typedef void (*DestinationFunctionPtr)(StateType&); @@ -276,7 +281,13 @@ namespace storm { {% endfor %} initialStates.push_back(state); }{% endfor %} - {% for edge in nonSynchronizingEdges %}{ + {% for edge in nonsynch_edges %}{ + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); + {% endfor %} + } + {% endfor %} + {% for edge in synch_edges %}{ edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}); {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); {% endfor %} @@ -306,6 +317,7 @@ namespace storm { for (auto const& stateEntry : stateIds) { auto const& state = stateEntry.first; + std::cout << state << std::endl; {% for label in labels %}if ({$label.predicate}) { this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1); } @@ -331,7 +343,7 @@ namespace storm { } void explore(StateType const& initialState) { - StateSet statesToExplore; + StateSet statesToExplore; getOrAddIndex(initialState, statesToExplore); StateBehaviour behaviour; @@ -345,7 +357,8 @@ namespace storm { #endif behaviour.setExpanded(); - exploreNonSynchronizingEdges(currentState, currentIndex, behaviour, statesToExplore); + exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore); + exploreSynchronizingEdges(currentState, behaviour, statesToExplore); } this->addStateBehaviour(currentIndex, behaviour); @@ -361,28 +374,32 @@ namespace storm { return false; } - void exploreNonSynchronizingEdges(StateType const& state, IndexType const& currentIndex, StateBehaviour& behaviour, StateSet& statesToExplore) { - {% for edge in nonSynchronizingEdges %}{ - {% for destination in edge.destinations %}{ - if ({$edge.guard}) { - Choice& choice = behaviour.addChoice(); - {% for destination in edge.destinations %}{ + void exploreNonSynchronizingEdges(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) { + {% for edge in nonsynch_edges %}{ + if ({$edge.guard}) { + Choice& choice = behaviour.addChoice(); + {% for destination in edge.destinations %}{ StateType targetState(state); destination_perform_{$edge.name}_{$destination.name}(targetState); - //for (auto const& destination : edge_{$edge.name}) { - //destination.perform(targetState); - IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore); - choice.add(targetStateIndex, {$destination.value}); - //} - }{% endfor %} - } + IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore); + choice.add(targetStateIndex, {$destination.value}); + }{% endfor %} } - {% endfor %} } {% endfor %} } - IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) { + {% for vector in synch_vectors %}{$vector.functions} + {% endfor %} + + void exploreSynchronizingEdges(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) { + {% for vector in synch_vectors %}{ + exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore); + } + {% endfor %} + } + + IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) { auto it = stateIds.find(state); if (it != stateIds.end()) { return it->second; @@ -423,7 +440,9 @@ namespace storm { std::vector initialStates; std::vector deadlockStates; - {% for edge in nonSynchronizingEdges %}Edge edge_{$edge.name}; + {% for edge in nonsynch_edges %}Edge edge_{$edge.name}; + {% endfor %} + {% for edge in synch_edges %}Edge edge_{$edge.name}; {% endfor %} }; @@ -437,8 +456,7 @@ namespace storm { modelData["stateVariables"] = generateStateVariables(); cpptempl::data_list initialStates = generateInitialStates(); modelData["initialStates"] = cpptempl::make_data(initialStates); - cpptempl::data_list nonSynchronizingEdges = generateNonSynchronizingEdges(); - modelData["nonSynchronizingEdges"] = cpptempl::make_data(nonSynchronizingEdges); + generateEdges(modelData); cpptempl::data_list labels = generateLabels(); modelData["labels"] = cpptempl::make_data(labels); cpptempl::data_list terminalExpressions = generateTerminalExpressions(); @@ -678,21 +696,220 @@ namespace storm { return terminalExpressions; } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateSynchronizationVector(storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) { + std::stringstream vectorSource; + uint64_t numberOfActionInputs = synchronizationVector.getNumberOfActionInputs(); + + vectorSource << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore, "; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "Destination const& destination" << index << ", "; + } + vectorSource << "Choice& choice) {" << std::endl; + vectorSource << "StateType targetState(state);" << std::endl; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "destination" << index << ".perform(targetState);" << std::endl; + } + vectorSource << "IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);" << std::endl; + vectorSource << "choice.add(targetStateIndex, "; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "destination" << index << ".value()"; + if (index + 1 < numberOfActionInputs) { + vectorSource << " * "; + } + } + vectorSource << ");" << std::endl; + vectorSource << "}" << std::endl; + + vectorSource << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore, "; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "Edge const& edge" << index << ", "; + } + vectorSource << "Choice& choice) {" << std::endl; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "for (auto const& destination" << index << " : edge" << index << ") {" << std::endl; + } + vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(state, behaviour, statesToExplore, "; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "destination" << index << ", "; + } + vectorSource << "choice);" << std::endl; + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "}" << std::endl; + } + vectorSource << "}" << std::endl; + + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { + vectorSource << "void performSynchronizedEdges_" << synchronizationVectorIndex << "_" << index << "(StateType const& state, std::vector>> const& edges, StateBehaviour& behaviour, StateSet& statesToExplore"; + if (index > 0) { + vectorSource << ", "; + } + for (uint64_t innerIndex = 0; innerIndex < index; ++innerIndex) { + vectorSource << "Edge const& edge" << innerIndex; + if (innerIndex + 1 < index) { + vectorSource << ", "; + } + } + vectorSource << ") {" << std::endl; + vectorSource << "for (auto const& edge" << index << " : edges[" << index << "]) {" << std::endl; + if (index + 1 < numberOfActionInputs) { + vectorSource << "performSynchronizedEdges_" << synchronizationVectorIndex << "_" << (index + 1) << "(state, edges, behaviour, statesToExplore, "; + for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) { + vectorSource << "edge" << innerIndex; + if (innerIndex + 1 <= index) { + vectorSource << ", "; + } + } + vectorSource << ");" << std::endl; + } else { + vectorSource << "Choice& choice = behaviour.addChoice();" << std::endl; + vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(state, behaviour, statesToExplore, "; + for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) { + vectorSource << "edge" << innerIndex << ", "; + } + vectorSource << " choice);" << std::endl; + + } + vectorSource << "}" << std::endl; + vectorSource << "}" << std::endl; + } + + vectorSource << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector>& edges, uint64_t position) {" << std::endl; + uint64_t position = 0; + uint64_t participatingPosition = 0; + std::cout << "synch vector " << synchronizationVector << std::endl; + for (auto const& inputActionName : synchronizationVector.getInput()) { + if (!storm::jani::SynchronizationVector::isNoActionInput(inputActionName)) { + vectorSource << "if (position == " << participatingPosition << ") {" << std::endl; + + storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName()); + uint64_t actionIndex = model.getActionIndex(inputActionName); + uint64_t edgeIndex = 0; + for (auto const& edge : automaton.getEdges()) { + std::cout << "[" << automaton.getName() << "], edge " << edgeIndex << " with guard " << edge.getGuard() << " has action " << model.getAction(edge.getActionIndex()).getName() << "[" << edge.getActionIndex() << "]" << std::endl; + if (edge.getActionIndex() == actionIndex) { + std::string edgeName = automaton.getName() + "_" + std::to_string(edgeIndex); + vectorSource << "if (edge_enabled_" << edgeName << "(state)) {" << std::endl; + vectorSource << "edges.emplace_back(edge_" << edgeName << ");" << std::endl; + vectorSource << "}" << std::endl; + } + ++edgeIndex; + } + + vectorSource << "}" << std::endl; + ++participatingPosition; + } + ++position; + } + vectorSource << "}" << std::endl; + + vectorSource << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; + vectorSource << "std::vector>> edges(" << synchronizationVector.getNumberOfActionInputs() << ");" << std::endl; + + participatingPosition = 0; + for (auto const& input : synchronizationVector.getInput()) { + if (!storm::jani::SynchronizationVector::isNoActionInput(input)) { + vectorSource << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl; + vectorSource << "if (edges[" << participatingPosition << "].empty()) {" << std::endl; + vectorSource << "return;" << std::endl; + vectorSource << "};" << std::endl; + ++participatingPosition; + } + } + vectorSource << "performSynchronizedEdges_" << synchronizationVectorIndex << "_0(state, edges, behaviour, statesToExplore);" << std::endl; + vectorSource << "}" << std::endl; + + cpptempl::data_map vector; + vector["functions"] = vectorSource.str(); + vector["index"] = asString(synchronizationVectorIndex); + return vector; + } template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateNonSynchronizingEdges() { - cpptempl::data_list edges; - for (auto const& automaton : this->model.getAutomata()) { + void ExplicitJitJaniModelBuilder::generateEdges(cpptempl::data_map& modelData) { + STORM_LOG_THROW(model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions."); + + cpptempl::data_list nonSynchronizingEdges; + cpptempl::data_list synchronizingEdges; + cpptempl::data_list vectors; + + storm::jani::Composition const& topLevelComposition = model.getSystemComposition(); + if (topLevelComposition.isAutomatonComposition()) { + storm::jani::Automaton const& automaton = model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName()); uint64_t edgeIndex = 0; for (auto const& edge : automaton.getEdges()) { - if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) { - edges.push_back(generateEdge(automaton, edgeIndex, edge)); - } + nonSynchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); ++edgeIndex; } + } else { + STORM_LOG_ASSERT(topLevelComposition.isParallelComposition(), "Expected parallel composition."); + storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition(); + for (auto const& composition : parallelComposition.getSubcompositions()) { + STORM_LOG_ASSERT(composition->isAutomatonComposition(), "Expected flat parallel composition."); + } + + std::vector> synchronizingActions(parallelComposition.getNumberOfSubcompositions()); + uint64_t synchronizationVectorIndex = 0; + for (auto const& synchronizationVector : parallelComposition.getSynchronizationVectors()) { + // If the synchronization vector has at most one action input, there is no synchronization going on. + if (synchronizationVector.getNumberOfActionInputs() <= 1) { + continue; + } + + bool createVector = true; + uint64_t position = 0; + for (auto const& inputActionName : synchronizationVector.getInput()) { + if (!storm::jani::SynchronizationVector::isNoActionInput(inputActionName)) { + uint64_t actionIndex = model.getActionIndex(inputActionName); + synchronizingActions[position].insert(actionIndex); + + storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName()); + bool hasParticipatingEdge = false; + for (auto const& edge : automaton.getEdges()) { + if (edge.getActionIndex() == actionIndex) { + hasParticipatingEdge = true; + break; + } + } + + if (!hasParticipatingEdge) { + createVector = false; + } + } + ++position; + } + + if (createVector) { + cpptempl::data_map vector = generateSynchronizationVector(parallelComposition, synchronizationVector, synchronizationVectorIndex); + vectors.push_back(vector); + } + ++synchronizationVectorIndex; + } + + uint64_t position = 0; + for (auto const& composition : parallelComposition.getSubcompositions()) { + storm::jani::Automaton const& automaton = model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()); + + // Add all edges with an action index that is not mentioned in any synchronization vector as + // non-synchronizing edges. + uint64_t edgeIndex = 0; + for (auto const& edge : automaton.getEdges()) { + if (synchronizingActions[position].find(edge.getActionIndex()) != synchronizingActions[position].end()) { + synchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); + } else { + nonSynchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); + } + ++edgeIndex; + } + + ++position; + } } - return edges; + modelData["nonsynch_edges"] = cpptempl::make_data(nonSynchronizingEdges); + modelData["synch_edges"] = cpptempl::make_data(synchronizingEdges); + modelData["synch_vectors"] = cpptempl::make_data(vectors); } template @@ -720,8 +937,13 @@ namespace storm { destinationData["name"] = asString(destinationIndex); destinationData["levels"] = cpptempl::make_data(levels); destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions("state.", "double")); - destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel()); - destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel()); + if (destination.getOrderedAssignments().empty()) { + destinationData["lowestLevel"] = "0"; + destinationData["highestLevel"] = "0"; + } else { + destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel()); + destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel()); + } return destinationData; } diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h index dd4085954..c6a5a7c2f 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -9,6 +9,7 @@ #include "cpptempl.h" #include "src/storage/jani/Model.h" +#include "src/storage/jani/ParallelComposition.h" #include "src/storage/expressions/ToCppVisitor.h" #include "src/builder/BuilderOptions.h" @@ -54,7 +55,8 @@ namespace storm { cpptempl::data_map generateStateVariables(); cpptempl::data_list generateLabels(); cpptempl::data_list generateTerminalExpressions(); - cpptempl::data_list generateNonSynchronizingEdges(); + void generateEdges(cpptempl::data_map& modelData); + cpptempl::data_map generateSynchronizationVector(storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex); cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments); cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge); diff --git a/src/builder/jit/ModelComponentsBuilder.cpp b/src/builder/jit/ModelComponentsBuilder.cpp index 64b6be403..9c2d55106 100644 --- a/src/builder/jit/ModelComponentsBuilder.cpp +++ b/src/builder/jit/ModelComponentsBuilder.cpp @@ -2,6 +2,9 @@ #include "src/models/sparse/StateLabeling.h" #include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/settings/SettingsManager.h" @@ -67,6 +70,10 @@ namespace storm { if (modelType == storm::jani::ModelType::DTMC) { return new storm::models::sparse::Dtmc>(this->transitionMatrixBuilder->build(), std::move(stateLabeling)); + } else if (modelType == storm::jani::ModelType::CTMC) { + return new storm::models::sparse::Ctmc>(this->transitionMatrixBuilder->build(), std::move(stateLabeling)); + } else if (modelType == storm::jani::ModelType::MDP) { + return new storm::models::sparse::Mdp>(this->transitionMatrixBuilder->build(), std::move(stateLabeling)); } else { return nullptr; } diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp index c60d60ff3..8787a21f2 100644 --- a/src/builder/jit/StateBehaviour.cpp +++ b/src/builder/jit/StateBehaviour.cpp @@ -42,6 +42,10 @@ namespace storm { if (modelType == storm::jani::ModelType::DTMC) { choices.front().divideDistribution(static_cast(totalCount)); } + } else { + for (auto& choice : choices) { + choice.compress(); + } } } else if (choices.size() == 1) { choices.front().compress(); diff --git a/src/builder/jit/StateSet.h b/src/builder/jit/StateSet.h new file mode 100644 index 000000000..09be87d5f --- /dev/null +++ b/src/builder/jit/StateSet.h @@ -0,0 +1,36 @@ +#pragma once + +#include + +namespace storm { + namespace builder { + namespace jit { + + template + class StateSet { + public: + StateType const& peek() const { + return storage.front(); + } + + StateType get() { + StateType result = std::move(storage.front()); + storage.pop(); + return result; + } + + void add(StateType const& state) { + storage.push(state); + } + + bool empty() const { + return storage.empty(); + } + + private: + std::queue storage; + }; + + } + } +} diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index f8bdde9fd..8a5d58ce5 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -107,6 +107,7 @@ namespace storm { } for (auto const& stateIndexPair : states) { unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); + std::cout << toValuation(stateIndexPair.first).toString(true) << std::endl; for (auto const& label : labelsAndExpressions) { // Add label to state, if the corresponding expression is true. diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 35dc1f7a2..5766b6dbc 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -354,12 +354,13 @@ namespace storm { // If there was no enabled command although the module has some command with the required action label, // we must not return anything. if (commands.size() == 0) { - return boost::optional>>>(); + return boost::none; } result.get().push_back(std::move(commands)); } + STORM_LOG_ASSERT(!result->empty(), "Expected non-empty list."); return result; } @@ -434,6 +435,8 @@ namespace storm { std::vector> result; for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { + std::cout << "got act " << actionIndex << std::endl; + std::cout << "name: " << program.getActionName(actionIndex) << std::endl; boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex); // Only process this action label, if there is at least one feasible solution. @@ -456,6 +459,7 @@ namespace storm { for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::prism::Command const& command = *iteratorList[i]; + std::cout << command << std::endl; for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { storm::prism::Update const& update = command.getUpdate(j); diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 3a7a995dc..2f241958a 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -112,8 +112,6 @@ namespace storm { std::string SimpleValuation::toString(bool pretty) const { - - std::stringstream sstr; if(pretty) { sstr << "valuation {" << std::endl; @@ -179,4 +177,4 @@ namespace storm { return SimpleValuation1->booleanValues < SimpleValuation2->booleanValues || SimpleValuation1->integerValues < SimpleValuation2->integerValues || SimpleValuation1->rationalValues < SimpleValuation2->rationalValues; } } -} \ No newline at end of file +} diff --git a/src/storage/jani/AutomatonComposition.cpp b/src/storage/jani/AutomatonComposition.cpp index ae1fe999e..9593c60b2 100644 --- a/src/storage/jani/AutomatonComposition.cpp +++ b/src/storage/jani/AutomatonComposition.cpp @@ -19,7 +19,7 @@ namespace storm { return inputEnabledActions; } - bool AutomatonComposition::isAutomaton() const { + bool AutomatonComposition::isAutomatonComposition() const { return true; } diff --git a/src/storage/jani/AutomatonComposition.h b/src/storage/jani/AutomatonComposition.h index d1e7604ba..af34855b1 100644 --- a/src/storage/jani/AutomatonComposition.h +++ b/src/storage/jani/AutomatonComposition.h @@ -25,7 +25,7 @@ namespace storm { std::set const& getInputEnabledActions() const; - bool isAutomaton() const override; + virtual bool isAutomatonComposition() const override; private: /// The name of the automaton this composition element refers to. diff --git a/src/storage/jani/Composition.cpp b/src/storage/jani/Composition.cpp index 7ba39eaba..b8e039447 100644 --- a/src/storage/jani/Composition.cpp +++ b/src/storage/jani/Composition.cpp @@ -1,7 +1,26 @@ #include "src/storage/jani/Composition.h" +#include "src/storage/jani/AutomatonComposition.h" +#include "src/storage/jani/ParallelComposition.h" + namespace storm { namespace jani { + + bool Composition::isAutomatonComposition() const { + return false; + } + + bool Composition::isParallelComposition() const { + return false; + } + + AutomatonComposition const& Composition::asAutomatonComposition() const { + return static_cast(*this); + } + + ParallelComposition const& Composition::asParallelComposition() const { + return static_cast(*this); + } std::ostream& operator<<(std::ostream& stream, Composition const& composition) { composition.write(stream); diff --git a/src/storage/jani/Composition.h b/src/storage/jani/Composition.h index 0e5c10bbe..769160685 100644 --- a/src/storage/jani/Composition.h +++ b/src/storage/jani/Composition.h @@ -9,12 +9,16 @@ namespace storm { class Composition { public: - virtual bool isAutomaton() const { return false; } - virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0; virtual void write(std::ostream& stream) const = 0; + virtual bool isAutomatonComposition() const; + AutomatonComposition const& asAutomatonComposition() const; + + virtual bool isParallelComposition() const; + ParallelComposition const& asParallelComposition() const; + friend std::ostream& operator<<(std::ostream& stream, Composition const& composition); }; diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index d2635c882..5cf116bfd 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -9,7 +9,7 @@ namespace storm { namespace jani { - CompositionInformation::CompositionInformation() : nonStandardParallelComposition(false) { + CompositionInformation::CompositionInformation() : nonStandardParallelComposition(false), nestedParallelComposition(false), parallelComposition(false) { // Intentionally left empty. } @@ -41,6 +41,22 @@ namespace storm { return nonStandardParallelComposition; } + void CompositionInformation::setContainsNestedParallelComposition(bool value) { + nestedParallelComposition = value; + } + + bool CompositionInformation::containsNestedParallelComposition() const { + return nestedParallelComposition; + } + + void CompositionInformation::setContainsParallelComposition(bool value) { + parallelComposition = value; + } + + bool CompositionInformation::containsParallelComposition() const { + return parallelComposition; + } + std::string const& CompositionInformation::getActionName(uint64_t index) const { return indexToNameMap.at(index); } @@ -130,9 +146,11 @@ namespace storm { } bool containsNonStandardParallelComposition = false; + bool containsSubParallelComposition = false; for (auto const& subinfo : subinformation) { containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition(); + containsSubParallelComposition |= subinfo.containsParallelComposition(); result.addMultiplicityMap(subinfo.getAutomatonToMultiplicityMap()); } @@ -217,6 +235,8 @@ namespace storm { containsNonStandardParallelComposition |= !std::includes(synchVectorSet.begin(), synchVectorSet.end(), expectedSynchVectorSetUnderApprox.begin(), expectedSynchVectorSetUnderApprox.end(), SynchronizationVectorLexicographicalLess()); result.setContainsNonStandardParallelComposition(containsNonStandardParallelComposition); + result.setContainsParallelComposition(true); + result.setContainsNestedParallelComposition(containsSubParallelComposition); result.addNonSilentActionIndices(nonSilentActionIndices); return result; diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h index 7dfcb5a56..14914ebbf 100644 --- a/src/storage/jani/CompositionInformationVisitor.h +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -24,6 +24,12 @@ namespace storm { void setContainsNonStandardParallelComposition(bool value); bool containsNonStandardParallelComposition() const; + + void setContainsNestedParallelComposition(bool value); + bool containsNestedParallelComposition() const; + + void setContainsParallelComposition(bool value); + bool containsParallelComposition() const; std::string const& getActionName(uint64_t index) const; uint64_t getActionIndex(std::string const& name) const; @@ -57,6 +63,12 @@ namespace storm { /// A flag indicating whether the composition contains any non-standard parallel composition. bool nonStandardParallelComposition; + + /// A flag indicating whether the composition contains nested parallel compositions; + bool nestedParallelComposition; + + /// A flag indicating whether the composition contains a parallel composition; + bool parallelComposition; }; class CompositionInformationVisitor : public CompositionVisitor { diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 9bca2d689..46c4ef1be 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -59,7 +59,7 @@ namespace storm { std::vector elems; for (auto const& subcomp : composition.getSubcompositions()) { modernjson::json elemDecl; - if (subcomp->isAutomaton()) { + if (subcomp->isAutomatonComposition()) { modernjson::json autDecl; autDecl["automaton"] = std::static_pointer_cast(subcomp)->getAutomatonName(); std::vector elements; diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index ee2317df8..0203a2279 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -506,6 +506,15 @@ namespace storm { return true; } + bool Model::hasStandardCompliantComposition() const { + CompositionInformationVisitor visitor(*this, this->getSystemComposition()); + CompositionInformation info = visitor.getInformation(); + if (info.containsNestedParallelComposition()) { + return false; + } + return true; + } + bool Model::undefinedConstantsAreGraphPreserving() const { if (!this->hasUndefinedConstants()) { return true; diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 35a74ead0..8a69901e4 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -227,6 +227,7 @@ namespace storm { * @see getStandardSystemComposition */ void setStandardSystemComposition(); + /*! * Gets the system composition as the standard, fully-synchronizing parallel composition. */ @@ -314,6 +315,11 @@ namespace storm { */ bool hasStandardComposition() const; + /*! + * Checks whether the composition has no nesting. + */ + bool hasStandardCompliantComposition() const; + /*! * After adding all components to the model, this method has to be called. It recursively calls * finalize on all contained elements. All subsequent changes to the model require another call diff --git a/src/storage/jani/OrderedAssignments.cpp b/src/storage/jani/OrderedAssignments.cpp index b98d543c5..e38b93918 100644 --- a/src/storage/jani/OrderedAssignments.cpp +++ b/src/storage/jani/OrderedAssignments.cpp @@ -82,6 +82,10 @@ namespace storm { return false; } + bool OrderedAssignments::empty() const { + return allAssignments.empty(); + } + int_fast64_t OrderedAssignments::getLowestLevel() const { return allAssignments.front()->getLevel(); } diff --git a/src/storage/jani/OrderedAssignments.h b/src/storage/jani/OrderedAssignments.h index f21b09fb8..e4556c3e2 100644 --- a/src/storage/jani/OrderedAssignments.h +++ b/src/storage/jani/OrderedAssignments.h @@ -42,6 +42,11 @@ namespace storm { */ bool hasMultipleLevels() const; + /*! + * Retrieves whether this set of assignments is empty. + */ + bool empty() const; + /*! * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least * one assignment. diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index aad0e2d3d..30c28b7f4 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -74,6 +74,16 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Synchronization vector must have at least one participating action."); } + uint64_t SynchronizationVector::getNumberOfActionInputs() const { + uint64_t result = 0; + for (auto const& inputEntry : input) { + if (!isNoActionInput(inputEntry)) { + ++result; + } + } + return result; + } + bool SynchronizationVector::isNoActionInput(std::string const& action) { return action == NO_ACTION_INPUT; } @@ -151,6 +161,10 @@ namespace storm { } } + bool ParallelComposition::isParallelComposition() const { + return true; + } + Composition const& ParallelComposition::getSubcomposition(uint64_t index) const { return *subcompositions[index]; } diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h index b6ae63fdd..fd54b40b0 100644 --- a/src/storage/jani/ParallelComposition.h +++ b/src/storage/jani/ParallelComposition.h @@ -40,7 +40,11 @@ namespace storm { * Retrieves the position of the first participating action. */ uint64_t getPositionOfFirstParticipatingAction() const; - + + /*! + * Retrieves the number of action inputs, i.e. participating subcompositions. + */ + uint64_t getNumberOfActionInputs() const; // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding // automaton takes part in the synchronization. @@ -85,6 +89,8 @@ namespace storm { */ ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet); + virtual bool isParallelComposition() const override; + /*! * Retrieves the subcomposition with the given index. */ diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 0a4347396..9db4f57f8 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -172,6 +172,18 @@ namespace storm { return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands); } + Module Module::restrictActionIndices(boost::container::flat_set const& actionIndices) const { + // First construct the new vector of commands. + std::vector newCommands; + for (auto const& command : commands) { + if (actionIndices.find(command.getActionIndex()) != actionIndices.end()) { + newCommands.push_back(command); + } + } + + return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands); + } + Module Module::substitute(std::map const& substitution) const { std::vector newBooleanVariables; newBooleanVariables.reserve(this->getNumberOfBooleanVariables()); diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index c3179b407..1e60e7270 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -209,6 +209,14 @@ namespace storm { */ Module restrictCommands(boost::container::flat_set const& indexSet) const; + /*! + * Creates a new module that drops all commands whose action indices are not in the given set. + * + * @param indexSet The set of action indices for which to keep the commands. + * @return The module resulting from erasing all commands whose action indices are not in the given set. + */ + Module restrictActionIndices(boost::container::flat_set const& actionIndices) const; + /*! * Substitutes all variables in the module according to the given map. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 095e54fee..fde99fbfe 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -764,7 +764,7 @@ namespace storm { auto const& constant = newConstants[constantIndex]; // Put the corresponding expression in the substitution. - if(constant.isDefined()) { + if (constant.isDefined()) { constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression().simplify()); // If there is at least one more constant to come, we substitute the constants we have so far. @@ -1306,7 +1306,7 @@ namespace storm { std::vector cleanedModules; cleanedModules.reserve(newModules.size()); for (auto const& module : newModules) { - cleanedModules.emplace_back(module.restrictCommands(actionsToKeep)); + cleanedModules.emplace_back(module.restrictActionIndices(actionsToKeep)); } newModules = std::move(cleanedModules);