// One can model IOAs with LTSs by using completely specified IOA, 
// that is, in each state, transitions for the reception of all possible input interactions are specified 
// - some of those transitions may go to the error state, in the following called NR (for non-specified reception).
// Here is a simple example: Machine A (initial state A1) sends b and receives a and c interactions;
//                           Machine B (initial state B1) sends a and c interactions and receives b;

A1 = (a -> A2 | c -> A_NR),
A2 = (a -> A_NR | c -> A1 | b -> A2),
A_NR = (a -> A_NR | c -> A_NR).

B1 = (b -> B2 | a -> B1),
B2 = (b -> B_NR | c -> B1),
B_NR = (b -> B_NR).

||COMPOSITION = (A1 || B1).

// the same, but using ERROR (with predefined meaning in LTSA) instead of NR

A1x = (a -> A2x | c -> ERROR),
A2x = (a -> ERROR | c -> A1x | b -> A2x).

B1x = (b -> B2x | a -> B1x),
B2x = (b -> ERROR | c -> B1x).

||COMPOSITIONx = (A1x || B1x).