/** Two SDL processes (with implied receptions) - Example of Figure 12.1 in book by Braek
 *  
 *  Gregor v. Bochmann, January 2009 */

// "implied reception" means that the State Machine remains in its current state
//      when it receives a signal for which no transition is specified (the case of non-specified reception)
//      This is how the behavior of an SDL process is defined.

// les deux processus SDL ("rar" stands for Ra received; "sbs" stands for Gb sent; etc )
// note that the last three inputs in state A1 (leading back to A1) are the cases of non-specified reception
A1 = (rar -> sbs -> A3 | sar -> gas -> A8 | {gbr, ear, qar} -> A1),
A3 = (gbr -> aas -> A5 | {rar, sar, ear, qar} -> A3), 
A5 = (ear -> qbs -> A1 | {gbr, rar, sar, qar} -> A5),  
A8 = (qar -> A1 | {gbr, rar, sar, ear} -> A8).

B1 = (rbr -> sas -> B3 |  sbr -> gbs -> B8 | {gar, ebr, qbr} -> B1),
B3 = (gar -> abs -> B5 | {rbr, sbr, ebr, qbr} -> B3), 
B5 = (ebr -> qas -> B1 | {gar, rbr, sbr, qbr} -> B5),  
B8 = (qbr -> B1 | {gar, rbr, sbr, ebr} -> B8).

// medium de communication de A vers B - at most one message may be in transit in one direction (after sending, it must be received
MAB = (gas -> gar -> MAB | sbs -> sbr -> MAB | qbs -> qbr -> MAB). 

// medium de communication de A vers B
MBA = (gbs -> gbr -> MBA | sas -> sar -> MBA | qas -> qar -> MBA). 

// The SDL SYSTEM, that is, the composition of the above four components; this means arbitrary interactions with the ENVIRONMENT
||SYS = (A1 || B1 || MAB || MBA).

// let us put two users as the ENVIRONMENT; USERA inputs an Ra, then waits for an As and then inputs an Ea; similar for USERB
USERA = (rar -> aas -> ear -> END).  
USERB = (rbr -> abs -> ebr -> END).  

// this is the system with the two users
||ALL = (SYS || USERA || USERB).