From a7dcdcd84d450061470915d51f105e5651459e5b Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 23 Aug 2017 14:45:19 +0200 Subject: [PATCH] started on tests and added a ton of debug output --- resources/examples/testfiles/mdp/leader3.nm | 3 + .../dd/bisimulation/MdpPartitionRefiner.cpp | 2 +- .../dd/bisimulation/QuotientExtractor.cpp | 1 + .../dd/bisimulation/SignatureRefiner.cpp | 36 +++-- .../SymbolicBisimulationDecompositionTest.cpp | 146 ++++++++++++++++++ 5 files changed, 178 insertions(+), 10 deletions(-) create mode 100644 src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp diff --git a/resources/examples/testfiles/mdp/leader3.nm b/resources/examples/testfiles/mdp/leader3.nm index 96339dd96..b8f365984 100644 --- a/resources/examples/testfiles/mdp/leader3.nm +++ b/resources/examples/testfiles/mdp/leader3.nm @@ -84,6 +84,9 @@ module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23 module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule //---------------------------------------------------------------------------------------------------------------------------- +rewards "rounds" + [c12] true : 1; +endrewards //---------------------------------------------------------------------------------------------------------------------------- formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0); diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 80ef0761a..5381fa915 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -32,7 +32,7 @@ namespace storm { // If the choice partition changed, refine the state partition. Use qualitative mode we must properly abstract from choice counts. STORM_LOG_TRACE("Refining state partition."); Partition newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Qualitative); - + if (newStatePartition == this->statePartition) { this->status = Status::FixedPoint; return false; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 0e6e310f5..83201cfbe 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -846,6 +846,7 @@ namespace storm { auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs()); storm::dd::Bdd partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd(); + partitionAsBdd.exportToDot("part.dot"); partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); auto start = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index a67fa9962..bf7c0037a 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -26,6 +26,9 @@ #include "sylvan_table.h" #include "sylvan_int.h" +// FIXME: remove +#include "storm/storage/dd/DdManager.h" + namespace storm { namespace dd { namespace bisimulation { @@ -58,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()), 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) : 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) { // Initialize precomputed data. auto const& ddMetaVariable = manager.getMetaVariable(blockVariable); @@ -81,6 +84,7 @@ namespace storm { // Clear the caches. signatureCache.clear(); reuseBlocksCache.clear(); + std::cout << "clearing reuse, " << reuseBlocksCache.size() << std::endl; nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex(); // Perform the actual recursive refinement step. @@ -98,22 +102,20 @@ namespace storm { blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0; blockIndex >>= 1; } - ::DdManager* ddMan = internalDdManager.getCuddManager().getManager(); - DdNodePtr bddEncoding = Cudd_CubeArrayToBdd(ddMan, blockEncoding.data()); + DdNodePtr bddEncoding = Cudd_CubeArrayToBdd(ddman, blockEncoding.data()); Cudd_Ref(bddEncoding); - DdNodePtr result = Cudd_BddToAdd(ddMan, bddEncoding); + DdNodePtr result = Cudd_BddToAdd(ddman, bddEncoding); Cudd_Ref(result); - Cudd_RecursiveDeref(ddMan, bddEncoding); + Cudd_RecursiveDeref(ddman, bddEncoding); Cudd_Deref(result); return result; } DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { - ::DdManager* ddman = internalDdManager.getCuddManager().getManager(); - // If we arrived at the constant zero node, then this was an illegal state encoding (we require // all states to be non-deadlock). if (partitionNode == Cudd_ReadZero(ddman)) { + std::cout << "returning zero " << partitionNode << std::endl; return partitionNode; } @@ -121,6 +123,7 @@ namespace storm { auto nodePair = std::make_pair(signatureNode, partitionNode); auto it = signatureCache.find(nodePair); if (it != signatureCache.end()) { + std::cout << "cache hit " << it->second << std::endl; // If so, we return the corresponding result. return it->second; } @@ -129,13 +132,18 @@ namespace storm { if (Cudd_IsConstant(nonBlockVariablesNode)) { // If this is the first time (in this traversal) that we encounter this signature, we check // whether we can assign the old block number to it. + std::cout << "reuse size: " << reuseBlocksCache.size() << std::endl; auto& reuseEntry = reuseBlocksCache[partitionNode]; + std::cout << "reused? " << reuseEntry.isReused() << std::endl; if (!reuseEntry.isReused()) { reuseEntry.setReused(); + std::cout << "setting " << partitionNode << " to being reused" << std::endl; signatureCache[nodePair] = partitionNode; + std::cout << "reuse cache hit " << partitionNode << std::endl; return partitionNode; } else { DdNode* result = encodeBlock(nextFreeBlockIndex++); + std::cout << "block encoding " << result << std::endl; signatureCache[nodePair] = result; return result; } @@ -190,7 +198,10 @@ namespace storm { Cudd_Ref(thenResult); DdNode* elseResult = refine(partitionElse, signatureElse, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); Cudd_Ref(elseResult); - + + std::cout << "got then " << thenResult << std::endl; + std::cout << "got else " << elseResult << std::endl; + DdNode* result; if (thenResult == elseResult) { Cudd_Deref(thenResult); @@ -200,6 +211,7 @@ namespace storm { // Get the node to connect the subresults. bool complemented = Cudd_IsComplement(thenResult); result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult); + std::cout << "got " << result << " as a result node, idx " << (Cudd_NodeReadIndex(nonBlockVariablesNode) + offset) << " and children " << Cudd_NodeReadIndex(thenResult) << " [" << Cudd_IsConstant(thenResult) << "] (" << thenResult << ") and " << Cudd_NodeReadIndex(elseResult) << " [" << Cudd_IsConstant(elseResult) << "] (" << elseResult << ")" << std::endl; if (complemented) { result = Cudd_Not(result); } @@ -210,12 +222,14 @@ namespace storm { // Store the result in the cache. signatureCache[nodePair] = result; + std::cout << "returning " << result << " with index " << Cudd_NodeReadIndex(result) << ", const? " << Cudd_IsConstant(result) << std::endl; return result; } } storm::dd::DdManager const& manager; storm::dd::InternalDdManager const& internalDdManager; + ::DdManager* ddman; storm::expressions::Variable const& blockVariable; // The cubes representing all non-block and all nondeterminism variables, respectively. @@ -480,7 +494,11 @@ namespace storm { template Partition SignatureRefiner::refine(Partition const& oldPartition, Signature const& signature) { - return internalRefiner->refine(oldPartition, signature); + oldPartition.asAdd().getDdManager().debugCheck(); + oldPartition.asAdd().exportToDot("lastpart.dot"); + Partition result = internalRefiner->refine(oldPartition, signature); + oldPartition.asAdd().getDdManager().debugCheck(); + return result; } template class SignatureRefiner; diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp new file mode 100644 index 000000000..df250bc59 --- /dev/null +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -0,0 +1,146 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/parser/PrismParser.h" +#include "storm/parser/FormulaParser.h" + +#include "storm/builder/DdPrismModelBuilder.h" + +#include "storm/storage/dd/BisimulationDecomposition.h" +#include "storm/storage/SymbolicModelDescription.h" + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" + +TEST(SymbolicModelBisimulationDecomposition, Die_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::storage::BisimulationType::Strong); + decomposition.compute(); + std::shared_ptr> quotient = decomposition.getQuotient(); + + EXPECT_EQ(11ul, quotient->getNumberOfStates()); + EXPECT_EQ(17ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + std::vector> formulas; + formulas.push_back(formula); + + storm::dd::BisimulationDecomposition decomposition2(*model, formulas, storm::storage::BisimulationType::Strong); + decomposition2.compute(); + quotient = decomposition2.getQuotient(); + + EXPECT_EQ(5ul, quotient->getNumberOfStates()); + EXPECT_EQ(8ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); +} + +TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) { + storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm"); + + // Preprocess model to substitute all constants. + smd = smd.preprocess(); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(smd.asPrismProgram()); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::storage::BisimulationType::Strong); + decomposition.compute(); + std::shared_ptr> quotient = decomposition.getQuotient(); + + EXPECT_EQ(2007ul, quotient->getNumberOfStates()); + EXPECT_EQ(3738ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + + std::vector> formulas; + formulas.push_back(formula); + + storm::dd::BisimulationDecomposition decomposition2(*model, formulas, storm::storage::BisimulationType::Strong); + decomposition2.compute(); + quotient = decomposition2.getQuotient(); + + EXPECT_EQ(65ul, quotient->getNumberOfStates()); + EXPECT_EQ(105ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); +} + +TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::storage::BisimulationType::Strong); + decomposition.compute(); + std::shared_ptr> quotient = decomposition.getQuotient(); + + EXPECT_EQ(77ul, quotient->getNumberOfStates()); + EXPECT_EQ(210ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); + EXPECT_EQ(116ul, (quotient->as>()->getNumberOfChoices())); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + + std::vector> formulas; + formulas.push_back(formula); + + storm::dd::BisimulationDecomposition decomposition2(*model, formulas, storm::storage::BisimulationType::Strong); + decomposition2.compute(); + quotient = decomposition2.getQuotient(); + + EXPECT_EQ(19ul, quotient->getNumberOfStates()); + EXPECT_EQ(58ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); + EXPECT_EQ(34ul, (quotient->as>()->getNumberOfChoices())); +} + +TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) { + storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm"); + + // Preprocess model to substitute all constants. + smd = smd.preprocess(); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(smd.asPrismProgram()); + + storm::dd::BisimulationDecomposition decomposition(*model, storm::storage::BisimulationType::Strong); + decomposition.compute(); + std::shared_ptr> quotient = decomposition.getQuotient(); + + EXPECT_EQ(252ul, quotient->getNumberOfStates()); + EXPECT_EQ(624ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); + EXPECT_EQ(500ul, (quotient->as>()->getNumberOfChoices())); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); + + std::vector> formulas; + formulas.push_back(formula); + + storm::dd::BisimulationDecomposition decomposition2(*model, formulas, storm::storage::BisimulationType::Strong); + decomposition2.compute(); + quotient = decomposition2.getQuotient(); + + EXPECT_EQ(19ul, quotient->getNumberOfStates()); + EXPECT_EQ(58ul, quotient->getNumberOfTransitions()); + EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType()); + EXPECT_TRUE(quotient->isSymbolicModel()); + EXPECT_EQ(34ul, (quotient->as>()->getNumberOfChoices())); +}