From 5f57cbb12a67016d1c9bdace1e4d0560fff475a4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 28 Jan 2013 19:58:41 +0100 Subject: [PATCH] Now able to build the BDD for the die example, including the reachability analysis! Booyah --- src/adapters/SymbolicModelAdapter.h | 28 ++++++++++++---------------- src/utility/CuddUtility.cpp | 4 ++-- src/utility/CuddUtility.h | 2 +- 3 files changed, 15 insertions(+), 19 deletions(-) diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index 7e8674dae..f42d8f873 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/src/adapters/SymbolicModelAdapter.h @@ -161,9 +161,13 @@ private: } void performReachability(storm::ir::Program const& program, ADD* systemAdd) { + ADD* systemAdd01 = new ADD(systemAdd->GreaterThan(*cuddUtility->getZero())); + cuddUtility->dumpDotToFile(systemAdd01, "system01.add"); + cuddUtility->dumpDotToFile(systemAdd, "reachtransold.add"); ADD* reachableStates = getInitialStateDecisionDiagram(program); - ADD* newReachableStates = reachableStates; + cuddUtility->dumpDotToFile(reachableStates, "init.add"); + ADD* newReachableStates = new ADD(*reachableStates); ADD* rowCube = cuddUtility->getOne(); for (auto variablePtr : allRowDecisionDiagramVariables) { @@ -174,31 +178,23 @@ private: int iter = 0; do { changed = false; - std::cout << "iter " << ++iter << std::endl; - - *newReachableStates = *reachableStates * *systemAdd; - newReachableStates->ExistAbstract(*rowCube); + *newReachableStates = *reachableStates * *systemAdd01; + newReachableStates = new ADD(newReachableStates->ExistAbstract(*rowCube)); cuddUtility->dumpDotToFile(newReachableStates, "reach1.add"); - cuddUtility->permuteVariables(newReachableStates, allColumnDecisionDiagramVariables, allRowDecisionDiagramVariables, allDecisionDiagramVariables.size()); + newReachableStates = cuddUtility->permuteVariables(newReachableStates, allColumnDecisionDiagramVariables, allRowDecisionDiagramVariables, allDecisionDiagramVariables.size()); - cuddUtility->dumpDotToFile(newReachableStates, "reach2.add"); - cuddUtility->dumpDotToFile(reachableStates, "reachplus.add"); *newReachableStates += *reachableStates; + newReachableStates = new ADD(newReachableStates->GreaterThan(*cuddUtility->getZero())); - cuddUtility->dumpDotToFile(newReachableStates, "reach3.add"); - cuddUtility->dumpDotToFile(reachableStates, "reach4.add"); - - if (*newReachableStates != *reachableStates) { - std::cout << "changed ..." << std::endl; - changed = true; - } + if (*newReachableStates != *reachableStates) changed = true; *reachableStates = *newReachableStates; } while (changed); *systemAdd *= *reachableStates; - cuddUtility->dumpDotToFile(systemAdd, "reachtrans.add"); + std::cout << "got " << systemAdd->nodeCount() << " nodes" << std::endl; + std::cout << "and " << systemAdd->CountMinterm(allRowDecisionDiagramVariables.size() + allColumnDecisionDiagramVariables.size()) << std::endl; } void createIdentityDecisionDiagrams(storm::ir::Program const& program) { diff --git a/src/utility/CuddUtility.cpp b/src/utility/CuddUtility.cpp index ec9726b18..ab3d85797 100644 --- a/src/utility/CuddUtility.cpp +++ b/src/utility/CuddUtility.cpp @@ -155,7 +155,7 @@ ADD* CuddUtility::getConstant(double value) const { return new ADD(manager.constant(value)); } -void CuddUtility::permuteVariables(ADD* add, std::vector fromVariables, std::vector toVariables, uint_fast64_t totalNumberOfVariables) const { +ADD* CuddUtility::permuteVariables(ADD* add, std::vector fromVariables, std::vector toVariables, uint_fast64_t totalNumberOfVariables) const { std::vector permutation; permutation.resize(totalNumberOfVariables); for (uint_fast64_t i = 0; i < totalNumberOfVariables; ++i) { @@ -164,7 +164,7 @@ void CuddUtility::permuteVariables(ADD* add, std::vector fromVariables, st for (uint_fast64_t i = 0; i < fromVariables.size(); ++i) { permutation[fromVariables[i]->NodeReadIndex()] = toVariables[i]->NodeReadIndex(); } - add->Permute(&permutation[0]); + return new ADD(add->Permute(&permutation[0])); } void CuddUtility::dumpDotToFile(ADD* add, std::string filename) const { diff --git a/src/utility/CuddUtility.h b/src/utility/CuddUtility.h index 7eb679c82..8102eb012 100644 --- a/src/utility/CuddUtility.h +++ b/src/utility/CuddUtility.h @@ -35,7 +35,7 @@ public: ADD* getConstant(double value) const; - void permuteVariables(ADD* add, std::vector fromVariables, std::vector toVariables, uint_fast64_t totalNumberOfVariables) const; + ADD* permuteVariables(ADD* add, std::vector fromVariables, std::vector toVariables, uint_fast64_t totalNumberOfVariables) const; void dumpDotToFile(ADD* add, std::string filename) const;