EMETTEUR == message : string; cpt : integer := 0; alea : integer; * [ true -> cpt := cpt + 1; message := "message " + cpt; recepteur!message; sleep(1000); alea := random (1, 10); /* action aleatoire */ [ alea <= 2 -> recepteur?relance() [] alea > 2 -> skip ] ] RECEPTEUR == message : string; alive : boolean := true; *[ alive; emetteur?message -> dog!ack(); print (message + "\n") [] alive; dog?erreur() -> print("erreur\n"); emetteur!relance(); dog!ackErreur () ] DOG == delai : integer := 4; *[ recepteur?ack() -> delai := 4 [] horloge?bip() -> delai := delai -1 [] delai = 0 -> recepteur!erreur(); recepteur?ackErreur(); delai := 4 ] HORLOGE == *[true -> dog!bip();sleep(1000)] MAIN == [ emetteur :: EMETTEUR || recepteur :: RECEPTEUR || dog :: DOG || horloge :: HORLOGE ]