Add `ex(C)` computations for remaining primitives
Overview
This PR will introduce what should be the completed ex(C)
computation for the rest of the primitives described in The Anh Pham's thesis, as well as the ActorJoin
transition (which is considered independent with everything else).
Note on Failing Tests
For the moment, the PR modifies the dependency relation between CommWait
and CommTest
events, marking them as independent with respect to other communication events if the communication is different. This is not fully complete yet; further, changing the dependency relation would require us to change any teshsuite tests testing the model checker against communication transitions. Before doing so, let's make sure we get this correct.