Deterministic matching

[rensink]

Current rule matching is non-deterministic, i.e., there is not guaranteed on the order for the matches of rules in a host graph. Normally this is not a problem but the results of an abstract state space exploration depend on the order in which matches are processed. Maybe we can add an option to the match collector to ensure a deterministic behaviour when needed.

Reported by: zambon

[rensink]

There's a choice here: - Either use order-preserving structures everywehere (risky, broken easily) - Or reorder matches (which takes time)

Original comment by: rensink

[rensink]

Concerning the two choices given: I was facing the same problem when implementing the abstraction code. My solution was to create a sort of C-like "macro" classes :P for hash sets and maps. I used this classes everywhere in the code instead of the normal Java collection names and it was then very easy to switch between order-preserving structures or normal ones. (Just a change in the header of the "macro" classes. The reorder option seems a bit more invasive to the code. It would certainly require a static flag and extra structures to keep the ordering. In any case the intended use of this request is to make debugging easier so I guess we should go for the option that is simpler to implement, regardless of performance, since we'll shift back to normal mode once debugging is done.

Original comment by: zambon

[rensink]

Update on my last comment: it seems that this is useful not only for debugging. I'm getting a very annoying behaviour with the firewall grammar: you get different state spaces whether you have a type graph enabled or not. As far as I could trace the cause down it seems that the problem is caused by different ordering of rule matches...

Original comment by: zambon

[rensink]

• Group: --> None

Original comment by: rensink