diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 3230232d6..bd585fa83 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, 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.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 ef23ffa5b..4fe427ffa 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, 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.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 803c7f7cb..f9df015bd 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::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) { + 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) { // Initialize precomputed data. auto const& ddMetaVariable = manager.getMetaVariable(blockVariable); @@ -108,52 +108,13 @@ 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)); @@ -222,6 +183,8 @@ namespace storm { bool skipped = true; DdNode* partitionThen; DdNode* partitionElse; + DdNode* signatureThen; + DdNode* signatureElse; short offset; bool isNondeterminismVariable = false; while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) { @@ -465,7 +428,6 @@ namespace storm { } } - storm::models::symbolic::Model const& model; storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; ::DdManager* ddman; @@ -504,7 +466,7 @@ namespace storm { template class InternalSignatureRefiner { public: - 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() { + 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() { // Perform garbage collection to clean up stuff not needed anymore. LACE_ME; sylvan_gc(); @@ -526,52 +488,14 @@ 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()); - -// 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; -// } + storm::dd::InternalBdd internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result.first)); + storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); -// 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)); @@ -881,7 +805,6 @@ namespace storm { } } - storm::models::symbolic::Model const& model; storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; storm::expressions::Variable blockVariable; @@ -922,7 +845,7 @@ namespace storm { }; template - 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) { + 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) { storm::dd::Bdd nonBlockVariablesCube = manager.getBddOne(); storm::dd::Bdd nondeterminismVariablesCube = manager.getBddOne(); @@ -936,7 +859,7 @@ namespace storm { nonBlockVariablesCube &= cube; } - internalRefiner = std::make_unique>(model, manager, blockVariable, shiftStateVariables ? stateColumnVariables : stateRowVariables, nondeterminismVariablesCube, nonBlockVariablesCube, InternalSignatureRefinerOptions(shiftStateVariables)); + internalRefiner = std::make_unique>(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 8a1a1bfac..0dedc46d7 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.h @@ -17,14 +17,11 @@ namespace storm { template class SignatureRefiner { public: - 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()); + 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()); 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;