Skip to content

Add `ex(C)` computations for remaining primitives

Maxwell Pirtle requested to merge maxwellpirtle/simgrid:udpor-phase8 into master

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.

Merge request reports