-- =====================================================================
-- =====================================================================
-- HyTech source file 
-- by Laurent Fribourg and Stephane Messika and Claudine Picaronny (LSV)
--
-- CSMA/CD protocol
-- =====================================================================
-- =====================================================================

var     x1,x2,y,z,t             -- 
           : clock;

        alea1,          --
        alea2           -- 
           : discrete;

        lambda, sigma, c          -- ,
           : parameter;


--****************************************************--
--****************************************************--
-- AUTOMATA
--****************************************************--
--****************************************************--


--****************************************************--
  automaton Sender1
--****************************************************--
synclabs: beg1,cd,end1,ready1, busy1;

initially Idle1;

loc Idle1: while x1>=0 & x2>=0 & y>=0 & t>=0  wait {}
        when True do {z'=0} goto Wait1;  -- {x1'=0}

loc Postwait1: while x1>=0 & x2>=0 & y>=0 & t>=0  & z=0 wait {}
        when True sync beg1 do {x1'=0} goto Transm1;  


loc Wait1: while x1>=0 & x2>=0 & y>=0 & t>=0 &  z=0 wait {}
	when True sync ready1 do {z'=0} goto Postwait1; --Transm1;
	when True sync busy1 do {x1'=0, alea1'>=0}  goto Retry1; -- Retry1bis; 


loc Retry1: 
          while x1>=0 & x2>=0 & y>=0 & t>=0 &  x1 <= alea1 & alea1 <= c  
        wait {}
	when x1=alea1 do {z'=0} goto Wait1;

loc Transm1: while x1>=0 & x2>=0 & y>=0 & t>=0 &  x1 <= lambda wait {}
	when True sync cd do {x1'=0, alea1'>=0} goto Retry1; -- NEW
	when x1=lambda do {z'=0} goto Ok1;



loc Ok1: while x1>=0 & x2>=0 & y>=0 & t>=0 &  z=0 wait {}
	when True sync end1 goto Idle1;


end -- Sender1

--****************************************************--
automaton Sender2
--****************************************************--
synclabs: beg2,cd,end2,ready2,busy2;

initially Idle2;

loc Idle2: while x1>=0 & x2>=0 & y>=0 & t>=0  wait {}
        when True do {z'=0} goto Wait2;  -- {x2'=0}


loc Postwait2: while x1>=0 & x2>=0 & y>=0 & t>=0  & z=0 wait {}
        when True sync beg2 do {x2'=0} goto Transm2;  


loc Wait2: while x1>=0 & x2>=0 & y>=0 & t>=0 &  z=0 wait {}
	when True sync ready2 do {z'=0} goto Postwait2; --Transm12
	when True sync busy2 do {x2'=0, alea2'>=0}  goto Retry2; --Retry2bis; -- Calcul2; -- Retry2bis;

-- loc Retry2bis: while x1>=0 & x2>=0 & y>=0 & t>=0 &  x2<= 1*sigma wait {}            -- NEW
--	when x2=1*sigma do {z'=0} goto Wait2;

loc Retry2: 
        while x1>=0 & x2>=0 & y>=0 & t>=0 &  x2 <= alea2 & 
        alea2 <=c -- alea2 <= 2*sigma  
        wait {}
	when x2=alea2 do {z'=0} goto Wait2;

loc Transm2: while x1>=0 & x2>=0 & y>=0 & t>=0 &  x2 <= lambda wait {}
	when True sync cd do {x2'=0, alea2'>=0} goto Retry2;  -- NEW
	when x2=lambda  do {z'=0} goto Ok2; --do {z'=0} goto Ok2;



loc Ok2: while x1>=0 & x2>=0 & y>=0 & t>=0 &  z=0 wait {}
	when True sync end2 goto Idle2;


end -- Sender2

--****************************************************--
  automaton Bus
--****************************************************--
synclabs: beg1,beg2,cd,end1,end2,ready1,ready2,busy1,busy2;

initially Idlebus;

loc Idlebus: 
        while x1>=0 & x2>=0 & y>=0 & t>=0  wait {}
	when True sync ready1 goto Idlebus;
	when True sync ready2 goto Idlebus;
	when True sync beg1 do {y'=0}  goto Preactive1;
	when True sync beg2 do {y'=0}  goto Preactive2;

loc Preactive1:
       while x1>=0 & x2>=0 & y>=0 & t>=0 &  y<= sigma wait {}  -- NEW
	when y<sigma sync ready2 goto Preactive1;
       when y=sigma goto Active1;  
--       when True sync beg2 do {y'=0} goto Col;
--       when y<=sigma do {w1'=1,w2'=1} goto Active1; -- Kronos: Yovine ???
       when y<sigma sync beg2 do {y'=0} goto Col; --  --Kronos: Yovine

loc Preactive2:
       while x1>=0 & x2>=0 & y>=0 & t>=0 &  y<= sigma wait {}  -- NEW
	when y<sigma sync ready1 goto Preactive2;
       when y=sigma goto Active2;    
--       when True sync beg1 do {y'=0} goto Col;
--       when y<=sigma do {w1'=1,w2'=1} goto Active2; -- Kronos: Yovine ???
       when y<sigma sync beg1 do {y'=0} goto Col;   --Kronos: Yovine

loc Col: while x1>=0 & x2>=0 & y>=0 & t>=0 &  y<= sigma wait {}
	when y = sigma sync cd  goto Idlebus;  -- Nicollin
--	when y = sigma sync cd1 do {z'=0} goto Colbis2;  -- Nicollin
--	when y <= sigma sync cd1 do {z'=0} goto Colbis; -- Kronos: Yovine

--loc Colbis2: while x1>=0 & x2>=0 & y>=0 & t>=0 &  z=0 wait {}
--	when z=0 sync cd2 do {w1'=0, w2'=0} goto Idlebus; -- y'=0

--loc Colbis1: while x1>=0 & x2>=0 & y>=0 & t>=0 &  z=0 wait {}
--	when z=0 sync cd1 do {w1'=0, w2'=0} goto Idlebus; -- y'=0

loc Active1:
       while x1>=0 & x2>=0 & y>=0 & t>=0  wait {}
	when True sync busy2 goto Active1;
       when True sync end1 do {y'=0} goto End;

loc Active2:
       while x1>=0 & x2>=0 & y>=0 & t>=0  wait {}
	when True sync busy1 goto Active2;
       when True sync end2 do {y'=0} goto End;

loc End: while x1>=0 & x2>=0 & y>=0 & t>=0 &   y<= sigma wait {}
	when y<sigma sync busy1 goto End;
	when y<sigma sync busy2 goto End;
	when y = sigma goto Idlebus;  -- Nicollin
--	when y <= sigma do {w1'=0,w2'=0} goto Idlebus; 
--        when True sync beg1 do {w2'=1,y'=0} goto Preactive1;
--        when True sync beg2 do {w1'=1,y'=0} goto Preactive2;

end -- Bus


--****************************************************--
--****************************************************--
-- ANALYSIS
--****************************************************--
--****************************************************--

var init_reg, post_reg, notU, notV, notW : region;

init_reg := True
	----------------------
	-- Initial locations
	----------------------
	& loc[Sender1]=Idle1 & loc[Sender2]=Idle2 & loc[Bus]=Idlebus
        & x1=0 & x2=0 & y=0 & t=0 & z=0 


	---START PI0---
--        & lambda=780
--       & c=52
--	& sigma =26
	---END PI0---

	& lambda >0 & c>0 & sigma>0 
;

post_reg := reach forward from init_reg endreach;

prints "---START LOG---";
print(hide non_parameters in post_reg endhide);
prints "---END LOG---";