nProcessSolution_LTL.mso

Turn=[un, deux, trois]{
	etat=3;
	init = 0;
	0=un;
	1=deux;
	2=trois;
	0->2[vers3];
	1->2[vers3];
	2->2[vers3];
	0->1[vers2];
	1->1[vers2];
	2->1[vers2];
	2->0[vers1];
	1->0[vers1];
	0->0[vers1];
	0->0[estCe1];
	1->1[estCe2];
	2->2[estCe3];
};;

Qx=[zero, un, deux]{
    etat=3;
	init=0;
	0=zero;
	1=un;
	2=deux;
	0->1[zeroVers1];
    1->2[unVers2];
	2->0[reinit];
	1->1[estCe1];
	2->2[estCe2];
	0->0[estCe0Ou1];
	0->0[estCe0];
	1->1[estCe0Ou1];
};;

Processus=[crit, debut, fin, etape1, attente]{
    etat=5;
    init=0;
    0=debut;
    1=etape1;
    2=attente;
    3=crit;
    4=fin;
    0->1[veutCrit];
    1->2[versEtape2];
    2->1[retourDeBoucle];
    2->3[execCrit];
    3->4[fin];
};;

Systeme=<Qx Q1, Qx Q2, Qx Q3, Turn T1, Turn T2, Processus P1, Processus P2, Processus P3>{

    // N1
    
    <zeroVers1,_,_,_,_,veutCrit,_,_>;                   // Q[1] = j
    
    <estCe1,_,_,vers1,_,versEtape2,_,_>;                // TURN[j] := 1
    <estCe2,_,_,_,vers1,versEtape2,_,_>;
    
    <estCe2,estCe0Ou1,estCe0Ou1,_,_,execCrit,_,_>;      // Sortie de la boucle
    <estCe2,_,_,_,estCe2,execCrit,_,_>;
    <estCe2,_,_,_,estCe3,execCrit,_,_>;
    <unVers2,estCe0,estCe0,_,_,retourDeBoucle,_,_>;     // Nouveau tour de boucle + Q[1] = j
    <unVers2,_,_,estCe2,_,retourDeBoucle,_,_>;
    <unVers2,_,_,estCe3,_,retourDeBoucle,_,_>;
    
    <reinit,_,_,_,_,fin,_,_>;                           // Fin de la section critique
    
    // N2
    
    <_,zeroVers1,_,_,_,_,veutCrit,_>;
    
    <_,estCe1,_,vers2,_,_,versEtape2,_>;
    <_,estCe2,_,_,vers2,_,versEtape2,_>;
    
    <estCe0Ou1,estCe2,estCe0Ou1,_,_,_,execCrit,_>;
    <_,estCe2,_,_,estCe1,_,execCrit,_>;
    <_,estCe2,_,_,estCe3,_,execCrit,_>;
    <estCe0,unVers2,estCe0,_,_,_,retourDeBoucle,_>;
    <_,unVers2,_,estCe1,_,_,retourDeBoucle,_>;
    <_,unVers2,_,estCe3,_,_,retourDeBoucle,_>;
    
    <_,reinit,_,_,_,_,fin,_>;
    
    
    //N3
    
    <_,_,zeroVers1,_,_,_,_,veutCrit>;
    
    <_,_,estCe1,vers3,_,_,_,versEtape2>;
    <_,_,estCe2,_,vers3,_,_,versEtape2>;
    
    <estCe0Ou1,estCe0Ou1,estCe2,_,_,_,_,execCrit>;
    <_,_,estCe2,_,estCe1,_,_,execCrit>;
    <_,_,estCe2,_,estCe2,_,_,execCrit>;
    <estCe0,estCe0,unVers2,_,_,_,_,retourDeBoucle>;
    <_,_,unVers2,estCe1,_,_,_,retourDeBoucle>;
    <_,_,unVers2,estCe2,_,_,_,retourDeBoucle>;
    
    <_,_,reinit,_,_,_,_,fin>;
    
  
};;
// Surete 1 : Il existe au moins un chemin menant à la fin des deux processus
//Systeme += surete <- EF(P1.fin && P2.fin && P3.fin);;

autosurete = {
	etat = 1;
	acc = 0;
	init = 0;
	0 - (!P1 || !P2 || !P3) -> 0;
};;

//sysauto = automaton Systeme;;
//resultatsurete = sysauto && autosurete[P1 <- P1.fin,P2 <- P2.fin,P3 <- P3.fin];;
//resultat = reduce resultatsurete;;

//todot resultatnproc.dot resultat;;


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

automutex = {
	etat = 2;
	acc = 1;
	init = 0;
	0 - (!P2 && !P3) || (!P1 && !P2) || (!P1 && !P3) -> 0;
	0 - (P2 && P3) || (P1 && P2) || (P1 && P3) -> 1;
	1 - true -> 1 [0];
};;

//resultatmutex = sysauto && automutex[P1 <- P1.crit,P2<-P2.crit,P3<-P3.crit];;
//resultat = reduce resultatmutex;;

//todot resultat.dot automutex;;
//todot resultat.dot resultat;;


// 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)) && (P3.attente -> AF(P3.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)) && (P3.attente -> AF(P3.crit)));;

autoequite = {
	etat = 4;
	acc = 1;
	init = 0;
	0 - true -> 0;
	0 - P1 && !P11 -> 1;
	0 - P2 && !P21 -> 2;
	0 - P3 && !P31 -> 3;
	1 - !P11 -> 1 [0];
	2 - !P21 -> 2 [0];
	3 - !P31 -> 3 [0];
};;

//todot resultat.dot autoequite;;

resultatequite = sysauto && autoequite[P1 <- P1.attente,P11 <- P1.crit,P2 <- P2.attente,P21 <- P2.crit,P3 <- P3.attente, P31 <- P3.crit];;
resultat = reduce resultatequite;;

todot resultat.dot resultat;;

/*
todot nProcessSolutionCTL.dot Systeme;;
*/