Current algorithm is guaranteed to produce correct results only for the case when the given program
is dynamically causally ordered unitary.
We need an automatic check that establishes that a program belongs to that class.
Note that it can work only for some programs (e.g, sometimes the solver can say:
the program is proven to be dcou. Sometimes it can keep silence (In that case, the correctness of the answer is not guaranteed).
Current algorithm is guaranteed to produce correct results only for the case when the given program is dynamically causally ordered unitary.
We need an automatic check that establishes that a program belongs to that class. Note that it can work only for some programs (e.g, sometimes the solver can say: