Symbolic engines: Clear ODD when clearing the model (fix memory leak)

Previously, the ODD data structure (for mapping between reachable states and their index)
on the C side was not deallocated when the model was cleared.

Closes https://sourceforge.net/p/prism-mc/bugs/9/



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11468 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/NondetModel.java

@@ -213,7 +213,10 @@ public class NondetModel extends ProbModel
 		// work out number of reachable states
 		numStates = JDD.GetNumMinterms(reach, allDDRowVars.n());
 
-		// build odd
+		// build odd, clear old one
+		if (odd != null) {
+			ODDUtils.ClearODD(odd);
+		}
 		odd = ODDUtils.BuildODD(reach, allDDRowVars);
 	}
 

prism/src/prism/ProbModel.java

@@ -505,7 +505,10 @@ public class ProbModel implements Model
 		// work out number of reachable states
 		numStates = Math.pow(2, allDDRowVars.n());
 
-		// build odd
+		// build odd, clear old one
+		if (odd != null) {
+			ODDUtils.ClearODD(odd);
+		}
 		odd = ODDUtils.BuildODD(reach, allDDRowVars);
 	}
 
@@ -522,7 +525,10 @@ public class ProbModel implements Model
 		// work out number of reachable states
 		numStates = JDD.GetNumMinterms(reach, allDDRowVars.n());
 
-		// build odd
+		// build odd, clear old one
+		if (odd != null) {
+			ODDUtils.ClearODD(odd);
+		}
 		odd = ODDUtils.BuildODD(reach, allDDRowVars);
 	}
 
@@ -928,5 +934,11 @@ public class ProbModel implements Model
 				JDD.Deref(transPerAction[i]);
 			}
 		}
+
+		if (odd != null) {
+			// clear ODD
+			ODDUtils.ClearODD(odd);
+			odd = null;
+		}
 	}
 }