nProcessSolution.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, etape2]{
    etat=5;
    init=0;
    0=debut;
    1=etape1;
    2=etape2;
    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 N1, Processus N2, Processus N3>{

    // 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>;
    
  
};;

todot nProcessSolution.dot Systeme;;