r_in := 15;
r_out := 15.7;

automaton lake
contr_var: x, t;

synclabs: lakelab;
loc single: 
    while x >= 0 wait 
        { 0.7 * r_in - r_out <= x' <= r_in - r_out & t' == 1}
    
initially: single & x == 25.7 & t == 0;
end



// Compute the reachable set
//
region=lake.reachable;

//
// Output to file

region.print("lake_regions.txt", 0);

region.project_to(t, x);
region.print("lake.txt", 2);

// Safety verification

forbidden = lake.{$ & x < 0};
reach_set = lake.is_reachable(forbidden);
reach_set.intersection_assign(forbidden);

echo "The intersection between the reachable set and the bad region is:";
reach_set.is_empty;