From 0c3b163a1406cd5e865003aaae4c74eb35d3e225 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 19 Sep 2016 20:01:35 +0200 Subject: [PATCH] bugfix in unsynchronized action combination Former-commit-id: 79f1df1f0d5122140f305b8118bd56686e77345e [formerly 1a8d4203a9c908fe41d138f6361ec23f5598ce45] Former-commit-id: 0aae7434ededecec678f5f654294cc4a897788a3 --- src/builder/DdJaniModelBuilder.cpp | 23 ++++++++----------- src/builder/DdPrismModelBuilder.cpp | 2 -- .../prism/CompositionToJaniVisitor.cpp | 1 - 3 files changed, 9 insertions(+), 17 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 745aaea99..c8b6ca4ea 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1133,7 +1133,6 @@ 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()); } @@ -1255,11 +1254,7 @@ namespace storm { result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables()); } } - - for (auto act : result.actionIndexToAction) { - act.second.transitions.exportToDot("act__" + actionInformation.getActionName(act.first) + ".dot"); - } - + return result; } @@ -1323,16 +1318,22 @@ namespace storm { uint_fast64_t highestLocalNondeterminismVariable = actions.front().getHighestLocalNondeterminismVariable(); for (auto const& action : actions) { STORM_LOG_ASSERT(action.getLowestLocalNondeterminismVariable() == lowestLocalNondeterminismVariable, "Mismatching lowest nondeterminism variable indices."); + highestLocalNondeterminismVariable = std::max(highestLocalNondeterminismVariable, action.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(); + storm::dd::Bdd nondeterminismEncodingBdd = this->variables.manager->getBddOne(); for (uint_fast64_t i = action.getHighestLocalNondeterminismVariable(); i < highestLocalNondeterminismVariable; ++i) { - nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); + nondeterminismEncodingBdd &= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0); } + storm::dd::Add nondeterminismEncoding = nondeterminismEncodingBdd.template toAdd(); + action.transitions *= nondeterminismEncoding; + for (auto& variableFragment : action.variableToWritingFragment) { + variableFragment.second &= nondeterminismEncodingBdd; + } for (auto& transientAssignment : action.transientEdgeAssignments) { transientAssignment.second *= nondeterminismEncoding; } @@ -1853,7 +1854,6 @@ 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())); } @@ -1903,7 +1903,6 @@ 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); @@ -1915,7 +1914,6 @@ namespace storm { } result += extendedTransitions; - result.exportToDot("result_after_" + actionInformation.getActionName(action.first) + ".dot"); } return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, numberOfUsedNondeterminismVariables); @@ -2179,13 +2177,10 @@ 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 84c9a3292..5a1a38b98 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1393,8 +1393,6 @@ 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/prism/CompositionToJaniVisitor.cpp b/src/storage/prism/CompositionToJaniVisitor.cpp index 625372072..0a8b1cce7 100644 --- a/src/storage/prism/CompositionToJaniVisitor.cpp +++ b/src/storage/prism/CompositionToJaniVisitor.cpp @@ -10,7 +10,6 @@ namespace storm { std::shared_ptr CompositionToJaniVisitor::toJani(Composition const& composition, storm::jani::Model const& model) { auto result = boost::any_cast>(composition.accept(*this, model)); - std::cout << "got composition " << *result << std::endl; return result; }