Issue with `RunCommutativity`

[lduranovic]

Hey @kushti. I know it's been a while since you worked on this, but I really appreciated reading through your code. That being said, I think there might be an issue with how you defined the axiom RunCommutativity. In the original paper, this is a statement about disjoint schedules applied to the same configuration, and I don't think that is the case in your formulation. In particular, one of the preconditions on your s1 and s2 should be that they involve strictly different processes. Written your way, I think the axiom is way too powerful and simply incorrect.