% lamport-shostak ls_syn.sal

ls_syn_with_nil_liar_changes_initialized: CONTEXT = 

BEGIN
  N: NATURAL = 4 ;	% Number of nodes/processes
  Node: TYPE = [1..N];	% Nodes are named 1..N

  % Information Unit being sent (nil and nil2 are synonyms)
  CHInfoUnit: TYPE = {zero, one, nil, nil2};
    
  % Information Unit being stored in each component of the consistency vector
  CVInfoUnit: TYPE = CHInfoUnit;

  element[i: Node]: MODULE = 
  BEGIN
    % consistency vector of the ith node
    OUTPUT consistencyVector_i: ARRAY [1..N] OF CVInfoUnit
    % Input of the ith node
    INPUT input_i: ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit
    INPUT cvUpdate_zero_nil_zero_zero, cvUpdate_zero_zero_nil_nil, cvUpdate_zero_nil_zero_nil, cvUpdate_nil_zero_zero_nil, cvUpdate_one_nil_zero_one, cvUpdate_nil_nil_zero_one, cvUpdate_zero_one_one_one, cvUpdate_one_one_one_one, cvUpdate_one_zero_zero_nil, cvUpdate_one_zero_one_one, cvUpdate_zero_nil_one_one, cvUpdate_nil_zero_zero_zero, cvUpdate_one_nil_one_one, cvUpdate_nil_one_zero_nil, cvUpdate_zero_nil_nil_nil, cvUpdate_zero_one_zero_zero, cvUpdate_one_zero_zero_zero, cvUpdate_one_one_zero_zero, cvUpdate_nil_zero_nil_nil, cvUpdate_zero_one_nil_nil, cvUpdate_nil_nil_zero_nil, cvUpdate_nil_one_one_one, cvUpdate_zero_nil_zero_one, cvUpdate_one_zero_nil_nil, cvUpdate_nil_nil_nil_nil, cvUpdate_zero_zero_one_one, cvUpdate_zero_one_zero_one, cvUpdate_one_one_zero_nil, cvUpdate_one_one_zero_one, cvUpdate_one_zero_one_nil, cvUpdate_nil_zero_one_nil, cvUpdate_nil_nil_one_nil, cvUpdate_zero_zero_zero_nil, cvUpdate_nil_nil_one_one, cvUpdate_zero_zero_zero_one, cvUpdate_zero_one_one_nil, cvUpdate_zero_nil_one_nil, cvUpdate_zero_zero_zero_zero, cvUpdate_one_one_one_nil, cvUpdate_nil_one_zero_one, cvUpdate_zero_zero_one_nil, cvUpdate_one_one_nil_nil, cvUpdate_one_zero_zero_one, cvUpdate_one_nil_one_nil, cvUpdate_nil_one_nil_nil, cvUpdate_one_nil_nil_nil, cvUpdate_nil_nil_zero_zero, cvUpdate_zero_one_zero_nil, cvUpdate_nil_one_one_nil, cvUpdate_nil_zero_zero_one, cvUpdate_nil_one_zero_zero, cvUpdate_nil_zero_one_one, cvUpdate_one_nil_zero_zero, cvUpdate_one_nil_zero_nil: CVInfoUnit

    
    % The initial state of each consistency vector is nil for all positions except the ith
    INITIALIZATION consistencyVector_i IN 
        {a: ARRAY [1..N] OF CVInfoUnit | (a[i] = zero OR a[i] = one) AND FORALL (j:[1..N]): j/=i => a[j] = nil} 

    TRANSITION
  
    [  FORALL (j:[1..N]):
         ((j=i => consistencyVector_i'[j]=consistencyVector_i[j])
       AND
         (j/=i =>
         FORALL (k:[1..N]):FORALL (l:[1..N]): 
         (k/=i AND l/=i AND j/=k AND j/=l AND k/=l =>
%case #1
                (consistencyVector_i'[j] = cvUpdate_one_one_one_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #2
                (consistencyVector_i'[j] = cvUpdate_one_one_zero_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #3
                (consistencyVector_i'[j] = cvUpdate_one_one_one_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #4
                (consistencyVector_i'[j] = cvUpdate_one_one_zero_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #5
                (consistencyVector_i'[j] = cvUpdate_one_one_zero_zero AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #6
                (consistencyVector_i'[j] = cvUpdate_one_one_zero_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #7
                (consistencyVector_i'[j] = cvUpdate_one_one_one_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #8
                (consistencyVector_i'[j] = cvUpdate_one_one_zero_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #9
                (consistencyVector_i'[j] = cvUpdate_one_one_nil_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #10
                (consistencyVector_i'[j] = cvUpdate_one_zero_one_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #11
                (consistencyVector_i'[j] = cvUpdate_one_zero_zero_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #12
                (consistencyVector_i'[j] = cvUpdate_one_zero_one_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #13
                (consistencyVector_i'[j] = cvUpdate_one_zero_zero_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #14
                (consistencyVector_i'[j] = cvUpdate_one_zero_zero_zero AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #15
                (consistencyVector_i'[j] = cvUpdate_one_zero_zero_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #16
                (consistencyVector_i'[j] = cvUpdate_one_zero_one_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #17
                (consistencyVector_i'[j] = cvUpdate_one_zero_zero_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #18
                (consistencyVector_i'[j] = cvUpdate_one_zero_nil_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #19
                (consistencyVector_i'[j] = cvUpdate_one_nil_one_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #20
                (consistencyVector_i'[j] = cvUpdate_one_nil_zero_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #21
                (consistencyVector_i'[j] = cvUpdate_one_nil_one_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #22
                (consistencyVector_i'[j] = cvUpdate_one_nil_zero_one AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #23
                (consistencyVector_i'[j] = cvUpdate_one_nil_zero_zero AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #24
                (consistencyVector_i'[j] = cvUpdate_one_nil_zero_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #25
                (consistencyVector_i'[j] = cvUpdate_one_nil_one_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #26
                (consistencyVector_i'[j] = cvUpdate_one_nil_zero_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #27
                (consistencyVector_i'[j] = cvUpdate_one_nil_nil_nil AND
                 (input_i[j][j] = one) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #28
                (consistencyVector_i'[j] = cvUpdate_zero_one_one_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #29
                (consistencyVector_i'[j] = cvUpdate_zero_one_zero_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #30
                (consistencyVector_i'[j] = cvUpdate_zero_one_one_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #31
                (consistencyVector_i'[j] = cvUpdate_zero_one_zero_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #32
                (consistencyVector_i'[j] = cvUpdate_zero_one_zero_zero AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #33
                (consistencyVector_i'[j] = cvUpdate_zero_one_zero_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #34
                (consistencyVector_i'[j] = cvUpdate_zero_one_one_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #35
                (consistencyVector_i'[j] = cvUpdate_zero_one_zero_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #36
                (consistencyVector_i'[j] = cvUpdate_zero_one_nil_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #37
                (consistencyVector_i'[j] = cvUpdate_zero_zero_one_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #38
                (consistencyVector_i'[j] = cvUpdate_zero_zero_zero_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #39
                (consistencyVector_i'[j] = cvUpdate_zero_zero_one_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #40
                (consistencyVector_i'[j] = cvUpdate_zero_zero_zero_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #41
                (consistencyVector_i'[j] = cvUpdate_zero_zero_zero_zero AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #42
                (consistencyVector_i'[j] = cvUpdate_zero_zero_zero_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #43
                (consistencyVector_i'[j] = cvUpdate_zero_zero_one_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #44
                (consistencyVector_i'[j] = cvUpdate_zero_zero_zero_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #45
                (consistencyVector_i'[j] = cvUpdate_zero_zero_nil_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #46
                (consistencyVector_i'[j] = cvUpdate_zero_nil_one_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #47
                (consistencyVector_i'[j] = cvUpdate_zero_nil_zero_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #48
                (consistencyVector_i'[j] = cvUpdate_zero_nil_one_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #49
                (consistencyVector_i'[j] = cvUpdate_zero_nil_zero_one AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #50
                (consistencyVector_i'[j] = cvUpdate_zero_nil_zero_zero AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #51
                (consistencyVector_i'[j] = cvUpdate_zero_nil_zero_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #52
                (consistencyVector_i'[j] = cvUpdate_zero_nil_one_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #53
                (consistencyVector_i'[j] = cvUpdate_zero_nil_zero_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #54
                (consistencyVector_i'[j] = cvUpdate_zero_nil_nil_nil AND
                 (input_i[j][j] = zero) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #55
                (consistencyVector_i'[j] = cvUpdate_nil_one_one_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #56
                (consistencyVector_i'[j] = cvUpdate_nil_one_zero_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #57
                (consistencyVector_i'[j] = cvUpdate_nil_one_one_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #58
                (consistencyVector_i'[j] = cvUpdate_nil_one_zero_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #59
                (consistencyVector_i'[j] = cvUpdate_nil_one_zero_zero AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #60
                (consistencyVector_i'[j] = cvUpdate_nil_one_zero_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #61
                (consistencyVector_i'[j] = cvUpdate_nil_one_one_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #62
                (consistencyVector_i'[j] = cvUpdate_nil_one_zero_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #63
                (consistencyVector_i'[j] = cvUpdate_nil_one_nil_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = one) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #64
                (consistencyVector_i'[j] = cvUpdate_nil_zero_one_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #65
                (consistencyVector_i'[j] = cvUpdate_nil_zero_zero_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #66
                (consistencyVector_i'[j] = cvUpdate_nil_zero_one_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #67
                (consistencyVector_i'[j] = cvUpdate_nil_zero_zero_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #68
                (consistencyVector_i'[j] = cvUpdate_nil_zero_zero_zero AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #69
                (consistencyVector_i'[j] = cvUpdate_nil_zero_zero_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #70
                (consistencyVector_i'[j] = cvUpdate_nil_zero_one_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #71
                (consistencyVector_i'[j] = cvUpdate_nil_zero_zero_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #72
                (consistencyVector_i'[j] = cvUpdate_nil_zero_nil_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = zero) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #73
                (consistencyVector_i'[j] = cvUpdate_nil_nil_one_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = one))
              OR
               %case #74
                (consistencyVector_i'[j] = cvUpdate_nil_nil_zero_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = zero))
              OR
               %case #75
                (consistencyVector_i'[j] = cvUpdate_nil_nil_one_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = one) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #76
                (consistencyVector_i'[j] = cvUpdate_nil_nil_zero_one AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = one))
              OR
               %case #77
                (consistencyVector_i'[j] = cvUpdate_nil_nil_zero_zero AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = zero))
              OR
               %case #78
                (consistencyVector_i'[j] = cvUpdate_nil_nil_zero_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = zero) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))
              OR
               %case #79
                (consistencyVector_i'[j] = cvUpdate_nil_nil_one_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = one))
              OR
               %case #80
                (consistencyVector_i'[j] = cvUpdate_nil_nil_zero_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = zero))
              OR
               %case #81
                (consistencyVector_i'[j] = cvUpdate_nil_nil_nil_nil AND
                 (input_i[j][j] = nil OR input_i[j][j] = nil2) AND
                 (input_i[i][j] = nil OR input_i[i][j] = nil2) AND
                 (input_i[k][j] = nil OR input_i[k][j] = nil2) AND
                 (input_i[l][j] = nil OR input_i[l][j] = nil2))           
          ) 
         )   
       ) 
       -->
        
       consistencyVector_i' IN {a: ARRAY [1..N] OF CVInfoUnit | TRUE}   
    ]
  END;


calculator: MODULE =

 BEGIN

  INPUT consistencyVectors: ARRAY [1..N] OF ARRAY [1..N] OF CVInfoUnit
  OUTPUT cheater: Node 
  OUTPUT dataExchanges: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit

  INITIALIZATION dataExchanges IN {a:ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit |
       FORALL (i:Node): 
         FORALL (j:Node):
           (FORALL (l:Node):
              a[i][j][l] = nil)
    }
  INITIALIZATION cheater IN {1,2,3,4}
  
  TRANSITION

  [

    FORALL(i: Node):
     ((i /= cheater) => 
      (FORALL(k: Node): 
         (FORALL(l: Node): 
            (i=l => dataExchanges'[k][i][l] = consistencyVectors[i][i]) AND
            (i/=l => dataExchanges'[k][i][l] = dataExchanges[i][l][l])            
         )
      )
     
     ) -->

    dataExchanges' IN {a: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | TRUE };    
    cheater' IN {a:Node | TRUE}
     
  ]
 END;



 control: MODULE = 
  %cvUpdate_zero_nil_zero_zero cvUpdate_zero_zero_nil_nil cvUpdate_zero_nil_zero_nil cvUpdate_nil_zero_zero_nil cvUpdate_one_nil_zero_one cvUpdate_nil_nil_zero_one cvUpdate_zero_one_one_one cvUpdate_one_one_one_one cvUpdate_one_zero_zero_nil cvUpdate_one_zero_one_one cvUpdate_zero_nil_one_one cvUpdate_nil_zero_zero_zero cvUpdate_one_nil_one_one cvUpdate_nil_one_zero_nil cvUpdate_zero_nil_nil_nil cvUpdate_zero_one_zero_zero cvUpdate_one_zero_zero_zero cvUpdate_one_one_zero_zero cvUpdate_nil_zero_nil_nil cvUpdate_zero_one_nil_nil cvUpdate_nil_nil_zero_nil cvUpdate_nil_one_one_one cvUpdate_zero_nil_zero_one cvUpdate_one_zero_nil_nil cvUpdate_nil_nil_nil_nil cvUpdate_zero_zero_one_one cvUpdate_zero_one_zero_one cvUpdate_one_one_zero_nil cvUpdate_one_one_zero_one cvUpdate_one_zero_one_nil cvUpdate_nil_zero_one_nil cvUpdate_nil_nil_one_nil cvUpdate_zero_zero_zero_nil cvUpdate_nil_nil_one_one cvUpdate_zero_zero_zero_one cvUpdate_zero_one_one_nil cvUpdate_zero_nil_one_nil cvUpdate_zero_zero_zero_zero cvUpdate_one_one_one_nil cvUpdate_nil_one_zero_one cvUpdate_zero_zero_one_nil cvUpdate_one_one_nil_nil cvUpdate_one_zero_zero_one cvUpdate_one_nil_one_nil cvUpdate_nil_one_nil_nil cvUpdate_one_nil_nil_nil cvUpdate_nil_nil_zero_zero cvUpdate_zero_one_zero_nil cvUpdate_nil_one_one_nil cvUpdate_nil_zero_zero_one cvUpdate_nil_one_zero_zero cvUpdate_nil_zero_one_one cvUpdate_one_nil_zero_zero cvUpdate_one_nil_zero_nil


  BEGIN
     OUTPUT cvUpdate_zero_nil_zero_zero, cvUpdate_zero_zero_nil_nil, cvUpdate_zero_nil_zero_nil, cvUpdate_nil_zero_zero_nil, cvUpdate_one_nil_zero_one, cvUpdate_nil_nil_zero_one, cvUpdate_zero_one_one_one, cvUpdate_one_one_one_one, cvUpdate_one_zero_zero_nil, cvUpdate_one_zero_one_one, cvUpdate_zero_nil_one_one, cvUpdate_nil_zero_zero_zero, cvUpdate_one_nil_one_one, cvUpdate_nil_one_zero_nil, cvUpdate_zero_nil_nil_nil, cvUpdate_zero_one_zero_zero, cvUpdate_one_zero_zero_zero, cvUpdate_one_one_zero_zero, cvUpdate_nil_zero_nil_nil, cvUpdate_zero_one_nil_nil, cvUpdate_nil_nil_zero_nil, cvUpdate_nil_one_one_one, cvUpdate_zero_nil_zero_one, cvUpdate_one_zero_nil_nil, cvUpdate_nil_nil_nil_nil, cvUpdate_zero_zero_one_one, cvUpdate_zero_one_zero_one, cvUpdate_one_one_zero_nil, cvUpdate_one_one_zero_one, cvUpdate_one_zero_one_nil, cvUpdate_nil_zero_one_nil, cvUpdate_nil_nil_one_nil, cvUpdate_zero_zero_zero_nil, cvUpdate_nil_nil_one_one, cvUpdate_zero_zero_zero_one, cvUpdate_zero_one_one_nil, cvUpdate_zero_nil_one_nil, cvUpdate_zero_zero_zero_zero, cvUpdate_one_one_one_nil, cvUpdate_nil_one_zero_one, cvUpdate_zero_zero_one_nil, cvUpdate_one_one_nil_nil, cvUpdate_one_zero_zero_one, cvUpdate_one_nil_one_nil, cvUpdate_nil_one_nil_nil, cvUpdate_one_nil_nil_nil, cvUpdate_nil_nil_zero_zero, cvUpdate_zero_one_zero_nil, cvUpdate_nil_one_one_nil, cvUpdate_nil_zero_zero_one, cvUpdate_nil_one_zero_zero, cvUpdate_nil_zero_one_one, cvUpdate_one_nil_zero_zero, cvUpdate_one_nil_zero_nil: CVInfoUnit
   

    TRANSITION [ TRUE --> ]       

  END;

 system: MODULE = 
  calculator || control ||
  ( WITH OUTPUT consistencyVectors: ARRAY [1..N] OF ARRAY [1..N] OF CVInfoUnit
    WITH INPUT dataExchanges: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit
  (|| (i: Node): RENAME consistencyVector_i TO consistencyVectors[i], input_i TO dataExchanges[i] IN element[i]));


 p0: THEOREM     
  system |- F(G( EXISTS(k:Node): FORALL(i: Node): FORALL(j: Node):  i = k OR j = k OR consistencyVectors[i] = consistencyVectors[j])) ;



 p1: THEOREM
  system |- X(X(G( EXISTS(k:Node): FORALL(i: Node): FORALL(j: Node):  i = k OR j = k OR (FORALL(l:Node):consistencyVectors[i][l] = consistencyVectors[j][l])))) ;



 p2: THEOREM
  system |- X(X(X(G(FORALL(i: Node): FORALL(j: Node): consistencyVectors[i] = consistencyVectors[j])))) ;


 p3: THEOREM
 system |- X(X(G(FORALL(i: Node): FORALL(j: Node):  
             (i/=1 AND j/=1) => (FORALL(l:Node):consistencyVectors[i][l] = consistencyVectors[j][l])))) ;


END