/* * Automatically generated by verbus-j 0.1a4 */ #define BPEL_lc_basic_state_not_started 0 #define BPEL_lc_basic_state_running 1 #define BPEL_lc_basic_state_completed 2 #define BPEL_lc_basic_state_cancelled 3 #define BPEL_lc_state_not_started 0 #define BPEL_lc_state_running 1 #define BPEL_lc_state_completed 2 #define BPEL_lc_state_compensating 3 #define BPEL_lc_state_compensated 4 #define BPEL_lc_state_faulted 5 #define BPEL_lc_state_fault_cancelling 6 #define BPEL_lc_state_cancelling 7 #define BPEL_lc_state_terminating 8 #define BPEL_lc_state_cancelled 9 #define BPEL_lc_fault_none 0 #define BPEL_lc_fault_urn_echo_echoService_orderCancelled 1 #define BPEL_lc_fault_handler_none 0 #define BPEL_lc_fault_handler_wait_catch_act_1 1 #define OrderMessage_order__productId__abstract__none 0 #define OrderMessage_order__color_white 0 #define OrderMessage_order__color_red 1 #define OrderMessage_order__color_blue 2 #define OrderMessage_order__color_black 3 #define InvoiceMessage_price__abstract__none 0 #define InvoiceMessage_order__productId__abstract__none 0 #define InvoiceMessage_order__color_white 0 #define InvoiceMessage_order__color_red 1 #define InvoiceMessage_order__color_blue 2 #define InvoiceMessage_order__color_black 3 #define switch_act_4_switch_sel___selected_none 0 #define switch_act_4_switch_sel___selected_case_0 1 #define switch_act_4_switch_sel___selected_otherwise 2 #define unnamed_act_8_pick_sel___activated_none 0 #define unnamed_act_8_pick_sel___activated_receive_not_0 1 #define unnamed_act_8_pick_sel___activated_onAlarm_0 2 /* variable declarations */ bool order_urgent = 0; byte order_order__productId = OrderMessage_order__productId__abstract__none; byte order_order__color = OrderMessage_order__color_white; byte invoice_price = InvoiceMessage_price__abstract__none; bool invoice_urgent = 0; byte invoice_order__productId = InvoiceMessage_order__productId__abstract__none; byte invoice_order__color = InvoiceMessage_order__color_white; byte process_ordersProcess_lc___state = BPEL_lc_state_not_started; byte process_ordersProcess_lc___fault = BPEL_lc_fault_none; byte process_ordersProcess_lc___fault_handler = BPEL_lc_fault_handler_none; byte wait_catch_act_1_lc___state = BPEL_lc_basic_state_not_started; byte main_act_2_lc___state = BPEL_lc_basic_state_not_started; byte init_act_3_lc___state = BPEL_lc_basic_state_not_started; byte switch_act_4_lc___state = BPEL_lc_basic_state_not_started; byte switch_act_4_switch_sel___selected = switch_act_4_switch_sel___selected_none; byte urgent_req_act_5_lc___state = BPEL_lc_state_not_started; byte urgent_req_act_5_lc___fault = BPEL_lc_fault_none; byte urgent_req_act_5_lc___fault_handler = BPEL_lc_fault_handler_none; byte unnamed_act_6_lc___state = BPEL_lc_basic_state_not_started; byte schedule_act_7_lc___state = BPEL_lc_state_not_started; byte schedule_act_7_lc___fault = BPEL_lc_fault_none; byte schedule_act_7_lc___fault_handler = BPEL_lc_fault_handler_none; byte unnamed_act_8_lc___state = BPEL_lc_basic_state_not_started; byte unnamed_act_8_pick_sel___activated = unnamed_act_8_pick_sel___activated_none; byte unnamed_act_9_lc___state = BPEL_lc_basic_state_not_started; byte urgent_req2_act_10_lc___state = BPEL_lc_state_not_started; byte urgent_req2_act_10_lc___fault = BPEL_lc_fault_none; byte urgent_req2_act_10_lc___fault_handler = BPEL_lc_fault_handler_none; byte end_act_11_lc___state = BPEL_lc_state_not_started; byte end_act_11_lc___fault = BPEL_lc_fault_none; byte end_act_11_lc___fault_handler = BPEL_lc_fault_handler_none; byte unnamed_act_12_lc___state = BPEL_lc_basic_state_not_started; /* Process to run the specification */ proctype ordersProcess() { /* main loop */ do :: if /* transition process_ordersProcess_act__::catchCompletion */ :: ((process_ordersProcess_lc___state==BPEL_lc_state_faulted) && ((wait_catch_act_1_lc___state==BPEL_lc_basic_state_completed))) ->process_ordersProcess_lc___state=BPEL_lc_state_cancelled /* transition process_ordersProcess_act__::fault_cancel_begin */ :: ((process_ordersProcess_lc___fault_handler!=BPEL_lc_fault_handler_none) && (process_ordersProcess_lc___state==BPEL_lc_state_running)) ->process_ordersProcess_lc___state=BPEL_lc_state_fault_cancelling /* transition process_ordersProcess_act__::fault_cancel_end */ :: ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) && ((init_act_3_lc___state==BPEL_lc_basic_state_completed) || (init_act_3_lc___state==BPEL_lc_basic_state_not_started) || (init_act_3_lc___state==BPEL_lc_basic_state_cancelled)) && ((urgent_req_act_5_lc___state==BPEL_lc_state_completed) || (urgent_req_act_5_lc___state==BPEL_lc_state_not_started) || (urgent_req_act_5_lc___state==BPEL_lc_state_cancelled)) && ((schedule_act_7_lc___state==BPEL_lc_state_completed) || (schedule_act_7_lc___state==BPEL_lc_state_not_started) || (schedule_act_7_lc___state==BPEL_lc_state_cancelled)) && ((unnamed_act_9_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_9_lc___state==BPEL_lc_basic_state_not_started)) && ((urgent_req2_act_10_lc___state==BPEL_lc_state_completed) || (urgent_req2_act_10_lc___state==BPEL_lc_state_not_started) || (urgent_req2_act_10_lc___state==BPEL_lc_state_cancelled)) && ((unnamed_act_8_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_8_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_8_lc___state==BPEL_lc_basic_state_cancelled)) && ((unnamed_act_6_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_6_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_6_lc___state==BPEL_lc_basic_state_cancelled)) && ((switch_act_4_lc___state==BPEL_lc_basic_state_completed) || (switch_act_4_lc___state==BPEL_lc_basic_state_not_started) || (switch_act_4_lc___state==BPEL_lc_basic_state_cancelled)) && ((end_act_11_lc___state==BPEL_lc_state_completed) || (end_act_11_lc___state==BPEL_lc_state_not_started) || (end_act_11_lc___state==BPEL_lc_state_cancelled)) && ((main_act_2_lc___state==BPEL_lc_basic_state_completed) || (main_act_2_lc___state==BPEL_lc_basic_state_not_started) || (main_act_2_lc___state==BPEL_lc_basic_state_cancelled))) ->process_ordersProcess_lc___state=BPEL_lc_state_faulted /* transition process_ordersProcess_act__::terminate_end */ :: ((process_ordersProcess_lc___state==BPEL_lc_state_terminating) && ((init_act_3_lc___state==BPEL_lc_basic_state_completed) || (init_act_3_lc___state==BPEL_lc_basic_state_not_started) || (init_act_3_lc___state==BPEL_lc_basic_state_cancelled)) && ((urgent_req_act_5_lc___state==BPEL_lc_state_completed) || (urgent_req_act_5_lc___state==BPEL_lc_state_not_started) || (urgent_req_act_5_lc___state==BPEL_lc_state_cancelled)) && ((schedule_act_7_lc___state==BPEL_lc_state_completed) || (schedule_act_7_lc___state==BPEL_lc_state_not_started) || (schedule_act_7_lc___state==BPEL_lc_state_cancelled)) && ((unnamed_act_9_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_9_lc___state==BPEL_lc_basic_state_not_started)) && ((urgent_req2_act_10_lc___state==BPEL_lc_state_completed) || (urgent_req2_act_10_lc___state==BPEL_lc_state_not_started) || (urgent_req2_act_10_lc___state==BPEL_lc_state_cancelled)) && ((unnamed_act_8_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_8_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_8_lc___state==BPEL_lc_basic_state_cancelled)) && ((unnamed_act_6_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_6_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_6_lc___state==BPEL_lc_basic_state_cancelled)) && ((switch_act_4_lc___state==BPEL_lc_basic_state_completed) || (switch_act_4_lc___state==BPEL_lc_basic_state_not_started) || (switch_act_4_lc___state==BPEL_lc_basic_state_cancelled)) && ((end_act_11_lc___state==BPEL_lc_state_completed) || (end_act_11_lc___state==BPEL_lc_state_not_started) || (end_act_11_lc___state==BPEL_lc_state_cancelled)) && ((main_act_2_lc___state==BPEL_lc_basic_state_completed) || (main_act_2_lc___state==BPEL_lc_basic_state_not_started) || (main_act_2_lc___state==BPEL_lc_basic_state_cancelled))) ->process_ordersProcess_lc___state=BPEL_lc_state_cancelled /* transition process_ordersProcess_act__::complete */ :: ((main_act_2_lc___state==BPEL_lc_basic_state_completed) && (process_ordersProcess_lc___state==BPEL_lc_state_running)) ->process_ordersProcess_lc___state=BPEL_lc_state_completed /* transition wait_catch_act_1::begin */ :: ((process_ordersProcess_lc___state==BPEL_lc_state_faulted) && (wait_catch_act_1_lc___state==BPEL_lc_basic_state_not_started) && (process_ordersProcess_lc___fault_handler==BPEL_lc_fault_handler_wait_catch_act_1)) ->wait_catch_act_1_lc___state=BPEL_lc_basic_state_running /* transition wait_catch_act_1::complete */ :: ((wait_catch_act_1_lc___state==BPEL_lc_basic_state_running)) ->wait_catch_act_1_lc___state=BPEL_lc_basic_state_completed /* transition main_act_2::begin */ :: ((main_act_2_lc___state==BPEL_lc_basic_state_not_started)) ->main_act_2_lc___state=BPEL_lc_basic_state_running /* transition main_act_2::complete */ :: ((main_act_2_lc___state==BPEL_lc_basic_state_running) && (end_act_11_lc___state==BPEL_lc_state_completed)) ->main_act_2_lc___state=BPEL_lc_basic_state_completed /* transition main_act_2::cancel */ :: ((main_act_2_lc___state==BPEL_lc_basic_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->main_act_2_lc___state=BPEL_lc_basic_state_cancelled /* transition init_act_3::begin */ :: ((main_act_2_lc___state==BPEL_lc_basic_state_running) && (init_act_3_lc___state==BPEL_lc_basic_state_not_started)) ->init_act_3_lc___state=BPEL_lc_basic_state_running /* transition init_act_3::complete */ :: ((init_act_3_lc___state==BPEL_lc_basic_state_running)) ->atomic{init_act_3_lc___state=BPEL_lc_basic_state_completed; process_ordersProcess_lc___state=BPEL_lc_state_running} /* transition init_act_3::cancel */ :: ((init_act_3_lc___state==BPEL_lc_basic_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->init_act_3_lc___state=BPEL_lc_basic_state_cancelled /* transition switch_act_4::begin */ :: ((init_act_3_lc___state==BPEL_lc_basic_state_completed) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (switch_act_4_lc___state==BPEL_lc_basic_state_not_started)) ->atomic{switch_act_4_lc___state=BPEL_lc_basic_state_running; switch_act_4_switch_sel___selected=switch_act_4_switch_sel___selected_none} /* transition switch_act_4::begin_case_0 */ :: ((switch_act_4_lc___state==BPEL_lc_basic_state_running) && (switch_act_4_switch_sel___selected==switch_act_4_switch_sel___selected_none) && (order_urgent)) ->switch_act_4_switch_sel___selected=switch_act_4_switch_sel___selected_case_0 /* transition switch_act_4::complete_case_0 */ :: ((switch_act_4_lc___state==BPEL_lc_basic_state_running) && (urgent_req_act_5_lc___state==BPEL_lc_state_completed) && (switch_act_4_switch_sel___selected==switch_act_4_switch_sel___selected_case_0)) ->atomic{switch_act_4_lc___state=BPEL_lc_basic_state_completed; switch_act_4_switch_sel___selected=switch_act_4_switch_sel___selected_none} /* transition switch_act_4::begin_otherwise */ :: ((switch_act_4_lc___state==BPEL_lc_basic_state_running) && (switch_act_4_switch_sel___selected==switch_act_4_switch_sel___selected_none) && (!(order_urgent))) ->switch_act_4_switch_sel___selected=switch_act_4_switch_sel___selected_otherwise /* transition switch_act_4::complete_otherwise */ :: ((switch_act_4_lc___state==BPEL_lc_basic_state_running) && (unnamed_act_6_lc___state==BPEL_lc_basic_state_completed) && (switch_act_4_switch_sel___selected==switch_act_4_switch_sel___selected_otherwise)) ->atomic{switch_act_4_lc___state=BPEL_lc_basic_state_completed; switch_act_4_switch_sel___selected=switch_act_4_switch_sel___selected_none} /* transition switch_act_4::cancel */ :: ((switch_act_4_lc___state==BPEL_lc_basic_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->switch_act_4_lc___state=BPEL_lc_basic_state_cancelled /* transition urgent_req_act_5::throw1 */ :: ((urgent_req_act_5_lc___state==BPEL_lc_state_running)) ->atomic{urgent_req_act_5_lc___state=BPEL_lc_state_completed; process_ordersProcess_lc___fault_handler=BPEL_lc_fault_handler_wait_catch_act_1} /* transition urgent_req_act_5::begin */ :: ((switch_act_4_switch_sel___selected==switch_act_4_switch_sel___selected_case_0) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (urgent_req_act_5_lc___state==BPEL_lc_state_not_started)) ->urgent_req_act_5_lc___state=BPEL_lc_state_running /* transition urgent_req_act_5::complete */ :: ((urgent_req_act_5_lc___state==BPEL_lc_state_running)) ->urgent_req_act_5_lc___state=BPEL_lc_state_completed /* transition urgent_req_act_5::cancel */ :: ((urgent_req_act_5_lc___state==BPEL_lc_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->urgent_req_act_5_lc___state=BPEL_lc_state_cancelled /* transition unnamed_act_6::begin */ :: ((switch_act_4_switch_sel___selected==switch_act_4_switch_sel___selected_otherwise) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (unnamed_act_6_lc___state==BPEL_lc_basic_state_not_started)) ->unnamed_act_6_lc___state=BPEL_lc_basic_state_running /* transition unnamed_act_6::complete */ :: ((unnamed_act_6_lc___state==BPEL_lc_basic_state_running) && (unnamed_act_8_lc___state==BPEL_lc_basic_state_completed)) ->unnamed_act_6_lc___state=BPEL_lc_basic_state_completed /* transition unnamed_act_6::cancel */ :: ((unnamed_act_6_lc___state==BPEL_lc_basic_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->unnamed_act_6_lc___state=BPEL_lc_basic_state_cancelled /* transition schedule_act_7::begin */ :: ((unnamed_act_6_lc___state==BPEL_lc_basic_state_running) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (schedule_act_7_lc___state==BPEL_lc_state_not_started)) ->schedule_act_7_lc___state=BPEL_lc_state_running /* transition schedule_act_7::complete */ :: ((schedule_act_7_lc___state==BPEL_lc_state_running)) ->schedule_act_7_lc___state=BPEL_lc_state_completed /* transition schedule_act_7::cancel */ :: ((schedule_act_7_lc___state==BPEL_lc_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->schedule_act_7_lc___state=BPEL_lc_state_cancelled /* transition unnamed_act_8::begin */ :: ((schedule_act_7_lc___state==BPEL_lc_state_completed) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (unnamed_act_8_lc___state==BPEL_lc_basic_state_not_started)) ->atomic{unnamed_act_8_lc___state=BPEL_lc_basic_state_running; unnamed_act_8_pick_sel___activated=unnamed_act_8_pick_sel___activated_none} /* transition unnamed_act_8::begin_receive_not_0 */ :: ((unnamed_act_8_lc___state==BPEL_lc_basic_state_running) && (unnamed_act_8_pick_sel___activated==unnamed_act_8_pick_sel___activated_none)) ->unnamed_act_8_pick_sel___activated=unnamed_act_8_pick_sel___activated_receive_not_0 /* transition unnamed_act_8::complete_receive_not_0 */ :: ((unnamed_act_8_lc___state==BPEL_lc_basic_state_running) && (unnamed_act_9_lc___state==BPEL_lc_basic_state_completed) && (unnamed_act_8_pick_sel___activated==unnamed_act_8_pick_sel___activated_receive_not_0)) ->atomic{unnamed_act_8_lc___state=BPEL_lc_basic_state_completed; unnamed_act_8_pick_sel___activated=unnamed_act_8_pick_sel___activated_none} /* transition unnamed_act_8::begin_onAlarm_0 */ :: ((unnamed_act_8_lc___state==BPEL_lc_basic_state_running) && (unnamed_act_8_pick_sel___activated==unnamed_act_8_pick_sel___activated_none)) ->unnamed_act_8_pick_sel___activated=unnamed_act_8_pick_sel___activated_onAlarm_0 /* transition unnamed_act_8::complete_onAlarm_0 */ :: ((unnamed_act_8_lc___state==BPEL_lc_basic_state_running) && (urgent_req2_act_10_lc___state==BPEL_lc_state_completed) && (unnamed_act_8_pick_sel___activated==unnamed_act_8_pick_sel___activated_onAlarm_0)) ->atomic{unnamed_act_8_lc___state=BPEL_lc_basic_state_completed; unnamed_act_8_pick_sel___activated=unnamed_act_8_pick_sel___activated_none} /* transition unnamed_act_8::cancel */ :: ((unnamed_act_8_lc___state==BPEL_lc_basic_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->unnamed_act_8_lc___state=BPEL_lc_basic_state_cancelled /* transition unnamed_act_9::empty */ :: ((unnamed_act_8_pick_sel___activated==unnamed_act_8_pick_sel___activated_receive_not_0) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (unnamed_act_9_lc___state==BPEL_lc_basic_state_not_started)) ->unnamed_act_9_lc___state=BPEL_lc_basic_state_completed /* transition urgent_req2_act_10::throw1 */ :: ((urgent_req2_act_10_lc___state==BPEL_lc_state_running)) ->atomic{urgent_req2_act_10_lc___state=BPEL_lc_state_completed; process_ordersProcess_lc___fault_handler=BPEL_lc_fault_handler_wait_catch_act_1} /* transition urgent_req2_act_10::begin */ :: ((unnamed_act_8_pick_sel___activated==unnamed_act_8_pick_sel___activated_onAlarm_0) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (urgent_req2_act_10_lc___state==BPEL_lc_state_not_started)) ->urgent_req2_act_10_lc___state=BPEL_lc_state_running /* transition urgent_req2_act_10::complete */ :: ((urgent_req2_act_10_lc___state==BPEL_lc_state_running)) ->urgent_req2_act_10_lc___state=BPEL_lc_state_completed /* transition urgent_req2_act_10::cancel */ :: ((urgent_req2_act_10_lc___state==BPEL_lc_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_terminating))) ->urgent_req2_act_10_lc___state=BPEL_lc_state_cancelled /* transition end_act_11::fault_cancel_begin */ :: ((end_act_11_lc___fault!=BPEL_lc_fault_none)) ->end_act_11_lc___state=BPEL_lc_state_fault_cancelling /* transition end_act_11::fault_cancel_end */ :: ((end_act_11_lc___state==BPEL_lc_state_fault_cancelling) && ((unnamed_act_12_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_12_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_12_lc___state==BPEL_lc_basic_state_cancelled))) ->end_act_11_lc___state=BPEL_lc_state_faulted /* transition end_act_11::cancel_begin */ :: ((end_act_11_lc___state==BPEL_lc_state_running) && ((process_ordersProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_ordersProcess_lc___state==BPEL_lc_state_cancelling))) ->end_act_11_lc___state=BPEL_lc_state_cancelling /* transition end_act_11::cancel_end */ :: (((end_act_11_lc___state==BPEL_lc_state_cancelling) || (end_act_11_lc___state==BPEL_lc_state_terminating)) && ((unnamed_act_12_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_12_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_12_lc___state==BPEL_lc_basic_state_cancelled))) ->end_act_11_lc___state=BPEL_lc_state_cancelled /* transition end_act_11::terminate */ :: ((process_ordersProcess_lc___state==BPEL_lc_state_terminating)) ->end_act_11_lc___state=BPEL_lc_state_terminating /* transition end_act_11::begin */ :: ((switch_act_4_lc___state==BPEL_lc_basic_state_completed) && (process_ordersProcess_lc___state==BPEL_lc_state_running) && (end_act_11_lc___state==BPEL_lc_state_not_started)) ->end_act_11_lc___state=BPEL_lc_state_running /* transition end_act_11::complete */ :: ((unnamed_act_12_lc___state==BPEL_lc_basic_state_completed) && (end_act_11_lc___state==BPEL_lc_state_running)) ->end_act_11_lc___state=BPEL_lc_state_completed /* transition unnamed_act_12::reply */ :: ((end_act_11_lc___state==BPEL_lc_state_running) && (end_act_11_lc___state==BPEL_lc_state_running) && (unnamed_act_12_lc___state==BPEL_lc_basic_state_not_started)) ->unnamed_act_12_lc___state=BPEL_lc_basic_state_completed /* transition unnamed_act_12::cancel */ :: ((unnamed_act_12_lc___state==BPEL_lc_basic_state_running) && ((end_act_11_lc___state==BPEL_lc_state_fault_cancelling) || (end_act_11_lc___state==BPEL_lc_state_cancelling) || (end_act_11_lc___state==BPEL_lc_state_terminating))) ->unnamed_act_12_lc___state=BPEL_lc_basic_state_cancelled :: else ->break fi; od; end: assert(((!(process_ordersProcess_lc___state==BPEL_lc_state_running)) && (!(wait_catch_act_1_lc___state==BPEL_lc_basic_state_running)) && (!(main_act_2_lc___state==BPEL_lc_basic_state_running)) && (!(init_act_3_lc___state==BPEL_lc_basic_state_running)) && (!(switch_act_4_lc___state==BPEL_lc_basic_state_running)) && (!(urgent_req_act_5_lc___state==BPEL_lc_state_running)) && (!(unnamed_act_6_lc___state==BPEL_lc_basic_state_running)) && (!(schedule_act_7_lc___state==BPEL_lc_state_running)) && (!(unnamed_act_8_lc___state==BPEL_lc_basic_state_running)) && (!(unnamed_act_9_lc___state==BPEL_lc_basic_state_running)) && (!(urgent_req2_act_10_lc___state==BPEL_lc_state_running)) && (!(end_act_11_lc___state==BPEL_lc_state_running)) && (!(unnamed_act_12_lc___state==BPEL_lc_basic_state_running)))) } /* Init process */ init { run ordersProcess() }