-- -------------- -- -- Mobile example -- -- -------------- -- -- this version v2.0 is different from the first one -- first one is buggy: the computed strategy is not -- deterministic because we didn't implement correctly -- our procedure -- Names of variables have been changed a bit var x,y: clock; t,t1: analog; cost, cost_x, cost_y: analog; cost0, cost1, cost2, cost3, cost4: parameter; c,u,a: discrete; -- Legend -- a =-1 --> Uncontrollable action -- a = 0 --> delay -- a = 1 --> low_x->Win -- a = 2 --> high_x->A -- a = 3 --> low_y->Win -- a = 4 --> high_y->low_y -- -- c --> If c changed -> controllable action -- u --> If u changed -> uncontrollable action -- -- t, t1 --> These variables are not part of the model -- we just need them to some existential quantification -- to compute the \lambda(X) of a set automaton Antenna_1 synclabs: jam_x; initially low_x & x=0; loc low_x: while x>=0 wait {dcost_x=-1} when x>=10 & a=1 do {c'=1-c,u'=u,cost'=cost-7} goto Win; when True sync jam_x do {x'=0,c'=c,u'=1-u} goto high_x; loc high_x: while x>=0 & x<=10 wait {dcost_x=-10} when x>=5 & a=2 do {y'=0,c'=1-c,u'=u} goto low_x; when True sync jam_x do {x'=0,c'=c,u'=1-u} goto high_x; loc Win: while x>=0 wait {dcost_x=0} end -- Antenna_1 automaton Antenna_2 synclabs: jam_y; initially low_y & y=0; loc low_y: while y>=0 wait {dcost_y=-2} when y>=10 & a=3 do {c'=1-c,u'=u,cost'=cost-1} goto Win; when True sync jam_y do {y'=0,c'=c,u'=1-u} goto high_y; loc high_y: while y>=0 & y<=10 wait {dcost_y=-20} when y>=2 & a=4 do {x'=0,c'=1-c,u'=u} goto low_y; when True sync jam_y do {y'=0,c'=c,u'=1-u} goto high_y; loc Win: while y>=0 wait {dcost_y=0} end -- Antenna_2 automaton Jammer synclabs: jam_x, jam_y; initially lX; loc lX: while True wait {dcost=dcost_x+dcost_y,dt=-1,dt1=-1} when x>6 sync jam_x goto lX; when x>6 sync jam_y goto lY; loc lY: while True wait {dcost=dcost_x+dcost_y,dt=-1,dt1=-1} when y>6 sync jam_y goto lY; when y>6 sync jam_x goto lX; end -- Jammer ------------------ -- Computations -- ------------------ var init, -- Initial states winning, -- Winning locations reachable, -- Reachable regions fix, -- fixpoint = winning states uPrebarX, -- Uncontrollable predecessors of the complement of X Stopped, -- stop states uPreX, cPreX, X,Y,Z, fix_strat, nonstop, r0, r1, r2, r3, r4, B0,B1,B2,B3,B4, inf_0_1, inf_0_2, inf_0_3, inf_0_4, inf_1_0, inf_1_2, inf_1_3, inf_1_4, inf_2_0, inf_2_1, inf_2_3, inf_2_4, inf_3_0, inf_3_1, inf_3_2, inf_3_4, inf_4_0, inf_4_1, inf_4_2, inf_4_3 : region; -- Initial region -- init := x=0 & y=0 & loc[Antenna_1]=low_x & loc[Antenna_2]=low_y & loc[Jammer]=lX; -- Winning region -- winning := (loc[Antenna_1]=Win | loc[Antenna_2]=Win) & cost>=0 ; -- Compute reachable regions -- -- ------------------------- -- prints ""; prints "Reachable regions"; prints "------------------"; reachable := iterate reachable from (hide cost,cost_x,cost_y,cost0,cost1,cost2,cost3,cost4, c,u,t,t1,a in init endhide) using { reachable := (hide cost,cost_x,cost_y,cost0,cost1,cost2,cost3,cost4, c,u,t,t1,a in post(reachable) endhide); }; -- Backward analysis -- -- ----------------- -- prints ""; prints "Computing the winning states"; prints "----------------------------"; -- now start the computation of the fixpoint fix_strat := False; -- this set is ised to extract the strategies fix := winning; -- is the fixpoint we want to compute i.e. set of winning states Stopped := ~(hide t,c,u in t>0 & c=0 & u=0 & pre(True & t=0 & c=0 & u=0) endhide) ; -- ---------------------------------------------- -- -- Backward analysis: look for a fix point of \pi -- -- ---------------------------------------------- -- -- compute the fixpoint by \pi X := iterate X from winning using { -- uncontrollable predecessors of the complement of X uPrebarX := hide t,u in t=0 & u=0 & pre(~X & u=1 & t=0) endhide; -- controllable predecessors of X cPreX := hide t,c in t=0 & c=0 & pre(X & t=0 & c=1) endhide ; prints "cPreX"; print cPreX; -- uncontrollable predecessors leading to winning states uPreX := hide t,u in t=0 & u=0 & pre(X & u=1 & t=0) endhide; -- Z is the the first argument of \pi' in the paper Z := (X | (hide a in cPreX endhide) | (uPreX & ~uPrebarX & Stopped)) ; -- time predecessors of Z from which we can reach Z -- and avoid \bar{X} all along -- (works only if time deterministic !!) X := hide t in (hide c,u in t>=0 & c=0 & u=0 & pre(Z & t=0 & c=0 & u=0) endhide) & ~(hide t1 in (hide c,u in t1>=0 & t1<=t & c=0 & u=0 & pre(uPrebarX & t1=0 & c=0 & u=0) endhide) endhide) endhide; prints "X"; print X; -- add the newly computed regions to the set of already -- computed region Y := X & ~fix ; -- new states fix := fix | X ; -- computation of nonstop nonstop := a=0 & Y & hide t,c,u in t>0 & c=0 & u=0 & pre(Y & t=0 & u=0 & c=0) endhide; -- computation of fix_strat fix_strat := fix_strat | (Y & cPreX) | nonstop ; } ; -- -------- -- -- End Loop -- -- -------- -- prints ""; prints "------------------"; prints "-- Optimal cost --"; prints "------------------"; print omit all locations hide x,y in fix & init endhide; prints "----------------------------------------" ; prints "----------------------------------------" ; prints "fix_strat"; print fix_strat ; prints ""; prints "--------------"; prints "-- Strategy --"; prints "--------------"; r0 := hide a,cost in cost0=cost & fix_strat & a=0 endhide ; r1 := hide a,cost in cost1=cost & fix_strat & a=1 endhide ; r2 := hide a,cost in cost2=cost & fix_strat & a=2 endhide ; r3 := hide a,cost in cost3=cost & fix_strat & a=3 endhide ; r4 := hide a,cost in cost4=cost & fix_strat & a=4 endhide ; -- compute inf A <= inf B -- hide a in A & ~(hide b in B & blow_y (a=4) on:"; prints "--------------------"; B4 := inf_4_0 & inf_4_1 & inf_4_2 & inf_4_3; print B4; prints ""; prints "Do low_y->Win (a=3) on:"; prints "-----------------"; B3:= inf_3_0 & inf_3_1 & inf_3_2 & inf_3_4 & ~B4 ; print B3; prints ""; prints "Do high_x->low_x (a=2) on:"; prints "--------------------"; B2 := inf_2_0 & inf_2_1 & inf_2_3 & inf_2_4 & ~B3 & ~B4; print B2; prints ""; prints "Do low_x->Win (a=1) on:"; prints "-----------------"; B1 := inf_1_0 & inf_1_2 & inf_1_3 & inf_1_4 & ~B2 & ~B3 & ~B4; print B1; prints "Delay (a=0) on:"; prints "---------"; B0:= inf_0_1 & inf_0_2 & inf_0_3 & inf_0_4 & ~B1 & ~B2 & ~B3 & ~B4 ; print B0;