From 81e9d2ae507b95d59a5dca18f8916291f9af28a5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 4 Aug 2017 14:35:38 +0200 Subject: [PATCH] added some sanity checks and debug output --- .../dd/bisimulation/QuotientExtractor.cpp | 34 ++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index ff114b482..3027badf0 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -542,13 +542,26 @@ namespace storm { std::shared_ptr> QuotientExtractor::extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { auto modelType = model.getType(); + bool useRepresentativesForThisExtraction = this->useRepresentatives; if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp) { + if (modelType == storm::models::ModelType::Mdp) { + STORM_LOG_WARN_COND(!useRepresentativesForThisExtraction, "Using representatives is unsupported for MDPs, falling back to regular extraction."); + useRepresentativesForThisExtraction = false; + } + + // Sanity checks. + STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); + partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).exportToDot("partstates.dot"); + model.getReachableStates().exportToDot("origstates.dot"); + std::cout << "equal? " << (partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).template toAdd().notZero() == model.getReachableStates().template toAdd().notZero()) << std::endl; + STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition."); + std::set blockVariableSet = {partition.getBlockVariable()}; std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); - if (useRepresentatives) { + if (useRepresentativesForThisExtraction) { storm::dd::Bdd partitionAsBddOverPrimedBlockVariable = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet); storm::dd::Bdd representativePartition = partitionAsBddOverPrimedBlockVariable.existsAbstractRepresentative(model.getColumnVariables()).renameVariables(model.getColumnVariables(), blockVariableSet); partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet); @@ -556,12 +569,26 @@ namespace storm { storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); partitionAsAdd.exportToDot("partition.dot"); + model.getTransitionMatrix().sumAbstract(model.getColumnVariables()).exportToDot("origdist.dot"); auto start = std::chrono::high_resolution_clock::now(); storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables()); + STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(model.getTransitionMatrix().sumAbstract(model.getColumnVariables()), ValueType(1e-6)), "Expected something else."); + quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("sanity.dot"); quotientTransitionMatrix.exportToDot("trans-1.dot"); + partitionAsAdd = partitionAsAdd / partitionAsAdd.sumAbstract(model.getColumnVariables()); quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables()); quotientTransitionMatrix.exportToDot("quottrans.dot"); + auto partCount = partitionAsAdd.sumAbstract(model.getColumnVariables()); + partCount.exportToDot("partcount.dot"); auto end = std::chrono::high_resolution_clock::now(); + + // Check quotient matrix for sanity. + auto quotdist = quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet); + quotdist.exportToDot("quotdists.dot"); + (quotdist / partCount).exportToDot("distcount.dot"); + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd(), ValueType(1e-6)), "Illegal non-probabilistic matrix."); + STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); @@ -616,10 +643,15 @@ namespace storm { storm::dd::Add partitionAsAdd = partition.storedAsBdd() ? partition.asBdd().template toAdd() : partition.asAdd(); storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd, model.getColumnVariables()); quotientTransitionMatrix = quotientTransitionMatrix.renameVariables(blockVariableSet, model.getColumnVariables()); + partitionAsAdd = partitionAsAdd / partitionAsAdd.sumAbstract(model.getColumnVariables()); quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()); quotientTransitionMatrix = quotientTransitionMatrix.renameVariables(blockVariableSet, model.getRowVariables()); storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); + // Check quotient matrix for sanity. + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd(), ValueType(1e-6)), "Illegal non-probabilistic matrix."); + storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); storm::dd::Bdd partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables()).renameVariables(blockVariableSet, model.getRowVariables());