MODULE dn_main IVAR input: {UNDEF , VTA_not_avail , VTA_offer , Hotel_hAck , Hotel_hNack , Hotel_hRequest , Flight_fNack , Flight_fAck , Flight_fRequest , local_VTA_offer_time-$-VTA_offer_time , R-46-$NOP , Flight_fOffer_time-$-local_VTA_offer_time , VTA_request_time-$-Flight_fRequest_time , VTA_request_time-$-Flight_fRequest_time , R-39-$NOP , Flight_fOffer_flight-$-VTA_offer_flight , Flight_fOffer_time-$-local_Hotel_hRequest_time , Flight_fOffer_time-$-local_VTA_offer_time , local_Hotel_hRequest_time-$-Hotel_hRequest_time , local_VTA_offer_time-$-VTA_offer_time , Hotel_hOffer_hotel-$-VTA_offer_hotel , local_Flight_fRequest_location-$-Flight_fRequest_location , R-42-$NOP , VTA_request_location-$-local_Flight_fRequest_location , R-47-$NOP , Hotel_hOffer_hotel-$-VTA_offer_hotel , local_Hotel_hRequest_location-$-Hotel_hRequest_location , VTA_request_location-$-local_Hotel_hRequest_location , R-41-$NOP , local_Hotel_hRequest_location-$-Hotel_hRequest_location , R-45-$NOP , Flight_fOffer_time-$-local_Hotel_hRequest_time , local_Hotel_hRequest_time-$-Hotel_hRequest_time , local_Flight_fRequest_location-$-Flight_fRequest_location , Flight_fOffer_flight-$-VTA_offer_flight , R-43-$NOP , VTA_request_location-$-local_Hotel_hRequest_location , VTA_request_location-$-local_Flight_fRequest_location}; IVAR output: {UNDEF , VTA_request , VTA_nack , VTA_ack , Hotel_hNot_avail , Hotel_hOffer , Flight_fOffer , Flight_fNot_avail}; VAR VTA_state : 1 .. 6; INIT VTA_state = 1 VAR Hotel_state : 1 .. 6; INIT Hotel_state = 1 VAR Flight_state : 1 .. 6; INIT Flight_state = 1 VAR R-46_pc: {s0, s1}; INIT R-46_pc = s0 VAR R-Flight_fRequest_time_pc: {s0, s1}; INIT R-Flight_fRequest_time_pc = s0 VAR R-39_pc: {s0, s1}; INIT R-39_pc = s0 VAR R-VTA_offer_flight_pc: {s0, s1}; INIT R-VTA_offer_flight_pc = s0 VAR R-44_pc: {s0, s1, s2}; INIT R-44_pc = s0 VAR R-Hotel_hRequest_time_pc: {s0, s1}; INIT R-Hotel_hRequest_time_pc = s0 VAR R-VTA_offer_time_pc: {s0, s1}; INIT R-VTA_offer_time_pc = s0 VAR R-VTA_offer_hotel_pc: {s0, s1}; INIT R-VTA_offer_hotel_pc = s0 VAR R-42_pc: {s0, s1}; INIT R-42_pc = s0 VAR R-47_pc: {s0, s1}; INIT R-47_pc = s0 VAR R-Hotel_hRequest_location_pc: {s0, s1}; INIT R-Hotel_hRequest_location_pc = s0 VAR R-41_pc: {s0, s1}; INIT R-41_pc = s0 VAR R-45_pc: {s0, s1}; INIT R-45_pc = s0 VAR R-Flight_fRequest_location_pc: {s0, s1}; INIT R-Flight_fRequest_location_pc = s0 VAR R-43_pc: {s0, s1}; INIT R-43_pc = s0 VAR R-40_pc: {s0, s1, s2}; INIT R-40_pc = s0 TRANS ((VTA_state = 1) & (input = VTA_not_avail)) -> FALSE TRANS ((VTA_state = 1) & ((input = UNDEF & output = UNDEF))) -> next(VTA_state = 1) TRANS ((VTA_state = 1) & ((input = UNDEF & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 3) & (input = VTA_not_avail)) -> FALSE TRANS ((VTA_state = 3) & ((input = UNDEF & output = UNDEF))) -> next(VTA_state = 3) TRANS ((VTA_state = 3) & ((input = UNDEF & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 3) & (((input = UNDEF & output = VTA_request) | (input = UNDEF & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 3) & (input = VTA_offer)) -> FALSE TRANS ((VTA_state = 2) & ((input = VTA_not_avail & output = UNDEF))) -> next(VTA_state = 3) TRANS ((VTA_state = 2) & ((input = VTA_not_avail & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 2) & (((input = VTA_not_avail & output = VTA_request) | (input = VTA_not_avail & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 2) & ((input = VTA_not_avail & output = UNDEF))) -> next(VTA_state = 3) TRANS ((VTA_state = 2) & ((input = VTA_not_avail & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 2) & (((input = VTA_not_avail & output = VTA_request) | (input = VTA_not_avail & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 2) & ((input = UNDEF & output = UNDEF))) -> next(VTA_state = 2) TRANS ((VTA_state = 2) & ((input = UNDEF & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 2) & (((input = UNDEF & output = VTA_request) | (input = UNDEF & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 4) & (input = VTA_not_avail)) -> FALSE TRANS ((VTA_state = 4) & ((input = UNDEF & output = UNDEF))) -> next(VTA_state = 4) TRANS ((VTA_state = 5) & (input = VTA_not_avail)) -> FALSE TRANS ((VTA_state = 5) & ((input = UNDEF & output = UNDEF))) -> next(VTA_state = 5) TRANS ((VTA_state = 5) & ((input = UNDEF & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 5) & (((input = UNDEF & output = VTA_request) | (input = UNDEF & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 5) & (input = VTA_offer)) -> FALSE TRANS ((VTA_state = 4) & ((input = UNDEF & output = VTA_nack))) -> next(VTA_state = 5) TRANS ((VTA_state = 4) & ((input = UNDEF & output = VTA_request))) -> FALSE TRANS ((VTA_state = 6) & (input = VTA_not_avail)) -> FALSE TRANS ((VTA_state = 6) & ((input = UNDEF & output = UNDEF))) -> next(VTA_state = 6) TRANS ((VTA_state = 6) & ((input = UNDEF & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 6) & (((input = UNDEF & output = VTA_request) | (input = UNDEF & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 6) & (input = VTA_offer)) -> FALSE TRANS ((VTA_state = 4) & ((input = UNDEF & output = VTA_ack))) -> next(VTA_state = 6) TRANS ((VTA_state = 4) & (input = VTA_offer)) -> FALSE TRANS ((VTA_state = 2) & ((input = VTA_offer & output = UNDEF))) -> next(VTA_state = 4) TRANS ((VTA_state = 2) & ((input = VTA_offer & output = VTA_nack))) -> FALSE TRANS ((VTA_state = 2) & (((input = VTA_offer & output = VTA_request) | (input = VTA_offer & output = VTA_ack)))) -> FALSE TRANS ((VTA_state = 1) & ((input = UNDEF & output = VTA_request))) -> next(VTA_state = 2) TRANS ((VTA_state = 1) & ((input = UNDEF & output = VTA_ack))) -> FALSE TRANS ((VTA_state = 1) & (input = VTA_offer)) -> FALSE TRANS ((Hotel_state = 1) & ((input = UNDEF & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 1) & ((input = UNDEF & output = UNDEF))) -> next(Hotel_state = 1) TRANS ((Hotel_state = 1) & ((input = UNDEF & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 1) & (input = Hotel_hNack)) -> FALSE TRANS ((Hotel_state = 1) & (input = Hotel_hAck)) -> FALSE TRANS ((Hotel_state = 1) & ((input = Hotel_hRequest & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 3) & ((input = UNDEF & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 3) & ((input = UNDEF & output = UNDEF))) -> next(Hotel_state = 3) TRANS ((Hotel_state = 3) & ((input = UNDEF & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 3) & (input = Hotel_hNack)) -> FALSE TRANS ((Hotel_state = 3) & ((input = Hotel_hAck | input = Hotel_hRequest))) -> FALSE TRANS ((Hotel_state = 2) & ((input = UNDEF & output = Hotel_hNot_avail))) -> next(Hotel_state = 3) TRANS ((Hotel_state = 2) & ((input = UNDEF & output = Hotel_hNot_avail))) -> next(Hotel_state = 3) TRANS ((Hotel_state = 2) & ((input = UNDEF & output = UNDEF))) -> next(Hotel_state = 2) TRANS ((Hotel_state = 4) & ((input = UNDEF & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 4) & ((input = UNDEF & output = UNDEF))) -> next(Hotel_state = 4) TRANS ((Hotel_state = 4) & ((input = UNDEF & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 4) & ((input = Hotel_hNack & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 5) & ((input = UNDEF & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 5) & ((input = UNDEF & output = UNDEF))) -> next(Hotel_state = 5) TRANS ((Hotel_state = 5) & ((input = UNDEF & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 5) & (input = Hotel_hNack)) -> FALSE TRANS ((Hotel_state = 5) & ((input = Hotel_hAck | input = Hotel_hRequest))) -> FALSE TRANS ((Hotel_state = 4) & ((input = Hotel_hNack & output = UNDEF))) -> next(Hotel_state = 5) TRANS ((Hotel_state = 4) & ((input = Hotel_hNack & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 4) & ((input = Hotel_hAck & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 6) & ((input = UNDEF & output = Hotel_hNot_avail))) -> FALSE TRANS ((Hotel_state = 6) & ((input = UNDEF & output = UNDEF))) -> next(Hotel_state = 6) TRANS ((Hotel_state = 6) & ((input = UNDEF & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 6) & (input = Hotel_hNack)) -> FALSE TRANS ((Hotel_state = 6) & ((input = Hotel_hAck | input = Hotel_hRequest))) -> FALSE TRANS ((Hotel_state = 4) & ((input = Hotel_hAck & output = UNDEF))) -> next(Hotel_state = 6) TRANS ((Hotel_state = 4) & ((input = Hotel_hAck & output = Hotel_hOffer))) -> FALSE TRANS ((Hotel_state = 4) & (input = Hotel_hRequest)) -> FALSE TRANS ((Hotel_state = 2) & ((input = UNDEF & output = Hotel_hOffer))) -> next(Hotel_state = 4) TRANS ((Hotel_state = 2) & (input = Hotel_hNack)) -> FALSE TRANS ((Hotel_state = 2) & ((input = Hotel_hAck | input = Hotel_hRequest))) -> FALSE TRANS ((Hotel_state = 1) & ((input = Hotel_hRequest & output = UNDEF))) -> next(Hotel_state = 2) TRANS ((Hotel_state = 1) & ((input = Hotel_hRequest & output = Hotel_hOffer))) -> FALSE TRANS ((Flight_state = 1) & ((input = UNDEF & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 1) & ((input = UNDEF & output = UNDEF))) -> next(Flight_state = 1) TRANS ((Flight_state = 1) & ((input = UNDEF & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 1) & (input = Flight_fAck)) -> FALSE TRANS ((Flight_state = 1) & (input = Flight_fNack)) -> FALSE TRANS ((Flight_state = 1) & ((input = Flight_fRequest & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 3) & ((input = UNDEF & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 3) & ((input = UNDEF & output = UNDEF))) -> next(Flight_state = 3) TRANS ((Flight_state = 3) & ((input = UNDEF & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 3) & ((input = Flight_fAck & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 4) & ((input = UNDEF & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 4) & ((input = UNDEF & output = UNDEF))) -> next(Flight_state = 4) TRANS ((Flight_state = 4) & ((input = UNDEF & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 4) & (input = Flight_fAck)) -> FALSE TRANS ((Flight_state = 4) & ((input = Flight_fNack | input = Flight_fRequest))) -> FALSE TRANS ((Flight_state = 3) & ((input = Flight_fAck & output = UNDEF))) -> next(Flight_state = 4) TRANS ((Flight_state = 3) & ((input = Flight_fAck & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 3) & ((input = Flight_fNack & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 5) & ((input = UNDEF & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 5) & ((input = UNDEF & output = UNDEF))) -> next(Flight_state = 5) TRANS ((Flight_state = 5) & ((input = UNDEF & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 5) & (input = Flight_fAck)) -> FALSE TRANS ((Flight_state = 5) & ((input = Flight_fNack | input = Flight_fRequest))) -> FALSE TRANS ((Flight_state = 3) & ((input = Flight_fNack & output = UNDEF))) -> next(Flight_state = 5) TRANS ((Flight_state = 3) & ((input = Flight_fNack & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 3) & (input = Flight_fRequest)) -> FALSE TRANS ((Flight_state = 2) & ((input = UNDEF & output = Flight_fOffer))) -> next(Flight_state = 3) TRANS ((Flight_state = 2) & ((input = UNDEF & output = Flight_fOffer))) -> next(Flight_state = 3) TRANS ((Flight_state = 2) & ((input = UNDEF & output = UNDEF))) -> next(Flight_state = 2) TRANS ((Flight_state = 6) & ((input = UNDEF & output = Flight_fOffer))) -> FALSE TRANS ((Flight_state = 6) & ((input = UNDEF & output = UNDEF))) -> next(Flight_state = 6) TRANS ((Flight_state = 6) & ((input = UNDEF & output = Flight_fNot_avail))) -> FALSE TRANS ((Flight_state = 6) & (input = Flight_fAck)) -> FALSE TRANS ((Flight_state = 6) & ((input = Flight_fNack | input = Flight_fRequest))) -> FALSE TRANS ((Flight_state = 2) & ((input = UNDEF & output = Flight_fNot_avail))) -> next(Flight_state = 6) TRANS ((Flight_state = 2) & (input = Flight_fAck)) -> FALSE TRANS ((Flight_state = 2) & ((input = Flight_fNack | input = Flight_fRequest))) -> FALSE TRANS ((Flight_state = 1) & ((input = Flight_fRequest & output = UNDEF))) -> next(Flight_state = 2) TRANS ((Flight_state = 1) & ((input = Flight_fRequest & output = Flight_fNot_avail))) -> FALSE ---R-46 TRANSITIONS --- TRANS (input = Flight_fOffer_time-$-local_VTA_offer_time) -> (R-46_pc = s0 & next(R-46_pc) = s1) TRANS (input = Flight_fOffer_time-$-local_VTA_offer_time) -> (output = UNDEF) TRANS (input = R-46-$NOP) -> (R-46_pc = s1 & next(R-46_pc) = s0) TRANS (input = R-46-$NOP) -> (output = UNDEF) TRANS (input = local_VTA_offer_time-$-VTA_offer_time) -> (R-46_pc = s1 & next(R-46_pc) = s0) TRANS (input = local_VTA_offer_time-$-VTA_offer_time) -> (output = UNDEF) ---R-Flight_fRequest_time TRANSITIONS --- TRANS (input = VTA_request_time-$-Flight_fRequest_time) -> (R-Flight_fRequest_time_pc = s0 & next(R-Flight_fRequest_time_pc) = s1) TRANS (input = VTA_request_time-$-Flight_fRequest_time) -> (output = UNDEF) TRANS (input = Flight_fRequest) -> (R-Flight_fRequest_time_pc = s1 & next(R-Flight_fRequest_time_pc) = s0) TRANS (input = Flight_fRequest) -> (output = UNDEF) ---R-39 TRANSITIONS --- TRANS (output = VTA_request) -> (R-39_pc = s0 & next(R-39_pc) = s1) TRANS (output = VTA_request) -> (input = UNDEF) TRANS (input = R-39-$NOP) -> (R-39_pc = s1 & next(R-39_pc) = s0) TRANS (input = R-39-$NOP) -> (output = UNDEF) TRANS (input = VTA_request_time-$-Flight_fRequest_time) -> (R-39_pc = s1 & next(R-39_pc) = s0) TRANS (input = VTA_request_time-$-Flight_fRequest_time) -> (output = UNDEF) ---R-VTA_offer_flight TRANSITIONS --- TRANS (input = Flight_fOffer_flight-$-VTA_offer_flight) -> (R-VTA_offer_flight_pc = s0 & next(R-VTA_offer_flight_pc) = s1) TRANS (input = Flight_fOffer_flight-$-VTA_offer_flight) -> (output = UNDEF) TRANS (input = VTA_offer) -> (R-VTA_offer_flight_pc = s1 & next(R-VTA_offer_flight_pc) = s0) TRANS (input = VTA_offer) -> (output = UNDEF) ---R-44 TRANSITIONS --- TRANS (output = Flight_fOffer) -> (R-44_pc = s0 & next(R-44_pc) = s1) TRANS (output = Flight_fOffer) -> (input = UNDEF) TRANS (input = Flight_fOffer_time-$-local_Hotel_hRequest_time) -> (R-44_pc = s1 & next(R-44_pc) = s2) TRANS (input = Flight_fOffer_time-$-local_Hotel_hRequest_time) -> (output = UNDEF) TRANS (input = Flight_fOffer_time-$-local_VTA_offer_time) -> (R-44_pc = s2 & next(R-44_pc) = s0) TRANS (input = Flight_fOffer_time-$-local_VTA_offer_time) -> (output = UNDEF) ---R-Hotel_hRequest_time TRANSITIONS --- TRANS (input = local_Hotel_hRequest_time-$-Hotel_hRequest_time) -> (R-Hotel_hRequest_time_pc = s0 & next(R-Hotel_hRequest_time_pc) = s1) TRANS (input = local_Hotel_hRequest_time-$-Hotel_hRequest_time) -> (output = UNDEF) TRANS (input = Hotel_hRequest) -> (R-Hotel_hRequest_time_pc = s1 & next(R-Hotel_hRequest_time_pc) = s0) TRANS (input = Hotel_hRequest) -> (output = UNDEF) ---R-VTA_offer_time TRANSITIONS --- TRANS (input = local_VTA_offer_time-$-VTA_offer_time) -> (R-VTA_offer_time_pc = s0 & next(R-VTA_offer_time_pc) = s1) TRANS (input = local_VTA_offer_time-$-VTA_offer_time) -> (output = UNDEF) TRANS (input = VTA_offer) -> (R-VTA_offer_time_pc = s1 & next(R-VTA_offer_time_pc) = s0) TRANS (input = VTA_offer) -> (output = UNDEF) ---R-VTA_offer_hotel TRANSITIONS --- TRANS (input = Hotel_hOffer_hotel-$-VTA_offer_hotel) -> (R-VTA_offer_hotel_pc = s0 & next(R-VTA_offer_hotel_pc) = s1) TRANS (input = Hotel_hOffer_hotel-$-VTA_offer_hotel) -> (output = UNDEF) TRANS (input = VTA_offer) -> (R-VTA_offer_hotel_pc = s1 & next(R-VTA_offer_hotel_pc) = s0) TRANS (input = VTA_offer) -> (output = UNDEF) ---R-42 TRANSITIONS --- TRANS (input = VTA_request_location-$-local_Flight_fRequest_location) -> (R-42_pc = s0 & next(R-42_pc) = s1) TRANS (input = VTA_request_location-$-local_Flight_fRequest_location) -> (output = UNDEF) TRANS (input = R-42-$NOP) -> (R-42_pc = s1 & next(R-42_pc) = s0) TRANS (input = R-42-$NOP) -> (output = UNDEF) TRANS (input = local_Flight_fRequest_location-$-Flight_fRequest_location) -> (R-42_pc = s1 & next(R-42_pc) = s0) TRANS (input = local_Flight_fRequest_location-$-Flight_fRequest_location) -> (output = UNDEF) ---R-47 TRANSITIONS --- TRANS (output = Hotel_hOffer) -> (R-47_pc = s0 & next(R-47_pc) = s1) TRANS (output = Hotel_hOffer) -> (input = UNDEF) TRANS (input = R-47-$NOP) -> (R-47_pc = s1 & next(R-47_pc) = s0) TRANS (input = R-47-$NOP) -> (output = UNDEF) TRANS (input = Hotel_hOffer_hotel-$-VTA_offer_hotel) -> (R-47_pc = s1 & next(R-47_pc) = s0) TRANS (input = Hotel_hOffer_hotel-$-VTA_offer_hotel) -> (output = UNDEF) ---R-Hotel_hRequest_location TRANSITIONS --- TRANS (input = local_Hotel_hRequest_location-$-Hotel_hRequest_location) -> (R-Hotel_hRequest_location_pc = s0 & next(R-Hotel_hRequest_location_pc) = s1) TRANS (input = local_Hotel_hRequest_location-$-Hotel_hRequest_location) -> (output = UNDEF) TRANS (input = Hotel_hRequest) -> (R-Hotel_hRequest_location_pc = s1 & next(R-Hotel_hRequest_location_pc) = s0) TRANS (input = Hotel_hRequest) -> (output = UNDEF) ---R-41 TRANSITIONS --- TRANS (input = VTA_request_location-$-local_Hotel_hRequest_location) -> (R-41_pc = s0 & next(R-41_pc) = s1) TRANS (input = VTA_request_location-$-local_Hotel_hRequest_location) -> (output = UNDEF) TRANS (input = R-41-$NOP) -> (R-41_pc = s1 & next(R-41_pc) = s0) TRANS (input = R-41-$NOP) -> (output = UNDEF) TRANS (input = local_Hotel_hRequest_location-$-Hotel_hRequest_location) -> (R-41_pc = s1 & next(R-41_pc) = s0) TRANS (input = local_Hotel_hRequest_location-$-Hotel_hRequest_location) -> (output = UNDEF) ---R-45 TRANSITIONS --- TRANS (input = Flight_fOffer_time-$-local_Hotel_hRequest_time) -> (R-45_pc = s0 & next(R-45_pc) = s1) TRANS (input = Flight_fOffer_time-$-local_Hotel_hRequest_time) -> (output = UNDEF) TRANS (input = R-45-$NOP) -> (R-45_pc = s1 & next(R-45_pc) = s0) TRANS (input = R-45-$NOP) -> (output = UNDEF) TRANS (input = local_Hotel_hRequest_time-$-Hotel_hRequest_time) -> (R-45_pc = s1 & next(R-45_pc) = s0) TRANS (input = local_Hotel_hRequest_time-$-Hotel_hRequest_time) -> (output = UNDEF) ---R-Flight_fRequest_location TRANSITIONS --- TRANS (input = local_Flight_fRequest_location-$-Flight_fRequest_location) -> (R-Flight_fRequest_location_pc = s0 & next(R-Flight_fRequest_location_pc) = s1) TRANS (input = local_Flight_fRequest_location-$-Flight_fRequest_location) -> (output = UNDEF) TRANS (input = Flight_fRequest) -> (R-Flight_fRequest_location_pc = s1 & next(R-Flight_fRequest_location_pc) = s0) TRANS (input = Flight_fRequest) -> (output = UNDEF) ---R-43 TRANSITIONS --- TRANS (output = Flight_fOffer) -> (R-43_pc = s0 & next(R-43_pc) = s1) TRANS (output = Flight_fOffer) -> (input = UNDEF) TRANS (input = R-43-$NOP) -> (R-43_pc = s1 & next(R-43_pc) = s0) TRANS (input = R-43-$NOP) -> (output = UNDEF) TRANS (input = Flight_fOffer_flight-$-VTA_offer_flight) -> (R-43_pc = s1 & next(R-43_pc) = s0) TRANS (input = Flight_fOffer_flight-$-VTA_offer_flight) -> (output = UNDEF) ---R-40 TRANSITIONS --- TRANS (output = VTA_request) -> (R-40_pc = s0 & next(R-40_pc) = s1) TRANS (output = VTA_request) -> (input = UNDEF) TRANS (input = VTA_request_location-$-local_Hotel_hRequest_location) -> (R-40_pc = s1 & next(R-40_pc) = s2) TRANS (input = VTA_request_location-$-local_Hotel_hRequest_location) -> (output = UNDEF) TRANS (input = VTA_request_location-$-local_Flight_fRequest_location) -> (R-40_pc = s2 & next(R-40_pc) = s0) TRANS (input = VTA_request_location-$-local_Flight_fRequest_location) -> (output = UNDEF) --------INPUT XOR OUTPUT TRANSITION--------- TRANS (1-(input = UNDEF)) + (1-(output = UNDEF)) = 1 ---------- INVARIANTS ---------- TRANS (input = local_Hotel_hRequest_time-$-Hotel_hRequest_time) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = local_Hotel_hRequest_time-$-Hotel_hRequest_time) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = local_Hotel_hRequest_location-$-Hotel_hRequest_location) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = local_Hotel_hRequest_location-$-Hotel_hRequest_location) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Flight_fNack) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state) TRANS (input = Flight_fNack) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Hotel_hRequest) -> ( TRUE & next(VTA_state) = VTA_state & next(Flight_state) = Flight_state) TRANS (input = Hotel_hRequest) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = VTA_request_location-$-local_Flight_fRequest_location) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = VTA_request_location-$-local_Flight_fRequest_location) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = R-43-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-43-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc) TRANS (input = local_Flight_fRequest_location-$-Flight_fRequest_location) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = local_Flight_fRequest_location-$-Flight_fRequest_location) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = R-47-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-47-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Hotel_hAck) -> ( TRUE & next(VTA_state) = VTA_state & next(Flight_state) = Flight_state) TRANS (input = Hotel_hAck) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = VTA_offer) -> ( TRUE & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = VTA_offer) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-43_pc) = R-43_pc) TRANS (input = R-45-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-45-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Flight_fOffer_time-$-local_Hotel_hRequest_time) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = Flight_fOffer_time-$-local_Hotel_hRequest_time) -> ( TRUE & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = R-42-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-42-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Flight_fRequest) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state) TRANS (input = Flight_fRequest) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = VTA_request_time-$-Flight_fRequest_time) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = VTA_request_time-$-Flight_fRequest_time) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = VTA_request_location-$-local_Hotel_hRequest_location) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = VTA_request_location-$-local_Hotel_hRequest_location) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Hotel_hNack) -> ( TRUE & next(VTA_state) = VTA_state & next(Flight_state) = Flight_state) TRANS (input = Hotel_hNack) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = VTA_not_avail) -> ( TRUE & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = VTA_not_avail) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = local_VTA_offer_time-$-VTA_offer_time) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = local_VTA_offer_time-$-VTA_offer_time) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = R-46-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-46-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Flight_fOffer_time-$-local_VTA_offer_time) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = Flight_fOffer_time-$-local_VTA_offer_time) -> ( TRUE & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Hotel_hOffer_hotel-$-VTA_offer_hotel) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = Hotel_hOffer_hotel-$-VTA_offer_hotel) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Flight_fAck) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state) TRANS (input = Flight_fAck) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = Flight_fOffer_flight-$-VTA_offer_flight) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = Flight_fOffer_flight-$-VTA_offer_flight) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc) TRANS (input = R-41-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-41-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (input = R-39-$NOP) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (input = R-39-$NOP) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (output = Flight_fNot_avail) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state) TRANS (output = Flight_fNot_avail) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (output = VTA_nack) -> ( TRUE & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (output = VTA_nack) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (output = Flight_fOffer) -> ( TRUE & next(VTA_state) = VTA_state & next(Hotel_state) = Hotel_state) TRANS (output = Flight_fOffer) -> ( TRUE & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc) TRANS (output = VTA_ack) -> ( TRUE & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (output = VTA_ack) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (output = VTA_request) -> ( TRUE & next(Hotel_state) = Hotel_state & next(Flight_state) = Flight_state) TRANS (output = VTA_request) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (output = Hotel_hNot_avail) -> ( TRUE & next(VTA_state) = VTA_state & next(Flight_state) = Flight_state) TRANS (output = Hotel_hNot_avail) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) TRANS (output = Hotel_hOffer) -> ( TRUE & next(VTA_state) = VTA_state & next(Flight_state) = Flight_state) TRANS (output = Hotel_hOffer) -> ( TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) ------- CLOSE TRANSITION ------- TRANS ( FALSE | (R-46_pc = s0 & next(R-46_pc) = s1) | (R-46_pc = s1 & next(R-46_pc) = s0) | (R-46_pc = s1 & next(R-46_pc) = s0) | (R-Flight_fRequest_time_pc = s0 & next(R-Flight_fRequest_time_pc) = s1) | (R-Flight_fRequest_time_pc = s1 & next(R-Flight_fRequest_time_pc) = s0) | (R-39_pc = s0 & next(R-39_pc) = s1) | (R-39_pc = s1 & next(R-39_pc) = s0) | (R-39_pc = s1 & next(R-39_pc) = s0) | (R-VTA_offer_flight_pc = s0 & next(R-VTA_offer_flight_pc) = s1) | (R-VTA_offer_flight_pc = s1 & next(R-VTA_offer_flight_pc) = s0) | (R-44_pc = s0 & next(R-44_pc) = s1) | (R-44_pc = s1 & next(R-44_pc) = s2) | (R-44_pc = s2 & next(R-44_pc) = s0) | (R-Hotel_hRequest_time_pc = s0 & next(R-Hotel_hRequest_time_pc) = s1) | (R-Hotel_hRequest_time_pc = s1 & next(R-Hotel_hRequest_time_pc) = s0) | (R-VTA_offer_time_pc = s0 & next(R-VTA_offer_time_pc) = s1) | (R-VTA_offer_time_pc = s1 & next(R-VTA_offer_time_pc) = s0) | (R-VTA_offer_hotel_pc = s0 & next(R-VTA_offer_hotel_pc) = s1) | (R-VTA_offer_hotel_pc = s1 & next(R-VTA_offer_hotel_pc) = s0) | (R-42_pc = s0 & next(R-42_pc) = s1) | (R-42_pc = s1 & next(R-42_pc) = s0) | (R-42_pc = s1 & next(R-42_pc) = s0) | (R-47_pc = s0 & next(R-47_pc) = s1) | (R-47_pc = s1 & next(R-47_pc) = s0) | (R-47_pc = s1 & next(R-47_pc) = s0) | (R-Hotel_hRequest_location_pc = s0 & next(R-Hotel_hRequest_location_pc) = s1) | (R-Hotel_hRequest_location_pc = s1 & next(R-Hotel_hRequest_location_pc) = s0) | (R-41_pc = s0 & next(R-41_pc) = s1) | (R-41_pc = s1 & next(R-41_pc) = s0) | (R-41_pc = s1 & next(R-41_pc) = s0) | (R-45_pc = s0 & next(R-45_pc) = s1) | (R-45_pc = s1 & next(R-45_pc) = s0) | (R-45_pc = s1 & next(R-45_pc) = s0) | (R-Flight_fRequest_location_pc = s0 & next(R-Flight_fRequest_location_pc) = s1) | (R-Flight_fRequest_location_pc = s1 & next(R-Flight_fRequest_location_pc) = s0) | (R-43_pc = s0 & next(R-43_pc) = s1) | (R-43_pc = s1 & next(R-43_pc) = s0) | (R-43_pc = s1 & next(R-43_pc) = s0) | (R-40_pc = s0 & next(R-40_pc) = s1) | (R-40_pc = s1 & next(R-40_pc) = s2) | (R-40_pc = s2 & next(R-40_pc) = s0) | (TRUE & next(R-44_pc) = R-44_pc & next(R-VTA_offer_time_pc) = R-VTA_offer_time_pc & next(R-46_pc) = R-46_pc & next(R-Hotel_hRequest_time_pc) = R-Hotel_hRequest_time_pc & next(R-45_pc) = R-45_pc & next(R-VTA_offer_hotel_pc) = R-VTA_offer_hotel_pc & next(R-47_pc) = R-47_pc & next(R-40_pc) = R-40_pc & next(R-Flight_fRequest_location_pc) = R-Flight_fRequest_location_pc & next(R-42_pc) = R-42_pc & next(R-Hotel_hRequest_location_pc) = R-Hotel_hRequest_location_pc & next(R-41_pc) = R-41_pc & next(R-Flight_fRequest_time_pc) = R-Flight_fRequest_time_pc & next(R-39_pc) = R-39_pc & next(R-VTA_offer_flight_pc) = R-VTA_offer_flight_pc & next(R-43_pc) = R-43_pc) ) DEFINE VTA_pcFAILVTA_pcFAIL_NACKVTA_pcSTART := ((VTA_state = 5 | VTA_state = 3) | VTA_state = 1); DEFINE VTA_pcSUCC := VTA_state = 6; DEFINE Hotel_pcFAILHotel_pcFAIL_NACKHotel_pcSTART := ((Hotel_state = 5 | Hotel_state = 3) | Hotel_state = 1); DEFINE Hotel_pcSUCC := Hotel_state = 6; DEFINE Flight_pcFAILFlight_pcFAIL_NACKFlight_pcSTART := ((Flight_state = 6 | Flight_state = 5) | Flight_state = 1); DEFINE Flight_pcSUCC := Flight_state = 4; DEFINE R-46SUCC := R-46_pc = s0; DEFINE R-46FAIL := (R-46_pc = s0); DEFINE R-Flight_fRequest_timeSUCC := R-Flight_fRequest_time_pc = s0; DEFINE R-Flight_fRequest_timeFAIL := (R-Flight_fRequest_time_pc = s0); DEFINE R-39SUCC := R-39_pc = s0; DEFINE R-39FAIL := (R-39_pc = s0); DEFINE R-VTA_offer_flightSUCC := R-VTA_offer_flight_pc = s0; DEFINE R-VTA_offer_flightFAIL := (R-VTA_offer_flight_pc = s0); DEFINE R-44SUCC := R-44_pc = s0; DEFINE R-44FAIL := (R-44_pc = s0); DEFINE R-Hotel_hRequest_timeSUCC := R-Hotel_hRequest_time_pc = s0; DEFINE R-Hotel_hRequest_timeFAIL := (R-Hotel_hRequest_time_pc = s0); DEFINE R-VTA_offer_timeSUCC := R-VTA_offer_time_pc = s0; DEFINE R-VTA_offer_timeFAIL := (R-VTA_offer_time_pc = s0); DEFINE R-VTA_offer_hotelSUCC := R-VTA_offer_hotel_pc = s0; DEFINE R-VTA_offer_hotelFAIL := (R-VTA_offer_hotel_pc = s0); DEFINE R-42SUCC := R-42_pc = s0; DEFINE R-42FAIL := (R-42_pc = s0); DEFINE R-47SUCC := R-47_pc = s0; DEFINE R-47FAIL := (R-47_pc = s0); DEFINE R-Hotel_hRequest_locationSUCC := R-Hotel_hRequest_location_pc = s0; DEFINE R-Hotel_hRequest_locationFAIL := (R-Hotel_hRequest_location_pc = s0); DEFINE R-41SUCC := R-41_pc = s0; DEFINE R-41FAIL := (R-41_pc = s0); DEFINE R-45SUCC := R-45_pc = s0; DEFINE R-45FAIL := (R-45_pc = s0); DEFINE R-Flight_fRequest_locationSUCC := R-Flight_fRequest_location_pc = s0; DEFINE R-Flight_fRequest_locationFAIL := (R-Flight_fRequest_location_pc = s0); DEFINE R-43SUCC := R-43_pc = s0; DEFINE R-43FAIL := (R-43_pc = s0); DEFINE R-40SUCC := R-40_pc = s0; DEFINE R-40FAIL := (R-40_pc = s0); -- Variable section for composition -- MODULE main VAR dn_main : dn_main; DEFINE _ME := VTA ; -- Goal section for composition -- GOAL ONEOF(((dn_main.Hotel_pcSUCC&dn_main.Flight_pcSUCC&dn_main.VTA_pcSUCC)&dn_main.R-46SUCC&dn_main.R-Flight_fRequest_timeSUCC&dn_main.R-39SUCC&dn_main.R-VTA_offer_flightSUCC&dn_main.R-44SUCC&dn_main.R-Hotel_hRequest_timeSUCC&dn_main.R-VTA_offer_timeSUCC&dn_main.R-VTA_offer_hotelSUCC&dn_main.R-42SUCC&dn_main.R-47SUCC&dn_main.R-Hotel_hRequest_locationSUCC&dn_main.R-41SUCC&dn_main.R-45SUCC&dn_main.R-Flight_fRequest_locationSUCC&dn_main.R-43SUCC&dn_main.R-40SUCC), 1;((dn_main.Hotel_pcFAILHotel_pcFAIL_NACKHotel_pcSTART&dn_main.Flight_pcFAILFlight_pcFAIL_NACKFlight_pcSTART&dn_main.VTA_pcFAILVTA_pcFAIL_NACKVTA_pcSTART)&dn_main.R-46FAIL&dn_main.R-Flight_fRequest_timeFAIL&dn_main.R-39FAIL&dn_main.R-VTA_offer_flightFAIL&dn_main.R-44FAIL&dn_main.R-Hotel_hRequest_timeFAIL&dn_main.R-VTA_offer_timeFAIL&dn_main.R-VTA_offer_hotelFAIL&dn_main.R-42FAIL&dn_main.R-47FAIL&dn_main.R-Hotel_hRequest_locationFAIL&dn_main.R-41FAIL&dn_main.R-45FAIL&dn_main.R-Flight_fRequest_locationFAIL&dn_main.R-43FAIL&dn_main.R-40FAIL), 0)