Confluence check: improve performance by interleaving the zero variables
Currently, the extra zero variables are added at the end, so the nodes for these variables are on the top. It is likely more efficient to interleave them with the existing current/old and new variables.
Now that we've changed the CIF controller properties checker to do a separate conversion to BDD/MDD per check, we could likely do this now. It would require functionality in CIF to BDD to request adding a number of extra variables to be added during the conversion. We need only one such set of extra variables for the confluence check.
Addresses #892
Designs
Activity
-
Newest first Oldest first
-
Show all activity Show comments only Show history only
- Dennis Hendriks added CIF TypeEnhancement labels
added CIF TypeEnhancement labels
- Dennis Hendriks mentioned in issue #892
mentioned in issue #892
- Dennis Hendriks marked this issue as related to #892
marked this issue as related to #892
- Author Maintainer
Probably we should try:
- Variables at the end (like we have now).
- Variables at the start.
- Variables interleaved.
And see what works best. I expect that last one to work best.
Collapse replies - Developer
Makes sense.
- Please register or sign in to reply
- Dennis Hendriks assigned to @ddennis
assigned to @ddennis
- Dennis Hendriks changed milestone to %v6.0
changed milestone to %v6.0
- Dennis Hendriks mentioned in issue #1010 (closed)
mentioned in issue #1010 (closed)
- Author Maintainer
I did two experiments for creating 'x0 = x and y0 = y and z0 = z and ...' relations:
- Using interleaved old/new variables, with the zero variables added at the end (as we have now in the implementation).
- Using interleaved old/new/zero variables.
The results are:
Click to expand and show results
Picked up _JAVA_OPTIONS: -Djava.net.preferIPv4Stack=true interleaved: i=0/9 -- nodeCount=3 -- pathCount=2 interleaved: i=1/9 -- nodeCount=6 -- pathCount=4 interleaved: i=2/9 -- nodeCount=9 -- pathCount=8 interleaved: i=3/9 -- nodeCount=12 -- pathCount=16 interleaved: i=4/9 -- nodeCount=15 -- pathCount=32 interleaved: i=5/9 -- nodeCount=18 -- pathCount=64 interleaved: i=6/9 -- nodeCount=21 -- pathCount=128 interleaved: i=7/9 -- nodeCount=24 -- pathCount=256 interleaved: i=8/9 -- nodeCount=27 -- pathCount=512 interleaved: i=9/9 -- nodeCount=30 -- pathCount=1024 not interleaved: i=0/9 -- nodeCount=3 -- pathCount=2 not interleaved: i=1/9 -- nodeCount=9 -- pathCount=4 not interleaved: i=2/9 -- nodeCount=21 -- pathCount=8 not interleaved: i=3/9 -- nodeCount=45 -- pathCount=16 not interleaved: i=4/9 -- nodeCount=93 -- pathCount=32 not interleaved: i=5/9 -- nodeCount=189 -- pathCount=64 not interleaved: i=6/9 -- nodeCount=381 -- pathCount=128 not interleaved: i=7/9 -- nodeCount=765 -- pathCount=256 not interleaved: i=8/9 -- nodeCount=1533 -- pathCount=512 not interleaved: i=9/9 -- nodeCount=3069 -- pathCount=1024
Thus, with the current non-interleaved approach, the node count blows up exponentially. With the interleaved approach, it grows linearly.
Code I used: Main.java
Collapse replies - Author Maintainer
The reason that interleaving works is that you get a small subtree per CIF/BDD variable, but all true paths of that connect to the same node at the leaves (true node). When all the relations are combined with
and
, the leaf of one tree is essentially merged with the root of the next tree. They are sort of put in sequence. That doesn't blow up.If we don't interleave, we split at the old variable, and then split for the next old variable, etc, etc, and we get an exponentially growing tree over all possible valuations of old variables. Only much further down the tree come the zero variables, but then the damage is already done. Furthermore, we build per CIF/BDD variable a relation and then merge them. We thus get per relation something near a top level and something near a bottom level. We combine those for different CIF/BDD variables. This means also a lot of nodes need to be recreated, as we're not building from bottom to top.
- Author Maintainer
I've implemented it. Code is not final yet, but the first test results are very promising. The confluence check can be completed in:
- Waterway lock < 2s
- Locomobiel MCC < 15s
- Lock Linne < 3m31s
- Dennis Hendriks created branch
1006-confluence-check-interleave-zero-variables
to address this issuecreated branch
1006-confluence-check-interleave-zero-variables
to address this issue - Dennis Hendriks mentioned in commit beff0e90
mentioned in commit beff0e90
- Dennis Hendriks mentioned in commit ce446cec
mentioned in commit ce446cec
- Dennis Hendriks mentioned in commit 326163a1
mentioned in commit 326163a1
- Dennis Hendriks mentioned in commit 7c0135a6
mentioned in commit 7c0135a6
- Dennis Hendriks mentioned in commit 82f26e4a
mentioned in commit 82f26e4a
- Dennis Hendriks mentioned in commit 9581356a
mentioned in commit 9581356a
- Dennis Hendriks mentioned in commit c17b463f
mentioned in commit c17b463f
- Dennis Hendriks mentioned in commit 6995ddd9
mentioned in commit 6995ddd9
- Dennis Hendriks mentioned in commit d8ff1383
mentioned in commit d8ff1383
- Dennis Hendriks mentioned in commit aad66c71
mentioned in commit aad66c71
- Dennis Hendriks mentioned in commit 55746464
mentioned in commit 55746464
- Dennis Hendriks mentioned in commit 0876081c
mentioned in commit 0876081c
- Dennis Hendriks mentioned in commit b0eee049
mentioned in commit b0eee049
- Dennis Hendriks mentioned in commit 20377277
mentioned in commit 20377277
- Dennis Hendriks mentioned in merge request !1105 (merged)
mentioned in merge request !1105 (merged)
- Dennis Hendriks mentioned in merge request !1106 (closed)
mentioned in merge request !1106 (closed)
- Dennis Hendriks mentioned in commit 033082d4
mentioned in commit 033082d4
- Dennis Hendriks mentioned in commit 4271a607
mentioned in commit 4271a607
- Dennis Hendriks closed with merge request !1105 (merged)
closed with merge request !1105 (merged)
- Dennis Hendriks mentioned in issue #695 (closed)
mentioned in issue #695 (closed)
- Dennis Hendriks mentioned in issue #1004 (closed)
mentioned in issue #1004 (closed)