1_Plant_Requirements.cif

//Button automaton for the GUI.
plant def button():
    uncontrollable u_push, u_release;
    location released:
        initial; marked;
        edge u_push goto pushed;
    location pushed:
        edge u_release goto released;
end

//Initialize 20 push buttons, 4 stop buttons and the emergency stop.
button1 : button(); button2 : button(); button3 : button(); button4 : button(); button5 : button(); button6 : button();
button7 : button(); button8 : button(); button9 : button(); button10: button(); button11: button(); button12: button();
button13: button(); button14: button(); button15: button(); button16: button(); button17: button(); button18: button();
button19: button(); button20: button();
emergencystop: button(); stop1:    button(); stop2:    button(); stop3:    button(); stop4:    button();

//Specify the button combinations
alg bool cmd_stop         = emergencystop.pushed or stop1.pushed or stop2.pushed or stop4.pushed or stop4.pushed;
alg bool cmd_stop_culvert = emergencystop.pushed or stop3.pushed;
alg bool cmd_stop_pad     = emergencystop.pushed or stop4.pushed;
alg bool cmd_stop_D_gate  = emergencystop.pushed or stop1.pushed;
alg bool cmd_stop_U_gate  = emergencystop.pushed or stop2.pushed;

alg bool cmd_D_in_g     = button14.pushed and not button10.pushed and not button17.pushed;
alg bool cmd_D_in_rg    = button17.pushed and not button10.pushed;
alg bool cmd_D_in_r     = button10.pushed;
alg bool cmd_D_in_rr    = button18.pushed and not button10.pushed;
alg bool cmd_D_out_g    = button13.pushed and not button9.pushed;
alg bool cmd_D_out_r    = button9.pushed;
alg bool cmd_pad_o      = button1.pushed  and not button2.pushed;
alg bool cmd_pad_c      = button2.pushed;
alg bool cmd_D_gate_o   = button5.pushed  and not button6.pushed;
alg bool cmd_D_gate_c   = button6.pushed;

alg bool cmd_U_in_g     = button16.pushed and not button12.pushed and not button19.pushed;
alg bool cmd_U_in_rg    = button19.pushed and not button12.pushed;
alg bool cmd_U_in_r     = button12.pushed;
alg bool cmd_U_in_rr    = button20.pushed and not button12.pushed;
alg bool cmd_U_out_g    = button15.pushed and not button11.pushed;
alg bool cmd_U_out_r    = button11.pushed;
alg bool cmd_culvert_o  = button3.pushed  and not button4.pushed;
alg bool cmd_culvert_c  = button4.pushed;
alg bool cmd_U_gate_o   = button7.pushed  and not button8.pushed;
alg bool cmd_U_gate_c   = button8.pushed;

group def paddle():
    controllable c_open, c_close, c_stop;
    plant A:
        location rest:
            initial; marked;
            edge c_open  goto opening;
            edge c_close goto closing;
        location opening:
            edge c_close goto closing;
            edge c_stop  goto rest;
            edge S1.u_closed_off, S1.u_open_on;
            edge S2.u_closed_off, S2.u_open_on;
            edge S3.u_closed_off, S3.u_open_on;
        location closing:
            edge c_open  goto opening;
            edge c_stop  goto rest;
            edge S1.u_closed_on, S1.u_open_off;
            edge S2.u_closed_on, S2.u_open_off;
            edge S3.u_closed_on, S3.u_open_off;
    end
    plant def S():
        uncontrollable u_closed_on, u_closed_off, u_open_on, u_open_off;
        location closed:
            initial; marked;
            edge u_closed_off goto between;
        location between:
            edge u_closed_on  goto closed;
            edge u_open_on    goto open;
        location open:
            edge u_open_off   goto between;
    end
    S1 : S();
    S2 : S();
    S3 : S();

    requirement c_open  needs cmd_pad_o;
    requirement c_open  needs not S1.open   or not S2.open   or not S3.open;

    requirement c_close needs cmd_pad_c;
    requirement c_close needs not S1.closed or not S2.closed or not S3.closed;

    requirement c_stop  needs cmd_stop_pad or
                              (S1.closed and S2.closed and S3.closed and A.closing) or
                              (S1.open   and S2.open   and S3.open   and A.opening);

    requirement cmd_stop_pad disables {c_open, c_close};
end

//Initialize two sets of paddles
pad_N : paddle(); pad_S : paddle();

group def culvert():
    controllable c_enable, c_disable;
    uncontrollable u_on, u_off;
    plant A:
        location closed:
            initial; marked;
            edge c_enable  goto open;
            edge u_off;
        location open:
            edge c_disable goto closed;
            edge u_on;
    end
    plant S:
        location noflow:
            initial; marked;
            edge u_on  goto flow;
        location flow:
            edge u_off goto noflow;
    end
    requirement c_enable  needs cmd_culvert_o;
    requirement c_disable needs cmd_culvert_c or cmd_stop_culvert;

    requirement cmd_stop_culvert disables c_enable;
end

//Initialize two culverts.
culvert_N : culvert(); culvert_S : culvert();

group def gate(alg bool cmd_gate_o, cmd_gate_c, cmd_stop_gate):
    controllable c_high_on, c_high_off, c_low_on, c_low_off, c_open, c_close, c_stop,
                 c_fc_off, c_fc_on, c_sc_on, c_sc_off,
                 c_fo_off, c_fo_on, c_so_on, c_so_off;
    uncontrollable u_s1_on, u_s1_off, u_s2_on, u_s2_off, u_s3_on, u_s3_off,
                   u_s4_on, u_s4_off, u_s5_on, u_s5_off, u_s6_on, u_s6_off;
    plant S:
        location closed:
            initial; marked;
            edge u_s1_on  goto bclosed;
        location bclosed:
            edge u_s1_off goto closed;
            edge u_s2_on  goto fclosed;
        location fclosed:
            edge u_s2_off goto bclosed;
            edge u_s3_on  goto middle;
        location middle:
            edge u_s3_off goto fclosed;
            edge u_s4_off goto fopen;
        location fopen:
            edge u_s4_on  goto middle;
            edge u_s5_off goto bopen;
        location bopen:
            edge u_s5_on  goto fopen;
            edge u_s6_off goto open;
        location open:
            edge u_s6_on  goto bopen;
    end
    plant Dir:
        location off:
            marked;
            initial;
            edge c_open   goto opening;
            edge c_close  goto closing;
        location opening:
            edge c_close  goto closing;
            edge c_stop   goto off;
            edge u_s1_on, u_s2_on, u_s3_on, u_s4_off, u_s5_off, u_s6_off;
        location closing:
            edge c_open    goto opening;
            edge c_stop    goto off;
            edge u_s6_on, u_s5_on, u_s4_on, u_s3_off, u_s2_off, u_s1_off;
    end
    plant Spe:
        location off:
            initial; marked;
            edge c_fc_on  goto fast_c;
            edge c_sc_on  goto slow_c;
            edge c_fo_on  goto fast_o;
            edge c_so_on  goto slow_o;
        location fast_c:
            edge c_fc_off goto off;
        location slow_c:
            edge c_sc_off goto off;
        location fast_o:
            edge c_fo_off goto off;
        location slow_o:
            edge c_so_off goto off;
    end
    plant Pre:
        location off:
            initial;
            marked;
            edge c_high_on  goto high;
            edge c_low_on   goto low;
        location high:
            edge c_high_off goto off;
        location low:
            edge c_low_off  goto off;
    end

    requirement c_open  needs cmd_gate_o and not S.open;
    requirement c_close needs cmd_gate_c and not S.closed;
    requirement c_stop  needs cmd_stop_gate or (S.closed and Dir.closing) or (S.open and Dir.opening);
    requirement cmd_stop_gate disables {c_open, c_close};
end

gate_D_N : gate(cmd_D_gate_o, cmd_D_gate_c, cmd_stop_D_gate); gate_D_S : gate(cmd_D_gate_o, cmd_D_gate_c, cmd_stop_D_gate);
gate_U_N : gate(cmd_U_gate_o, cmd_U_gate_c, cmd_stop_U_gate); gate_U_S : gate(cmd_U_gate_o, cmd_U_gate_c, cmd_stop_U_gate);

//Sensor for equal water over the gate at D, initial state on.
plant s_equal_D:
    uncontrollable u_equal_on, u_equal_off;
    location off:
        marked;
        edge u_equal_on  goto on;
    location on:
        initial; marked;
        edge u_equal_off goto off;
end

//Sensor for equal water over the gate at U, initial state off.
plant s_equal_U:
    uncontrollable u_equal_on, u_equal_off;
    location off:
        initial; marked;
        edge u_equal_on  goto on;
    location on:
        marked;
        edge u_equal_off goto off;
end

group def outgoing(alg bool cmd_out_r, cmd_out_g):
    controllable c_red, c_green;
    uncontrollable u_r_on, u_r_off, u_g_on, u_g_off;
    plant S:
        location off:
            edge u_r_on  goto red;
            edge u_g_on  goto green;
        location red:
            initial; marked;
            edge u_r_off goto off;
            edge u_g_on  goto redgreen;
        location green:
            edge u_r_on  goto redgreen;
            edge u_g_off goto off;
        location redgreen:
            edge u_r_off goto green;
            edge u_g_off goto red;
    end
    plant A:
        location red:
            initial; marked;
            edge c_green goto green;
            edge u_r_on, u_g_off;
        location green:
            edge c_red   goto red;
            edge u_g_on, u_r_off;
    end
    requirement c_red   needs cmd_out_r or cmd_stop;
    requirement c_green needs cmd_out_g;

    requirement cmd_stop disables c_green;
end

//Initialize four outgoing traffic lights
out_D_N : outgoing(cmd_D_out_r, cmd_D_out_g); out_D_S : outgoing(cmd_D_out_r, cmd_D_out_g);
out_U_N : outgoing(cmd_U_out_r, cmd_U_out_g); out_U_S : outgoing(cmd_U_out_r, cmd_U_out_g);

group def incoming(alg bool cmd_in_red, cmd_in_green, cmd_in_rg, cmd_in_redred):
    controllable c_red, c_green, c_redgreen, c_redred;
    uncontrollable u_r_on, u_r_off, u_g_on, u_g_off, u_s_on, u_s_off;
    plant S:
        location off:
            edge u_r_on  goto red;
            edge u_g_on  goto green;
            edge u_s_on  goto lowred;
        location red:
            initial; marked;
            edge u_r_off goto off;
            edge u_g_on  goto redgreen;
            edge u_s_on  goto redred;
        location green:
            edge u_r_on  goto redgreen;
            edge u_g_off goto off;
            edge u_s_on  goto greenred;
        location lowred:
            edge u_r_on  goto redred;
            edge u_g_on  goto greenred;
            edge u_s_off goto off;
        location redgreen:
            edge u_r_off goto green;
            edge u_g_off goto red;
            edge u_s_on  goto redgreenred;
        location redred:
            edge u_r_off goto lowred;
            edge u_g_on  goto redgreenred;
            edge u_s_off goto red;
        location greenred:
            edge u_r_on  goto redgreenred;
            edge u_g_off goto lowred;
            edge u_s_off goto green;
        location redgreenred:
            edge u_r_off goto greenred;
            edge u_g_off goto redred;
            edge u_s_off goto redgreen;
    end
    plant A:
        location red:
        initial; marked;
            edge c_redgreen goto redgreen;
            edge c_redred   goto redred;
            edge u_r_on, u_g_off, u_s_off;
        location green:
            edge c_red      goto red;
            edge c_redgreen goto redgreen;
            edge u_r_off, u_g_on, u_s_off;
        location redred:
            edge c_red   goto red;
            edge u_r_on, u_g_off, u_s_on;
        location redgreen:
            edge c_green goto green;
            edge c_red   goto red;
            edge u_r_on, u_g_on, u_s_off;
    end
    requirement c_red      needs cmd_in_red or cmd_stop;
    requirement c_green    needs cmd_in_green;
    requirement c_redgreen needs cmd_in_rg;
    requirement c_redred   needs cmd_in_redred;
    requirement cmd_stop disables {c_green, c_redgreen, c_redred};
end

//Initialize four incoming traffic lights
in_D_N : incoming(cmd_D_in_r, cmd_D_in_g, cmd_D_in_rg, cmd_D_in_rr);
in_D_S : incoming(cmd_D_in_r, cmd_D_in_g, cmd_D_in_rg, cmd_D_in_rr);
in_U_N : incoming(cmd_U_in_r, cmd_U_in_g, cmd_U_in_rg, cmd_U_in_rr);
in_U_S : incoming(cmd_U_in_r, cmd_U_in_g, cmd_U_in_rg, cmd_U_in_rr);

group def gate_requirements(controllable c_speed_sc_on, c_speed_sc_off, c_speed_fc_on, c_speed_fc_off;
                            controllable c_speed_so_on, c_speed_so_off, c_speed_fo_on, c_speed_fo_off;
                            controllable c_high_on, c_high_off;
                            controllable c_low_on,  c_low_off;
                            alg bool s_closed, s_bclosed, s_frclosed, s_middle, s_fropen, s_bopen, s_open, closing, opening):

    requirement c_speed_fc_on   needs not(s_bclosed or s_closed) and closing;
    requirement c_speed_fc_off  needs s_bclosed or s_closed;

    requirement c_speed_sc_on   needs s_bclosed and closing;
    requirement c_speed_sc_off  needs not s_bclosed;

    requirement c_speed_fo_on   needs not (s_bopen or s_open) and opening;
    requirement c_speed_fo_off  needs s_bopen or s_open;

    requirement c_speed_so_on   needs s_bopen and opening;
    requirement c_speed_so_off  needs not s_bopen;

    requirement c_high_on  needs      (s_open   or s_bopen   or s_fropen   or s_middle) and closing or
                                      (s_closed or s_bclosed or s_frclosed or s_middle) and opening;
    requirement c_high_off needs not ((s_open   or s_bopen   or s_fropen   or s_middle) and closing or
                                      (s_closed or s_bclosed or s_frclosed or s_middle) and opening);

    requirement c_low_on   needs      (s_frclosed or s_bclosed) and closing or
                                      (s_fropen   or s_bopen)   and opening;
    requirement c_low_off  needs not ((s_frclosed or s_bclosed) and closing or
                                      (s_fropen   or s_bopen)   and opening);
end

req_gate_D_S :gate_requirements(gate_D_S.c_sc_on,   gate_D_S.c_sc_off, gate_D_S.c_fc_on, gate_D_S.c_fc_off,
                                gate_D_S.c_so_on,   gate_D_S.c_so_off, gate_D_S.c_fo_on, gate_D_S.c_fo_off,
                                gate_D_S.c_high_on, gate_D_S.c_high_off,
                                gate_D_S.c_low_on,  gate_D_S.c_low_off,
                                gate_D_S.S.closed,  gate_D_S.S.bclosed, gate_D_S.S.fclosed, gate_D_S.S.middle,
                                gate_D_S.S.fopen,   gate_D_S.S.bopen,   gate_D_S.S.open,
                                gate_D_S.Dir.closing, gate_D_S.Dir.opening);

req_gate_D_N :gate_requirements(gate_D_N.c_sc_on,   gate_D_N.c_sc_off, gate_D_N.c_fc_on, gate_D_N.c_fc_off,
                                gate_D_N.c_so_on,   gate_D_N.c_so_off, gate_D_N.c_fo_on, gate_D_N.c_fo_off,
                                gate_D_N.c_high_on, gate_D_N.c_high_off,
                                gate_D_N.c_low_on,  gate_D_N.c_low_off,
                                gate_D_N.S.closed,  gate_D_N.S.bclosed, gate_D_N.S.fclosed, gate_D_N.S.middle,
                                gate_D_N.S.fopen,   gate_D_N.S.bopen,   gate_D_N.S.open,
                                gate_D_N.Dir.closing, gate_D_N.Dir.opening);

req_gate_U_S :gate_requirements(gate_U_S.c_sc_on,   gate_U_S.c_sc_off, gate_U_S.c_fc_on, gate_U_S.c_fc_off,
                                gate_U_S.c_so_on,   gate_U_S.c_so_off, gate_U_S.c_fo_on, gate_U_S.c_fo_off,
                                gate_U_S.c_high_on, gate_U_S.c_high_off,
                                gate_U_S.c_low_on,  gate_U_S.c_low_off,
                                gate_U_S.S.closed,  gate_U_S.S.bclosed, gate_U_S.S.fclosed, gate_U_S.S.middle,
                                gate_U_S.S.fopen,   gate_U_S.S.bopen,   gate_U_S.S.open,
                                gate_U_S.Dir.closing, gate_U_S.Dir.opening);

req_gate_U_N :gate_requirements(gate_U_N.c_sc_on,   gate_U_N.c_sc_off, gate_U_N.c_fc_on, gate_U_N.c_fc_off,
                                gate_U_N.c_so_on,   gate_U_N.c_so_off, gate_U_N.c_fo_on, gate_U_N.c_fo_off,
                                gate_U_N.c_high_on, gate_U_N.c_high_off,
                                gate_U_N.c_low_on,  gate_U_N.c_low_off,
                                gate_U_N.S.closed,  gate_U_N.S.bclosed, gate_U_N.S.fclosed, gate_U_N.S.middle,
                                gate_U_N.S.fopen,   gate_U_N.S.bopen,   gate_U_N.S.open,
                                gate_U_N.Dir.closing, gate_U_N.Dir.opening);

//Emergency stop requirements
//If the emergency stop is active, no actuators may enable
requirement emergencystop.pushed disables
    {in_D_N.c_green,    in_D_S.c_green,    in_U_N.c_green,    in_U_S.c_green,
     in_D_N.c_redgreen, in_D_S.c_redgreen, in_U_N.c_redgreen, in_U_S.c_redgreen,
     out_D_N.c_green,   out_D_S.c_green,   out_U_N.c_green,   out_U_S.c_green,
     pad_N.c_open,      pad_S.c_open,      pad_N.c_close,     pad_S.c_close,
     culvert_N.c_enable, culvert_S.c_enable,
     gate_D_N.c_open,    gate_D_S.c_open,  gate_U_N.c_open,  gate_U_S.c_open,
     gate_D_N.c_close,   gate_D_S.c_close, gate_U_N.c_close, gate_U_S.c_close} ;

//SF: culvert/paddle - culvert/paddle
requirement culvert_N.S.flow or culvert_N.A.open or
            culvert_S.S.flow or culvert_S.A.open
            disables {pad_N.c_open, pad_S.c_open};

requirement not pad_N.S1.closed or not pad_N.S2.closed or
            not pad_N.S3.closed or     pad_N.A.opening or
            not pad_S.S1.closed or not pad_S.S2.closed or
            not pad_S.S3.closed or     pad_S.A.opening
            disables {culvert_N.c_enable, culvert_S.c_enable};

//SF: gate - culvert/paddle
requirement not gate_U_N.S.closed or gate_U_N.Dir.opening or
            not gate_U_S.S.closed or gate_U_S.Dir.opening
            disables {pad_N.c_open, pad_S.c_open};

requirement not gate_D_N.S.closed or gate_D_N.Dir.opening or
            not gate_D_S.S.closed or gate_D_S.Dir.opening
            disables {culvert_N.c_enable, culvert_S.c_enable};

//SF: equal water - gate
requirement s_equal_D.off //Sensor indicates no equal water
            disables {gate_D_N.c_open, gate_D_S.c_open};

requirement s_equal_U.off
            disables {gate_U_N.c_open, gate_U_S.c_open};

//SF: culvert/paddle - gate
requirement culvert_N.S.flow or culvert_N.A.open or
            culvert_S.S.flow or culvert_S.A.open
            disables {gate_D_N.c_open, gate_D_S.c_open};

requirement not pad_N.S1.closed or not pad_N.S2.closed or
            not pad_N.S3.closed or     pad_N.A.opening or
            not pad_S.S1.closed or not pad_S.S2.closed or
            not pad_S.S3.closed or     pad_S.A.opening
            disables {gate_U_N.c_open, gate_U_S.c_open};

//SF: gate - gate
requirement not gate_U_N.S.closed or gate_U_N.Dir.opening or
            not gate_U_S.S.closed or gate_U_S.Dir.opening
            disables {gate_D_N.c_open, gate_D_S.c_open};

requirement not gate_D_N.S.closed or gate_D_N.Dir.opening or
            not gate_D_S.S.closed or gate_D_S.Dir.opening
            disables {gate_U_N.c_open, gate_U_S.c_open};

//SF: leaving aspect - entering aspect
requirement out_D_N.S.green or out_D_N.A.green or
            out_D_S.S.green or out_D_S.A.green
            disables {in_D_N.c_green, in_D_S.c_green};

requirement out_U_N.S.green or out_U_N.A.green or
            out_U_S.S.green or out_U_S.A.green
            disables {in_U_N.c_green, in_U_S.c_green};

//SF: entering aspect - leaving aspect
requirement in_D_N.S.green or in_D_N.A.green or
            in_D_S.S.green or in_D_S.A.green
            disables {out_D_N.c_green, out_D_S.c_green};

requirement in_U_N.S.green or in_U_N.A.green or
            in_U_S.S.green or in_U_S.A.green
            disables {out_U_N.c_green, out_U_S.c_green};

//SF: gate - entering aspect
requirement not gate_D_N.S.open or gate_D_N.Dir.closing or
            not gate_D_S.S.open or gate_D_S.Dir.closing
            disables {in_D_N.c_green, in_D_S.c_green};

requirement not gate_U_N.S.open or gate_U_N.Dir.closing or
            not gate_U_S.S.open or gate_U_S.Dir.closing
            disables {in_U_N.c_green, in_U_S.c_green};

//SF: entering aspect - gate.
requirement not (in_D_N.S.red or in_D_N.S.redred) or
            not (in_D_N.A.red or in_D_N.A.redred) or
            not (in_D_S.S.red or in_D_S.S.redred) or
            not (in_D_S.A.red or in_D_S.A.redred)
            disables {gate_D_N.c_close, gate_D_S.c_close};

requirement not (in_U_N.S.red or in_U_N.S.redred) or
            not (in_U_N.A.red or in_U_N.A.redred) or
            not (in_U_S.S.red or in_U_S.S.redred) or
            not (in_U_S.A.red or in_U_S.A.redred)
            disables {gate_U_N.c_close, gate_U_S.c_close};

//SF: leaving aspect - gate.
requirement not out_D_N.S.red or not out_D_N.A.red or
            not out_D_S.S.red or not out_D_S.A.red
            disables {gate_D_N.c_close, gate_D_S.c_close};

requirement not out_U_N.S.red or not out_U_N.A.red or
            not out_U_S.S.red or not out_U_S.A.red
            disables {gate_U_N.c_close, gate_U_N.c_close};


//SF: gate - leaving aspect
requirement not gate_D_N.S.open or gate_D_N.Dir.closing or
            not gate_D_S.S.open or gate_D_S.Dir.closing
            disables {out_D_N.c_green, out_D_S.c_green};

requirement not gate_U_N.S.open or gate_U_N.Dir.closing or
            not gate_U_S.S.open or gate_U_S.Dir.closing
            disables {out_U_N.c_green, out_U_S.c_green};