Skip to content

GitLab

Commit 601882ff authored by Ferdie Reijnen's avatar Ferdie Reijnen
Browse files

#364 Improved waterway lock benchmark model.

parent fd964646
Pipeline #4020 passed with stage
in 0 seconds
Hide whitespace changes
Inline Side-by-side
cif/org.eclipse.escet.cif.examples/benchmarks/waterway_lock/synthesize.tooldef
View file @ 601882ff
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2018, 2022 Contributors to the Eclipse Foundation
// Copyright (c) 2017, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......
cif/org.eclipse.escet.cif.examples/benchmarks/waterway_lock/waterway_lock.cif
View file @ 601882ff
//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2022 Contributors to the Eclipse Foundation
// Copyright (c) 2017, 2022 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
......@@ -11,8 +11,8 @@
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////
// Button automaton for the GUI.
plant def button():
// Button component for the GUI.
plant def Button():
uncontrollable u_push, u_release;
location released:
initial; marked;
......@@ -22,13 +22,14 @@ plant def button():
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
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();
stop1: Button(); stop2: Button(); stop3: Button(); stop4: Button();
emergencystop: Button();
// Specify the button combinations.
alg bool cmd_stop = emergencystop.pushed or stop1.pushed or stop2.pushed or stop3.pushed or stop4.pushed;
alg bool cmd_stop_culvert = emergencystop.pushed or stop3.pushed;
alg bool cmd_stop_pad = emergencystop.pushed or stop4.pushed;
......@@ -57,8 +58,11 @@ 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():
// Gate paddle definition.
group def Paddle():
controllable c_open, c_close, c_stop;
// Paddle actuator.
plant A:
location rest:
initial; marked;
......@@ -67,16 +71,12 @@ group def paddle():
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
// Paddle sensor definition.
plant def S():
uncontrollable u_closed_on, u_closed_off, u_open_on, u_open_off;
location closed:
......@@ -88,10 +88,20 @@ group def paddle():
location open:
edge u_open_off goto between;
end
S1 : S();
S2 : S();
S3 : S();
// Gate dynamics.
plant {S1.u_closed_off, S1.u_open_on,
S2.u_closed_off, S2.u_open_on,
S3.u_closed_off, S3.u_open_on} needs A.opening;
plant {S1.u_closed_on, S1.u_open_off,
S2.u_closed_on, S2.u_open_off,
S3.u_closed_on, S3.u_open_off} needs A.closing;
// Gate local requirements.
requirement c_open needs cmd_pad_o;
requirement c_open needs not S1.open or not S2.open or not S3.open;
......@@ -105,20 +115,19 @@ group def paddle():
requirement cmd_stop_pad disables {c_open, c_close};
end
// Initialize two sets of paddles
pad_N : paddle(); pad_S : paddle();
// Instantiate two sets of paddles.
pad_N : Paddle(); pad_S : Paddle();
group def culvert():
// Culvert definition.
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:
......@@ -127,21 +136,30 @@ group def culvert():
location flow:
edge u_off goto noflow;
end
// Dynamics
plant u_off needs A.closed;
plant u_on needs A.open;
// Local requirements.
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();
// Instantiate two culverts.
culvert_N : Culvert(); culvert_S : Culvert();
group def gate(alg bool cmd_gate_o, cmd_gate_c, cmd_stop_gate):
// Gate definition.
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;
// Gate position sensor.
plant S:
location closed:
initial; marked;
......@@ -164,6 +182,8 @@ group def gate(alg bool cmd_gate_o, cmd_gate_c, cmd_stop_gate):
location open:
edge u_s6_on goto bopen;
end
// Gate direction actuator.
plant Dir:
location off:
marked; initial;
......@@ -172,12 +192,12 @@ group def gate(alg bool cmd_gate_o, cmd_gate_c, cmd_stop_gate):
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
// Gate speed actuator.
plant Spe:
location off:
initial; marked;
......@@ -194,6 +214,8 @@ group def gate(alg bool cmd_gate_o, cmd_gate_c, cmd_stop_gate):
location slow_o:
edge c_so_off goto off;
end
// Gate pressure actuator.
plant Pre:
location off:
initial; marked;
......@@ -205,14 +227,19 @@ group def gate(alg bool cmd_gate_o, cmd_gate_c, cmd_stop_gate):
edge c_low_off goto off;
end
// Dynamics.
plant {u_s1_on, u_s2_on, u_s3_on, u_s4_off, u_s5_off, u_s6_off} needs Dir.opening;
plant {u_s6_on, u_s5_on, u_s4_on, u_s3_off, u_s2_off, u_s1_off} needs Dir.closing;
// Local requirements.
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);
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:
......@@ -236,9 +263,12 @@ plant s_equal_U:
edge u_equal_off goto off;
end
group def outgoing(alg bool cmd_out_r, cmd_out_g):
// Definition for the traffic light for outgoing vessels.
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;
// Sensor for the traffic light.
plant S:
location off:
edge u_r_on goto red;
......@@ -254,33 +284,42 @@ group def outgoing(alg bool cmd_out_r, cmd_out_g):
edge u_r_off goto green;
edge u_g_off goto red;
end
// Actuator for the traffic light.
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
// Traffic light dynamics.
plant {u_r_on, u_g_off} needs A.red;
plant {u_g_on, u_r_off} needs A.green;
// Traffic light local requirements.
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);
// Instantiate 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):
// Definition for the traffic light for incoming vessels.
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;
// Sensor for the traffic light.
plant S:
location off:
edge u_r_on goto red;
edge u_g_on goto green;
edge u_s_on goto lowred;
edge u_s_on goto bottomred;
location red:
initial; marked;
edge u_r_off goto off;
......@@ -290,7 +329,7 @@ group def incoming(alg bool cmd_in_red, cmd_in_green, cmd_in_rg, cmd_in_redred):
edge u_r_on goto redgreen;
edge u_g_off goto off;
edge u_s_on goto greenred;
location lowred:
location bottomred:
edge u_r_on goto redred;
edge u_g_on goto greenred;
edge u_s_off goto off;
......@@ -299,36 +338,44 @@ group def incoming(alg bool cmd_in_red, cmd_in_green, cmd_in_rg, cmd_in_redred):
edge u_g_off goto red;
edge u_s_on goto redgreenred;
location redred:
edge u_r_off goto lowred;
edge u_r_off goto bottomred;
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_g_off goto bottomred;
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
// Traffic light actuator.
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
// Traffic light dynamics.
plant u_r_on needs A.red or A.redred or A.redgreen;
plant u_r_off needs A.green;
plant u_g_on needs A.green or A.redgreen;
plant u_g_off needs A.red or A.redred;
plant u_s_on needs A.redred;
plant u_s_off needs A.red or A.green or A.redgreen;
// Local traffic light requirements.
requirement c_red needs cmd_in_red or cmd_stop;
requirement c_green needs cmd_in_green;
requirement c_redgreen needs cmd_in_rg;
......@@ -336,17 +383,19 @@ group def incoming(alg bool cmd_in_red, cmd_in_green, cmd_in_rg, 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);
// Instantiate 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);
// Definition for the gate requirements.
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):
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;
......@@ -371,40 +420,41 @@ group def gate_requirements(controllable c_speed_sc_on, c_speed_sc_off, c_speed_
(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
// Instantiate gate requirements for all gates.
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,
......@@ -414,6 +464,7 @@ requirement emergencystop.pushed disables
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} ;
// Global requirements.
// 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
......@@ -510,7 +561,6 @@ 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_S.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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent