yanntm
commented
6 years ago To make it clearer; the matrices mayEnable/Disable, coEnabled are only computed using these control sets (with an intersection with write). For DNA I still need full read/write sets test. Control sets also give a nice approximation of Noack heuristic in orders that generalizes to non Petri net.
Hi, just as an idea, you might think about using : read, write and control dependencies.
I've found that separating the notion of control variables, i.e. a subset of read variables is a good idea.
Control variables, as their name implies, are variables that are read and decide whether or not we have successors/are fireable... If you have guards, the notion is close, but guards are pre tests, and they do not fit all semantics (e.g. GAL), and are complex for a user to provide in a path to LTSmin (should they be disjunctively decomposed ?...).
So, for a given event the control set solely influences the control flow. It is a subset of read.
E.g. if you are incrementing a place in a P/T net, you get it as a read and write variable, but it is not a control variable.
This is great info for e.g. transaction/structural agglomeration. Jeroen noticed this trick is useful when he used it for 1-safe nets, to say they were just write variables (discussed iirc in Torun).
I'm using this distinction read vs control to get much smaller dependency matrices (i.e. more refined). It's a simple idea to extend the matrices of PINS, but it's really nice in terms of what it implies on dependency matrices of events in POR for instance (if they are not user provided).
I do not think it's hard for a user to provide the distinction in a PINS bridge in most cases. Worst case, it can be overapproximated by read set, so we can be reverse compatible with older PINS that don't provide it.
I believe it covers some of the needs that led to other matrices/features of PINS to be introduced, that could be simplified a bit.
yann