/** abcd-Example - with message passing
 *  
 *  Gregor v. Bochmann, January 2015 */

// Message transmission media, MAB from A to B and MBA from B to A
// s means sending, r means receiving
// Note that these models mean that:
//      at most one message is in transit in each direction at any given time.
MAB = (sa -> ra -> MAB | sb -> rb -> MAB).
MBA = (sc -> rc -> MBA | sd -> rd -> MBA).

// state machine A 
// This machine includes explicit transitions for the reception of unexpected messages. 
//      These transitions lead to the state NSR (Non-Specified Reception)
// The state NSR has no outgoing transitions, therefore it is considered by LTSA as an error state 
//      (represented by number -1 in the drawn state diagram) 
A1 = (sa -> A2 | rc -> NSR | rd -> NSR),
A2 = (sb -> A3 | rc -> NSR | rd -> NSR),
A3 = (rc -> A4 | rd -> NSR),
A4 = (rd -> END | rc -> NSR).

// state machine B - organized similarly
B1 = (sc -> B2 | ra -> NSR2 | rb -> NSR2),
B2 = (ra -> B3 | rb -> NSR2),
B3 = (rb -> B4 | ra -> NSR2),
B4 = (sd -> END | ra -> NSR2 | rb -> NSR2).

// the composed system
||SYSTEM = (A1 || MAB || MBA || B1).