/** Conception du modèle.
 *  le passage de parametres par valeur n'est pas facile à décrire en AltaRica.
 *    - les valeurs sont codées dans le nom des événements
 *    - la boucle est dépliée pour différencier les valeurs des variables
**/

node EmetteurABP
  state
    co : [0,5];        // abstraction du Compteur Ordinal
  event  
    receive_M, send_M_T, send_M_F, receive_A_T, receive_A_F;
  trans
    co=0                |- receive_M   -> co := 1;
    co=1                |- send_M_T    -> co := 2;
    co=2                |- receive_A_F -> co := 1;
    co=2                |- receive_A_T -> co := 3;
    co=3                |- receive_M   -> co := 4;
    co=4                |- send_M_F    -> co := 5;
    co=5                |- receive_A_F -> co := 0;
    co=5                |- receive_A_T -> co := 4;
  init
    co := 0;
edon
/** Conception du modèle.
 *  le passage de parametres par valeur n'est pas facile à décrire en AltaRica.
 *    - les valeurs sont codées dans le nom des événements
 *    - la boucle est dépliée pour différencier les valeurs des variables
**/

node RecepteurABP
  state
    co : [0,7];        // abstraction du Compteur Ordinal
  event  
    send_M, send_A_T, send_A_F, receive_M_T, receive_M_F;
  trans
    co=0                |- receive_M_F -> co := 1;
    co=0                |- receive_M_T -> co := 2;
    co=1                |- send_A_F    -> co := 0;
    co=2                |- send_A_T    -> co := 3;
    co=3                |- send_M      -> co := 4;
    co=4                |- receive_M_F -> co := 6;
    co=4                |- receive_M_T -> co := 5;
    co=5                |- send_A_T    -> co := 4;
    co=6                |- send_A_F    -> co := 7;
    co=7                |- send_M      -> co := 0;
  init
    co := 0;
edon
/** Le modèle de communication est supposé synchrone.
 *    - la réception du message est simultanée à son émission
**/

node ABPparfait
  sub
    E : EmetteurABP;
    R : RecepteurABP;
  sync
    <E.send_M_T, R.receive_M_T>;
    <E.send_M_F, R.receive_M_F>;
    <E.receive_A_T, R.send_A_T>;
    <E.receive_A_F, R.send_A_F>;
edon
/** Le modèle de communication est supposé synchrone.
 *    - la réception du message est simultanée à son émission
 *    - ou bien elle n'a pas lieu en cas de perte
**/

node ABPperteUnidirectionnelle
  sub
    E : EmetteurABP;
    R : RecepteurABP;
  sync
    <E.send_M_T, R.receive_M_T>;
    <E.send_M_F, R.receive_M_F>;
    <E.receive_A_T, R.send_A_T>;
    <E.receive_A_F, R.send_A_F>;
    // les pertes de messages
    <E.send_M_T>;
    <E.send_M_F>;
edon
/** Le modèle de communication est supposé synchrone.
 *    - la réception du message est simultanée à son émission
 *    - le message reçu est correct ou bien erroné
**/

node ABPerreurUnidirectionnelle
  sub
    E : EmetteurABP;
    R : RecepteurABP;
  sync
    <E.send_M_T, R.receive_M_T>;
    <E.send_M_F, R.receive_M_F>;
    <E.receive_A_T, R.send_A_T>;
    <E.receive_A_F, R.send_A_F>;
    // les erreurs de transmission T->F ou F->T est possible
    <E.send_M_T, R.receive_M_F>;
    <E.send_M_F, R.receive_M_T>;
edon