process ordersProcess
{
    enttype BPEL_lc_basic {
        state: enum (not_started, running, completed, cancelled);
    }
    enttype BPEL_lc {
        state: enum (not_started, running, completed, compensating, compensated, faulted, fault_cancelling, cancelling, terminating, cancelled);
        fault: enum (none, urn_echo_echoService_orderCancelled);
        fault_handler: enum (none, wait_catch_act_1);
    }
    enttype BPEL_lnk {
        fired: boolean;
    }
    /* message {urn:echo:echoService}OrderMessage */
    enttype OrderMessage {
        urgent: boolean;
        order__productId: enum (_abstract__none);
        order__color: enum (white, red, blue, black);
    }
    /* message {urn:echo:echoService}InvoiceMessage */
    enttype InvoiceMessage {
        price: enum (_abstract__none);
        urgent: boolean;
        order__productId: enum (_abstract__none);
        order__color: enum (white, red, blue, black);
    }
    enttype switch_act_4_switch_sel__ {
        selected: enum (none, case_0, otherwise);
    }
    enttype unnamed_act_8_pick_sel__ {
        activated: enum (none, receive_not_0, onAlarm_0);
    }
    entity order: OrderMessage;
    entity invoice: InvoiceMessage;
    entity process_ordersProcess_lc__: BPEL_lc;
    entity wait_catch_act_1_lc__: BPEL_lc_basic;
    entity main_act_2_lc__: BPEL_lc_basic;
    entity init_act_3_lc__: BPEL_lc_basic;
    entity switch_act_4_lc__: BPEL_lc_basic;
    entity switch_act_4_switch_sel__: switch_act_4_switch_sel__;
    entity urgent_req_act_5_lc__: BPEL_lc;
    entity unnamed_act_6_lc__: BPEL_lc_basic;
    entity schedule_act_7_lc__: BPEL_lc;
    entity unnamed_act_8_lc__: BPEL_lc_basic;
    entity unnamed_act_8_pick_sel__: unnamed_act_8_pick_sel__;
    entity unnamed_act_9_lc__: BPEL_lc_basic;
    entity urgent_req2_act_10_lc__: BPEL_lc;
    entity end_act_11_lc__: BPEL_lc;
    entity unnamed_act_12_lc__: BPEL_lc_basic;
    activity process_ordersProcess_act__ {
        transition catchCompletion {
            domain: {(process_ordersProcess_lc__.state=faulted & wait_catch_act_1_lc__.state=completed)}
            action: {process_ordersProcess_lc__.state=cancelled}
        }
        transition fault_cancel_begin {
            domain: {(process_ordersProcess_lc__.fault_handler!=none & process_ordersProcess_lc__.state=running)}
            action: {process_ordersProcess_lc__.state=fault_cancelling}
        }
        transition fault_cancel_end {
            domain: {(process_ordersProcess_lc__.state=fault_cancelling & (init_act_3_lc__.state=completed | init_act_3_lc__.state=not_started | init_act_3_lc__.state=cancelled) & (urgent_req_act_5_lc__.state=completed | urgent_req_act_5_lc__.state=not_started | urgent_req_act_5_lc__.state=cancelled) & (schedule_act_7_lc__.state=completed | schedule_act_7_lc__.state=not_started | schedule_act_7_lc__.state=cancelled) & (unnamed_act_9_lc__.state=completed | unnamed_act_9_lc__.state=not_started) & (urgent_req2_act_10_lc__.state=completed | urgent_req2_act_10_lc__.state=not_started | urgent_req2_act_10_lc__.state=cancelled) & (unnamed_act_8_lc__.state=completed | unnamed_act_8_lc__.state=not_started | unnamed_act_8_lc__.state=cancelled) & (unnamed_act_6_lc__.state=completed | unnamed_act_6_lc__.state=not_started | unnamed_act_6_lc__.state=cancelled) & (switch_act_4_lc__.state=completed | switch_act_4_lc__.state=not_started | switch_act_4_lc__.state=cancelled) & (end_act_11_lc__.state=completed | end_act_11_lc__.state=not_started | end_act_11_lc__.state=cancelled) & (main_act_2_lc__.state=completed | main_act_2_lc__.state=not_started | main_act_2_lc__.state=cancelled))}
            action: {process_ordersProcess_lc__.state=faulted}
        }
        transition terminate_end {
            domain: {(process_ordersProcess_lc__.state=terminating & (init_act_3_lc__.state=completed | init_act_3_lc__.state=not_started | init_act_3_lc__.state=cancelled) & (urgent_req_act_5_lc__.state=completed | urgent_req_act_5_lc__.state=not_started | urgent_req_act_5_lc__.state=cancelled) & (schedule_act_7_lc__.state=completed | schedule_act_7_lc__.state=not_started | schedule_act_7_lc__.state=cancelled) & (unnamed_act_9_lc__.state=completed | unnamed_act_9_lc__.state=not_started) & (urgent_req2_act_10_lc__.state=completed | urgent_req2_act_10_lc__.state=not_started | urgent_req2_act_10_lc__.state=cancelled) & (unnamed_act_8_lc__.state=completed | unnamed_act_8_lc__.state=not_started | unnamed_act_8_lc__.state=cancelled) & (unnamed_act_6_lc__.state=completed | unnamed_act_6_lc__.state=not_started | unnamed_act_6_lc__.state=cancelled) & (switch_act_4_lc__.state=completed | switch_act_4_lc__.state=not_started | switch_act_4_lc__.state=cancelled) & (end_act_11_lc__.state=completed | end_act_11_lc__.state=not_started | end_act_11_lc__.state=cancelled) & (main_act_2_lc__.state=completed | main_act_2_lc__.state=not_started | main_act_2_lc__.state=cancelled))}
            action: {process_ordersProcess_lc__.state=cancelled}
        }
        transition complete {
            domain: {(main_act_2_lc__.state=completed & process_ordersProcess_lc__.state=running)}
            action: {process_ordersProcess_lc__.state=completed}
        }
    }
    /* catch fault urn_echo_echoService_orderCancelled activity ordersProcess */
    activity wait_catch_act_1 {
        transition begin {
            domain: {(process_ordersProcess_lc__.state=faulted & wait_catch_act_1_lc__.state=not_started & process_ordersProcess_lc__.fault_handler=wait_catch_act_1)}
            action: {wait_catch_act_1_lc__.state=running}
        }
        transition complete {
            domain: {wait_catch_act_1_lc__.state=running}
            action: {wait_catch_act_1_lc__.state=completed}
        }
    }
    activity main_act_2 {
        transition begin {
            domain: {main_act_2_lc__.state=not_started}
            action: {main_act_2_lc__.state=running}
        }
        transition complete {
            domain: {(main_act_2_lc__.state=running & end_act_11_lc__.state=completed)}
            action: {main_act_2_lc__.state=completed}
        }
        transition cancel {
            domain: {(main_act_2_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {main_act_2_lc__.state=cancelled}
        }
    }
    activity init_act_3 {
        transition begin {
            domain: {(main_act_2_lc__.state=running & init_act_3_lc__.state=not_started)}
            action: {init_act_3_lc__.state=running}
        }
        transition complete {
            domain: {init_act_3_lc__.state=running}
            action: {(init_act_3_lc__.state=completed & process_ordersProcess_lc__.state=running)}
        }
        transition cancel {
            domain: {(init_act_3_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {init_act_3_lc__.state=cancelled}
        }
    }
    activity switch_act_4 {
        transition begin {
            domain: {(init_act_3_lc__.state=completed & process_ordersProcess_lc__.state=running & switch_act_4_lc__.state=not_started)}
            action: {(switch_act_4_lc__.state=running & switch_act_4_switch_sel__.selected=none)}
        }
        transition begin_case_0 {
            domain: {(switch_act_4_lc__.state=running & switch_act_4_switch_sel__.selected=none & order.urgent)}
            action: {switch_act_4_switch_sel__.selected=case_0}
        }
        transition complete_case_0 {
            domain: {(switch_act_4_lc__.state=running & urgent_req_act_5_lc__.state=completed & switch_act_4_switch_sel__.selected=case_0)}
            action: {(switch_act_4_lc__.state=completed & switch_act_4_switch_sel__.selected=none)}
        }
        transition begin_otherwise {
            domain: {(switch_act_4_lc__.state=running & switch_act_4_switch_sel__.selected=none & !order.urgent)}
            action: {switch_act_4_switch_sel__.selected=otherwise}
        }
        transition complete_otherwise {
            domain: {(switch_act_4_lc__.state=running & unnamed_act_6_lc__.state=completed & switch_act_4_switch_sel__.selected=otherwise)}
            action: {(switch_act_4_lc__.state=completed & switch_act_4_switch_sel__.selected=none)}
        }
        transition cancel {
            domain: {(switch_act_4_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {switch_act_4_lc__.state=cancelled}
        }
    }
    activity urgent_req_act_5 {
        transition throw1 {
            domain: {urgent_req_act_5_lc__.state=running}
            action: {(urgent_req_act_5_lc__.state=completed & process_ordersProcess_lc__.fault_handler=wait_catch_act_1)}
        }
        transition begin {
            domain: {(switch_act_4_switch_sel__.selected=case_0 & process_ordersProcess_lc__.state=running & urgent_req_act_5_lc__.state=not_started)}
            action: {urgent_req_act_5_lc__.state=running}
        }
        transition complete {
            domain: {urgent_req_act_5_lc__.state=running}
            action: {urgent_req_act_5_lc__.state=completed}
        }
        transition cancel {
            domain: {(urgent_req_act_5_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {urgent_req_act_5_lc__.state=cancelled}
        }
    }
    activity unnamed_act_6 {
        transition begin {
            domain: {(switch_act_4_switch_sel__.selected=otherwise & process_ordersProcess_lc__.state=running & unnamed_act_6_lc__.state=not_started)}
            action: {unnamed_act_6_lc__.state=running}
        }
        transition complete {
            domain: {(unnamed_act_6_lc__.state=running & unnamed_act_8_lc__.state=completed)}
            action: {unnamed_act_6_lc__.state=completed}
        }
        transition cancel {
            domain: {(unnamed_act_6_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {unnamed_act_6_lc__.state=cancelled}
        }
    }
    activity schedule_act_7 {
        transition begin {
            domain: {(unnamed_act_6_lc__.state=running & process_ordersProcess_lc__.state=running & schedule_act_7_lc__.state=not_started)}
            action: {schedule_act_7_lc__.state=running}
        }
        transition complete {
            domain: {schedule_act_7_lc__.state=running}
            action: {schedule_act_7_lc__.state=completed}
        }
        transition cancel {
            domain: {(schedule_act_7_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {schedule_act_7_lc__.state=cancelled}
        }
    }
    activity unnamed_act_8 {
        transition begin {
            domain: {(schedule_act_7_lc__.state=completed & process_ordersProcess_lc__.state=running & unnamed_act_8_lc__.state=not_started)}
            action: {(unnamed_act_8_lc__.state=running & unnamed_act_8_pick_sel__.activated=none)}
        }
        transition begin_receive_not_0 {
            domain: {(unnamed_act_8_lc__.state=running & unnamed_act_8_pick_sel__.activated=none)}
            action: {unnamed_act_8_pick_sel__.activated=receive_not_0}
        }
        transition complete_receive_not_0 {
            domain: {(unnamed_act_8_lc__.state=running & unnamed_act_9_lc__.state=completed & unnamed_act_8_pick_sel__.activated=receive_not_0)}
            action: {(unnamed_act_8_lc__.state=completed & unnamed_act_8_pick_sel__.activated=none)}
        }
        transition begin_onAlarm_0 {
            domain: {(unnamed_act_8_lc__.state=running & unnamed_act_8_pick_sel__.activated=none)}
            action: {unnamed_act_8_pick_sel__.activated=onAlarm_0}
        }
        transition complete_onAlarm_0 {
            domain: {(unnamed_act_8_lc__.state=running & urgent_req2_act_10_lc__.state=completed & unnamed_act_8_pick_sel__.activated=onAlarm_0)}
            action: {(unnamed_act_8_lc__.state=completed & unnamed_act_8_pick_sel__.activated=none)}
        }
        transition cancel {
            domain: {(unnamed_act_8_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {unnamed_act_8_lc__.state=cancelled}
        }
    }
    activity unnamed_act_9 {
        transition empty {
            domain: {(unnamed_act_8_pick_sel__.activated=receive_not_0 & process_ordersProcess_lc__.state=running & unnamed_act_9_lc__.state=not_started)}
            action: {unnamed_act_9_lc__.state=completed}
        }
    }
    activity urgent_req2_act_10 {
        transition throw1 {
            domain: {urgent_req2_act_10_lc__.state=running}
            action: {(urgent_req2_act_10_lc__.state=completed & process_ordersProcess_lc__.fault_handler=wait_catch_act_1)}
        }
        transition begin {
            domain: {(unnamed_act_8_pick_sel__.activated=onAlarm_0 & process_ordersProcess_lc__.state=running & urgent_req2_act_10_lc__.state=not_started)}
            action: {urgent_req2_act_10_lc__.state=running}
        }
        transition complete {
            domain: {urgent_req2_act_10_lc__.state=running}
            action: {urgent_req2_act_10_lc__.state=completed}
        }
        transition cancel {
            domain: {(urgent_req2_act_10_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling | process_ordersProcess_lc__.state=terminating))}
            action: {urgent_req2_act_10_lc__.state=cancelled}
        }
    }
    activity end_act_11 {
        transition fault_cancel_begin {
            domain: {end_act_11_lc__.fault!=none}
            action: {end_act_11_lc__.state=fault_cancelling}
        }
        transition fault_cancel_end {
            domain: {(end_act_11_lc__.state=fault_cancelling & (unnamed_act_12_lc__.state=completed | unnamed_act_12_lc__.state=not_started | unnamed_act_12_lc__.state=cancelled))}
            action: {end_act_11_lc__.state=faulted}
        }
        transition cancel_begin {
            domain: {(end_act_11_lc__.state=running & (process_ordersProcess_lc__.state=fault_cancelling | process_ordersProcess_lc__.state=cancelling))}
            action: {end_act_11_lc__.state=cancelling}
        }
        transition cancel_end {
            domain: {((end_act_11_lc__.state=cancelling | end_act_11_lc__.state=terminating) & (unnamed_act_12_lc__.state=completed | unnamed_act_12_lc__.state=not_started | unnamed_act_12_lc__.state=cancelled))}
            action: {end_act_11_lc__.state=cancelled}
        }
        transition terminate {
            domain: {process_ordersProcess_lc__.state=terminating}
            action: {end_act_11_lc__.state=terminating}
        }
        transition begin {
            domain: {(switch_act_4_lc__.state=completed & process_ordersProcess_lc__.state=running & end_act_11_lc__.state=not_started)}
            action: {end_act_11_lc__.state=running}
        }
        transition complete {
            domain: {(unnamed_act_12_lc__.state=completed & end_act_11_lc__.state=running)}
            action: {end_act_11_lc__.state=completed}
        }
    }
    activity unnamed_act_12 {
        transition reply {
            domain: {(end_act_11_lc__.state=running & end_act_11_lc__.state=running & unnamed_act_12_lc__.state=not_started)}
            action: {unnamed_act_12_lc__.state=completed}
        }
        transition cancel {
            domain: {(unnamed_act_12_lc__.state=running & (end_act_11_lc__.state=fault_cancelling | end_act_11_lc__.state=cancelling | end_act_11_lc__.state=terminating))}
            action: {unnamed_act_12_lc__.state=cancelled}
        }
    }
    goal noneRunning {
        (!process_ordersProcess_lc__.state=running & !wait_catch_act_1_lc__.state=running & !main_act_2_lc__.state=running & !init_act_3_lc__.state=running & !switch_act_4_lc__.state=running & !urgent_req_act_5_lc__.state=running & !unnamed_act_6_lc__.state=running & !schedule_act_7_lc__.state=running & !unnamed_act_8_lc__.state=running & !unnamed_act_9_lc__.state=running & !urgent_req2_act_10_lc__.state=running & !end_act_11_lc__.state=running & !unnamed_act_12_lc__.state=running)
    }
}