simpleSolutionReverse.mso

Turn=[libre, uti1, uti2]{
	etat=3;
	init = 0;
	0=libre;
	1=uti1;
	2=uti2;
	0->1[prend1];
	0->2[prend2];
	1->1[prend1];
	2->2[prend2];
	1->1[estCe1];
	2->2[estCe2];
	1->2[prend2];
	2->1[prend1];
};;

Qx=[vrai, faux]{
    etat=2;
	init=0;
	0=faux;
	1=vrai;
	0->1[devientVrai];
	1->0[devientFaux];
	1->1[estCeVrai];
	0->0[estCeFaux];
};;

Processus=[crit, debut, fin, attenteCrit,transition]{
    etat=5;
    init=2;
    0=attenteCrit;
    1=crit;
    2=debut;
    3=transition;
    4=fin;
    2->3[vaTransition];
    3->0[vaCrit];
    0->1[execCrit];
    1->4[fin];
};;

systeme=<Processus P1, Processus P2, Qx Q1, Qx Q2, Turn T>{
    <vaTransition,_,_,_,prend1>;
    <vaCrit,_,devientVrai,_,_>;
    <execCrit,_,_,estCeFaux,_>;
    <execCrit,_,_,_,estCe2>;
    <fin,_,devientFaux,_,_>;
    
    <_,vaTransition,_,_,prend2>;
    <_,vaCrit,_,devientVrai,_>;
    <_,execCrit,estCeFaux,_,_>;
    <_,execCrit,_,_,estCe1>;
    <_,fin,_,devientFaux,_>;
};;

todot simpleSolutionReverse.dot systeme;;