Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : new examples (with tesh) for verification of liveness properties...
[simgrid.git] / examples / msg / mc / promela_bugged1_liveness
1 never { /* !G(r->Fcs) */
2 T0_init :    /* init */
3         if
4         :: (1) -> goto T0_init
5         :: (!cs && r) -> goto accept_S2
6         fi;
7 accept_S2 :    /* 1 */
8         if
9         :: (!cs) -> goto accept_S2
10         fi;
11 }