40 lines
1.7 KiB
Text
40 lines
1.7 KiB
Text
with SystemNbPannesFNomDuControleur do
|
|
deadlock := any_s - src(any_t - self_epsilon);
|
|
notResettable := any_s -coreach(initial,any_t);
|
|
/* output */
|
|
out0 := any_s & [V[2].rate=0];
|
|
out1 := any_s & [V[2].rate=1];
|
|
out2 := any_s & [V[2].rate=2];
|
|
dec21 := any_t & label V[2].dec & rsrc(out2);
|
|
dec10 := any_t & label V[2].dec & rsrc(out1);
|
|
/* Niveaux critiques et Situations redoutees */
|
|
NC := any_s & [T.level=0 | T.level=nbSensors];
|
|
SR := deadlock | NC;
|
|
EPerdu := any_s - SR;
|
|
CGagne := any_s - SR;
|
|
/* systeme d'equation au point fixe
|
|
* CGagnant = CGagne & src(CCoupGagnant)
|
|
* CCoupGagnant = CCoup & rtgt(EPerdant)
|
|
* EPerdant = EPerdu & (src(ECoupPerdant) - src(ECoupNonPerdant))
|
|
* ECoupPerdant = ECoup & rtgt(CGgagnant)
|
|
* ECoupNonPerdant = ECoup & rtgt(any_s - CGagnant)
|
|
*/
|
|
CCoup := any_t & label cmd;
|
|
ECoup := any_t & label env;
|
|
CCoupGagnant -= CCoup & rtgt(EPerdu & (src(ECoup & rtgt(CGagne & src(CCoupGagnant))) - src(ECoup & rtgt(any_s - (CGagne & src(CCoupGagnant))))));
|
|
/* Controller projection */
|
|
/* Syntax and semantic of the "project" command
|
|
* param 1 : les configurations projetees
|
|
* param 2 : les transitions projetees
|
|
* - arg1 : projection existentielle
|
|
* - arg2 : projection universelle
|
|
* param 3 : nom du noeud AltaRica genere
|
|
* param 4 : simplification ou non des expressions booleennes
|
|
* param 5 (optionel) : noeud de la hierarchie servant a la projection
|
|
*/
|
|
/* Universal projection is use */
|
|
project(any_s, (empty_t,CCoupGagnant), 'CtrlInitialNbPannesFNumIter', true,C)
|
|
> 'Controleurs/CtrlInitialNbPannesFNumIter.alt';
|
|
/* record results */
|
|
show(any_s, any_t, deadlock, NC, SR , out0, out1, out2, dec21, dec10, CCoupGagnant) > 'Res/$NODENAME.res';
|
|
done
|