Now able to build the BDD for the die example, including the reachability analysis! Booyah

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) {

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<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const {
+ADD* CuddUtility::permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const {
 	std::vector<int> permutation;
 	permutation.resize(totalNumberOfVariables);
 	for (uint_fast64_t i = 0; i < totalNumberOfVariables; ++i) {
@@ -164,7 +164,7 @@ void CuddUtility::permuteVariables(ADD* add, std::vector<ADD*> 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 {

src/utility/CuddUtility.h

@@ -35,7 +35,7 @@ public:
 
 	ADD* getConstant(double value) const;
 
-	void permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const;
+	ADD* permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const;
 
 	void dumpDotToFile(ADD* add, std::string filename) const;