-------------------------------------------------------------------------------

"fifo.bcg" = generation of "fifo.lotos";

"interface.bcg" = generation of "interface.lotos";

-------------------------------------------------------------------------------

"rel_rel_A.bcg" = branching reduction of
                     total hide "CRASH .*", "GET !2 .*" in 
                        generation of "rel_rel_A.lotos";

"rel_rel_B.bcg" = branching reduction of
                     total hide "CRASH .*", "GET !2 .*" in 
                        generation of "rel_rel_B.lotos";

-------------------------------------------------------------------------------

% DEFAULT_PROCESS_FILE="rel_rel_B.lotos"

"rel_rel_B_compo.bcg" = branching reduction of
                           total hide "GET !2 .*", "CRASH .*" in
                              leaf strong reduction of 
    hide R_T1, R_T2, R1, R2, DEPOSE1, DEPOSE2 in
        (
            Crash_Transmitter [R_T1, R_T2]
            |[R_T1, R_T2]|
            (
                (
                    Receiver_Thread [R_T1, R1, R2, DEPOSE1, GET, CRASH] (1)
                    |[R_T1, R1, R2, GET, CRASH, DEPOSE1]|
                    Fail_Receiver [R_T1, R1, R2, GET, DEPOSE1, CRASH] (1)
                )
                |[R1, R2]|
                (
                    Receiver_Thread [R_T2, R2, R1, DEPOSE2, GET, CRASH] (2)
                    |[R_T2, R1, R2, GET, CRASH, DEPOSE2]|
                    Fail_Receiver [R_T2, R2, R1, GET, DEPOSE2, CRASH] (2)
                )
            )
        );

-------------------------------------------------------------------------------

% DEFAULT_PROCESS_FILE="rel_rel_C.lotos"

"crash_trans.bcg" = generation of CRASH_TRANSMITTER;

"rel_rel_C.bcg" = generation of
                     leaf strong reduction of
      hide R_T1, R_T2, R_T3, R12, R13, R21, R23, R31, R32  in
         (
            (
               (
                  (Receiver_Node [R_T1, R21, R31, R12, R13, GET, CRASH] (1)
                   -||? "interface.lotos":INTERFACE [R_T1, R21, R31])
               |[R12, R21, R13, R31]|
                  (
                     (Receiver_Node [R_T2, R12, R32, R21, R23, GET, CRASH] (2)
                      -||? "interface.lotos":INTERFACE [R_T2, R12, R32])
                  |[R23, R32]|
                     (Receiver_Node [R_T3, R13, R23, R31, R32, GET, CRASH] (3)
                      -||? "interface.lotos":INTERFACE [R_T3, R13, R23])
                  ) -|[R_T2, R_T3]| "crash_trans.bcg"
               ) -|[R_T1, R_T2, R_T3]| "crash_trans.bcg"
            )
            |[R_T1, R_T2, R_T3]|
            "crash_trans.bcg"
         );

-------------------------------------------------------------------------------