initial_fill := 6.5; wait_time := 1; react_time := 0.1; off_flow := 1; on_flow := -2; max_switch := 8; min_switch := 5; max_crash := 12; min_crash := 1; time_bound := 10; // -------------------------------------------------------- // System Definition // -------------------------------------------------------- automaton water synclabs : tau; state_var : w,t,m,time; loc OffxWait: while t<=wait_time & time<=time_bound wait {w'==off_flow & t'==1 & m'==0 & time'==1} when t==wait_time sync tau palt { 950: do {w'==w & t'==0 & m'<=w+2 & m'>=w-2 & time'==time} goto OffxReact, 50: do {w'==w & t'==0 & (m'>w+1.9 | m' max_crash sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash; loc OnxWait: while t<=wait_time & time<=time_bound wait {w'==on_flow & t'==1 & m'==0 & time'==1} when t==wait_time sync tau palt { 950: do {w'==w & t'==0 & m'<=w+2 & m'>=w-2 & time'==time} goto OnxReact, 50: do {w'==w & t'==0 & (m'>w+1.9 | m' max_crash sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash; loc OffxReact: while t<=react_time & time<=time_bound wait {w'==off_flow & t'==1 & m'==0 & time'==1} when t==react_time & m>=max_switch sync tau do {w'==w & t'==0 & m'==0 & time'==time} goto OnxWait; when t==react_time & m<=min_switch sync tau do {w'==w & t'==0 & m'==0 & time'==time} goto OffxWait; when t==react_time & m>min_switch & m max_crash sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash; loc OnxReact: while t<=react_time & time<=time_bound wait {w'==on_flow & t'==1 & m'==0 & time'==1} when t==react_time & m>=max_switch sync tau do {w'==w & t'==0 & m'==0 & time'==time} goto OnxWait; when t==react_time & m<=min_switch sync tau do {w'==w & t'==0 & m'==0 & time'==time} goto OffxWait; when t==react_time & m>min_switch & m max_crash sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash; loc Crash: while True wait {w'==0 & t'==0 & m'==0 & time'==0} initially OffxWait & w==initial_fill & t==0 & m==0 & time==0; end -- water forbidden=water.{Crash & True}; water.reach_graph("water-prob.graph", forbidden);