/*
 * Automatically generated by verbus-j 0.1a3
 */

#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_handler_none 0
#define BPEL_lc_fault_handler_unnamed_act_1 1
#define OliveOilRequest_request__customerId__abstract__none 0
#define OliveOilRequest_request__customerId_c102000 1
#define OliveOilResponse_request__customerId__abstract__none 0
#define OliveOilResponse_request__customerId_c102000 1
#define OilOrder_oilType_olive 0
#define OilOrder_oilType_soja 1
#define OilOrder_oilType_sunflower 2
#define OilOrder_customerId__abstract__none 0
#define OilOrder_customerId_c102000 1

/* variable declarations */
int request_request__quantity = 0;
int request_request__maxPrice = 0;
int request_request__deadline = 0;
byte request_request__customerId = OliveOilRequest_request__customerId__abstract__none;
int response_totalPrice = 0;
bool response_ordered = 0;
int response_waitingDays = 0;
int response_price = 0;
int response_request__quantity = 0;
int response_request__maxPrice = 0;
int response_request__deadline = 0;
byte response_request__customerId = OliveOilResponse_request__customerId__abstract__none;
int oPrice_price = 0;
byte oOrder_oilType = OilOrder_oilType_olive;
int oOrder_quantity = 0;
byte oOrder_customerId = OilOrder_customerId__abstract__none;
bool oOrderConfirm_accepted = 0;
byte process_oliveProcess_lc___state = BPEL_lc_state_not_started;
byte process_oliveProcess_lc___fault_handler = BPEL_lc_fault_handler_none;
byte unnamed_act_1_lc___state = BPEL_lc_basic_state_not_started;
byte prepare_neg_response_act_2_lc___state = BPEL_lc_basic_state_not_started;
byte response_neg_act_3_lc___state = BPEL_lc_basic_state_not_started;
byte main_act_4_lc___state = BPEL_lc_basic_state_not_started;
byte unnamed_act_5_lc___state = BPEL_lc_basic_state_not_started;
byte initializations_act_6_lc___state = BPEL_lc_basic_state_not_started;
byte askPrice1_act_7_lc___state = BPEL_lc_state_not_started;
byte askPrice1_act_7_lc___fault_handler = BPEL_lc_fault_handler_none;
byte wait_act_8_lc___state = BPEL_lc_basic_state_not_started;
byte loop_act_9_lc___state = BPEL_lc_basic_state_not_started;
byte white_a_day_act_10_lc___state = BPEL_lc_basic_state_not_started;
byte incdays_act_11_lc___state = BPEL_lc_basic_state_not_started;
byte askPrice2_act_12_lc___state = BPEL_lc_state_not_started;
byte askPrice2_act_12_lc___fault_handler = BPEL_lc_fault_handler_none;
byte unnamed_act_13_lc___state = BPEL_lc_state_not_started;
byte unnamed_act_13_lc___fault_handler = BPEL_lc_fault_handler_none;
byte prepare_response_act_14_lc___state = BPEL_lc_basic_state_not_started;
byte response_act_15_lc___state = BPEL_lc_basic_state_not_started;
/* Process to run the specification */
proctype oliveProcess()
{


    /* main loop */
    do
        :: if
            /* transition process_oliveProcess_act__::catchCompletion */
            :: ((process_oliveProcess_lc___state==BPEL_lc_state_faulted) && ((unnamed_act_1_lc___state==BPEL_lc_basic_state_completed)))
                ->process_oliveProcess_lc___state=BPEL_lc_state_cancelled
            /* transition process_oliveProcess_act__::fault_cancel_begin */
            :: ((process_oliveProcess_lc___fault_handler!=BPEL_lc_fault_handler_none) && (process_oliveProcess_lc___state==BPEL_lc_state_running))
                ->process_oliveProcess_lc___state=BPEL_lc_state_fault_cancelling
            /* transition process_oliveProcess_act__::fault_cancel_end */
            :: ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) && ((unnamed_act_5_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_5_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_5_lc___state==BPEL_lc_basic_state_cancelled)) && ((initializations_act_6_lc___state==BPEL_lc_basic_state_completed) || (initializations_act_6_lc___state==BPEL_lc_basic_state_not_started)) && ((askPrice1_act_7_lc___state==BPEL_lc_state_completed) || (askPrice1_act_7_lc___state==BPEL_lc_state_not_started) || (askPrice1_act_7_lc___state==BPEL_lc_state_cancelled)) && ((white_a_day_act_10_lc___state==BPEL_lc_basic_state_completed) || (white_a_day_act_10_lc___state==BPEL_lc_basic_state_not_started) || (white_a_day_act_10_lc___state==BPEL_lc_basic_state_cancelled)) && ((incdays_act_11_lc___state==BPEL_lc_basic_state_completed) || (incdays_act_11_lc___state==BPEL_lc_basic_state_not_started)) && ((askPrice2_act_12_lc___state==BPEL_lc_state_completed) || (askPrice2_act_12_lc___state==BPEL_lc_state_not_started) || (askPrice2_act_12_lc___state==BPEL_lc_state_cancelled)) && ((loop_act_9_lc___state==BPEL_lc_basic_state_completed) || (loop_act_9_lc___state==BPEL_lc_basic_state_not_started) || (loop_act_9_lc___state==BPEL_lc_basic_state_cancelled)) && ((wait_act_8_lc___state==BPEL_lc_basic_state_completed) || (wait_act_8_lc___state==BPEL_lc_basic_state_not_started) || (wait_act_8_lc___state==BPEL_lc_basic_state_cancelled)) && ((unnamed_act_13_lc___state==BPEL_lc_state_completed) || (unnamed_act_13_lc___state==BPEL_lc_state_not_started) || (unnamed_act_13_lc___state==BPEL_lc_state_cancelled)) && ((prepare_response_act_14_lc___state==BPEL_lc_basic_state_completed) || (prepare_response_act_14_lc___state==BPEL_lc_basic_state_not_started)) && ((response_act_15_lc___state==BPEL_lc_basic_state_completed) || (response_act_15_lc___state==BPEL_lc_basic_state_not_started) || (response_act_15_lc___state==BPEL_lc_basic_state_cancelled)) && ((main_act_4_lc___state==BPEL_lc_basic_state_completed) || (main_act_4_lc___state==BPEL_lc_basic_state_not_started) || (main_act_4_lc___state==BPEL_lc_basic_state_cancelled)))
                ->process_oliveProcess_lc___state=BPEL_lc_state_faulted
            /* transition process_oliveProcess_act__::terminate_end */
            :: ((process_oliveProcess_lc___state==BPEL_lc_state_terminating) && ((unnamed_act_5_lc___state==BPEL_lc_basic_state_completed) || (unnamed_act_5_lc___state==BPEL_lc_basic_state_not_started) || (unnamed_act_5_lc___state==BPEL_lc_basic_state_cancelled)) && ((initializations_act_6_lc___state==BPEL_lc_basic_state_completed) || (initializations_act_6_lc___state==BPEL_lc_basic_state_not_started)) && ((askPrice1_act_7_lc___state==BPEL_lc_state_completed) || (askPrice1_act_7_lc___state==BPEL_lc_state_not_started) || (askPrice1_act_7_lc___state==BPEL_lc_state_cancelled)) && ((white_a_day_act_10_lc___state==BPEL_lc_basic_state_completed) || (white_a_day_act_10_lc___state==BPEL_lc_basic_state_not_started) || (white_a_day_act_10_lc___state==BPEL_lc_basic_state_cancelled)) && ((incdays_act_11_lc___state==BPEL_lc_basic_state_completed) || (incdays_act_11_lc___state==BPEL_lc_basic_state_not_started)) && ((askPrice2_act_12_lc___state==BPEL_lc_state_completed) || (askPrice2_act_12_lc___state==BPEL_lc_state_not_started) || (askPrice2_act_12_lc___state==BPEL_lc_state_cancelled)) && ((loop_act_9_lc___state==BPEL_lc_basic_state_completed) || (loop_act_9_lc___state==BPEL_lc_basic_state_not_started) || (loop_act_9_lc___state==BPEL_lc_basic_state_cancelled)) && ((wait_act_8_lc___state==BPEL_lc_basic_state_completed) || (wait_act_8_lc___state==BPEL_lc_basic_state_not_started) || (wait_act_8_lc___state==BPEL_lc_basic_state_cancelled)) && ((unnamed_act_13_lc___state==BPEL_lc_state_completed) || (unnamed_act_13_lc___state==BPEL_lc_state_not_started) || (unnamed_act_13_lc___state==BPEL_lc_state_cancelled)) && ((prepare_response_act_14_lc___state==BPEL_lc_basic_state_completed) || (prepare_response_act_14_lc___state==BPEL_lc_basic_state_not_started)) && ((response_act_15_lc___state==BPEL_lc_basic_state_completed) || (response_act_15_lc___state==BPEL_lc_basic_state_not_started) || (response_act_15_lc___state==BPEL_lc_basic_state_cancelled)) && ((main_act_4_lc___state==BPEL_lc_basic_state_completed) || (main_act_4_lc___state==BPEL_lc_basic_state_not_started) || (main_act_4_lc___state==BPEL_lc_basic_state_cancelled)))
                ->process_oliveProcess_lc___state=BPEL_lc_state_cancelled
            /* transition process_oliveProcess_act__::complete */
            :: ((main_act_4_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running))
                ->process_oliveProcess_lc___state=BPEL_lc_state_completed
            /* transition unnamed_act_1::begin */
            :: ((process_oliveProcess_lc___state==BPEL_lc_state_faulted) && (unnamed_act_1_lc___state==BPEL_lc_basic_state_not_started) && (process_oliveProcess_lc___fault_handler==BPEL_lc_fault_handler_unnamed_act_1))
                ->unnamed_act_1_lc___state=BPEL_lc_basic_state_running
            /* transition unnamed_act_1::complete */
            :: ((unnamed_act_1_lc___state==BPEL_lc_basic_state_running) && (response_neg_act_3_lc___state==BPEL_lc_basic_state_completed))
                ->unnamed_act_1_lc___state=BPEL_lc_basic_state_completed
            /* transition prepare_neg_response_act_2::assign */
            :: ((unnamed_act_1_lc___state==BPEL_lc_basic_state_running) && (prepare_neg_response_act_2_lc___state==BPEL_lc_basic_state_not_started))
                ->atomic{prepare_neg_response_act_2_lc___state=BPEL_lc_basic_state_completed; atomic{response_request__quantity=request_request__quantity; response_request__maxPrice=request_request__maxPrice; response_request__deadline=request_request__deadline; response_request__customerId=request_request__customerId}; response_ordered=0}
            /* transition response_neg_act_3::reply */
            :: ((prepare_neg_response_act_2_lc___state==BPEL_lc_basic_state_completed) && (response_neg_act_3_lc___state==BPEL_lc_basic_state_not_started))
                ->response_neg_act_3_lc___state=BPEL_lc_basic_state_completed
            /* transition main_act_4::begin */
            :: ((main_act_4_lc___state==BPEL_lc_basic_state_not_started))
                ->main_act_4_lc___state=BPEL_lc_basic_state_running
            /* transition main_act_4::complete */
            :: ((main_act_4_lc___state==BPEL_lc_basic_state_running) && (response_act_15_lc___state==BPEL_lc_basic_state_completed))
                ->main_act_4_lc___state=BPEL_lc_basic_state_completed
            /* transition main_act_4::cancel */
            :: ((main_act_4_lc___state==BPEL_lc_basic_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->main_act_4_lc___state=BPEL_lc_basic_state_cancelled
            /* transition unnamed_act_5::begin_0 */
            :: ((main_act_4_lc___state==BPEL_lc_basic_state_running) && (unnamed_act_5_lc___state==BPEL_lc_basic_state_not_started))
                ->atomic{unnamed_act_5_lc___state=BPEL_lc_basic_state_running; atomic{request_request__customerId=OliveOilRequest_request__customerId_c102000; request_request__maxPrice=3; request_request__deadline=5; request_request__quantity=1}}
            /* transition unnamed_act_5::complete */
            :: ((unnamed_act_5_lc___state==BPEL_lc_basic_state_running))
                ->atomic{unnamed_act_5_lc___state=BPEL_lc_basic_state_completed; process_oliveProcess_lc___state=BPEL_lc_state_running}
            /* transition unnamed_act_5::cancel */
            :: ((unnamed_act_5_lc___state==BPEL_lc_basic_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->unnamed_act_5_lc___state=BPEL_lc_basic_state_cancelled
            /* transition initializations_act_6::assign */
            :: ((unnamed_act_5_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (initializations_act_6_lc___state==BPEL_lc_basic_state_not_started))
                ->atomic{initializations_act_6_lc___state=BPEL_lc_basic_state_completed; response_waitingDays=0; oOrder_quantity=request_request__quantity; oOrder_customerId=request_request__customerId; oOrder_oilType=OilOrder_oilType_olive}
            /* transition askPrice1_act_7::throw1 */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice1_act_7_lc___state=BPEL_lc_state_completed; process_oliveProcess_lc___fault_handler=BPEL_lc_fault_handler_unnamed_act_1}
            /* transition askPrice1_act_7::begin */
            :: ((initializations_act_6_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (askPrice1_act_7_lc___state==BPEL_lc_state_not_started))
                ->askPrice1_act_7_lc___state=BPEL_lc_state_running
            /* transition askPrice1_act_7::complete_0 */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice1_act_7_lc___state=BPEL_lc_state_completed; oPrice_price=1}
            /* transition askPrice1_act_7::complete_1 */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice1_act_7_lc___state=BPEL_lc_state_completed; oPrice_price=2}
            /* transition askPrice1_act_7::complete_2 */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice1_act_7_lc___state=BPEL_lc_state_completed; oPrice_price=4}
            /* transition askPrice1_act_7::complete_3 */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice1_act_7_lc___state=BPEL_lc_state_completed; oPrice_price=5}
            /* transition askPrice1_act_7::complete_4 */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice1_act_7_lc___state=BPEL_lc_state_completed; oPrice_price=6}
            /* transition askPrice1_act_7::cancel */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->askPrice1_act_7_lc___state=BPEL_lc_state_cancelled
            /* transition wait_act_8::begin */
            :: ((askPrice1_act_7_lc___state==BPEL_lc_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (wait_act_8_lc___state==BPEL_lc_basic_state_not_started))
                ->atomic{wait_act_8_lc___state=BPEL_lc_basic_state_running; white_a_day_act_10_lc___state=BPEL_lc_basic_state_not_started; incdays_act_11_lc___state=BPEL_lc_basic_state_not_started; askPrice2_act_12_lc___state=BPEL_lc_state_not_started; loop_act_9_lc___state=BPEL_lc_basic_state_not_started}
            /* transition wait_act_8::continue */
            :: ((((response_waitingDays < request_request__deadline)) && ((oPrice_price > request_request__maxPrice))) && (wait_act_8_lc___state==BPEL_lc_basic_state_running) && (loop_act_9_lc___state==BPEL_lc_basic_state_completed))
                ->atomic{white_a_day_act_10_lc___state=BPEL_lc_basic_state_not_started; incdays_act_11_lc___state=BPEL_lc_basic_state_not_started; askPrice2_act_12_lc___state=BPEL_lc_state_not_started; loop_act_9_lc___state=BPEL_lc_basic_state_not_started}
            /* transition wait_act_8::complete */
            :: ((loop_act_9_lc___state==BPEL_lc_basic_state_completed) && (!(((response_waitingDays < request_request__deadline)) && ((oPrice_price > request_request__maxPrice)))) && (wait_act_8_lc___state==BPEL_lc_basic_state_running))
                ->wait_act_8_lc___state=BPEL_lc_basic_state_completed
            /* transition wait_act_8::cancel */
            :: ((wait_act_8_lc___state==BPEL_lc_basic_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->wait_act_8_lc___state=BPEL_lc_basic_state_cancelled
            /* transition loop_act_9::begin */
            :: ((wait_act_8_lc___state==BPEL_lc_basic_state_running) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (loop_act_9_lc___state==BPEL_lc_basic_state_not_started))
                ->loop_act_9_lc___state=BPEL_lc_basic_state_running
            /* transition loop_act_9::complete */
            :: ((loop_act_9_lc___state==BPEL_lc_basic_state_running) && (askPrice2_act_12_lc___state==BPEL_lc_state_completed))
                ->loop_act_9_lc___state=BPEL_lc_basic_state_completed
            /* transition loop_act_9::cancel */
            :: ((loop_act_9_lc___state==BPEL_lc_basic_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->loop_act_9_lc___state=BPEL_lc_basic_state_cancelled
            /* transition white_a_day_act_10::begin */
            :: ((loop_act_9_lc___state==BPEL_lc_basic_state_running) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (white_a_day_act_10_lc___state==BPEL_lc_basic_state_not_started))
                ->white_a_day_act_10_lc___state=BPEL_lc_basic_state_running
            /* transition white_a_day_act_10::complete */
            :: ((white_a_day_act_10_lc___state==BPEL_lc_basic_state_running))
                ->white_a_day_act_10_lc___state=BPEL_lc_basic_state_completed
            /* transition white_a_day_act_10::cancel */
            :: ((white_a_day_act_10_lc___state==BPEL_lc_basic_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->white_a_day_act_10_lc___state=BPEL_lc_basic_state_cancelled
            /* transition incdays_act_11::assign */
            :: ((white_a_day_act_10_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (incdays_act_11_lc___state==BPEL_lc_basic_state_not_started))
                ->atomic{incdays_act_11_lc___state=BPEL_lc_basic_state_completed; response_waitingDays=(response_waitingDays+1)}
            /* transition askPrice2_act_12::throw1 */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice2_act_12_lc___state=BPEL_lc_state_completed; process_oliveProcess_lc___fault_handler=BPEL_lc_fault_handler_unnamed_act_1}
            /* transition askPrice2_act_12::begin */
            :: ((incdays_act_11_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (askPrice2_act_12_lc___state==BPEL_lc_state_not_started))
                ->askPrice2_act_12_lc___state=BPEL_lc_state_running
            /* transition askPrice2_act_12::complete_0 */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice2_act_12_lc___state=BPEL_lc_state_completed; oPrice_price=1}
            /* transition askPrice2_act_12::complete_1 */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice2_act_12_lc___state=BPEL_lc_state_completed; oPrice_price=2}
            /* transition askPrice2_act_12::complete_2 */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice2_act_12_lc___state=BPEL_lc_state_completed; oPrice_price=4}
            /* transition askPrice2_act_12::complete_3 */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice2_act_12_lc___state=BPEL_lc_state_completed; oPrice_price=5}
            /* transition askPrice2_act_12::complete_4 */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running))
                ->atomic{askPrice2_act_12_lc___state=BPEL_lc_state_completed; oPrice_price=6}
            /* transition askPrice2_act_12::cancel */
            :: ((askPrice2_act_12_lc___state==BPEL_lc_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->askPrice2_act_12_lc___state=BPEL_lc_state_cancelled
            /* transition unnamed_act_13::throw1 */
            :: ((unnamed_act_13_lc___state==BPEL_lc_state_running))
                ->atomic{unnamed_act_13_lc___state=BPEL_lc_state_completed; process_oliveProcess_lc___fault_handler=BPEL_lc_fault_handler_unnamed_act_1}
            /* transition unnamed_act_13::begin */
            :: ((wait_act_8_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (unnamed_act_13_lc___state==BPEL_lc_state_not_started))
                ->unnamed_act_13_lc___state=BPEL_lc_state_running
            /* transition unnamed_act_13::complete_0 */
            :: ((unnamed_act_13_lc___state==BPEL_lc_state_running))
                ->atomic{unnamed_act_13_lc___state=BPEL_lc_state_completed; oOrderConfirm_accepted=1}
            /* transition unnamed_act_13::complete_1 */
            :: ((unnamed_act_13_lc___state==BPEL_lc_state_running))
                ->atomic{unnamed_act_13_lc___state=BPEL_lc_state_completed; oOrderConfirm_accepted=0}
            /* transition unnamed_act_13::cancel */
            :: ((unnamed_act_13_lc___state==BPEL_lc_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->unnamed_act_13_lc___state=BPEL_lc_state_cancelled
            /* transition prepare_response_act_14::assign */
            :: ((unnamed_act_13_lc___state==BPEL_lc_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (prepare_response_act_14_lc___state==BPEL_lc_basic_state_not_started))
                ->atomic{prepare_response_act_14_lc___state=BPEL_lc_basic_state_completed; atomic{response_request__quantity=request_request__quantity; response_request__maxPrice=request_request__maxPrice; response_request__deadline=request_request__deadline; response_request__customerId=request_request__customerId}; response_ordered=oOrderConfirm_accepted; response_price=oPrice_price; response_totalPrice=(request_request__quantity*oPrice_price)}
            /* transition response_act_15::reply */
            :: ((prepare_response_act_14_lc___state==BPEL_lc_basic_state_completed) && (process_oliveProcess_lc___state==BPEL_lc_state_running) && (response_act_15_lc___state==BPEL_lc_basic_state_not_started))
                ->response_act_15_lc___state=BPEL_lc_basic_state_completed
            /* transition response_act_15::cancel */
            :: ((response_act_15_lc___state==BPEL_lc_basic_state_running) && ((process_oliveProcess_lc___state==BPEL_lc_state_fault_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_cancelling) || (process_oliveProcess_lc___state==BPEL_lc_state_terminating)))
                ->response_act_15_lc___state=BPEL_lc_basic_state_cancelled
            :: else
                ->break
            fi;
            /* invariant invariant_0 */
            assert((!(process_oliveProcess_lc___state==BPEL_lc_state_running)) || ((response_waitingDays <= request_request__deadline)));
            /* invariant invariant_2 */
            assert((!(process_oliveProcess_lc___state==BPEL_lc_state_running)) || (((response_price <= request_request__maxPrice)) || (response_waitingDays==request_request__deadline)));
        od;
end:
        assert(((response_act_15_lc___state==BPEL_lc_basic_state_completed) || (response_neg_act_3_lc___state==BPEL_lc_basic_state_completed)) && ((!(process_oliveProcess_lc___state==BPEL_lc_state_running)) && (!(unnamed_act_1_lc___state==BPEL_lc_basic_state_running)) && (!(prepare_neg_response_act_2_lc___state==BPEL_lc_basic_state_running)) && (!(response_neg_act_3_lc___state==BPEL_lc_basic_state_running)) && (!(main_act_4_lc___state==BPEL_lc_basic_state_running)) && (!(unnamed_act_5_lc___state==BPEL_lc_basic_state_running)) && (!(initializations_act_6_lc___state==BPEL_lc_basic_state_running)) && (!(askPrice1_act_7_lc___state==BPEL_lc_state_running)) && (!(wait_act_8_lc___state==BPEL_lc_basic_state_running)) && (!(loop_act_9_lc___state==BPEL_lc_basic_state_running)) && (!(white_a_day_act_10_lc___state==BPEL_lc_basic_state_running)) && (!(incdays_act_11_lc___state==BPEL_lc_basic_state_running)) && (!(askPrice2_act_12_lc___state==BPEL_lc_state_running)) && (!(unnamed_act_13_lc___state==BPEL_lc_state_running)) && (!(prepare_response_act_14_lc___state==BPEL_lc_basic_state_running)) && (!(response_act_15_lc___state==BPEL_lc_basic_state_running))))
    }
    /* Init process */
    init
    {
        run oliveProcess()
    }