process oliveProcess
{
    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_handler: enum (none, prepare_neg_response_act_1);
    }
    enttype BPEL_lnk {
        fired: boolean;
    }
    /* message {http://www.it.uc3m.es/jaf/ns/OliveOilService}OliveOilRequest */
    enttype OliveOilRequest {
        request__quantity: integer;
        request__maxPrice: integer;
        request__deadline: integer;
        request__customerId: enum (_abstract__none, c102000);
    }
    /* message {http://www.it.uc3m.es/jaf/ns/OliveOilService}OliveOilResponse */
    enttype OliveOilResponse {
        totalPrice: integer;
        ordered: boolean;
        waitingDays: integer;
        price: integer;
        request__quantity: integer;
        request__maxPrice: integer;
        request__deadline: integer;
        request__customerId: enum (_abstract__none, c102000);
    }
    /* message {http://www.it.uc3m.es/jaf/ns/OliveOilService}OilPriceResponse */
    enttype OilPriceResponse {
        price: integer;
    }
    /* message {http://www.it.uc3m.es/jaf/ns/OliveOilService}OilOrder */
    enttype OilOrder {
        oilType: enum (olive, soja, sunflower);
        quantity: integer;
        customerId: enum (_abstract__none, c102000);
    }
    /* message {http://www.it.uc3m.es/jaf/ns/OliveOilService}OilConfirmation */
    enttype OilConfirmation {
        accepted: boolean;
    }
    entity request: OliveOilRequest;
    entity response: OliveOilResponse;
    entity oPrice: OilPriceResponse;
    entity oOrder: OilOrder;
    entity oOrderConfirm: OilConfirmation;
    entity process_oliveProcess_lc__: BPEL_lc;
    entity prepare_neg_response_act_1_lc__: BPEL_lc_basic;
    entity main_act_2_lc__: BPEL_lc_basic;
    entity unnamed_act_3_lc__: BPEL_lc_basic;
    entity initializations_act_4_lc__: BPEL_lc_basic;
    entity askPrice1_act_5_lc__: BPEL_lc;
    entity wait_act_6_lc__: BPEL_lc_basic;
    entity loop_act_7_lc__: BPEL_lc_basic;
    entity white_a_day_act_8_lc__: BPEL_lc_basic;
    entity incdays_act_9_lc__: BPEL_lc_basic;
    entity askPrice2_act_10_lc__: BPEL_lc;
    entity unnamed_act_11_lc__: BPEL_lc;
    entity prepare_response_act_12_lc__: BPEL_lc_basic;
    entity unnamed_act_13_lc__: BPEL_lc_basic;
    activity process_oliveProcess_act__ {
        transition catchCompletion {
            domain: {(process_oliveProcess_lc__.state=faulted & prepare_neg_response_act_1_lc__.state=completed)}
            action: {process_oliveProcess_lc__.state=cancelled}
        }
        transition fault_cancel_begin {
            domain: {(process_oliveProcess_lc__.fault_handler!=none & process_oliveProcess_lc__.state=running)}
            action: {process_oliveProcess_lc__.state=fault_cancelling}
        }
        transition fault_cancel_end {
            domain: {(process_oliveProcess_lc__.state=fault_cancelling & (unnamed_act_3_lc__.state=completed | unnamed_act_3_lc__.state=not_started | unnamed_act_3_lc__.state=cancelled) & (initializations_act_4_lc__.state=completed | initializations_act_4_lc__.state=not_started) & (askPrice1_act_5_lc__.state=completed | askPrice1_act_5_lc__.state=not_started | askPrice1_act_5_lc__.state=cancelled) & (white_a_day_act_8_lc__.state=completed | white_a_day_act_8_lc__.state=not_started | white_a_day_act_8_lc__.state=cancelled) & (incdays_act_9_lc__.state=completed | incdays_act_9_lc__.state=not_started) & (askPrice2_act_10_lc__.state=completed | askPrice2_act_10_lc__.state=not_started | askPrice2_act_10_lc__.state=cancelled) & (loop_act_7_lc__.state=completed | loop_act_7_lc__.state=not_started | loop_act_7_lc__.state=cancelled) & (wait_act_6_lc__.state=completed | wait_act_6_lc__.state=not_started | wait_act_6_lc__.state=cancelled) & (unnamed_act_11_lc__.state=completed | unnamed_act_11_lc__.state=not_started | unnamed_act_11_lc__.state=cancelled) & (prepare_response_act_12_lc__.state=completed | prepare_response_act_12_lc__.state=not_started) & (unnamed_act_13_lc__.state=completed | unnamed_act_13_lc__.state=not_started | unnamed_act_13_lc__.state=cancelled) & (main_act_2_lc__.state=completed | main_act_2_lc__.state=not_started | main_act_2_lc__.state=cancelled))}
            action: {process_oliveProcess_lc__.state=faulted}
        }
        transition terminate_end {
            domain: {(process_oliveProcess_lc__.state=terminating & (unnamed_act_3_lc__.state=completed | unnamed_act_3_lc__.state=not_started | unnamed_act_3_lc__.state=cancelled) & (initializations_act_4_lc__.state=completed | initializations_act_4_lc__.state=not_started) & (askPrice1_act_5_lc__.state=completed | askPrice1_act_5_lc__.state=not_started | askPrice1_act_5_lc__.state=cancelled) & (white_a_day_act_8_lc__.state=completed | white_a_day_act_8_lc__.state=not_started | white_a_day_act_8_lc__.state=cancelled) & (incdays_act_9_lc__.state=completed | incdays_act_9_lc__.state=not_started) & (askPrice2_act_10_lc__.state=completed | askPrice2_act_10_lc__.state=not_started | askPrice2_act_10_lc__.state=cancelled) & (loop_act_7_lc__.state=completed | loop_act_7_lc__.state=not_started | loop_act_7_lc__.state=cancelled) & (wait_act_6_lc__.state=completed | wait_act_6_lc__.state=not_started | wait_act_6_lc__.state=cancelled) & (unnamed_act_11_lc__.state=completed | unnamed_act_11_lc__.state=not_started | unnamed_act_11_lc__.state=cancelled) & (prepare_response_act_12_lc__.state=completed | prepare_response_act_12_lc__.state=not_started) & (unnamed_act_13_lc__.state=completed | unnamed_act_13_lc__.state=not_started | unnamed_act_13_lc__.state=cancelled) & (main_act_2_lc__.state=completed | main_act_2_lc__.state=not_started | main_act_2_lc__.state=cancelled))}
            action: {process_oliveProcess_lc__.state=cancelled}
        }
        transition complete {
            domain: {(main_act_2_lc__.state=completed & process_oliveProcess_lc__.state=running)}
            action: {process_oliveProcess_lc__.state=completed}
        }
    }
    /* catch all activity oliveProcess */
    activity prepare_neg_response_act_1 {
        transition assign {
            domain: {(process_oliveProcess_lc__.state=faulted & prepare_neg_response_act_1_lc__.state=not_started & process_oliveProcess_lc__.fault_handler=prepare_neg_response_act_1)}
            action: {(prepare_neg_response_act_1_lc__.state=completed & (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)}
        }
    }
    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 & unnamed_act_13_lc__.state=completed)}
            action: {main_act_2_lc__.state=completed}
        }
        transition cancel {
            domain: {(main_act_2_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {main_act_2_lc__.state=cancelled}
        }
    }
    activity unnamed_act_3 {
        transition begin_0 {
            domain: {(main_act_2_lc__.state=running & unnamed_act_3_lc__.state=not_started)}
            action: {(unnamed_act_3_lc__.state=running & (request.request__customerId=c102000 & request.request__maxPrice=3 & request.request__deadline=5 & request.request__quantity=1))}
        }
        transition complete {
            domain: {unnamed_act_3_lc__.state=running}
            action: {(unnamed_act_3_lc__.state=completed & process_oliveProcess_lc__.state=running)}
        }
        transition cancel {
            domain: {(unnamed_act_3_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {unnamed_act_3_lc__.state=cancelled}
        }
    }
    activity initializations_act_4 {
        transition assign {
            domain: {(unnamed_act_3_lc__.state=completed & process_oliveProcess_lc__.state=running & initializations_act_4_lc__.state=not_started)}
            action: {(initializations_act_4_lc__.state=completed & response.waitingDays=0 & oOrder.quantity=request.request__quantity & oOrder.customerId=request.request__customerId & oOrder.oilType=olive)}
        }
    }
    activity askPrice1_act_5 {
        transition throw1 {
            domain: {askPrice1_act_5_lc__.state=running}
            action: {(askPrice1_act_5_lc__.state=completed & process_oliveProcess_lc__.fault_handler=prepare_neg_response_act_1)}
        }
        transition begin {
            domain: {(initializations_act_4_lc__.state=completed & process_oliveProcess_lc__.state=running & askPrice1_act_5_lc__.state=not_started)}
            action: {askPrice1_act_5_lc__.state=running}
        }
        transition complete_0 {
            domain: {askPrice1_act_5_lc__.state=running}
            action: {(askPrice1_act_5_lc__.state=completed & oPrice.price=1)}
        }
        transition complete_1 {
            domain: {askPrice1_act_5_lc__.state=running}
            action: {(askPrice1_act_5_lc__.state=completed & oPrice.price=2)}
        }
        transition complete_2 {
            domain: {askPrice1_act_5_lc__.state=running}
            action: {(askPrice1_act_5_lc__.state=completed & oPrice.price=4)}
        }
        transition complete_3 {
            domain: {askPrice1_act_5_lc__.state=running}
            action: {(askPrice1_act_5_lc__.state=completed & oPrice.price=5)}
        }
        transition complete_4 {
            domain: {askPrice1_act_5_lc__.state=running}
            action: {(askPrice1_act_5_lc__.state=completed & oPrice.price=6)}
        }
        transition cancel {
            domain: {(askPrice1_act_5_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {askPrice1_act_5_lc__.state=cancelled}
        }
    }
    activity wait_act_6 {
        transition begin {
            domain: {(askPrice1_act_5_lc__.state=completed & process_oliveProcess_lc__.state=running & wait_act_6_lc__.state=not_started)}
            action: {(wait_act_6_lc__.state=running & white_a_day_act_8_lc__.state=not_started & incdays_act_9_lc__.state=not_started & askPrice2_act_10_lc__.state=not_started & loop_act_7_lc__.state=not_started)}
        }
        transition continue {
            domain: {(((response.waitingDays < request.request__deadline) & (oPrice.price > request.request__maxPrice)) & wait_act_6_lc__.state=running & loop_act_7_lc__.state=completed)}
            action: {(white_a_day_act_8_lc__.state=not_started & incdays_act_9_lc__.state=not_started & askPrice2_act_10_lc__.state=not_started & loop_act_7_lc__.state=not_started)}
        }
        transition complete {
            domain: {(loop_act_7_lc__.state=completed & !((response.waitingDays < request.request__deadline) & (oPrice.price > request.request__maxPrice)) & wait_act_6_lc__.state=running)}
            action: {wait_act_6_lc__.state=completed}
        }
        transition cancel {
            domain: {(wait_act_6_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {wait_act_6_lc__.state=cancelled}
        }
    }
    activity loop_act_7 {
        transition begin {
            domain: {(wait_act_6_lc__.state=running & process_oliveProcess_lc__.state=running & loop_act_7_lc__.state=not_started)}
            action: {loop_act_7_lc__.state=running}
        }
        transition complete {
            domain: {(loop_act_7_lc__.state=running & askPrice2_act_10_lc__.state=completed)}
            action: {loop_act_7_lc__.state=completed}
        }
        transition cancel {
            domain: {(loop_act_7_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {loop_act_7_lc__.state=cancelled}
        }
    }
    activity white_a_day_act_8 {
        transition begin {
            domain: {(loop_act_7_lc__.state=running & process_oliveProcess_lc__.state=running & white_a_day_act_8_lc__.state=not_started)}
            action: {white_a_day_act_8_lc__.state=running}
        }
        transition complete {
            domain: {white_a_day_act_8_lc__.state=running}
            action: {white_a_day_act_8_lc__.state=completed}
        }
        transition cancel {
            domain: {(white_a_day_act_8_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {white_a_day_act_8_lc__.state=cancelled}
        }
    }
    activity incdays_act_9 {
        transition assign {
            domain: {(white_a_day_act_8_lc__.state=completed & process_oliveProcess_lc__.state=running & incdays_act_9_lc__.state=not_started)}
            action: {(incdays_act_9_lc__.state=completed & response.waitingDays=(response.waitingDays+1))}
        }
    }
    activity askPrice2_act_10 {
        transition throw1 {
            domain: {askPrice2_act_10_lc__.state=running}
            action: {(askPrice2_act_10_lc__.state=completed & process_oliveProcess_lc__.fault_handler=prepare_neg_response_act_1)}
        }
        transition begin {
            domain: {(incdays_act_9_lc__.state=completed & process_oliveProcess_lc__.state=running & askPrice2_act_10_lc__.state=not_started)}
            action: {askPrice2_act_10_lc__.state=running}
        }
        transition complete_0 {
            domain: {askPrice2_act_10_lc__.state=running}
            action: {(askPrice2_act_10_lc__.state=completed & oPrice.price=1)}
        }
        transition complete_1 {
            domain: {askPrice2_act_10_lc__.state=running}
            action: {(askPrice2_act_10_lc__.state=completed & oPrice.price=2)}
        }
        transition complete_2 {
            domain: {askPrice2_act_10_lc__.state=running}
            action: {(askPrice2_act_10_lc__.state=completed & oPrice.price=4)}
        }
        transition complete_3 {
            domain: {askPrice2_act_10_lc__.state=running}
            action: {(askPrice2_act_10_lc__.state=completed & oPrice.price=5)}
        }
        transition complete_4 {
            domain: {askPrice2_act_10_lc__.state=running}
            action: {(askPrice2_act_10_lc__.state=completed & oPrice.price=6)}
        }
        transition cancel {
            domain: {(askPrice2_act_10_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {askPrice2_act_10_lc__.state=cancelled}
        }
    }
    activity unnamed_act_11 {
        transition throw1 {
            domain: {unnamed_act_11_lc__.state=running}
            action: {(unnamed_act_11_lc__.state=completed & process_oliveProcess_lc__.fault_handler=prepare_neg_response_act_1)}
        }
        transition begin {
            domain: {(wait_act_6_lc__.state=completed & process_oliveProcess_lc__.state=running & unnamed_act_11_lc__.state=not_started)}
            action: {unnamed_act_11_lc__.state=running}
        }
        transition complete_0 {
            domain: {unnamed_act_11_lc__.state=running}
            action: {(unnamed_act_11_lc__.state=completed & oOrderConfirm.accepted)}
        }
        transition complete_1 {
            domain: {unnamed_act_11_lc__.state=running}
            action: {(unnamed_act_11_lc__.state=completed & !oOrderConfirm.accepted)}
        }
        transition cancel {
            domain: {(unnamed_act_11_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {unnamed_act_11_lc__.state=cancelled}
        }
    }
    activity prepare_response_act_12 {
        transition assign {
            domain: {(unnamed_act_11_lc__.state=completed & process_oliveProcess_lc__.state=running & prepare_response_act_12_lc__.state=not_started)}
            action: {(prepare_response_act_12_lc__.state=completed & (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))}
        }
    }
    activity unnamed_act_13 {
        transition reply {
            domain: {(prepare_response_act_12_lc__.state=completed & process_oliveProcess_lc__.state=running & unnamed_act_13_lc__.state=not_started)}
            action: {unnamed_act_13_lc__.state=completed}
        }
        transition cancel {
            domain: {(unnamed_act_13_lc__.state=running & (process_oliveProcess_lc__.state=fault_cancelling | process_oliveProcess_lc__.state=cancelling | process_oliveProcess_lc__.state=terminating))}
            action: {unnamed_act_13_lc__.state=cancelled}
        }
    }
    invariant invariant_0 {
        (!process_oliveProcess_lc__.state=running | (response.waitingDays <= request.request__deadline))
    }
    invariant invariant_2 {
        (!process_oliveProcess_lc__.state=running | ((response.price <= request.request__maxPrice) | response.waitingDays=request.request__deadline))
    }
    goal goal_1 {
        askPrice1_act_5_lc__.state=completed
    }
    goal noneRunning {
        (!process_oliveProcess_lc__.state=running & !prepare_neg_response_act_1_lc__.state=running & !main_act_2_lc__.state=running & !unnamed_act_3_lc__.state=running & !initializations_act_4_lc__.state=running & !askPrice1_act_5_lc__.state=running & !wait_act_6_lc__.state=running & !loop_act_7_lc__.state=running & !white_a_day_act_8_lc__.state=running & !incdays_act_9_lc__.state=running & !askPrice2_act_10_lc__.state=running & !unnamed_act_11_lc__.state=running & !prepare_response_act_12_lc__.state=running & !unnamed_act_13_lc__.state=running)
    }
}