// -------------------------------------------------------- // lawn-mower example // -------------------------------------------------------- vx := 10; vy := 10; vxp := 11; vyp := 9; l := 100; h := 200; xg := 10; yg := 20; time_bound := 1; // -------------------------------------------------------- // System Definition // -------------------------------------------------------- automaton mower synclabs : tau; state_var : x,y,t; loc init: while True wait {x'==0 & y'==0 & t'==0} when True sync tau goto s1; loc s1: while x<=l & y<=h & t<=time_bound wait {x'==vx & y'==vy & t'==1} when x==l sync tau palt { 95 : goto s2, 5 : goto s2p }; when y==h sync tau palt { 95 : goto s3, 5 : goto s3p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s1p: while x<=l & y<=h & t<=time_bound wait {x'==vxp & y'==vyp & t'==1} when x==l sync tau palt { 95 : goto s2, 5 : goto s2p }; when y==h sync tau palt { 95 : goto s3, 5 : goto s3p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s2: while x>=0 & y<=h & t<=time_bound wait {x'==-vx & y'==vy & t'==1} when x==0 sync tau palt { 95 : goto s1, 5 : goto s1p }; when y==h sync tau palt { 95 : goto s4, 5 : goto s4p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s2p: while x>=0 & y<=h & t<=time_bound wait {x'==-vxp & y'==vyp & t'==1} when x==0 sync tau palt { 95 : goto s1, 5 : goto s1p }; when y==h sync tau palt { 95 : goto s4, 5 : goto s4p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s3: while x<=l & y>=0 & t<=time_bound wait {x'==vx & y'==-vy & t'==1} when y==0 sync tau palt { 95 : goto s1, 5 : goto s1p }; when x==l sync tau palt { 95 : goto s4, 5 : goto s4p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s3p: while x<=l & y>=0 & t<=time_bound wait {x'==vxp & y'==-vyp & t'==1} when y==0 sync tau palt { 95 : goto s1, 5 : goto s1p }; when x==l sync tau palt { 95 : goto s4, 5 : goto s4p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s4: while x>=0 & y>=0 & t<=time_bound wait {x'==-vx & y'==-vy & t'==1} when y==0 sync tau palt { 95 : goto s2, 5 : goto s2p }; when x==0 sync tau palt { 95 : goto s3, 5 : goto s3p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc s4p: while x>=0 & y>=0 & t<=time_bound wait {x'==-vxp & y'==-vyp & t'==1} when y==0 sync tau palt { 95 : goto s2, 5 : goto s2p }; when x==0 sync tau palt { 95 : goto s3, 5 : goto s3p }; when x>=90 & x<=100 & y>=170 & y<=200 sync tau goto error; loc error: while True wait {x'==0 & y'==0 & t'==0} initially init & x==xg & y==yg & t==0; end -- mower // -------------------------------------------------------- // Definition of forbidden states // -------------------------------------------------------- //REACH_USE_CONVEX_HULL = true; mower.add_label(tick); //mower.set_refine_constraints((x,100),(y,100),tick); mower.set_refine_constraints((x,10),tick); forbidden=mower.{error & True}; mower.reach_graph("mower.graph", forbidden);