diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index b1cafceb2..745aaea99 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -211,7 +211,7 @@ namespace storm { } boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); + composition.getSubcomposition().accept(*this, data); return boost::none; } @@ -322,7 +322,7 @@ namespace storm { int_fast64_t high = variable.getUpperBound().evaluateAsInt(); std::pair variablePair = result.manager->addMetaVariable(variable.getName(), low, high); - STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "] and " << variablePair.second.getName() << "."); + STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << "."); result.rowMetaVariables.insert(variablePair.first); result.variableToRowMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.first); @@ -1133,6 +1133,7 @@ namespace storm { subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap))); } + std::cout << "composing " << composition << std::endl; return composeInParallel(subautomata, composition.getSynchronizationVectors()); } @@ -1211,6 +1212,7 @@ namespace storm { // Extend all other non-synchronizing actions with the identity of the current subautomaton. for (auto& actions : nonSynchronizingActions) { for (auto& action : actions.second) { + STORM_LOG_TRACE("Extending action '" << actionInformation.getActionName(actions.first) << "' with identity of next composition."); action.transitions *= subautomaton.identity; } } @@ -1219,6 +1221,7 @@ namespace storm { // add it to the overall non-synchronizing action result. for (auto const& action : subautomaton.actionIndexToAction) { if (actionsInSynch.find(action.first) == actionsInSynch.end()) { + STORM_LOG_TRACE("Adding action " << actionInformation.getActionName(action.first) << " to non-synchronizing actions and multiply it with system identity."); nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity)); } } @@ -1253,6 +1256,10 @@ namespace storm { } } + for (auto act : result.actionIndexToAction) { + act.second.transitions.exportToDot("act__" + actionInformation.getActionName(act.first) + ".dot"); + } + return result; } @@ -1505,7 +1512,7 @@ namespace storm { guard |= edge.guard.toBdd(); transitions += edge.transitions; - joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment); + variableToWritingFragment = joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment); joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments); } @@ -1846,6 +1853,7 @@ namespace storm { } ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); result.actionIndexToAction[actionIndex] = actionDd; + actionDd.transitions.exportToDot("build_" + action.getName() + ".dot"); result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable())); } @@ -1895,6 +1903,7 @@ namespace storm { // Add missing global variable identities, action and nondeterminism encodings. std::map> transientEdgeAssignments; for (auto& action : automaton.actionIndexToAction) { + action.second.transitions.exportToDot("build_from_aut_" + std::to_string(action.first) + ".dot"); illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); storm::dd::Add actionEncoding = encodeAction(action.first != this->model.getSilentActionIndex() ? boost::optional(action.first) : boost::none, this->variables); @@ -1906,6 +1915,7 @@ namespace storm { } result += extendedTransitions; + result.exportToDot("result_after_" + actionInformation.getActionName(action.first) + ".dot"); } return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, numberOfUsedNondeterminismVariables); @@ -1940,6 +1950,7 @@ namespace storm { template std::shared_ptr> createModel(storm::jani::ModelType const& modelType, CompositionVariables const& variables, ModelComponents const& modelComponents) { + if (modelType == storm::jani::ModelType::DTMC) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); } else if (modelType == storm::jani::ModelType::CTMC) { @@ -2141,7 +2152,7 @@ namespace storm { // Determine the actions that will appear in the parallel composition. storm::jani::CompositionActionInformationVisitor actionInformationVisitor(model); - storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation(); + storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation(model.getSystemComposition()); // Create all necessary variables. CompositionVariableCreator variableCreator(model, actionInformation); @@ -2168,10 +2179,13 @@ namespace storm { // Perform reachability analysis to obtain reachable states. storm::dd::Bdd transitionMatrixBdd = system.transitions.notZero(); + system.transitions.exportToDot("trans.dot"); + transitionMatrixBdd.template toAdd().exportToDot("transbdd.dot"); if (model.getModelType() == storm::jani::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables); } modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); + modelComponents.reachableStates.template toAdd().exportToDot("reach_jani.dot"); // Check that the reachable fragment does not overlap with the illegal fragment. storm::dd::Bdd reachableIllegalFragment = modelComponents.reachableStates && system.illegalFragment; diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 5a1a38b98..84c9a3292 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1393,6 +1393,8 @@ namespace storm { labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression()); } + reachableStates.template toAdd().exportToDot("prism_jani.dot"); + if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp index 292ab2c17..2058801ef 100644 --- a/src/storage/jani/CompositionActionInformationVisitor.cpp +++ b/src/storage/jani/CompositionActionInformationVisitor.cpp @@ -30,7 +30,7 @@ namespace storm { // Intentionally left empty. } - ActionInformation CompositionActionInformationVisitor::getActionInformation() { + ActionInformation CompositionActionInformationVisitor::getActionInformation(storm::jani::Composition const& composition) { indexToNameMap.clear(); nameToIndexMap.clear(); @@ -45,7 +45,7 @@ namespace storm { } ++nextFreeActionIndex; - std::set nonSilentActionIndices = boost::any_cast>(model.getSystemComposition().accept(*this, boost::none)); + std::set nonSilentActionIndices = boost::any_cast>(composition.accept(*this, boost::none)); return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap); } diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h index 705773c27..23b2555e3 100644 --- a/src/storage/jani/CompositionActionInformationVisitor.h +++ b/src/storage/jani/CompositionActionInformationVisitor.h @@ -30,7 +30,7 @@ namespace storm { public: CompositionActionInformationVisitor(storm::jani::Model const& model); - ActionInformation getActionInformation(); + ActionInformation getActionInformation(storm::jani::Composition const& composition); virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override; virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override; diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index 366c0372c..83d16cb47 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -48,6 +48,7 @@ namespace storm { stream << ", "; } stream << element; + first = false; } stream << ") -> " << synchronizationVector.getOutput(); return stream; @@ -130,9 +131,9 @@ namespace storm { for (auto const& subcomposition : subcompositions) { if (!first) { stream << " || "; - first = false; } stream << *subcomposition; + first = false; } stream << ")[" << boost::algorithm::join(synchronizationVectorsAsStrings, ", ") << "]"; } diff --git a/src/storage/jani/RenameComposition.cpp b/src/storage/jani/RenameComposition.cpp index 77ab94f5c..c54febb03 100644 --- a/src/storage/jani/RenameComposition.cpp +++ b/src/storage/jani/RenameComposition.cpp @@ -35,11 +35,14 @@ namespace storm { } else { stream << "tau"; } + renamingStrings.push_back(stream.str()); } - stream << "(" << subcomposition << ") / {" << boost::join(renamingStrings, ", ") << "}"; + stream << "("; + subcomposition->write(stream); + stream << ")/{" << boost::join(renamingStrings, ", ") << "} "; } } -} \ No newline at end of file +} diff --git a/src/storage/prism/CompositionToJaniVisitor.cpp b/src/storage/prism/CompositionToJaniVisitor.cpp index 173a70bdc..625372072 100644 --- a/src/storage/prism/CompositionToJaniVisitor.cpp +++ b/src/storage/prism/CompositionToJaniVisitor.cpp @@ -2,13 +2,16 @@ #include "src/storage/prism/Compositions.h" #include "src/storage/jani/Compositions.h" +#include "src/storage/jani/CompositionActionInformationVisitor.h" #include "src/storage/jani/Model.h" namespace storm { namespace prism { std::shared_ptr CompositionToJaniVisitor::toJani(Composition const& composition, storm::jani::Model const& model) { - return boost::any_cast>(composition.accept(*this, model)); + auto result = boost::any_cast>(composition.accept(*this, model)); + std::cout << "got composition " << *result << std::endl; + return result; } boost::any CompositionToJaniVisitor::visit(ModuleComposition const& composition, boost::any const& data) { @@ -41,11 +44,23 @@ namespace storm { auto rightSubcomposition = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); storm::jani::Model const& model = boost::any_cast(data); - std::set allActions; - for (auto const& action : model.getActions()) { - allActions.insert(action.getName()); + storm::jani::CompositionActionInformationVisitor visitor(model); + storm::jani::ActionInformation leftActionInformation = visitor.getActionInformation(*leftSubcomposition); + storm::jani::ActionInformation rightActionInformation = visitor.getActionInformation(*rightSubcomposition); + + std::set leftActions; + for (auto const& actionIndex : leftActionInformation.getNonSilentActionIndices()) { + leftActions.insert(leftActionInformation.getActionName(actionIndex)); + } + std::set rightActions; + for (auto const& actionIndex : rightActionInformation.getNonSilentActionIndices()) { + rightActions.insert(rightActionInformation.getActionName(actionIndex)); } - std::shared_ptr result = std::make_shared(leftSubcomposition, rightSubcomposition, allActions); + + std::set commonActions; + std::set_intersection(leftActions.begin(), leftActions.end(), rightActions.begin(), rightActions.end(), std::inserter(commonActions, commonActions.begin())); + + std::shared_ptr result = std::make_shared(leftSubcomposition, rightSubcomposition, commonActions); return result; } @@ -63,4 +78,4 @@ namespace storm { return result; } } -} \ No newline at end of file +} diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 1b0248ce5..4f343ec88 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -365,3 +365,54 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); } + +TEST(DdJaniModelBuilderTest_Sylvan, Composition) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(21ul, mdp->getNumberOfStates()); + EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(61ul, mdp->getNumberOfChoices()); + + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(8ul, mdp->getNumberOfStates()); + EXPECT_EQ(21ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(21ul, mdp->getNumberOfChoices()); +} + +TEST(DdJaniModelBuilderTest_Cudd, Composition) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + std::shared_ptr> model = builder.build(janiModel); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(21ul, mdp->getNumberOfStates()); + EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(61ul, mdp->getNumberOfChoices()); + + modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.nm"); + janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + model = builder.build(janiModel); + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(8ul, mdp->getNumberOfStates()); + EXPECT_EQ(21ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(21ul, mdp->getNumberOfChoices()); +} +