primitive_1_CTL.mso

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

Processus=[crit, debut, fin, attente]{
    etat=4;
    init=0;
    0=debut;
    1=attente;
    2=crit;
    3=fin;
    0->1[vaAttendre];
    1->2[vaCrit];
    2->3[execCrit];
};;

Systeme = <Turn t, Processus P1, Processus P2>{
    
    <prend1,vaAttendre,_>;
    <estCe2,vaCrit,_>;
    <_,execCrit,_>;
    
    <prend2,_,vaAttendre>;
    <estCe1,_,vaCrit>;
    <_,_,execCrit>;
};;

todot primitive1.dot systeme;;


//Sureté 1 : Prouve qu'il n'est pas possible de finir avec les deux sections critiques (deadlock)
Systeme += surete <- AF(P1.fin && P2.fin);;

// Sureté 2 : Existe-t-il au moins un chemin menant à un deadlock
Systeme += deadlock <- EF(!EX(true) && (!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));;

// 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 primitive1CTL.dot Systeme;;

/*
Propriété de sûreté
Propriété d'exclusion mutuelle
Propriété d'équité : -Faible EF
                     -Forte  AF
*/