From 983fcba898243c69b433047cd7ca5745a304e03b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 23 Dec 2016 12:59:17 +0000 Subject: [PATCH] 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 | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index e0f3067a..dafa9b91 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/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