primitive_2_CTL.mso

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, attente]{
    etat=4;
    init=2;
    0=attente;
    1=crit;
    2=debut;
    3=fin;
    2->0[vaCrit];
    0->1[execCrit];
    1->3[fin];
};;

Systeme=<Qx Q1, Qx Q2, Processus P1, Processus P2>{
    <devientVrai,_,vaCrit,_>;
    <_,estCeFaux,execCrit,_>;
    <devientFaux,_,fin,_>;
    
    <_,devientVrai,_,vaCrit>;
    <estCeFaux,_,_,execCrit>;
    <_,devientFaux,_,fin>;
    
};;

// Surete 1 : Il existe au moins un chemin menant à la fin des deux processus
Systeme += surete <- AF(P1.fin && P2.fin);;

// Exclusion mutuelle : Il n'existe pas de chemin menant à deux exécutions critiques simultanées
Systeme += exclusionMutuelle <- !(EF(P1.crit && P2.crit));;

// Surete 2 : Il existe au moins un chemin menant à un deadlock
Systeme += deadlock <- EF(!EX(true) && (!P1.fin || !P2.fin));;

// Equité Forte : Quel que soit le chemin, un processus au moins a effectué sa section critique
Systeme += equiteForte <- AG((P1.attente -> AF(P1.crit)) &&(P2.attente -> AF(P2.crit)));;
// Equité Faible : Il existe un chemin pour lequel p1 ou p2 peut exécuter sa section critique
Systeme += equiteFaible <- AG((P1.attente -> EF(P1.crit)) && (P2.attente -> EF(P2.crit)));;

todot primitive2CTL.dot Systeme;;