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

Load "constants.pf";

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

Func predecessor_states(states, rel);
  Local new := states;
  Local old := 0;
  While (!(old=new))
    Local fr := new & !old;
    Let old := new;
    Let new := pred(rel, fr) | new;
  End
  Return new;
End

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

To initialization;

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

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

   -- z is the id of the special process
   Let z := 4;

   -- ======================
   -- the properties p and q
   -- ======================
   Let p := loc[z]=1;
   Let q := loc[z]=2;
   
   
   Let reach:=reachable_states(_i,total);

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

   -- ===============================================================
   -- The set of pending states. all states that are reachable from a
   -- reachable p state along a q free path
   -- ===============================================================
   Let phi := reachable_states(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 - 1) mod NUMBER_OF_LOCATIONS;

      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], c[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 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 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

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 & prime(phi);

     While (j)
       Let delta[j][1] := predecessor_states(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)
    Let 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

  -- to prove the liveness, \exists quantifier is also needed
  Let rem := abs_reach & !reach;
  Let rem_1 := abstract_with_one(1,rem);
  
  Let abs_rem := 1;
  Local i := 1;
  While (i <= N)
    Let abs_rem := abs_rem & project1(1,i,rem_1);
    Let i := i + 1;
  End
  
  Let abs_reach := abs_reach & !abs_rem;

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

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



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

--*** For the special process z ***
--*** z=4

  Local sample := 2;
  Local j := 1;
  
  While (j <= NUMBER_OF_LOCATIONS)
    Local jj := (z - 1) * NUMBER_OF_LOCATIONS + j;

    Local help_z := abstract_with_one(z, help[jj]);
    Local help_s := abstract_with_one(sample, help[jj]);
    
    Local delta_z := abstract_with_one(z, delta[jj][1]);
    Local delta_s := abstract_with_one(sample, delta[jj][1]);
    
    Let abs_help[jj] := 1;
    Let abs_delta[jj][1] := 1;
    
    Local i := 1;
    While (i <= N)
      If (i = z)
        Let abs_help[jj] := abs_help[jj] & help_z;
        Let abs_delta[jj][1] := abs_delta[jj][1] & delta_z;
      Else
        Let abs_help[jj] := abs_help[jj] & project1(sample, i, help_s);
        Let abs_delta[jj][1] := abs_delta[jj][1] & project1(sample, i, delta_s);
      End
    
      Let i := i + 1;
    End
    
    Let abs_delta[jj][0] := abs_phi & !abs_delta[jj][1];
    Let j := j + 1;
  End

--*** For other processes jproc \ne z ***
-- special process is z = 4

-- for helpful assertions, we have 3 different cases:
-- process z
-- process jproc
-- processes other than z and jproc (sample1)

-- for ranking function delta, we have 4 different situations:
-- process z
-- process jproc
-- those processes token will pass through when going from jproc to z (sample1)
-- those processes token will pass through when going from z to jproc (sample2)
  
  Let sample_jproc := 1;
  Let sample1 := z - 1;	-- sample1 \in (jproc,z)
  Let sample2 := z + 1;	-- sample2 \in (z,jproc)
  
  Local low := (sample_jproc - 1) * NUMBER_OF_LOCATIONS + 1;
  Local high := sample_jproc * NUMBER_OF_LOCATIONS;
  Local j := low;
  While (j <= high)
    Local j1 := j mod NUMBER_OF_LOCATIONS;

    Let help_z [j1] := abstract_with_one(z, help[j]);
    Let help_j [j1] := abstract_with_one(sample_jproc, help[j]);
    Let help_s1[j1] := abstract_with_one(sample1, help[j]);
    
    Let delta_z[j1] := abstract_with_one(z, delta[j][1]);
    Let delta_j[j1] := abstract_with_one(sample_jproc, delta[j][1]);
    Let delta_s1[j1] := abstract_with_one(sample1, delta[j][1]);
    Let delta_s2[j1] := abstract_with_one(sample2, delta[j][1]);
  
    Let j := j + 1;
  End


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

    If (jproc=z)
      Let j := j + 1;
      Continue;
    End

    Let abs_help[j] := 1;
    Let abs_delta[j][1] := 1;
    Local j1 := j mod NUMBER_OF_LOCATIONS;

    Let i := 1;
    While (i <= N)

      If (i=z)
        Let abs_help[j] := abs_help[j] & help_z[j1];
        Let abs_delta[j][1] := abs_delta[j][1] & delta_z[j1];
      Else
        If (i=jproc)
          Let abs_help[j] := abs_help[j] & project1(sample_jproc, jproc, help_j[j1]);
          Let abs_delta[j][1] := abs_delta[j][1] & project1(sample_jproc, jproc, delta_j[j1]);    
        Else
          Let abs_help[j] := abs_help[j] & project1(sample1,i,help_s1[j1]);

          If ((jproc < i & i < z) | (z < jproc & (i<z | jproc<i)))
            Let abs_delta[j][1] := abs_delta[j][1] & project1(sample1, i, delta_s1[j1]);
          Else
            Let abs_delta[j][1] := abs_delta[j][1] & project1(sample2, i, delta_s2[j1]);
          End
        End
      End
      
      Let i := i + 1;
    End
 
    Let abs_delta[j][0] := abs_phi & !abs_delta[j][1];

    
    Let j := j + 1;
  End
  

End


-- transform to_b_proj(from) to to_b_proj(to)
Func project1(from, to, to_b_proj);
  Let tr1 := loc[from]=next(loc[to]) & c[from]=next(c[to]);
  Let ret := succ(tr1, to_b_proj);
  Return ret;
End

-- transform to_b_proj(from1,from2) to to_b_proj(to1,to2)
Func project2(from1, to1, from2, to2, to_b_proj);
  Let tr1 := loc[from1]=next(loc[to1]) & c[from1]=next(c[to1]) &
             loc[from2]=next(loc[to2]) & c[from2]=next(c[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



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

--=================================================================
-- inv & total -> inv'
--=================================================================
To check_inv;
  Let inv := abs_reach;
  Let counter := inv & total & !prime(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 & !prime(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] | prime(abs_delta[j][0]);
    Let j := j + 1;
  End

  Let counter := pend & total & !prime(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] & prime(abs_delta[j][0]);
    Let counter := pend & abs_help[j] & total & !prime(q) & !prime(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 -> prime(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;