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

-- ===================================================
-- initialization of p,q,phi,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 z := 1; -- check liveness for process z


   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]);
      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 number_of_states(f);
   Local count := 0;
   Local my_f := f;
   While (my_f)
      Local s := fsat(my_f);
      Let my_f := my_f & !s;
      Let count := count + 1;
      Print count, "\n";
   End
   Return count;
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) & my_cep(!all_states);
	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 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

   Print "Finishing computing explicit helpful conditions:\n";
   If (new_pending & DEBUG)
      Print " ** Pending is not empty **\n";
   Else
      Print " ** Pending is empty **\n";
   End
   Print "\n";

--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;
     Print "Computing ranking function\n";

     Let j := JNUM;
     Local tr := total & phi & next(phi);

     While (j)
--       Let delta[j] := predecessors(help[j],tr);

       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;

  Print "computing symbolic(abstract) assertions.\n";

--=============================================
--  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(z, 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_two(z, sample, help[j]);
    Local d1 := abstract_with_two(z, sample, delta[j][1]);
    
    Let abs_help[j] := 1;
    Let abs_delta[j][1] := 1;
    
    Local i := 1;
    While (i <= N)
      If (i != z)
        Let abs_help[j] := abs_help[j] & project2(z,z,sample,i,s1);
        Let abs_delta[j][1] := abs_delta[j][1] & project2(z,z,sample,i,d1);
      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_two(sample_jproc, sample, help[4+j]);
    Let ss[j mod 4] := abstract_with_two(sample_jproc, z, help[4+j]);
    
    Let d[j mod 4]  := abstract_with_two(sample_jproc, sample, delta[4+j][1]);
    Let dd[j mod 4] := abstract_with_two(sample_jproc, z, 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=z)
        Let abs_help[j] := abs_help[j] & project2(sample_jproc, jproc, z, z, ss[j mod 4]);
        Let abs_delta[j][1] := abs_delta[j][1] & project2(sample_jproc, jproc, z, z, dd[j mod 4]);
      Else
        If (i != jproc)
          Let abs_help[j] := abs_help[j] & project2(sample_jproc, jproc, sample, i, s[j mod 4]);
          Let abs_delta[j][1] := abs_delta[j][1] & project2(sample_jproc, jproc, 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]) ;
  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]) ;
  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


--=================================================================
-- Check deductive liveness rules PRE-RANK
--=================================================================

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

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

--=================================================================
-- R2: pend & total -> pend' | q'
--=================================================================
To check_R2;

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

--=================================================================
-- We can no longer use D3: pend -> \exists j: h(j), 
-- because D3 is not AE-formula
-- Instead, we define pre-order i \preceq j as
-- Define i << j as 
-- ((!h[j]&pend) W (h[i]&pend)) | !((!h[i]&pend) W (h[j]&pend))
-- and check
-- R5: \forall j: pend & \forall i: j \preceq i -> h(j)
--=================================================================
-- weak until
--=================================================================
Func unless(p1,p2);

  Local old := FALSE;
  Local new := phi & (p1 | p2);
  While (!(old=new))
    Let old := new;
    Local ax := new | !phi;
    Let new := new & (!pred(total,!ax) | p2);
  End
  Return new;

End -- unless


To check_preorder_reflexion;

  Let premiset := 1;
  
  Let j := JNUM;
  While(j)
    
     Let counter := abs_phi & !rel[j][j];
     If (counter)
       Print "\n ",j ,"\preceq ",j,"does not hold at the following state:\n";
       Print counter;
       Let premiset := 0;
     End -- if implies 

     Let j := j - 1;
   End -- while j


   If (premiset)
      Print "\n Relation is reflexive.\n";
   Else
      Print "\n Relation is not reflexive.\n";
   End

Let premiset := 0;
Let implies := 0;

End -- check_preorder_reflexion


To check_preorder_completeness;

   Let premiset := 1;
   
   Let j := JNUM;
   While(j)

     Local k := JNUM;
     While(k)
       Let counter := abs_phi & !rel[j][k] & !rel[k][j];
       If (counter)
        Print "\n Neither ",j," \preceq ",k," nor ",k," \preceq ",j," holds at the following state:\n";
        Print counter;
        Let premiset := 0;
       End

       Let k := k - 1;
     End
     
     Let j := j - 1;
   End -- while j

   If (premiset)
      Print "\n Relation is complete.\n";
   Else
      Print "\n Relation is not complete.\n";
   End

Let premiset := 0;
Let implies := 0;

End -- check_preorder_completeness


To check_preorder_transitivity;

   Let premiset := 1;
   
   Let j := JNUM;
   While(j)
   
     Let j1 := JNUM;
     While(j1)

       Let exists_rel[j][j1] := 0;
       Local k := JNUM;
       While(k)
         Let exists_rel[j][j1] := exists_rel[j][j1] | (rel[j][k] & rel[k][j1]);
         Let k := k - 1;
       End
     
       Let counter := (abs_phi & exists_rel[j][j1]) & ! rel[j][j1];
     
       If (counter)
         Print "\n \preceq is not transitive at the state: \n";
         Print counter;
         Let premiset := 0;
       End -- if implies 
       
       Let j1 := j1 - 1;
     End

     Let j := j - 1;
   End -- while j


   If (premiset)
      Print "\n Relation is transitive.\n";
   Else
      Print "\n Relation is not transitive.\n";
   End

Let premiset := 0;
Let implies := 0;

End -- check_preorder_transitivity



To compute_preorder;

  Print "\n computing preorder \n";

  Local i := 1;
  While (i <= JNUM)
    Local j := 1;
    While (j <= JNUM)
      Let w[i][j] := unless(!help[j],help[i]);
      Let j := j + 1;
    End
    Let i := i + 1;
  End

  Local i := 1;
  While (i <= JNUM)
    Local j := 1;
    While (j <= JNUM)

     -- concrete \prereq
--      Let rel[i][j] := w[i][j] | !w[j][i];
      
     -- abstract \prereq
      Let rel[i][j] := (abstract_with_three(1,Jproc[i],Jproc[j],w[i][j]) | 
                       !abstract_with_three(1,Jproc[i],Jproc[j],w[j][i])) & phi;

      Let j := j + 1;
    End
    Let i := i + 1;
  End
  
  Print " Finished computing preorder\n";
  Run check_preorder_reflexion;
  Run check_preorder_completeness;
  Run check_preorder_transitivity;

End

--===================================================================================
-- check R3
--===================================================================================
To check_R3;

  Run compute_preorder;

  Let pend := abs_phi;

  Let R3_valid := 1;

   Let j := JNUM;
   While(j)

     Let min[j] := 1;
     Local k := JNUM;
     While(k)
       Let min[j] := min[j] & rel[j][k];
       Let k := k - 1;
     End
     
     Let counter := pend & min[j] & !abs_help[j];
     
     If (counter)
       Print "\n R3 is not true for ",j,"\n";
       Print "\n Counter example follows\n";
       Print counter;
       Let R5_valid := 0;
     End -- if (counter)

     Let j := j - 1;
   End -- while j

  If (R3_valid)
    Print "\n R3: \forall j: pend & \forall i: j \preceq i -> h(j) is valid.\n";
  End
End -- check_R3

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

  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 R4 pend & total -> q' | \forall j: \delta'(j) >= \delta(j) is not valid.\n";
    Print "\n Counter example follows\n";
    Print counter;
  Else
    Print "\n R4 pend & total -> q' | \forall j: \delta'(j) >= \delta(j) is valid.\n";
  End
End -- check_R4

--====================================================================
-- R5: \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_R5;

  Let R5_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 R5_valid := 0;
    End -- If (counter)

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

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

End -- check_R5

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

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

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

End -- check_R6



-- =================================================================
-- 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_R1;
   Run check_R2;
   Run check_R3;
   Run check_R4;
   Run check_R5;
   Run check_R6;