-- =============================================================

Load "constants.pf";

-- ===================================================
-- initialization of p,q,phi,reach,q_free
-- ===================================================

To initialization;
   If (DEBUG)
      Print "initializing p,q, reach, and pending\n";
   End -- if debug

   -- ======================
   -- the properties p and q
   -- ======================
   Let p := P[2].loc=2 & !Err;
   Let q := P[2].loc=3 | Err;
   
   Let PID := 2; -- check liveness for process PID


   Let reach:=successors(_i,total);

   Let q_free := total& !q & !next(q);

   -- ===============================================================
   -- The set of pending states. all states that are reachable from a
   -- reachable p state along a q free path
   -- ===============================================================
   Let phi := successors(reach&p,q_free);
   If (DEBUG_BDD)
      Print "The candidate for pending states\n";
      Let stam := print_bdd(phi);
   End -- if debug


   Local j := 1;
   While (j <= JNUM)
      Let Jcomm[j] := j mod NUMBER_OF_LOCATIONS;
      If (Jcomm[j] = 0)
         Let Jcomm[j] := 3;
      End
      Let Jproc[j] := (j - 1) / NUMBER_OF_LOCATIONS + 1;
      
      Let j := j + 1;
   End

   Let setforks := vset();
   Local i := 1;
   While (i <= NUMBER_OF_PROCESSES)
      If (i != NUMBER_OF_PROCESSES)
--        Let setproc[i] := vset(P[i].loc, P[i].neverl1, P[i].neverl2, fork[i], fork[i+1]);
        Let setproc[i] := vset(P[i].loc, P[i].neverl1, P[i].neverl2, fork[i]);
      Else
--        Let setproc[i] := vset(P[i].loc, P[i].neverl1, P[i].neverl2, fork[i], fork[1]);
        Let setproc[i] := vset(P[i].loc, P[i].neverl1, P[i].neverl2, fork[i]);
      End
      Let i := i + 1;
   End 
   
End -- initialization

-- ===================================================
-- end of initialization
-- ===================================================

-- =========================================
-- Initialize the arrays justice
-- =========================================
To initialize_justice;
   If (DEBUG)
      Print "Initializing the justice arrays\n";
   End

   -- Initializing the justice conditions
   Let j := JNUM;
 
   While(j)
     Let just[j] := _j[j];
     Let j := j - 1;
   End -- while j

Let justice_number := 0;

End -- initialize_justice;
-- =========================================
-- end function initialize_justice
-- =========================================

-- ===================================================================
-- For every justice condition (J) compute the states where it is
-- helpful.
-- This is done by computing the greatest fixed point of psi=
-- phi & !J & cax(J -> !phi) & cex (J & !phi) & cax(psi | !phi)
--
-- Some intuition - a state is in the gfp of the formula if it is in
-- phi, the justice requirement does not hold for it, BUT its
-- successors who are just are out of phi, it has some just successor
-- and all its successors are either in the same set or out of phi
--
-- It has to be a greatest fixpoint because we want to be able to
-- circulate within this set of states that remain helpful until the
-- justice holds and then we are out of phi
-- ===================================================================
Func greatest_fixed_point(all_states,justice_req);

   Let gfp_old := 0;
   Let gfp_new := all_states;
   While ( ! (gfp_old = gfp_new) )
      Let gfp_old := gfp_new;
      Let gfp_new := gfp_old & !justice_req & 
                   cax(!all_states | gfp_old) &
                   cex(!all_states);
   End -- While

   Let gfp_old := 0;
   Return(gfp_new);

End -- Func greatest_fixed_point


Func my_cep(arg);
   Return succ(total, arg);
End

Func my_cap(arg);
   Return !my_cep(!arg);
End


Func gfp(all_states, justice_req);

   Let gfp_old := 0;
   Let gfp_new := all_states;
   While ( !(gfp_old = gfp_new) )
      Let gfp_old := gfp_new;
      Let gfp_new := gfp_old & !justice_req &
      			my_cap(!all_states | gfp_old);
   End
   
   Let gfp_old := 0;
   Return(gfp_new);
   
End


-- ==================================================================
-- Break up the pending states into ranks as follows:
-- Given the set of pending states we take all the states that with
-- one helpfull transition leave the pending states.
-- All these states are tagged as one rank and we continue with the
-- pending states minus this rank.
-- More details:
-- For every justice requirement we identify all the states that this
-- justice is helpfull for (see greatest_fixed_point).
-- Once we found these states for all justice requirements we remove
-- them from the set of pending
-- ==================================================================

To compute_helpful;


   If (DEBUG)
      Print "Computing explicit helpful conditions\n";
      Let debug_size := 0;
   End -- if debug

   Let j := JNUM;
   While (j)
     Let help[j] := 0;
     Let help1[j] := 0;
     
     Let j := j - 1;
   End --

   Let old_pending := 0;
   Let new_pending := phi;

   While(!(old_pending = new_pending))
      Let old_pending := new_pending;

      Let to_be_removed := 0;

      -- check all justice requirements for MP
      Let j := JNUM;
      While(j)
      --  Let r := rec[j];
        Let r := j;
      --  Let nh := greatest_fixed_point(new_pending,just[r]);
        Let nh := gfp(new_pending,just[r]);
      
        
        If (nh)
          Print r, "\n";
        
          Let help[r] := help[r] | nh;
--          Let new_pending := new_pending & !nh;
--          Break;

          Let to_be_removed := to_be_removed | nh;

        End -- if (nh)
	Let j := j - 1;
      End -- while j

      Let new_pending := new_pending & !to_be_removed;

   End -- while old_pending != new_pending

   If (new_pending & DEBUG)
      Print "Pending is not empty\n";
   Else
      Print "Pending is empty\n";
   End


Let new_pending := 0;
Let old_pending := 0;
Let to_be_removed := 0;

End -- of function compute_helpful


-- =================================================================
-- This function computes the functions delta[k,i].
-- The computation is as follows:
--
-- We take the immediate successors of helpful[k,i] conjuncted with
-- just[k,i] (check that indeed the helpful transition was taken).
-- Take the successors of this set and this is delta[k,i](0)
-- Take the negation of delta[k,i](0) and set it to delta[k,i](1)
-- =================================================================
To compute_delta;
     Let j := JNUM;
     Local tr := total & phi & next(phi);

     While (j)

       Let delta[j][1] := predecessors(help[j],tr);
       Let delta[j][0] := phi & !delta[j][1];
       
--       Let delta[j][0] := successors(help[j],tr) & !help[j];
--       Let delta[j][1] := phi & !delta[j][0];
       
       Let j := j - 1;
     End -- while j

Let temp := 0;

End -- function compute_delta

--===================================================================
--     A   B   S   T   R   A   C   T   I   O   N       P   A   R   T
--===================================================================

To compute_abs;

--=============================================
--  abstract reach 
--=============================================

  Let reach_12 := abstract_with_two(1, 2, reach);

  Let abs_reach := 1;
  Local i := 1;
  While (i <= N - 2)
      Let tr1 := P[1].loc=next(P[i].loc) & P[1].neverl1=next(P[i].neverl1) & P[1].neverl2=next(P[i].neverl2) &
                 P[2].loc=next(P[i+1].loc) & P[2].neverl1=next(P[i+1].neverl1) & P[2].neverl2=next(P[i+1].neverl2) &
                 fork[1]=next(fork[i]) & fork[2]=next(fork[i+1]);
   
    Let reach[i] := succ(tr1, reach_12);
  
    Let abs_reach := abs_reach & reach[i];
    Let i := i + 1;
  End

  Let reach[N - 1] := abstract_with_two(N - 1, N, reach);
  Let reach[N] := abstract_with_two(1, N, reach);

  Let abs_reach := abs_reach & reach[N - 1] & reach[N];


  
--=============================================
--  abstract phi(the pending states)
--=============================================
  Let phi[1] := abstract_with_two(1, 2, phi);
  Let phi[2] := abstract_with_two(2, 3, phi);
  Let phi[3] := abstract_with_two(3, 4, phi);
  Let phi[4] := abstract_with_two(4, 5, phi);
  Let phi[5] := abstract_with_two(5, 6, phi);
  Let phi[6] := abstract_with_two(1, 6, phi);

  Let abs_phi := phi[1] & phi[2] & phi[3] & phi[4] & phi[5] & phi[6];
  
  Let abs_phi_i := abstract_with_one(1, phi) &
                   abstract_with_one(2, phi) &
                   abstract_with_one(3, phi) &
                   abstract_with_one(4, phi) &
                   abstract_with_one(5, phi) &
                   abstract_with_one(6, phi) ;


--=============================================
--  abstract the helpful sets
--=============================================


  Local j := 1;
  While (j <= JNUM)
    Let pj := Jproc[j];

    If (pj > 2)
      Local varset := vset(P[pj - 1].loc, P[pj - 1].neverl2, P[pj].loc, P[pj].neverl2, fork[pj]);

      Let abs_help[j] := help[j] forsome set_minus(_vars, varset);
--      Let abs_delta[j][0] := delta[j][0] forsome set_minus(_vars, varset);
      Let abs_delta[j][1] := delta[j][1] forsome set_minus(_vars, varset);
    Else
      Local varset := vset(P[pj].loc, P[pj].neverl2);

      Let abs_help[j] := help[j] forsome set_minus(_vars, varset); 
--      Let abs_delta[j][0] := delta[j][0] forsome set_minus(_vars, varset);
      Let abs_delta[j][1] := delta[j][1] forsome set_minus(_vars, varset);
    End

    Let j := j + 1;
  End

  Local j := 1;
  While (j <= JNUM)
--    Let abs_delta[j][1] := abs_phi & !abs_delta[j][0];
    Let abs_delta[j][0] := abs_phi & !abs_delta[j][1];
    Let j := j + 1;
  End
  
  
  Local j := 1;
  While (j <= JNUM)
    If (help[j] & !abs_help[j])
      Print "***",j,"***\n";
    End
    Let j := j + 1;
  End
  
End


Func pro(from, to, to_b_abs);
      Let tr1 := P[from].loc=next(P[to].loc)			&
                 P[from].neverl1=next(P[to].neverl1) 	&
                 P[from].neverl2=next(P[to].neverl2) 	&
                 fork[from]=next(fork[to]);
      Return succ(tr1, to_b_abs);
End


Func abstract_with_one(proc1, to_b_abs);
--  Let not_setproc := set_minus(_vars, vset(P[proc1].loc, P[proc1].neverl1, P[proc1].neverl2));
  Let not_setproc := set_minus(_vars, setproc[proc1]);
  
  Local ret := to_b_abs forsome not_setproc;
  Return ret;
End


Func abstract_with_two(proc1, proc2, to_b_abs);
  Let not_setproc := set_minus(_vars, setproc[proc1]);
  Let not_setproc := set_minus(not_setproc, setproc[proc2]);
  
  Local ret := to_b_abs forsome not_setproc;
  Return ret;
End


Func abstract_with_three(proc1, proc2, proc3, to_b_abs);
  Let not_setproc := set_minus(_vars, setproc[proc1]);
  Let not_setproc := set_minus(not_setproc, setproc[proc2]);
  Let not_setproc := set_minus(not_setproc, setproc[proc3]);
  
  Local ret := to_b_abs forsome not_setproc;
  Return ret;
End



To check_overlap;
  Print "Check Overlapping abstract helpful\n";
  Local j := JNUM;
  While(j)
    Local i := JNUM;
    While(i)
      If (abs_h[j] & abs_h[i])
        Print j, " & ", i, "\n";
      End
      Let i := i - 1;
    End
    Let j := j - 1;
  End
End
 

To use_concrete;

  Local j := 1;
  While (j <= JNUM)
    Let abs_help[j] := help[j];
    Let abs_delta[j][1] := delta[j][1];
    Let abs_delta[j][0] := delta[j][0];
    Let j := j + 1;
  End
End


-- =================================================================
-- Execution phase
-- =================================================================

Run initialization;
Run initialize_justice;
        -- Settime;
-- Run compute_explicit_helpful;
        -- Print "computing explicit helpful took:\n";
        -- Chktime;

-- Run collect_helpful;

   Run compute_helpful;
        -- Settime;
   Run compute_delta;
        -- Print "computing delta took:\n";
        -- Chktime;

   Run compute_abs;