-- In this example we compute the best cost and
-- synthetize an optimal strategies. See the output, run hytech file.hy


var
        x,y: clock;  -- 
        cost: analog; -- the cost variable
        c,u,a: discrete; -- used to indicate that
	       -- if c is changed -> control action
	       -- if u is changed -> uncontrollable action
       t,t1: analog; -- these variables are not part of the model
	      	      -- we just need them to some existential quantification
		      -- to compute the \lambda(X) od a set
       cost1,cost0,cost2,d,b:parameter ; -- these are variables needed
					-- at the end to do some computatio
					-- but no part of the model

automaton H
synclabs: ;
initially l0 & x=0 & y=0; 
	  -- we need y to model the urgency of location l1
	  -- note also that Hytech does not use the constraint x>=0 when x
	  -- is a clock. This is why we add it in the invariant (important when
	  -- computing backward !!)

loc l0: while x>=0 & y>=0 wait {dcost=-5,dt=-1,dt1=-1}
    	-- one controllable transition -c changed- and this a_1
        when x>=0 & x<=2 & a=1 do {u'=u,c'=1-c,y'=0} goto l1;

loc l1: while y=0 wait {dcost=0,dt=-1,dt1=-1}
        when x<1 do {u'=1-u,c'=c} goto l2;
        when True  do {u'=1-u,c'=c} goto l2;
        when True  do {u'=1-u,c'=c} goto l3;


loc l2: while x>=0 & y>=0 wait {dcost=-10,dt=-1,dt1=-1}
        -- one controllable transition -c changed- and this a_2
        when x>=2 & a=2 do {c'=1-c,u'=u,cost'=cost-1} goto Win;

loc l3: while x>=0 & y>=0 wait {dcost=-1,dt=-1,dt1=-1}
        -- one controllable transition -c changed- and this a_2
        when x>=2  & a=2 do {c'=1-c,u'=u,cost'=cost-7} goto Win;

loc Win: while True wait {dcost=0,dt=-1,dt1=-1}

end


var init_reg,winning,fix,  -- set of states
    STOP, -- ste of states from whihc time is stopped
    r0,r1,r2,
    B0,B1,B2,
    inf_0_1,inf_0_2,inf_1_0,inf_1_2,inf_2_0,inf_2_1, -- needed to compute the best strategy
    
    uPreX,uPrebarX,cPreX,X,Y,Z,fix_strat,nonstop : region ;

-- first define the initial and winning regions 
init_reg := loc[H]=l0 & x=0  ;
winning := loc[H]=Win & cost>=0;

-- 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

prints "Initial value of winning";
print winning;

STOP := ~(hide t,c,u in t>0 & c=0 & u=0 & pre(True & t=0 & c=0 & u=0) endhide) ;

-- 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 & STOP)) ;

		-- 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 ;

	  } ;

-- now if we are  here it terminates !!

-- in the sequel we hide y
-- y is not useful, just to make l1 an urgent location

prints "----------------------------------------" ;
prints "----------------------------------------" ;
prints "winning states :" ;
print hide y in fix endhide  ;
prints "----------------------------------------" ;
prints "----------------------------------------" ;

prints "winning states and init :" ;
print hide y in fix & init_reg endhide ;

prints "----------------------------------------" ;
prints "----------------------------------------" ;

prints "the optimal cost is" ;
print omit all locations hide x,y in fix & init_reg endhide;

prints "----------------------------------------" ;
prints "----------------------------------------" ;
 

prints "fix_strat";
print fix_strat ;

-- now we have  linear equations with cost and x,y etc
-- we want to compute the function that gives the cost
-- function when the action is \lambda or a=1 or a=2
-- for this we create 3 cost functions. In fact we rename
-- cost in the function giving the cost when we do an a=1 action
-- by cost1 (and do this for the others) and compute a region r1
r1 :=   hide a,cost in cost1=cost & fix_strat & a=1  endhide ;
r0 :=    hide a,cost in cost0=cost & fix_strat & a=0  endhide ;
r2 :=    hide a,cost in cost2=cost & fix_strat & a=2  endhide ;
-- now ri (with costi) gives us the cost function when we do an a=i action

-- now we need to find the best moves. When an a=i action has a cost
-- function <= to any other a=k we should do an a=i action
-- so we split the winning states in regions inf_i_j 
-- meaning that on this region a=i is better than a=j

-- for this we need to compute the following:
-- compute the states for which  inf D <= inf B
-- hide d in  D  & ~(hide b in B & b<d  endhide) endhide ;

inf_0_1 := hide cost0 in r0  & ~(hide cost1 in r1 & cost1<cost0  endhide) endhide ;
inf_0_2 := hide cost0 in r0  & ~(hide cost2 in r2 & cost2<cost0  endhide) endhide ;
inf_1_0 := hide cost1 in r1  & ~(hide cost0 in r0 & cost0<cost1  endhide) endhide ;
inf_1_2 := hide cost1 in r1  & ~(hide cost2 in r2 & cost2<cost1  endhide) endhide ;
inf_2_0 := hide cost2 in r2  & ~(hide cost0 in r0 & cost0<cost2  endhide) endhide ;
inf_2_1 := hide cost2 in r2  & ~(hide cost1 in r1 & cost1<cost2  endhide) endhide ;

-- Now print the result taking the best action each time
-- Note that in case two actions are equivalent (same cost)
-- they might be both "enabled"  

prints "Optimal Winning Strategy" ; 
prints "do control from l3 or l4 to Win (a=2) on"; 
B2 := inf_2_0 & inf_2_1 ;
print B2 ;
prints "do control from l0 to l1 (a=1) on"; 
B1 := inf_1_0 & inf_1_2 & ~B2 ;
print B1 ;
prints "do wait (a=0) on"; 
B0 := inf_0_1 & inf_0_2 &  ~B1 & ~B2 ; 
print B0;