// Reachable set
// [TARGET]  to be replaced with actual target predicate



enum CS {0..4};
enum Thread {0..1};

class Threads{
 Thread  t0;
 Thread  t1;
 Thread  t2;
 Thread  t3;
 Thread  t4;
};


class Globals{
 Global  CG;
 Global  E_CG;
 Global  g1;
 Global  g2;
 Global  g3;
 Global  g4;
}
 CG  ~+ E_CG,
 CG  ~+ g1,
 g1  ~+ g2,
 g2  ~+ g3,
 g3  ~+ g4
;


bool thread(
CS      r,
Threads T,
Thread  i
)
(        ( r=0 & T.t0=i )
       | ( r=1 & T.t1=i )
       | ( r=2 & T.t2=i )
       | ( r=3 & T.t3=i )
       | ( r=4 & T.t4=i )
);



bool LessEqualCS(CS r, CS r')
r ~+ r'
(   ( r=0 )
  | ( r=1 & r' !=0 )
  | ( r=2 & r' !=0 & r'!=1 )
  | ( r=3 & r' !=0 & r'!=1 & r'!= 2 )
  | ( r'=4 )
);


bool First(
CS      r,
Threads T

)
(
    ( r=1 & !(T.t0=T.t1))
  | ( r=2 & !(T.t0=T.t2) & !(T.t1=T.t2))
  | ( r=3 & !(T.t0=T.t3) & !(T.t1=T.t3) & !(T.t2=T.t3))
  | ( r=4 & !(T.t0=T.t4) & !(T.t1=T.t4) & !(T.t2=T.t4) & !(T.t3=T.t4))
);


// Increase context-switch counter
bool increaseCS(CS r, CS r')
r ~+ r'
(   ( r=0 & r'=1 )
  | ( r=1 & r'=2 )
  | ( r=2 & r'=3 )
  | ( r=3 & r'=4 )
);




// sourceCS checks that u is the last state before the u.r+1'th switch on some run  consistent with the t- and g-tuples

bool sourceCS( CS r, Globals G )
r   <  G
(   ( r=0 & G.g1=G.CG )
  | ( r=1 & G.g2=G.CG )
  | ( r=2 & G.g3=G.CG )
  | ( r=3 & G.g4=G.CG )
);




// destCS checks that u is the first state after the u.r'th switch on some run  consistent with the t- and g-tuples
bool destCS( CS r, Globals G )
r   <  G
(   ( r=1 & G.g1=G.CG )
  | ( r=2 & G.g2=G.CG )
  | ( r=3 & G.g3=G.CG )
  | ( r=4 & G.g4=G.CG )
);


// for each possible pair (s.r,u.r),  Consecutive checks that s and u are in the same thread,
//  and anything in the between is not in the same thread


bool Consecutive(
CS      s_r,
CS      u_r,
Threads T
)
s_r ~+ u_r,
u_r <  T
(
          (s_r=2 & u_r=0 & T.t2=T.t0 & !(T.t1=T.t2))
        | (s_r=3 & (   (u_r=0 & !(T.t2=T.t3) & !(T.t1=T.t3))
                     | (u_r=1 & T.t1=T.t3 & !(T.t2=T.t3))
                   )
           )
        | (s_r=4
             & (   (u_r=0 & T.t0=T.t4 & !(T.t3=T.t4) & !(T.t2=T.t4) & !(T.t1=T.t4))
                 | (u_r=1 & T.t1=T.t4 & !(T.t3=T.t4) & !(T.t2=T.t4))
                 | (u_r=2 & T.t2=T.t4 & !(T.t3=T.t4) )
               )
          )
);



bool Copy_g(Globals s, Globals t)
s  ~+ t
(   s.g1=t.g1
  & s.g2=t.g2
  & s.g3=t.g3
  & s.g4=t.g4
);



mu bool Reachable(
 Module  s_mod,
 PrCount s_pc,
 Local   s_CL,
 Local   s_E_CL,
 CS      s_r,
 CS      s_E_r,
 Globals s_G,
 Threads s_T
)
 s_mod  <   s_pc,
 s_pc   <   s_r,
 s_r    ~+  s_E_r,
 s_r  <   s_CL,
 s_CL   ~+  s_E_CL,
 s_CL   <   s_G,
 s_G    <   s_T
(
  false

  // early termination
  | (  exists
              Module  t_mod,
              PrCount t_pc,
              Local   t_CL,
              Local   t_E_CL,
              CS      t_r,
              CS      t_E_r,
              Globals t_G,
              Threads t_T.
            (    target(t_mod,t_pc)
               & Reachable( t_mod, t_pc, t_CL, t_E_CL, t_r, t_E_r, t_G, t_T )
            )
    )

  // initial conf
  // Assuming init condition is separate on local and global variables
  // Hence we can always start with process 0, switching to process 1 immediately if required.
  // In fact, let's assume all initial values of local and global variables are feasible.

  |  (   LocalInit( s_r, s_mod, s_pc, s_CL, s_T )
         & GlobalInit(s_G.CG)
         & s_r=0
     )


  // first context-switch to process i
  | (     (LocalInit( s_r, s_mod, s_pc, s_CL, s_T )
        & First( s_r, s_T )
        & destCS( s_r, s_G ))
	& (exists
                Module  t_mod,
                PrCount t_pc,
                Local   t_CL,
                Local   t_E_CL,
                CS      t_r,
                CS      t_E_r,
                Globals t_G.
		(   Reachable( t_mod, t_pc, t_CL, t_E_CL, t_r, t_E_r, t_G, s_T )
                  & (   s_G.CG=t_G.CG
                      & Copy_g(s_G,t_G)
                      & increaseCS(t_r,s_r)
                    )
                )
     	 )
    )




  // General switching rule : If (Conf=(tCG,..),r-1,tg1,tg1'...tgk,tgk') is Reachable,
  //    and (Conf=(sCG',sCL), r-2,sg1,sg1'...sgk,sgk') is Reachable,
  //    where sg1=tg1,sg1'=tg1',...sgk=tgk,sgk'=tgk'
  //    and
  //    (either r-2=1 and s.CG'=s.g1, or r-2=0 and s.CG'=s.g0, or r-2=2 and s.CG'=s.g2)
  //  then add (Conf=(tCG,sCL), r,sg1,sg1',.., sgk,sgk') to WF
  //  Note: If r is less than k, then tg(r+x),tg'(r+x),... will be free, and hence there will be no restriction.
  //        Intermediate size may blow up a bit.


 | (
       ( exists
              Module  t_mod,
              PrCount t_pc,
              Local   t_CL,
              Local   t_E_CL,
              CS      t_r,
              CS      t_E_r,
              Globals t_G.
              (   Reachable( t_mod, t_pc, t_CL, t_E_CL, t_r, t_E_r, t_G, s_T )
                & (   t_G.CG=s_G.CG & Copy_g( s_G, t_G ) & increaseCS( t_r, s_r ) )
              )
       )
     & (exists  CS u_r.
          ( exists Globals u_G.
               ( Reachable( s_mod, s_pc, s_CL, s_E_CL, u_r, s_E_r, u_G, s_T )
	         & ( Copy_g(s_G,u_G) & sourceCS(u_r, u_G ) )
               )
          ) & Consecutive( s_r, u_r, s_T )
       )& destCS( s_r, s_G )
   )


  // forward propagation on internal transitions

  | ( exists
            PrCount t_pc,
            Local   t_CL,
            Globals t_G.
            (  (   (
                      Reachable( s_mod, t_pc, t_CL, s_E_CL, s_r, s_E_r, t_G, s_T )
                    & ( s_G.E_CG=t_G.E_CG & Copy_g(s_G,t_G) )
                   )
               ) & ProgramInt2( s_r, s_T, s_mod, s_pc, t_pc, s_CL, t_CL, s_G, t_G )
    )
  )


  // forward propagation on call transitions
  | (
       s_pc=0
     & CopyLocals( s_r, s_mod, s_CL, s_E_CL, s_T )
     & s_G.E_CG=s_G.CG
     & s_E_r=s_r
     & (exists
              Module  t_mod,
              PrCount t_pc,
              Local   t_CL,
              Globals t_G.
              (
                 ( exists
                     Local   t_E_CL,
                     CS      t_E_r.
                     ( Reachable( t_mod, t_pc, t_CL, t_E_CL, s_r, t_E_r, t_G, s_T ) )
                 )
                 & (s_G.CG=t_G.CG
                 & Copy_g(s_G,t_G) )
                 & programCall( s_r, s_T, t_mod, t_pc, t_CL, s_mod, s_CL, t_G )
              )
       )
    )


  // forward propagation on SkipCall (jump from exit to return)

  | ( exists

            PrCount t_pc,
            Local   t_CL,
            Globals t_G,
            CS      t_r.
	    (
	        (   Reachable( s_mod, t_pc, t_CL, s_E_CL, t_r, s_E_r, t_G, s_T )
	          & (
                        s_G.E_CG=t_G.E_CG
                      & Copy_g(s_G,t_G)
                      & LessEqualCS(t_r,s_r)
                    )
                )
                 & SkipCall( s_r, s_T, s_mod, s_pc, t_pc )

               &(exists Module  u_mod,  Local   u_E_CL.
                   programCall( s_r, s_T, s_mod, t_pc, t_CL, u_mod, u_E_CL, t_G )
                 &
                  (exists  PrCount u_pc, Local u_CL, Globals u_G.
                     (  (   SetReturn ( s_r, s_T, s_mod, s_CL, s_G, u_mod, t_pc, u_pc, t_CL, u_CL, u_G )
                          & t_G.CG=u_G.E_CG
                          & Copy_g( s_G, u_G )
                        )
                        & (exists
                             CS u_r,
                             CS u_E_r.
	  		          (     Reachable( u_mod, u_pc, u_CL, u_E_CL, s_r, u_E_r, u_G, s_T )
                                      & ( Exit( u_r, s_T, u_mod, u_pc ) & u_E_r=t_r )
                                  )
                          )
                     )
                  )
                )
	   )
      )

);


/******************************************************************************************************/
//                                    Reachabibility check                                            *
/******************************************************************************************************/


(  exists
              Module  t_mod,
              PrCount t_pc,
              Local   t_CL,
              Local   t_E_CL,
              CS      t_r,
              CS      t_E_r,
              Globals t_G,
              Threads t_T.
            (  [TARGET]
               & Reachable( t_mod, t_pc, t_CL, t_E_CL, t_r, t_E_r, t_G, t_T )
            )
);