Modules2MTBDD: add remark about state variable gap difference in -o2 and -o1 variable ordering

The current behaviour for the -o2 (MTBDD) variable order (no
pre-allocation of state variables before the model variables) is there
since the initial support for LTL in PRISM. We need some benchmarks
to see if it's a good idea to use preallocation as for the -o1 order.


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

prism/src/prism/Modules2MTBDD.java

@@ -463,7 +463,13 @@ public class Modules2MTBDD
 					ddChoiceVars[i] = modelVariables.allocateVariable("l" + i);
 				}
 			}
-			
+
+			// TODO: For the other variable order (-o1, used for sparse/hybrid by default,
+			// see above), we preallocate a certain number of state variables.
+			// For consistency, it would make sense to do the same here. However,
+			// we should first do some testing to see if this negatively impacts
+			// performance.
+
 			// go through all vars in order (incl. global variables)
 			// so overall ordering can be specified by ordering in the input file
 			// use 'last' to detect when starting a new module