From a427eae699722895380a5f69d3e83031c88a2f62 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 12 Oct 2017 14:27:36 +0200 Subject: [PATCH] fixed severe bug in symbolic bisimulation minimization --- .../SymbolicMinMaxLinearEquationSolver.cpp | 8 ++++ .../SymbolicNativeLinearEquationSolver.cpp | 2 +- .../storage/dd/BisimulationDecomposition.cpp | 2 +- .../dd/bisimulation/MdpPartitionRefiner.cpp | 2 +- .../storage/dd/bisimulation/Partition.cpp | 2 +- .../dd/bisimulation/PartitionRefiner.cpp | 4 +- .../dd/bisimulation/SignatureRefiner.cpp | 37 ++++++++++++------- .../dd/bisimulation/SignatureRefiner.h | 2 +- .../SymbolicBisimulationDecompositionTest.cpp | 24 ++++++------ 9 files changed, 50 insertions(+), 33 deletions(-) diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 2df70a371..904458646 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -35,6 +35,14 @@ namespace storm { default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } + + // Adjust the method if none was specified and we are using rational numbers. + if (std::is_same::value) { + if (settings.isMinMaxEquationSolvingMethodSetFromDefaultValue() && this->solutionMethod != SolutionMethod::RationalSearch) { + STORM_LOG_INFO("Selecting 'rational search' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method."); + this->solutionMethod = SolutionMethod::RationalSearch; + } + } } template diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 5c6da4572..209623ef2 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -39,7 +39,7 @@ namespace storm { // Adjust the method if none was specified and we are using rational numbers. if (std::is_same::value) { if (settings.isLinearEquationSystemTechniqueSetFromDefaultValue() && this->method != SolutionMethod::RationalSearch) { - STORM_LOG_INFO("Selecting the rational search as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method."); + STORM_LOG_INFO("Selecting 'rational search' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method."); this->method = SolutionMethod::RationalSearch; } } diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index f1bd4ef88..9476e39da 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -94,7 +94,7 @@ namespace storm { template std::shared_ptr> BisimulationDecomposition::getQuotient() const { STORM_LOG_THROW(this->refiner->getStatus() == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed."); - + STORM_LOG_TRACE("Starting quotient extraction."); QuotientExtractor extractor; std::shared_ptr> quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation); diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index a79c67720..0a1715a5d 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -8,7 +8,7 @@ namespace storm { namespace bisimulation { template - MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) { + MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables(), true) { // Intentionally left empty. } diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 0fa4dffd4..33e3fd48e 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -100,7 +100,7 @@ namespace storm { template Partition Partition::createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel const& model, std::pair const& blockVariables) { - storm::dd::Bdd choicePartitionBdd = !model.getIllegalMask().renameVariables(model.getRowVariables(), model.getColumnVariables()) && model.getManager().getEncoding(blockVariables.first, 0, false); + storm::dd::Bdd choicePartitionBdd = (!model.getIllegalMask() && model.getReachableStates()).renameVariables(model.getRowVariables(), model.getColumnVariables()) && model.getManager().getEncoding(blockVariables.first, 0, false); // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 8d566d036..167efd529 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -10,7 +10,7 @@ namespace storm { namespace bisimulation { template - PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getNondeterminismVariables()) { + PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), !model.isOfType(storm::models::ModelType::Mdp), model.getNondeterminismVariables()) { // Intentionally left empty. } @@ -50,7 +50,7 @@ namespace storm { STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); auto refinementStart = std::chrono::high_resolution_clock::now(); - newPartition = signatureRefiner.refine(statePartition, signature); + newPartition = signatureRefiner.refine(oldPartition, signature); auto refinementEnd = std::chrono::high_resolution_clock::now(); totalRefinementTime += (refinementEnd - refinementStart); diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 3dcb5a5b9..eb16ecf57 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -61,7 +61,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, bool shiftStateVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), shiftStateVariables(shiftStateVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { // Initialize precomputed data. auto const& ddMetaVariable = manager.getMetaVariable(blockVariable); @@ -147,12 +147,14 @@ namespace storm { DdNode* partitionElse; DdNode* signatureThen; DdNode* signatureElse; - short offset = 1; + short offset; + bool isNondeterminismVariable = false; while (skippedBoth && !Cudd_IsConstant(nonBlockVariablesNode)) { // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - offset = 1; + offset = shiftStateVariables ? 1 : 0; if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { offset = 0; + isNondeterminismVariable = true; } if (Cudd_NodeReadIndex(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { @@ -175,7 +177,7 @@ namespace storm { if (skippedBoth) { // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. nonBlockVariablesNode = Cudd_T(nonBlockVariablesNode); - if (offset == 0) { + if (isNondeterminismVariable) { nondeterminismVariablesNode = Cudd_T(nondeterminismVariablesNode); } } @@ -186,9 +188,9 @@ namespace storm { return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - DdNode* thenResult = refine(partitionThen, signatureThen, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNode* thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(thenResult); - DdNode* elseResult = refine(partitionElse, signatureElse, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNode* elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(elseResult); DdNode* result; @@ -223,6 +225,9 @@ namespace storm { storm::dd::Bdd nondeterminismVariables; storm::dd::Bdd nonBlockVariables; + // A flag indicating whether we are to shift the state variables by one. + bool shiftStateVariables; + // The indices of the DD variables associated with the block variable. std::vector blockDdVariableIndices; @@ -248,7 +253,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, bool shiftStateVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), shiftStateVariables(shiftStateVariables), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { // Perform garbage collection to clean up stuff not needed anymore. LACE_ME; sylvan_gc(); @@ -363,12 +368,14 @@ namespace storm { BDD partitionElse; MTBDD signatureThen; MTBDD signatureElse; - short offset = 1; + short offset; + bool isNondeterminismVariable = false; while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) { // Remember an offset that indicates whether the top variable is a nondeterminism variable or not. - offset = 1; + offset = shiftStateVariables ? 1 : 0; if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) { offset = 0; + isNondeterminismVariable = true; } if (storm::dd::InternalAdd::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { @@ -391,7 +398,7 @@ namespace storm { if (skippedBoth) { // If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables. nonBlockVariablesNode = sylvan_high(nonBlockVariablesNode); - if (offset == 0) { + if (isNondeterminismVariable) { nondeterminismVariablesNode = sylvan_high(nondeterminismVariablesNode); } } @@ -402,9 +409,9 @@ namespace storm { return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); } - BDD thenResult = refine(partitionThen, signatureThen, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); bdd_refs_push(thenResult); - BDD elseResult = refine(partitionElse, signatureElse, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); bdd_refs_push(elseResult); BDD result; @@ -432,6 +439,8 @@ namespace storm { storm::dd::Bdd nondeterminismVariables; storm::dd::Bdd nonBlockVariables; + bool shiftStateVariables; + uint64_t numberOfBlockVariables; storm::dd::Bdd blockCube; @@ -462,7 +471,7 @@ namespace storm { }; template - SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, std::set const& nondeterminismVariables) : manager(&manager), stateVariables(stateVariables) { + SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, bool shiftStateVariables, std::set const& nondeterminismVariables) : manager(&manager), stateVariables(stateVariables) { storm::dd::Bdd nonBlockVariablesCube = manager.getBddOne(); storm::dd::Bdd nondeterminismVariablesCube = manager.getBddOne(); @@ -476,7 +485,7 @@ namespace storm { nonBlockVariablesCube &= cube; } - internalRefiner = std::make_unique>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube); + internalRefiner = std::make_unique>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube, shiftStateVariables); } template diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.h b/src/storm/storage/dd/bisimulation/SignatureRefiner.h index 72498152c..e96ad8f4e 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.h @@ -17,7 +17,7 @@ namespace storm { template class SignatureRefiner { public: - SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, std::set const& nondeterminismVariables = std::set()); + SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, bool shiftStateVariables, std::set const& nondeterminismVariables = std::set()); Partition refine(Partition const& oldPartition, Signature const& signature); diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index 7c174b018..f7f15fd42 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -87,11 +87,11 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) { decomposition.compute(); std::shared_ptr> quotient = decomposition.getQuotient(); - EXPECT_EQ(77ul, quotient->getNumberOfStates()); - EXPECT_EQ(210ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(135ul, quotient->getNumberOfStates()); + EXPECT_EQ(366ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(116ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(194ul, (quotient->as>()->getNumberOfChoices())); storm::parser::FormulaParser formulaParser; std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -103,11 +103,11 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) { decomposition2.compute(); quotient = decomposition2.getQuotient(); - EXPECT_EQ(19ul, quotient->getNumberOfStates()); - EXPECT_EQ(58ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(40ul, quotient->getNumberOfStates()); + EXPECT_EQ(110ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(34ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(66ul, (quotient->as>()->getNumberOfChoices())); } TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { @@ -125,11 +125,11 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { decomposition.compute(); std::shared_ptr> quotient = decomposition.getQuotient(); - EXPECT_EQ(252ul, quotient->getNumberOfStates()); - EXPECT_EQ(624ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(1166ul, quotient->getNumberOfStates()); + EXPECT_EQ(2769ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(500ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(2237ul, (quotient->as>()->getNumberOfChoices())); std::vector> formulas; formulas.push_back(formula); @@ -138,9 +138,9 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { decomposition2.compute(); quotient = decomposition2.getQuotient(); - EXPECT_EQ(252ul, quotient->getNumberOfStates()); - EXPECT_EQ(624ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(1166ul, quotient->getNumberOfStates()); + EXPECT_EQ(2769ul, quotient->getNumberOfTransitions()); EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); EXPECT_TRUE(quotient->isSymbolicModel()); - EXPECT_EQ(500ul, (quotient->as>()->getNumberOfChoices())); + EXPECT_EQ(2237ul, (quotient->as>()->getNumberOfChoices())); }