diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index bd585fa83..3230232d6 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), mdp(mdp), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables(), mdp.getColumnVariables(), true) { + MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), mdp(mdp), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureRefiner(mdp, mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables(), mdp.getColumnVariables(), true) { // Intentionally left empty. } diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 4fe427ffa..ef23ffa5b 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.getColumnVariables(), !model.isOfType(storm::models::ModelType::Mdp), model.getNondeterminismVariables()) { + PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model, model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isOfType(storm::models::ModelType::Mdp), model.getNondeterminismVariables()) { // Intentionally left empty. } diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index f9df015bd..803c7f7cb 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -81,7 +81,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { + InternalSignatureRefiner(storm::models::symbolic::Model const& model, storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()) : model(model), manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { // Initialize precomputed data. auto const& ddMetaVariable = manager.getMetaVariable(blockVariable); @@ -108,13 +108,52 @@ namespace storm { nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; + std::cout << "refining" << std::endl; + + auto start = std::chrono::high_resolution_clock::now(); + storm::dd::Bdd unchangedPartition; + storm::dd::Bdd changedPartition; + if (oldPartition.hasChangedStates()) { + auto oldPartitionBdd = oldPartition.asAdd().notZero(); + auto changedBlocks = model.getTransitionMatrix().notZero().andExists(oldPartition.changedStatesAsAdd().notZero(), model.getColumnVariables()).swapVariables(model.getRowColumnMetaVariablePairs()).andExists(oldPartitionBdd, model.getColumnVariables()); + unchangedPartition = oldPartitionBdd && !changedBlocks; + changedPartition = oldPartitionBdd && changedBlocks; + } else { + unchangedPartition = manager.getBddZero(); + changedPartition = oldPartition.asAdd().notZero(); + } + auto end = std::chrono::high_resolution_clock::now(); + std::cout << "[1] took " << std::chrono::duration_cast(end - start).count() << "ms" << std::endl; + + + // Experiment start here: + std::pair resultTmp = refine(changedPartition.template toAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); + + storm::dd::InternalAdd internalNewPartitionAddTmp(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), resultTmp.first)); + storm::dd::Add newPartitionAddTmp(oldPartition.asAdd().getDdManager(), internalNewPartitionAddTmp, oldPartition.asAdd().getContainedMetaVariables()); + newPartitionAddTmp = unchangedPartition.template toAdd() + newPartitionAddTmp; + // Perform the actual recursive refinement step. + clearCaches(); + nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); std::pair result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode()); - + // Construct resulting ADD from the obtained node and the meta information. storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result.first)); storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); + if (newPartitionAdd != newPartitionAddTmp) { + std::cout << "failed " << nextFreeBlockIndex << std::endl; + unchangedPartition.template toAdd().exportToDot("unchanged.dot"); + changedPartition.template toAdd().exportToDot("changed.dot"); + newPartitionAdd.exportToDot("new.dot"); + newPartitionAddTmp.exportToDot("new_experiment.dot"); + exit(-1); + } else { + std::cout << "passed!" << std::endl; + } + + boost::optional> optionalChangedAdd; if (result.second) { storm::dd::InternalAdd internalChangedAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result.second)); @@ -183,8 +222,6 @@ namespace storm { bool skipped = true; DdNode* partitionThen; DdNode* partitionElse; - DdNode* signatureThen; - DdNode* signatureElse; short offset; bool isNondeterminismVariable = false; while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) { @@ -428,6 +465,7 @@ namespace storm { } } + storm::models::symbolic::Model const& model; storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; ::DdManager* ddman; @@ -466,7 +504,7 @@ namespace storm { template class InternalSignatureRefiner { public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() { + InternalSignatureRefiner(storm::models::symbolic::Model const& model, storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : model(model), manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), 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(); @@ -488,14 +526,52 @@ namespace storm { STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; + + auto start = std::chrono::high_resolution_clock::now(); + storm::dd::Bdd unchangedPartition; + storm::dd::Bdd changedPartition; + if (oldPartition.hasChangedStates()) { + auto changedBlocks = model.getTransitionMatrix().notZero().andExists(oldPartition.changedStatesAsBdd(), model.getColumnVariables()).swapVariables(model.getRowColumnMetaVariablePairs()).andExists(oldPartition.asBdd(), model.getColumnVariables()); + unchangedPartition = oldPartition.asBdd() && !changedBlocks; + changedPartition = oldPartition.asBdd() && changedBlocks; + } else { + unchangedPartition = manager.getBddZero(); + changedPartition = oldPartition.asBdd(); + } + auto end = std::chrono::high_resolution_clock::now(); + std::cout << "[1] took " << std::chrono::duration_cast(end - start).count() << "ms" << std::endl; + + + // Experiment start here: +// std::pair resultTmp = refine(changedPartition.getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); +// storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(resultTmp.first)); +// storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); +// newPartitionBdd = unchangedPartition || newPartitionBdd; // Perform the actual recursive refinement step. - std::pair result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); + std::pair result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD()); // Construct resulting BDD from the obtained node and the meta information. - storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result.first)); - storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); + storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result.first)); + storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); + +// if (newPartitionBdd != newPartitionBddTmp) { +// std::cout << "failed " << std::endl; +// newPartitionBdd.template toAdd().exportToDot("new.dot"); +// newPartitionBddTmp.template toAdd().exportToDot("new_experiment.dot"); +// exit(-1); +// } else { +// std::cout << "passed!" << std::endl; +// } +// if (false) { +// auto start = std::chrono::high_resolution_clock::now(); +// uint64_t blocks = newPartitionBdd.existsAbstract(stateVariables).getNonZeroCount(); +// STORM_LOG_ASSERT(blocks == nextFreeBlockIndex, "as;df"); +// auto end = std::chrono::high_resolution_clock::now(); +// std::cout << "[2] took " << std::chrono::duration_cast(end - start).count() << "ms" << std::endl; +// } + boost::optional> optionalChangedBdd; if (options.createChangedStates) { storm::dd::InternalBdd internalChangedBdd(&internalDdManager, sylvan::Bdd(result.second)); @@ -805,6 +881,7 @@ namespace storm { } } + storm::models::symbolic::Model const& model; storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; storm::expressions::Variable blockVariable; @@ -845,7 +922,7 @@ namespace storm { }; template - SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateRowVariables, std::set const& stateColumnVariables, bool shiftStateVariables, std::set const& nondeterminismVariables) : manager(&manager) { + SignatureRefiner::SignatureRefiner(storm::models::symbolic::Model const& model, storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateRowVariables, std::set const& stateColumnVariables, bool shiftStateVariables, std::set const& nondeterminismVariables) : model(model), manager(&manager) { storm::dd::Bdd nonBlockVariablesCube = manager.getBddOne(); storm::dd::Bdd nondeterminismVariablesCube = manager.getBddOne(); @@ -859,7 +936,7 @@ namespace storm { nonBlockVariablesCube &= cube; } - internalRefiner = std::make_unique>(manager, blockVariable, shiftStateVariables ? stateColumnVariables : stateRowVariables, nondeterminismVariablesCube, nonBlockVariablesCube, InternalSignatureRefinerOptions(shiftStateVariables)); + internalRefiner = std::make_unique>(model, manager, blockVariable, shiftStateVariables ? stateColumnVariables : stateRowVariables, nondeterminismVariablesCube, nonBlockVariablesCube, InternalSignatureRefinerOptions(shiftStateVariables)); } template diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.h b/src/storm/storage/dd/bisimulation/SignatureRefiner.h index 0dedc46d7..8a1a1bfac 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.h @@ -17,11 +17,14 @@ namespace storm { template class SignatureRefiner { public: - SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateRowVariables, std::set const& stateColumnVariables, bool shiftStateVariables, std::set const& nondeterminismVariables = std::set()); + SignatureRefiner(storm::models::symbolic::Model const& model, storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateRowVariables, std::set const& stateColumnVariables, bool shiftStateVariables, std::set const& nondeterminismVariables = std::set()); Partition refine(Partition const& oldPartition, Signature const& signature); private: + // The model. + storm::models::symbolic::Model const& model; + // The manager responsible for the DDs. storm::dd::DdManager const* manager;