CHEAP_CONTAIN_RETURN_OTHERS=false;


// --------------------------------------------------------
// Water-level monitor example
// --------------------------------------------------------

// --------------------------------------------------------
// System Definition 
// --------------------------------------------------------

time_bound := 1;

automaton waterlevel
synclabs : tau;
state_var : x,y,t;

loc init: while True wait {x'==0 & y'==0 & t'==0}
    when True sync tau goto s0;
    when (y<1 | y>12) sync tau goto error;

loc s0: while y<=10 & t<=time_bound wait {x'==0 & y'==1 & t'==1}
    when y==10 sync tau palt {
    95 : do {x'==0 & y'==y & t'==t} goto s1,
     5 : do {x'==0 & y'==y & t'==t} goto s1p
    };
    when (y<1 | y>12) sync tau goto error;

loc s1: while x<=2 & t<=time_bound  wait {x'==1 & y'==1 & t'==1}
    when x==2 sync tau do {x'==0 & y'==y & t'==t} goto s2;
    when (y<1 | y>12) sync tau goto error;

loc s1p: while x<=3 & t<=time_bound wait {x'==1 & y'==1 & t'==1}
    when x==3 sync tau do {x'==0 & y'==y & t'==t} goto s2;
    when (y<1 | y>12) sync tau goto error;

loc s2: while y>=5 & t<=time_bound wait {x'==0 & y'==-2 & t'==1}
    when y==5 sync tau palt {
      95 : do {x'==0 & y'==y & t'==t} goto s3,
       5 : do {x'==0 & y'==y & t'==t} goto s3p
    };
    when (y<1 | y>12) sync tau goto error;

loc s3: while x<=2 & t<=time_bound wait {x'==1 & y'==-2 & t'==1}
    when x==2 sync tau do {x'==0 & y'==y & t'==t} goto s0;
    when (y<1 | y>12) sync tau goto error;

loc s3p: while x<=3 & t<=time_bound wait {x'==1 & y'==-2 & t'==1}
	when x==3 sync tau do {x'==0 & y'==y & t'==t} goto s0;
    when (y<1 | y>12) sync tau goto error;

loc error: while True wait {x'==0 & y'==0 & t'==0}

initially init & x==0 & y==1 & t==0;

end -- waterlevel


waterlevel.add_label(tick);
waterlevel.set_refine_constraints((x,2),tick);

// --------------------------------------------------------
// Definition of forbidden states
// --------------------------------------------------------

forbidden=waterlevel.{error & True};
waterlevel.reach_graph("waterlevel.graph", forbidden);