MODULE dn_main

IVAR input: {UNDEF , MP3_ABS_mNackAuthor , MP3_ABS_mNackTitle , MP3_ABS_mAckTitle , MP3_ABS_mAckAuthor , MP3_ABS_mRequest , Buy_ABS_bRequest , CD-Mania_ABS_not_avail , CD-Mania_ABS_offer};
IVAR output: {UNDEF , MP3_ABS_InvokeByTitle , MP3_ABS_mNot_avail , MP3_ABS_InvokeByAuthor , Buy_ABS_bInvoke20 , Buy_ABS_bInvoke10_10 , CD-Mania_ABS_request , CD-Mania_ABS_ack , CD-Mania_ABS_nack};


VAR MP3_ABS_state : 1 .. 9;
INIT MP3_ABS_state = 1

VAR Buy_ABS_state : 1 .. 4;
INIT Buy_ABS_state = 1

VAR CD-Mania_ABS_state : 1 .. 6;
INIT CD-Mania_ABS_state = 1



TRANS ((MP3_ABS_state = 1) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 1) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 1)
TRANS ((MP3_ABS_state = 1) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 1) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 1) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 1) & (input = MP3_ABS_mAckTitle)) -> FALSE
TRANS ((MP3_ABS_state = 1) & (input = MP3_ABS_mNackAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 2) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 2) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 2)
TRANS ((MP3_ABS_state = 3) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 3) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 3)
TRANS ((MP3_ABS_state = 3) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 3) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 3) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 3) & ((input = MP3_ABS_mNackAuthor | (input = MP3_ABS_mAckTitle | input = MP3_ABS_mRequest)))) -> FALSE
TRANS ((MP3_ABS_state = 2) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> next(MP3_ABS_state = 3)
TRANS ((MP3_ABS_state = 5) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 5) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 5)
TRANS ((MP3_ABS_state = 5) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 5) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 5) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 5) & ((input = MP3_ABS_mNackAuthor | (input = MP3_ABS_mAckTitle | input = MP3_ABS_mRequest)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mNackTitle & output = UNDEF))) -> next(MP3_ABS_state = 5)
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mNackTitle & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 4) & (((input = MP3_ABS_mNackTitle & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mNackTitle & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mNackTitle & output = UNDEF))) -> next(MP3_ABS_state = 5)
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mNackTitle & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 4) & (((input = MP3_ABS_mNackTitle & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mNackTitle & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 4)
TRANS ((MP3_ABS_state = 4) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 4) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 6) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 6) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 6)
TRANS ((MP3_ABS_state = 6) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 6) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 6) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 6) & ((input = MP3_ABS_mNackAuthor | (input = MP3_ABS_mAckTitle | input = MP3_ABS_mRequest)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mAckTitle & output = UNDEF))) -> next(MP3_ABS_state = 6)
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mAckTitle & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 4) & (((input = MP3_ABS_mAckTitle & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mAckTitle & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mAckTitle & output = UNDEF))) -> next(MP3_ABS_state = 6)
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mAckTitle & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 4) & (((input = MP3_ABS_mAckTitle & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mAckTitle & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 4) & ((input = MP3_ABS_mNackAuthor | input = MP3_ABS_mRequest))) -> FALSE
TRANS ((MP3_ABS_state = 2) & ((input = UNDEF & output = MP3_ABS_InvokeByTitle))) -> next(MP3_ABS_state = 4)
TRANS ((MP3_ABS_state = 7) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 7) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 7)
TRANS ((MP3_ABS_state = 7) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 7) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 8) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 8) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 8)
TRANS ((MP3_ABS_state = 8) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 8) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 8) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 8) & ((input = MP3_ABS_mNackAuthor | (input = MP3_ABS_mAckTitle | input = MP3_ABS_mRequest)))) -> FALSE
TRANS ((MP3_ABS_state = 7) & ((input = MP3_ABS_mAckAuthor & output = UNDEF))) -> next(MP3_ABS_state = 8)
TRANS ((MP3_ABS_state = 7) & ((input = MP3_ABS_mAckAuthor & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 7) & (((input = MP3_ABS_mAckAuthor & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mAckAuthor & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 7) & (input = MP3_ABS_mAckTitle)) -> FALSE
TRANS ((MP3_ABS_state = 9) & (input = MP3_ABS_mNackTitle)) -> FALSE
TRANS ((MP3_ABS_state = 9) & ((input = UNDEF & output = UNDEF))) -> next(MP3_ABS_state = 9)
TRANS ((MP3_ABS_state = 9) & ((input = UNDEF & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 9) & (((input = UNDEF & output = MP3_ABS_InvokeByTitle) | (input = UNDEF & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 9) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 9) & ((input = MP3_ABS_mNackAuthor | (input = MP3_ABS_mAckTitle | input = MP3_ABS_mRequest)))) -> FALSE
TRANS ((MP3_ABS_state = 7) & ((input = MP3_ABS_mNackAuthor & output = UNDEF))) -> next(MP3_ABS_state = 9)
TRANS ((MP3_ABS_state = 7) & ((input = MP3_ABS_mNackAuthor & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 7) & (((input = MP3_ABS_mNackAuthor & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mNackAuthor & output = MP3_ABS_InvokeByAuthor)))) -> FALSE
TRANS ((MP3_ABS_state = 7) & (input = MP3_ABS_mRequest)) -> FALSE
TRANS ((MP3_ABS_state = 2) & ((input = UNDEF & output = MP3_ABS_InvokeByAuthor))) -> next(MP3_ABS_state = 7)
TRANS ((MP3_ABS_state = 2) & (input = MP3_ABS_mAckAuthor)) -> FALSE
TRANS ((MP3_ABS_state = 2) & ((input = MP3_ABS_mNackAuthor | (input = MP3_ABS_mAckTitle | input = MP3_ABS_mRequest)))) -> FALSE
TRANS ((MP3_ABS_state = 1) & ((input = MP3_ABS_mRequest & output = UNDEF))) -> next(MP3_ABS_state = 2)
TRANS ((MP3_ABS_state = 1) & ((input = MP3_ABS_mRequest & output = MP3_ABS_mNot_avail))) -> FALSE
TRANS ((MP3_ABS_state = 1) & (((input = MP3_ABS_mRequest & output = MP3_ABS_InvokeByTitle) | (input = MP3_ABS_mRequest & output = MP3_ABS_InvokeByAuthor)))) -> FALSE

TRANS ((Buy_ABS_state = 1) & ((input = UNDEF & output = Buy_ABS_bInvoke20))) -> FALSE
TRANS ((Buy_ABS_state = 1) & ((input = UNDEF & output = UNDEF))) -> next(Buy_ABS_state = 1)
TRANS ((Buy_ABS_state = 1) & ((input = UNDEF & output = Buy_ABS_bInvoke10_10))) -> FALSE
TRANS ((Buy_ABS_state = 1) & ((input = Buy_ABS_bRequest & output = Buy_ABS_bInvoke20))) -> FALSE
TRANS ((Buy_ABS_state = 3) & ((input = UNDEF & output = Buy_ABS_bInvoke20))) -> FALSE
TRANS ((Buy_ABS_state = 3) & ((input = UNDEF & output = UNDEF))) -> next(Buy_ABS_state = 3)
TRANS ((Buy_ABS_state = 3) & ((input = UNDEF & output = Buy_ABS_bInvoke10_10))) -> FALSE
TRANS ((Buy_ABS_state = 3) & (input = Buy_ABS_bRequest)) -> FALSE
TRANS ((Buy_ABS_state = 2) & ((input = UNDEF & output = Buy_ABS_bInvoke20))) -> next(Buy_ABS_state = 3)
TRANS ((Buy_ABS_state = 2) & ((input = UNDEF & output = Buy_ABS_bInvoke20))) -> next(Buy_ABS_state = 3)
TRANS ((Buy_ABS_state = 2) & ((input = UNDEF & output = UNDEF))) -> next(Buy_ABS_state = 2)
TRANS ((Buy_ABS_state = 4) & ((input = UNDEF & output = Buy_ABS_bInvoke20))) -> FALSE
TRANS ((Buy_ABS_state = 4) & ((input = UNDEF & output = UNDEF))) -> next(Buy_ABS_state = 4)
TRANS ((Buy_ABS_state = 4) & ((input = UNDEF & output = Buy_ABS_bInvoke10_10))) -> FALSE
TRANS ((Buy_ABS_state = 4) & (input = Buy_ABS_bRequest)) -> FALSE
TRANS ((Buy_ABS_state = 2) & ((input = UNDEF & output = Buy_ABS_bInvoke10_10))) -> next(Buy_ABS_state = 4)
TRANS ((Buy_ABS_state = 2) & (input = Buy_ABS_bRequest)) -> FALSE
TRANS ((Buy_ABS_state = 1) & ((input = Buy_ABS_bRequest & output = UNDEF))) -> next(Buy_ABS_state = 2)
TRANS ((Buy_ABS_state = 1) & ((input = Buy_ABS_bRequest & output = Buy_ABS_bInvoke10_10))) -> FALSE

TRANS ((CD-Mania_ABS_state = 1) & (input = CD-Mania_ABS_not_avail)) -> FALSE
TRANS ((CD-Mania_ABS_state = 1) & ((input = UNDEF & output = UNDEF))) -> next(CD-Mania_ABS_state = 1)
TRANS ((CD-Mania_ABS_state = 1) & ((input = UNDEF & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 3) & (input = CD-Mania_ABS_not_avail)) -> FALSE
TRANS ((CD-Mania_ABS_state = 3) & ((input = UNDEF & output = UNDEF))) -> next(CD-Mania_ABS_state = 3)
TRANS ((CD-Mania_ABS_state = 3) & ((input = UNDEF & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 3) & (((input = UNDEF & output = CD-Mania_ABS_request) | (input = UNDEF & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 3) & (input = CD-Mania_ABS_offer)) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & ((input = CD-Mania_ABS_not_avail & output = UNDEF))) -> next(CD-Mania_ABS_state = 3)
TRANS ((CD-Mania_ABS_state = 2) & ((input = CD-Mania_ABS_not_avail & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & (((input = CD-Mania_ABS_not_avail & output = CD-Mania_ABS_request) | (input = CD-Mania_ABS_not_avail & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & ((input = CD-Mania_ABS_not_avail & output = UNDEF))) -> next(CD-Mania_ABS_state = 3)
TRANS ((CD-Mania_ABS_state = 2) & ((input = CD-Mania_ABS_not_avail & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & (((input = CD-Mania_ABS_not_avail & output = CD-Mania_ABS_request) | (input = CD-Mania_ABS_not_avail & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & ((input = UNDEF & output = UNDEF))) -> next(CD-Mania_ABS_state = 2)
TRANS ((CD-Mania_ABS_state = 2) & ((input = UNDEF & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & (((input = UNDEF & output = CD-Mania_ABS_request) | (input = UNDEF & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 4) & (input = CD-Mania_ABS_not_avail)) -> FALSE
TRANS ((CD-Mania_ABS_state = 4) & ((input = UNDEF & output = UNDEF))) -> next(CD-Mania_ABS_state = 4)
TRANS ((CD-Mania_ABS_state = 5) & (input = CD-Mania_ABS_not_avail)) -> FALSE
TRANS ((CD-Mania_ABS_state = 5) & ((input = UNDEF & output = UNDEF))) -> next(CD-Mania_ABS_state = 5)
TRANS ((CD-Mania_ABS_state = 5) & ((input = UNDEF & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 5) & (((input = UNDEF & output = CD-Mania_ABS_request) | (input = UNDEF & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 5) & (input = CD-Mania_ABS_offer)) -> FALSE
TRANS ((CD-Mania_ABS_state = 4) & ((input = UNDEF & output = CD-Mania_ABS_ack))) -> next(CD-Mania_ABS_state = 5)
TRANS ((CD-Mania_ABS_state = 4) & ((input = UNDEF & output = CD-Mania_ABS_request))) -> FALSE
TRANS ((CD-Mania_ABS_state = 6) & (input = CD-Mania_ABS_not_avail)) -> FALSE
TRANS ((CD-Mania_ABS_state = 6) & ((input = UNDEF & output = UNDEF))) -> next(CD-Mania_ABS_state = 6)
TRANS ((CD-Mania_ABS_state = 6) & ((input = UNDEF & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 6) & (((input = UNDEF & output = CD-Mania_ABS_request) | (input = UNDEF & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 6) & (input = CD-Mania_ABS_offer)) -> FALSE
TRANS ((CD-Mania_ABS_state = 4) & ((input = UNDEF & output = CD-Mania_ABS_nack))) -> next(CD-Mania_ABS_state = 6)
TRANS ((CD-Mania_ABS_state = 4) & (input = CD-Mania_ABS_offer)) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & ((input = CD-Mania_ABS_offer & output = UNDEF))) -> next(CD-Mania_ABS_state = 4)
TRANS ((CD-Mania_ABS_state = 2) & ((input = CD-Mania_ABS_offer & output = CD-Mania_ABS_ack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 2) & (((input = CD-Mania_ABS_offer & output = CD-Mania_ABS_request) | (input = CD-Mania_ABS_offer & output = CD-Mania_ABS_nack)))) -> FALSE
TRANS ((CD-Mania_ABS_state = 1) & ((input = UNDEF & output = CD-Mania_ABS_request))) -> next(CD-Mania_ABS_state = 2)
TRANS ((CD-Mania_ABS_state = 1) & ((input = UNDEF & output = CD-Mania_ABS_nack))) -> FALSE
TRANS ((CD-Mania_ABS_state = 1) & (input = CD-Mania_ABS_offer)) -> FALSE



--------INPUT XOR OUTPUT TRANSITION---------

TRANS (1-(input = UNDEF)) + (1-(output = UNDEF)) = 1


---------- INVARIANTS ----------

TRANS (input = CD-Mania_ABS_not_avail) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(Buy_ABS_state) = Buy_ABS_state)
TRANS (input = CD-Mania_ABS_not_avail) -> ( TRUE )

TRANS (input = MP3_ABS_mAckAuthor) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (input = MP3_ABS_mAckAuthor) -> ( TRUE )

TRANS (input = Buy_ABS_bRequest) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (input = Buy_ABS_bRequest) -> ( TRUE )

TRANS (input = MP3_ABS_mAckTitle) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (input = MP3_ABS_mAckTitle) -> ( TRUE )

TRANS (input = CD-Mania_ABS_offer) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(Buy_ABS_state) = Buy_ABS_state)
TRANS (input = CD-Mania_ABS_offer) -> ( TRUE )

TRANS (input = MP3_ABS_mRequest) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (input = MP3_ABS_mRequest) -> ( TRUE )

TRANS (input = MP3_ABS_mNackTitle) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (input = MP3_ABS_mNackTitle) -> ( TRUE )

TRANS (input = MP3_ABS_mNackAuthor) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (input = MP3_ABS_mNackAuthor) -> ( TRUE )

TRANS (output = MP3_ABS_InvokeByAuthor) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (output = MP3_ABS_InvokeByAuthor) -> ( TRUE )

TRANS (output = MP3_ABS_mNot_avail) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (output = MP3_ABS_mNot_avail) -> ( TRUE )

TRANS (output = MP3_ABS_InvokeByTitle) -> ( TRUE  & next(Buy_ABS_state) = Buy_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (output = MP3_ABS_InvokeByTitle) -> ( TRUE )

TRANS (output = CD-Mania_ABS_request) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(Buy_ABS_state) = Buy_ABS_state)
TRANS (output = CD-Mania_ABS_request) -> ( TRUE )

TRANS (output = Buy_ABS_bInvoke10_10) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (output = Buy_ABS_bInvoke10_10) -> ( TRUE )

TRANS (output = CD-Mania_ABS_ack) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(Buy_ABS_state) = Buy_ABS_state)
TRANS (output = CD-Mania_ABS_ack) -> ( TRUE )

TRANS (output = Buy_ABS_bInvoke20) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(CD-Mania_ABS_state) = CD-Mania_ABS_state)
TRANS (output = Buy_ABS_bInvoke20) -> ( TRUE )

TRANS (output = CD-Mania_ABS_nack) -> ( TRUE  & next(MP3_ABS_state) = MP3_ABS_state & next(Buy_ABS_state) = Buy_ABS_state)
TRANS (output = CD-Mania_ABS_nack) -> ( TRUE )



------- CLOSE TRANSITION -------

TRANS (
   FALSE 
   | (TRUE)
)



DEFINE MP3_ABS_pcFAILMP3_ABS_pcFAIL_NACKMP3_ABS_pcSTART := ((MP3_ABS_state = 9 | MP3_ABS_state = 3) | MP3_ABS_state = 1);
DEFINE MP3_ABS_pcSUCC := MP3_ABS_state = 8;


DEFINE Buy_ABS_pcFAILBuy_ABS_pcSTART := Buy_ABS_state = 1;
DEFINE Buy_ABS_pcSUCC := Buy_ABS_state = 3;


DEFINE CD-Mania_ABS_pcFAILCD-Mania_ABS_pcFAIL_NACKCD-Mania_ABS_pcSTART := ((CD-Mania_ABS_state = 6 | CD-Mania_ABS_state = 3) | CD-Mania_ABS_state = 1);
DEFINE CD-Mania_ABS_pcSUCC := CD-Mania_ABS_state = 5;




-- Variable section for composition --
MODULE main 

VAR dn_main : dn_main;

DEFINE _ME := CD-Mania ;


-- Goal section for composition --

GOAL ONEOF(((dn_main.MP3_ABS_pcSUCC&dn_main.Buy_ABS_pcSUCC&dn_main.CD-Mania_ABS_pcSUCC)), 1;((dn_main.MP3_ABS_pcFAILMP3_ABS_pcFAIL_NACKMP3_ABS_pcSTART&dn_main.Buy_ABS_pcFAILBuy_ABS_pcSTART&dn_main.CD-Mania_ABS_pcFAILCD-Mania_ABS_pcFAIL_NACKCD-Mania_ABS_pcSTART)), 0)