EXPLICATION:

 (Key c, [events]) correspond aux événements causés par l'appuie sur la touche c du téléphone
 (Int p, [events]) correspond aux événements internes générés par le processus p
 
les transitions des automates sont déclenchées par les événements et ont la possiblité de:
 - créer des processus (c'est à dire lancer une nouvelle copie d'un automate)
 - générer des événements internes


TRACE D'EXÉCUTION 1 montrant:
 - la création de processus, 
 - la gestion de la bascule PLAY/PAUSE des lecteurs mp3 
 - la mise en PAUSE automatique lorsque le son est coupé, à l'aide d'événements internes envoyés par le Volume Manager.


val scenario1 : char list = ['o'; '.'; 'm'; 'm'; 'p'; 'p'; 'p'; '+'; '-'; '-'; '-'; '+'; 'p'; 's'; 'f';  '.']

# load scenario1;;

- : system =
{input =
  [(Key 'o', [Phone_event On]); (Int "", []); (Key 'm', [OS_event Music]);
   (Key 'm', [OS_event Music]); (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes = [{aut = "phone"; id = 1; current_state = Phone_state OFF}]}


# step();;        


- : system =
{input =
  [(Int "", []); (Key 'm', [OS_event Music]); (Key 'm', [OS_event Music]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "os"; id = 2; current_state = OS_state BOOTING};
   {aut = "phone"; id = 1; current_state = Phone_state ON}]}


# step();;        


- : system =
{input =
  [(Key 'm', [OS_event Music]); (Key 'm', [OS_event Music]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key 'm', [OS_event Music]); (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PLAY};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key '+', [Vol_event Inc]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PLAY};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key '+', [Vol_event Inc]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '+', [Vol_event Inc]); (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 's', [Mp3_event Stop]); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}


# step();;        


- : system =
{input =
  [(Key '-', [Vol_event Dec]); (Key '-', [Vol_event Dec]);
   (Key '+', [Vol_event Inc]); (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 's', [Mp3_event Stop]); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Int "volume manager", [Mp3_event Pause]); (Key '-', [Vol_event Dec]);
   (Key '+', [Vol_event Inc]); (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 's', [Mp3_event Stop]); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state MUTE}]}


# step();;        


- : system =
{input =
  [(Key '-', [Vol_event Dec]); (Key '+', [Vol_event Inc]);
   (Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state MUTE}]}


# step();;        


- : system =
{input =
  [(Key '+', [Vol_event Inc]); (Key 'p', [Mp3_event Play; Mp3_event Pause]);
   (Key 's', [Mp3_event Stop]); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state MUTE}]}


# step();;        


- : system =
{input =
  [(Key 'p', [Mp3_event Play; Mp3_event Pause]); (Key 's', [Mp3_event Stop]);
   (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PAUSE};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input =
  [(Key 's', [Mp3_event Stop]); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Mp3_state PLAY};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input = [(Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 5; current_state = Killed_state};
   {aut = "mp3 player"; id = 4; current_state = Killed_state};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}


# step();;        


- : system =
{input = [(Int "", [])];
 processes =
  [{aut = "os"; id = 2; current_state = Killed_state};
   {aut = "phone"; id = 1; current_state = Phone_state SHUTDOWN};
   {aut = "volume manager"; id = 3; current_state = Killed_state}]}


# step();;        


- : system =
{input = [];
 processes = [{aut = "phone"; id = 1; current_state = Phone_state OFF}]}
# 


TRACE D'EXÉCUTION 2 montrant la gestion des appels multiples:

val scenario2 : char list = ['o'; '.'; 'm'; '+'; '#'; '#'; 'd'; '#'; 'r'; '#'; 'd'; 'r'; 'r'; '.'; 'f'; '.']

# load scenario2 ;;

- : system =
{input =
  [(Key 'o', [Phone_event On]); (Int "", []); (Key 'm', [OS_event Music]);
   (Key '+', [Vol_event Inc]); (Ext '#', [OS_event Appel]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes = [{aut = "phone"; id = 1; current_state = Phone_state OFF}]}

# step();;

- : system =
{input =
  [(Int "", []); (Key 'm', [OS_event Music]); (Key '+', [Vol_event Inc]);
   (Ext '#', [OS_event Appel]); (Ext '#', [OS_event Appel]);
   (Key 'd', [Com_event Decrocher]); (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "os"; id = 2; current_state = OS_state BOOTING};
   {aut = "phone"; id = 1; current_state = Phone_state ON}]}

# step();;


- : system =
{input =
  [(Key 'm', [OS_event Music]); (Key '+', [Vol_event Inc]);
   (Ext '#', [OS_event Appel]); (Ext '#', [OS_event Appel]);
   (Key 'd', [Com_event Decrocher]); (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}

# step();;


- : system =
{input =
  [(Key '+', [Vol_event Inc]); (Ext '#', [OS_event Appel]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state NORMAL}]}

# step();;


- : system =
{input =
  [(Ext '#', [OS_event Appel]); (Ext '#', [OS_event Appel]);
   (Key 'd', [Com_event Decrocher]); (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 5; current_state = Com_state RINGING};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Key 'd', [Com_event Decrocher]); (Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 6; current_state = Com_state RINGING};
   {aut = "communication"; id = 5; current_state = Com_state RINGING};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PLAY};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Ext '#', [OS_event Appel]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 6; current_state = Com_state COMMUNICATION};
   {aut = "communication"; id = 5; current_state = Com_state COMMUNICATION};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 7; current_state = Com_state RINGING};
   {aut = "communication"; id = 6; current_state = Com_state MULTIPLE_CALL};
   {aut = "communication"; id = 5; current_state = Com_state MULTIPLE_CALL};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Ext '#', [OS_event Appel]); (Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 7; current_state = Killed_state};
   {aut = "communication"; id = 6; current_state = Com_state COMMUNICATION};
   {aut = "communication"; id = 5; current_state = Com_state COMMUNICATION};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Key 'd', [Com_event Decrocher]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 8; current_state = Com_state RINGING};
   {aut = "communication"; id = 6; current_state = Com_state MULTIPLE_CALL};
   {aut = "communication"; id = 5; current_state = Com_state MULTIPLE_CALL};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 8; current_state = Com_state COMMUNICATION};
   {aut = "communication"; id = 6; current_state = Com_state SUSPENDED};
   {aut = "communication"; id = 5; current_state = Com_state SUSPENDED};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input =
  [(Key 'r', [Com_event Raccrocher; Com_event Reject; Com_event Reprise]);
   (Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 8; current_state = Killed_state};
   {aut = "communication"; id = 6; current_state = Com_state COMMUNICATION};
   {aut = "communication"; id = 5; current_state = Com_state COMMUNICATION};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input = [(Int "", []); (Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "communication"; id = 6; current_state = Killed_state};
   {aut = "communication"; id = 5; current_state = Killed_state};
   {aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}

# step();;


- : system =
{input = [(Key 'f', [Phone_event Off]); (Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 4; current_state = Mp3_state PAUSE};
   {aut = "os"; id = 2; current_state = OS_state RUNNING};
   {aut = "phone"; id = 1; current_state = Phone_state ON};
   {aut = "volume manager"; id = 3; current_state = Vol_state HIGH}]}


# step();;


- : system =
{input = [(Int "", [])];
 processes =
  [{aut = "mp3 player"; id = 4; current_state = Killed_state};
   {aut = "os"; id = 2; current_state = Killed_state};
   {aut = "phone"; id = 1; current_state = Phone_state SHUTDOWN};
   {aut = "volume manager"; id = 3; current_state = Killed_state}]}


# step();;


- : system =
{input = [];
 processes = [{aut = "phone"; id = 1; current_state = Phone_state OFF}]}