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

-- Load "constants.pf";

-- ===================================================
-- initialization of p,q,phi(pending states),reach,q_free
-- ===================================================

To initialization;

   Let DEBUG := 1;
   Let DEBUG_BDD := 0;
   Let NUMBER_OF_PROCESSES := N;

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

   Let NUMBER_OF_LOCATIONS := 4;
   Let JNUM := N * 4;

   -- ======================
   -- the properties p and q
   -- ======================
   Let p := loc[1]=1;
   Let q := loc[1]=3;
   
   
   Let PID := 1; -- 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] := 4;
      End
      Let Jproc[j] := (j - 1) / NUMBER_OF_LOCATIONS + 1;
      
      Let j := j + 1;
   End

   --========================================================
   -- setproc[i] is a set of variables related to process i
   --========================================================
   Local i := 1;
   While (i <= NUMBER_OF_PROCESSES)
      Let setproc[i] := vset(loc[i], y[i], min_id);
      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

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


--=============================================
-- To compute the gfp of the formula topdown
--=============================================
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";
   End -- if debug

   Let j := 1;
   While (j<=JNUM)
     Let help[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 := 1;
      While(j<=JNUM)
      --  Let nh := greatest_fixed_point(new_pending,just[j]);
        Let nh := gfp(new_pending,just[j]);
        
        If (nh)
          Let help[j] := help[j] | nh;
          Let new_pending := new_pending & !nh;
                    
          Break;
        End -- if (nh)
	Let j := j + 1;
      End -- while j

   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 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 i1 := 1;
  While (i1 <= N)
  
    Local i2 := i1 + 1;
    While(i2 <= N)
      Let abs_reach := abs_reach & project2(1,i1,2,i2,reach_12);
      Let i2 := i2 + 1;
    End
    
    Let i1 := i1 + 1;
  End


--=============================================
--  abstract phi(the pending states)
--=============================================

  Let abs_phi := abstract_with_one(PID, phi);
  Let abs_phi := abs_phi & abs_reach;



--=============================================
--  abstract the helpful and delta
--=============================================

--*** For the special process ***
  
  Local sample := 2;
  Local j := 1;
  While (j <= NUMBER_OF_LOCATIONS)
    Local s1 := abstract_with_one(sample, help[j]);
    Local d1 := abstract_with_one(sample, delta[j][1]);
--    Local d1 := abstract_with_one(sample, delta[j][0]);
    
    Let abs_help[j] := 1;
    Let abs_delta[j][1] := 1;


    Local i := 1;
    While (i <= N)
      If (i != PID)
        Let abs_help[j] := abs_help[j] & project1(sample, i, s1);
        Let abs_delta[j][1] := abs_delta[j][1] & project1(sample, i, d1);

      Else
        Let abs_help[j] := abs_help[j] & abstract_with_one(PID, help[j]);
        Let abs_delta[j][1] := abs_delta[j][1] & abstract_with_one(PID, delta[j][1]);

      End
    
      Let i := i + 1;
    End
    
    Let abs_delta[j][0] := abs_phi & !abs_delta[j][1];

    Let j := j + 1;
  End

--*** For other processes ***
-- special process is process 1
  
  Local sample_jproc := 2;
  Local sample := 3;

  Local j := 1;
  While (j <= 4)
    
    Let s[j mod 4]  := abstract_with_one(sample, help[4+j]);
    Let sj[j mod 4] := abstract_with_one(sample_jproc, help[4+j]);
    Let ss[j mod 4] := abstract_with_one(PID, help[4+j]);
    
    Let d[j mod 4]  := abstract_with_one(sample, delta[4+j][1]);
    Let dj[j mod 4] := abstract_with_one(sample_jproc, delta[4+j][1]);
    Let dd[j mod 4] := abstract_with_two(sample_jproc, PID, delta[4+j][1]);
  
    Let j := j + 1;
  End


  Let j := 5;
  While(j <= JNUM)
    Let jproc := Jproc[j];

    Let abs_help[j] := 1;
    Let abs_delta[j][1] := 1;
    
    Let i := 1;
    While (i <= N)
          
      If (i=PID)
        Let abs_help[j] := abs_help[j] & project1(PID, PID, ss[j mod 4]);
        Let abs_delta[j][1] := abs_delta[j][1] & project2(sample_jproc, jproc, PID, PID, dd[j mod 4]);

      Else
        If (i=jproc)
          Let abs_help[j] := abs_help[j] & project1(sample_jproc, jproc, sj[j mod 4]);
          Let abs_delta[j][1] := abs_delta[j][1] & project1(sample_jproc, jproc, dj[j mod 4]);

        Else
          Let abs_help[j] := abs_help[j] & project1(sample, i, s[j mod 4]);
          Let abs_delta[j][1] := abs_delta[j][1] & project1(sample, i, d[j mod 4]);

        End
      End
      
      Let i := i + 1;
    End
 
    Let abs_delta[j][0] := abs_phi & !abs_delta[j][1];
    
    Let j := j + 1;
  End
  

End


Func project1(from, to, to_b_proj);
  Let tr1 := loc[from]=next(loc[to]) & 
             y[from]=next(y[to]) &
             (min_id=from <-> next(min_id)=to);
  Let ret := succ(tr1, to_b_proj);
  Return ret;
End


Func project2(from1, to1, from2, to2, to_b_proj);
  Let tr1 := loc[from1]=next(loc[to1]) & 
             y[from1]=next(y[to1]) &
             loc[from2]=next(loc[to2]) & 
             y[from2]=next(y[to2]) &
             (min_id=from1 <-> next(min_id)=to1) &
             (min_id=from2 <-> next(min_id)=to2);
  Let ret := succ(tr1, to_b_proj);
  Return ret;
End

 
Func abstract_with_one(proc1, to_b_abs);
  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 set_assertion;
  Let i := N;
  While (i)
   If (i=1)
     Let abs_help[1] := loc[1]=1;
     Let abs_help[2] := loc[1]=2 & min_id=1;
     Let abs_help[3] := 0;
     Let abs_help[4] := 0;

     Let abs_delta[1][1] := loc[1]=1;
     Let abs_delta[2][1] := loc[1] in {1,2};
     Let abs_delta[3][1] := 0;
     Let abs_delta[4][1] := 0;
   Else
     Let j := (i - 1) * 4;
     Let abs_help[j+1] := 0;
     Let abs_help[j+2] := loc[1]=2 & min_id=i & loc[i]=2;
     Let abs_help[j+3] := loc[1]=2 & loc[i]=3;
     Let abs_help[j+4] := loc[1]=2 & loc[i]=4;

     Let abs_delta[j+1][1] := 0;
     Let abs_delta[j+1][2] := loc[1]=1 | loc[1]=2 & loc[i]=2 & y[1]>y[i];
     Let abs_delta[j+1][3] := loc[1]=1 | loc[1]=2 & loc[i] in {2,3} & y[1]>y[i];
     Let abs_delta[j+1][4] := loc[1]=1 | loc[1]=2 & loc[i] in {2,3,4} & y[1]>y[i];
   End -- If (i=1)
  
   Let i := i - 1;
  End -- While (i)
  
  Let j := JNUM;
  While (j)
    Let abs_delta[j][0] := abs_phi & !abs_delta[j][1];
    Let j := j - 1;
  End
End


--=================================================================
-- Check deductive liveness rules DISTRANK
--=================================================================

--=================================================================
-- inv & total -> inv'
--=================================================================
To check_inv;
  Let inv := abs_reach;
  Let counter := inv & total & !next(inv);
  If (counter)
    Print "\n inv assertion is not inductive\n";
    Print "\n Counter example follows\n";
    Print counter;
  Else
    Print "\n inv assertion are inductive\n";
  End -- If (counter)
End -- check_inv

--=================================================================
-- D1: p & inv -> q | pend
--=================================================================
To check_D1;
  Let inv := abs_reach;
  Let pend := abs_phi;
  Let counter := p & inv & !q & !pend;
  If (counter)
    Print "\n D1: p & inv -> q | pend is not valid.\n";
    Print "\n Counter example follows\n";
    Print counter;
  Else
    Print "\n D1: p & inv -> q | pend is valid.\n";
  End
End -- check_D1

--=================================================================
-- D2: pend & total -> pend' | q'
--=================================================================
To check_D2;

  Let pend := abs_phi;
  Let counter := pend & total & !next(pend | q);
  If (counter)
    Print "\n D2: pend & total -> pend' | q' is not valid.\n";
    Print "\n Counter example follows\n";
    Print counter;
  Else
    Print "\n D2: pend & total -> pend' | q' is valid.\n";
  End
End -- check_D2

--=================================================================
-- D3: pend -> \exists j: h(j)
--=================================================================
To check_D3;

  Let pend := abs_phi;

  Let ex_help := 0;
  Let j := 1;
  While (j <= JNUM)
    Let ex_help := ex_help | abs_help[j];
    Let j := j + 1;
  End

  Let counter := pend & !ex_help;
  If (counter)
    Print "\n D3: pend -> \exists j: h(j) is not valid.\n";
    Print "\n Counter example follows\n";
    Print counter;
  Else
    Print "\n D3: pend -> \exists j: h(j) is valid.\n";
  End
End -- check_D3

--=================================================================
-- D4: pend & total -> q' | \forall j: \delta'(j) >= \delta(j)
--=================================================================
To check_D4;

  Let pend := abs_phi;

  Let forall_delta_ge := 1;
  Let j := 1;
  While (j <= JNUM)
    Let forall_delta_ge := forall_delta_ge & abs_delta[j][1] | next(abs_delta[j][0]);
    Let j := j + 1;
  End

  Let counter := pend & total & !next(q) & !forall_delta_ge;
  If (counter)
    Print "\n D4 pend & total -> q' | \forall j: \delta'(j) >= \delta(j) is not valid.\n";
    Print "\n Counter example follows\n";
    Print counter;
  Else
    Print "\n D4 pend & total -> q' | \forall j: \delta'(j) >= \delta(j) is valid.\n";
  End
End -- check_D4

--====================================================================
-- D5: \forall j: h(j) & total -> q' | h'(j) | \delta'(j) > \delta(j)
--====================================================================
-- since h(j) is too "abstract", we need to take pend as one conjuncts
To check_D5;

  Let D5_valid := 1;
  Let pend := abs_phi;

  Let j := 1;
  While (j <= JNUM)
    Let delta_dec[j] := abs_delta[j][1] & next(abs_delta[j][0]);
    Let counter := pend & abs_help[j] & total & !next(q) & !next(abs_help[j]) & !delta_dec[j];

    If (counter)
      Print "\n \delta[",j,"] does not strictly decrease. D5 is not valid.\n";
      Print "\n Counter example follows\n";
      Print counter;
      Let D5_valid := 0;
    End -- If (counter)

    Let j := j + 1;
  End -- While

  If (D5_valid)
    Print "\n D5: pend & total -> next(q) | \forall j: \delta'(j) >= \delta(j) is valid.\n";
  End

End -- check_D5

--=================================================================
-- D6: \forall j: h(j) -> !J(j)
--=================================================================
To check_D6;
  Let D6_valid := 1;
  Let pend := abs_phi;

  Let j := 1;
  While (j <= JNUM)
    Let counter := pend & abs_help[j] & _j[j];
    
    If (counter)
      Print "\n h(",j,") does not violate Justice.\n";
      Print "Counter example follows\n";
      Print counter;
      Let D6_valid := 0;
    End

    Let j := j + 1;
  End
  
  If (D6_valid)
    Print "\n D6: \forall j: h(j) -> !J(j) is valid.\n";
  End

End -- check_D6

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

Run initialization;
Run initialize_justice;

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

   Run compute_abs;
   
   Run check_inv;
   Run check_D1;
   Run check_D2;
   Run check_D3;
   Run check_D4;
   Run check_D5;
   Run check_D6;