init_t := 8;
wait_time := 1;
react_time := 0.1;
on_flow := -2;
max_switch := 9;
min_switch := 6;
max_unsafe := 12;
min_unsafe := 3;
time_bound := 1;

// --------------------------------------------------------
// System Definition 
// --------------------------------------------------------
automaton temperature
synclabs : tau;
state_var : w,t,m,time;

loc HeatxWait: while t<=wait_time & time<=time_bound
      wait {w'==2 & t'==1 & m'==0 & time'==1}
    when t==wait_time sync tau palt {
      788700452: do {w'==w & t'==0 & m'<=w+0.25 & m'>=w-0.25 & time'==time} goto HeatxReact,
      105649774: do {w'==w & t'==0 & (m'<w-0.25) & time'==time} goto HeatxReact,
      105649774: do {w'==w & t'==0 & (m'>w+0.25) & time'==time} goto HeatxReact};
    when w < min_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;
    when w > max_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;

loc CoolxWait: while t<=wait_time & time<=time_bound
      wait {w'==-w & t'==1 & m'==0 & time'==1}
    when t==wait_time sync tau palt {
      788700452: do {w'==w & t'==0 & m'<=w+0.25 & m'>=w-0.25 & time'==time} goto CoolxReact,
      105649774: do {w'==w & t'==0 & (m'<w-0.25) & time'==time} goto CoolxReact,
      105649774: do {w'==w & t'==0 & (m'>w+0.25) & time'==time} goto CoolxReact};
    when w < min_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;
    when w > max_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;

loc HeatxReact: while t<=react_time & time<=time_bound
      wait {w'==2 & 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 CoolxWait;
    when t==react_time & m<=min_switch sync tau
      do {w'==w & t'==0 & m'==0 & time'==time} goto HeatxWait;
    when t==react_time & m>min_switch & m<max_switch sync tau
      do {w'==w & t'==0 & m'==0 & time'==time} goto HeatxWait;
    when w < min_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;
    when w > max_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;

loc CoolxReact: while t<=react_time & time<=time_bound
      wait {w'==-w & 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 CoolxWait;
    when t==react_time & m<=min_switch sync tau
      do {w'==w & t'==0 & m'==0 & time'==time} goto HeatxWait;
    when t==react_time & m>min_switch & m<max_switch sync tau
      do {w'==w & t'==0 & m'==0 & time'==time} goto CoolxWait;
    when w < min_unsafe sync tau do {w'==0 & t'==0 & m'==0 & time'==time} goto Crash;
    when w > max_unsafe 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 HeatxWait & w==init_t & t==0 & m==0 & time==0;

end -- temperature

//temperature.add_label(tick);
//temperature.set_refine_constraints((w,2),tick);
//temperature.set_refine_constraints((w,1),tick);
//temperature.set_refine_constraints((w,0.5),tick);

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

forbidden=temperature.{Crash & True};
temperature.reach_graph("ts.graph", forbidden);