% The module called 'control' contains the synthesis variables, and % the initialization of the variables in that module is the strategy % obtained by our synthesis tool by solving the QBF problem % NFM2014_submission16.qdimacs and mapping the solution to the Boolean % problem to an initialization for the control module using % the correspondences in NFM2014_submission16.variable_mapping % % The synthetized strategy can be also verified as follows: % % First, check that there are no deadlocks % sal-deadlock-checker -v 10 NFM2014_submission16.sal system % Second, bounded-model-check and make sure p1 is true, but p2 and p3 are not % sal-bmc -d 6 NFM2014_submission16.sal p1|p2|p3 % FINALLY, Prove property p1 using % sal-bmc -i -d 5 -l l1 -l l2 NFM2014_submission16 p1 % Note that we needed two lemmas, so prove them: % sal-bmc -i -d 2 -l l1 NFM2014_submission16 l2 % sal-bmc -i -d 2 NFM2014_submission16 l1 NFM2014_submission16: 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_3: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit INPUT cvUpdate_zero_zero_zero_zero_zero, cvUpdate_one_nil_one_one_nil, cvUpdate_nil_zero_nil_zero_nil, cvUpdate_zero_zero_nil_nil_nil, cvUpdate_nil_one_one_one_one, cvUpdate_nil_nil_nil_one_nil, cvUpdate_nil_zero_nil_nil_nil, cvUpdate_nil_nil_one_nil_one, cvUpdate_zero_nil_nil_zero_zero, cvUpdate_one_one_nil_one_nil, cvUpdate_nil_nil_one_one_one, cvUpdate_nil_zero_zero_nil_zero, cvUpdate_one_nil_one_nil_nil, cvUpdate_nil_nil_nil_nil_one, cvUpdate_zero_zero_nil_zero_nil, cvUpdate_zero_nil_nil_nil_nil, cvUpdate_nil_zero_nil_nil_zero, cvUpdate_one_one_one_one_one, cvUpdate_zero_nil_zero_zero_zero, cvUpdate_one_one_one_nil_nil, cvUpdate_nil_nil_nil_one_one, cvUpdate_zero_zero_nil_zero_zero, cvUpdate_nil_zero_zero_nil_nil, cvUpdate_zero_nil_zero_nil_nil, cvUpdate_nil_one_one_nil_one, cvUpdate_zero_zero_zero_nil_zero, cvUpdate_nil_nil_nil_nil_zero, cvUpdate_nil_one_nil_nil_nil, cvUpdate_nil_nil_zero_nil_nil, cvUpdate_nil_nil_zero_zero_zero, cvUpdate_nil_one_one_one_nil, cvUpdate_nil_nil_nil_zero_nil, cvUpdate_zero_nil_nil_nil_zero, cvUpdate_zero_zero_zero_nil_nil, cvUpdate_nil_one_nil_one_one, cvUpdate_one_nil_one_one_one, cvUpdate_nil_one_nil_one_nil, cvUpdate_nil_nil_nil_zero_zero, cvUpdate_one_nil_nil_nil_one, cvUpdate_nil_nil_one_nil_nil, cvUpdate_nil_nil_zero_nil_zero, cvUpdate_nil_nil_nil_nil_nil, cvUpdate_zero_zero_zero_zero_nil, cvUpdate_one_nil_one_nil_one, cvUpdate_one_nil_nil_one_nil, cvUpdate_one_nil_nil_one_one, cvUpdate_zero_nil_zero_zero_nil, cvUpdate_nil_zero_zero_zero_nil, cvUpdate_one_one_one_nil_one, cvUpdate_nil_nil_one_one_nil, cvUpdate_nil_one_one_nil_nil, cvUpdate_zero_zero_nil_nil_zero, cvUpdate_one_one_nil_nil_nil, cvUpdate_nil_nil_zero_zero_nil, cvUpdate_one_one_one_one_nil, cvUpdate_zero_nil_zero_nil_zero, cvUpdate_nil_zero_nil_zero_zero, cvUpdate_nil_zero_zero_zero_zero, cvUpdate_nil_one_nil_nil_one, cvUpdate_one_one_nil_nil_one, cvUpdate_one_one_nil_one_one, cvUpdate_zero_nil_nil_zero_nil, cvUpdate_one_nil_nil_nil_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 OR (consistencyVector_i[j] /= nil AND consistencyVector_i[j] /= nil2)) => consistencyVector_i'[j]=consistencyVector_i[j]) AND ((j/=i AND (consistencyVector_i[j] = nil OR consistencyVector_i[j] = nil2)) => FORALL (k:[1..N]): FORALL (l:[1..N]): (k/=i AND l/=i AND j/=k AND j/=l AND k ( %case #0 IF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_one_one_one_one %case #1 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_one_one_one_nil %case #2 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_one_one_nil_one %case #3 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_one_one_nil_nil %case #4 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_one_nil_one_one %case #5 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_one_nil_one_nil %case #6 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_one_nil_nil_one %case #7 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_one_nil_nil_nil %case #8 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_one_one_one %case #9 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_one_one_nil %case #10 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_one_nil_one %case #11 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_one_nil_nil %case #12 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_nil_one_one %case #13 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_nil_one_nil %case #14 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_nil_nil_one %case #15 ELSIF ((input_i_3'[j][k][j] = one) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_one_nil_nil_nil_nil %case #16 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_zero_zero_zero %case #17 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_zero_zero_nil %case #18 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_zero_nil_zero %case #19 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_zero_nil_nil %case #20 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_nil_zero_zero %case #21 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_nil_zero_nil %case #22 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_nil_nil_zero %case #23 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_zero_nil_nil_nil %case #24 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_zero_zero_zero %case #25 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_zero_zero_nil %case #26 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_zero_nil_zero %case #27 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_zero_nil_nil %case #28 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_nil_zero_zero %case #29 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_nil_zero_nil %case #30 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_nil_nil_zero %case #31 ELSIF ((input_i_3'[j][k][j] = zero) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_zero_nil_nil_nil_nil %case #32 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_one_one_one %case #33 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_one_one_nil %case #34 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_one_nil_one %case #35 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_one_nil_nil %case #36 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_nil_one_one %case #37 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_nil_one_nil %case #38 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_nil_nil_one %case #39 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = one) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_one_nil_nil_nil %case #40 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_zero_zero_zero %case #41 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_zero_zero_nil %case #42 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_zero_nil_zero %case #43 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_zero_nil_nil %case #44 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_nil_zero_zero %case #45 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_nil_zero_nil %case #46 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_nil_nil_zero %case #47 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = zero) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_zero_nil_nil_nil %case #48 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_one_one_one %case #49 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_one_one_nil %case #50 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_one_nil_one %case #51 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = one) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_one_nil_nil %case #52 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_zero_zero_zero %case #53 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_zero_zero_nil %case #54 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_zero_nil_zero %case #55 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = zero) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_zero_nil_nil %case #56 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_one_one %case #57 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = one) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_one_nil %case #58 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_zero_zero %case #59 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = zero) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_zero_nil %case #60 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = one)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_nil_one %case #61 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = zero)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_nil_zero %case #62 ELSIF ((input_i_3'[j][k][j] = nil OR input_i_3'[j][k][j] = nil2) AND (input_i_3'[k][k][j] = nil OR input_i_3'[k][k][j] = nil2) AND (input_i_3'[i][i][j] = nil OR input_i_3'[i][i][j] = nil2) AND (input_i_3'[j][l][j] = nil OR input_i_3'[j][l][j] = nil2) AND (input_i_3'[l][l][j] = nil OR input_i_3'[l][l][j] = nil2)) THEN consistencyVector_i'[j] = cvUpdate_nil_nil_nil_nil_nil ELSE consistencyVector_i'[j] = nil ENDIF ) ) ) ) --> 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_1: ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit OUTPUT dataExchanges_2: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit OUTPUT dataExchanges_3: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit INITIALIZATION dataExchanges_3 IN {a:ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | FORALL (i:Node): FORALL (j:Node): FORALL (k:Node): FORALL (l:Node): a[i][j][k][l] = nil } INITIALIZATION dataExchanges_2 IN {a:ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | FORALL (i:Node): FORALL (j:Node): FORALL (k:Node): a[i][j][k] = nil } INITIALIZATION dataExchanges_1 IN {a:ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | FORALL (i:Node): FORALL (j:Node): a[i][j] = nil } INITIALIZATION cheater IN {1,2,3,4} TRANSITION [ FORALL(i: Node): ( ( (i /= cheater) => ( FORALL(j: Node): dataExchanges_1'[j][i] = consistencyVectors[i][i] AND FORALL(k: Node): dataExchanges_2'[k][i][j] = dataExchanges_1[i][j] AND FORALL(l: Node): dataExchanges_3'[l][i][k][j] = dataExchanges_2[i][k][j] ) ) AND ( (i = cheater) => ( FORALL(j: Node): (dataExchanges_1'[j][i] = consistencyVectors[i][i] OR (j/=i AND dataExchanges_1'[j][i] = nil)) AND FORALL(k: Node): (dataExchanges_2'[k][i][j] = dataExchanges_1[i][j] OR (k/=i AND k/=j AND dataExchanges_2'[k][i][j] = nil)) AND FORALL(l: Node): (dataExchanges_3'[l][i][k][j] = dataExchanges_2[i][k][j] OR (l/=i AND l/=k AND l/=j AND dataExchanges_3'[l][i][k][j] = nil)) ) ) ) --> dataExchanges_3' IN {a:ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | TRUE}; dataExchanges_2' IN {a:ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | TRUE}; dataExchanges_1' IN {a:ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit | TRUE}; cheater' IN {a:Node | TRUE} ] END; control: MODULE = %cvUpdate_zero_zero_zero_zero_zero cvUpdate_one_nil_one_one_nil cvUpdate_nil_zero_nil_zero_nil cvUpdate_zero_zero_nil_nil_nil cvUpdate_nil_one_one_one_one cvUpdate_nil_nil_nil_one_nil cvUpdate_nil_zero_nil_nil_nil cvUpdate_nil_nil_one_nil_one cvUpdate_zero_nil_nil_zero_zero cvUpdate_one_one_nil_one_nil cvUpdate_nil_nil_one_one_one cvUpdate_nil_zero_zero_nil_zero cvUpdate_one_nil_one_nil_nil cvUpdate_nil_nil_nil_nil_one cvUpdate_zero_zero_nil_zero_nil cvUpdate_zero_nil_nil_nil_nil cvUpdate_nil_zero_nil_nil_zero cvUpdate_one_one_one_one_one cvUpdate_zero_nil_zero_zero_zero cvUpdate_one_one_one_nil_nil cvUpdate_nil_nil_nil_one_one cvUpdate_zero_zero_nil_zero_zero cvUpdate_nil_zero_zero_nil_nil cvUpdate_zero_nil_zero_nil_nil cvUpdate_nil_one_one_nil_one cvUpdate_zero_zero_zero_nil_zero cvUpdate_nil_nil_nil_nil_zero cvUpdate_nil_one_nil_nil_nil cvUpdate_nil_nil_zero_nil_nil cvUpdate_nil_nil_zero_zero_zero cvUpdate_nil_one_one_one_nil cvUpdate_nil_nil_nil_zero_nil cvUpdate_zero_nil_nil_nil_zero cvUpdate_zero_zero_zero_nil_nil cvUpdate_nil_one_nil_one_one cvUpdate_one_nil_one_one_one cvUpdate_nil_one_nil_one_nil cvUpdate_nil_nil_nil_zero_zero cvUpdate_one_nil_nil_nil_one cvUpdate_nil_nil_one_nil_nil cvUpdate_nil_nil_zero_nil_zero cvUpdate_nil_nil_nil_nil_nil cvUpdate_zero_zero_zero_zero_nil cvUpdate_one_nil_one_nil_one cvUpdate_one_nil_nil_one_nil cvUpdate_one_nil_nil_one_one cvUpdate_zero_nil_zero_zero_nil cvUpdate_nil_zero_zero_zero_nil cvUpdate_one_one_one_nil_one cvUpdate_nil_nil_one_one_nil cvUpdate_nil_one_one_nil_nil cvUpdate_zero_zero_nil_nil_zero cvUpdate_one_one_nil_nil_nil cvUpdate_nil_nil_zero_zero_nil cvUpdate_one_one_one_one_nil cvUpdate_zero_nil_zero_nil_zero cvUpdate_nil_zero_nil_zero_zero cvUpdate_nil_zero_zero_zero_zero cvUpdate_nil_one_nil_nil_one cvUpdate_one_one_nil_nil_one cvUpdate_one_one_nil_one_one cvUpdate_zero_nil_nil_zero_nil cvUpdate_one_nil_nil_nil_nil BEGIN OUTPUT cvUpdate_zero_zero_zero_zero_zero, cvUpdate_one_nil_one_one_nil, cvUpdate_nil_zero_nil_zero_nil, cvUpdate_zero_zero_nil_nil_nil, cvUpdate_nil_one_one_one_one, cvUpdate_nil_nil_nil_one_nil, cvUpdate_nil_zero_nil_nil_nil, cvUpdate_nil_nil_one_nil_one, cvUpdate_zero_nil_nil_zero_zero, cvUpdate_one_one_nil_one_nil, cvUpdate_nil_nil_one_one_one, cvUpdate_nil_zero_zero_nil_zero, cvUpdate_one_nil_one_nil_nil, cvUpdate_nil_nil_nil_nil_one, cvUpdate_zero_zero_nil_zero_nil, cvUpdate_zero_nil_nil_nil_nil, cvUpdate_nil_zero_nil_nil_zero, cvUpdate_one_one_one_one_one, cvUpdate_zero_nil_zero_zero_zero, cvUpdate_one_one_one_nil_nil, cvUpdate_nil_nil_nil_one_one, cvUpdate_zero_zero_nil_zero_zero, cvUpdate_nil_zero_zero_nil_nil, cvUpdate_zero_nil_zero_nil_nil, cvUpdate_nil_one_one_nil_one, cvUpdate_zero_zero_zero_nil_zero, cvUpdate_nil_nil_nil_nil_zero, cvUpdate_nil_one_nil_nil_nil, cvUpdate_nil_nil_zero_nil_nil, cvUpdate_nil_nil_zero_zero_zero, cvUpdate_nil_one_one_one_nil, cvUpdate_nil_nil_nil_zero_nil, cvUpdate_zero_nil_nil_nil_zero, cvUpdate_zero_zero_zero_nil_nil, cvUpdate_nil_one_nil_one_one, cvUpdate_one_nil_one_one_one, cvUpdate_nil_one_nil_one_nil, cvUpdate_nil_nil_nil_zero_zero, cvUpdate_one_nil_nil_nil_one, cvUpdate_nil_nil_one_nil_nil, cvUpdate_nil_nil_zero_nil_zero, cvUpdate_nil_nil_nil_nil_nil, cvUpdate_zero_zero_zero_zero_nil, cvUpdate_one_nil_one_nil_one, cvUpdate_one_nil_nil_one_nil, cvUpdate_one_nil_nil_one_one, cvUpdate_zero_nil_zero_zero_nil, cvUpdate_nil_zero_zero_zero_nil, cvUpdate_one_one_one_nil_one, cvUpdate_nil_nil_one_one_nil, cvUpdate_nil_one_one_nil_nil, cvUpdate_zero_zero_nil_nil_zero, cvUpdate_one_one_nil_nil_nil, cvUpdate_nil_nil_zero_zero_nil, cvUpdate_one_one_one_one_nil, cvUpdate_zero_nil_zero_nil_zero, cvUpdate_nil_zero_nil_zero_zero, cvUpdate_nil_zero_zero_zero_zero, cvUpdate_nil_one_nil_nil_one, cvUpdate_one_one_nil_nil_one, cvUpdate_one_one_nil_one_one, cvUpdate_zero_nil_nil_zero_nil, cvUpdate_one_nil_nil_nil_nil : CVInfoUnit INITIALIZATION cvUpdate_zero_zero_zero_zero_zero = zero INITIALIZATION cvUpdate_one_nil_one_one_nil = nil INITIALIZATION cvUpdate_one_one_nil_one_one = zero INITIALIZATION cvUpdate_nil_zero_nil_zero_nil = zero INITIALIZATION cvUpdate_zero_zero_nil_zero_zero = one INITIALIZATION cvUpdate_nil_one_one_one_one = one INITIALIZATION cvUpdate_nil_nil_nil_nil_zero = nil INITIALIZATION cvUpdate_nil_zero_zero_zero_nil = zero INITIALIZATION cvUpdate_nil_nil_one_nil_one = zero INITIALIZATION cvUpdate_zero_nil_nil_zero_zero = one INITIALIZATION cvUpdate_one_one_nil_one_nil = zero INITIALIZATION cvUpdate_zero_zero_zero_nil_nil = one INITIALIZATION cvUpdate_one_nil_one_nil_nil = zero INITIALIZATION cvUpdate_nil_nil_nil_nil_one = nil INITIALIZATION cvUpdate_zero_zero_nil_zero_nil = one INITIALIZATION cvUpdate_zero_nil_zero_nil_nil = one INITIALIZATION cvUpdate_zero_nil_zero_nil_zero = zero INITIALIZATION cvUpdate_one_one_one_one_one = one INITIALIZATION cvUpdate_zero_nil_zero_zero_zero = zero INITIALIZATION cvUpdate_nil_nil_one_one_one = zero INITIALIZATION cvUpdate_nil_nil_nil_one_one = nil INITIALIZATION cvUpdate_zero_zero_nil_nil_nil = nil INITIALIZATION cvUpdate_zero_nil_nil_nil_nil = nil INITIALIZATION cvUpdate_nil_one_one_nil_one = one INITIALIZATION cvUpdate_zero_zero_zero_nil_zero = zero INITIALIZATION cvUpdate_one_nil_nil_nil_one = zero INITIALIZATION cvUpdate_nil_one_nil_nil_nil = nil INITIALIZATION cvUpdate_nil_nil_zero_zero_nil = one INITIALIZATION cvUpdate_nil_one_one_one_nil = zero INITIALIZATION cvUpdate_nil_nil_zero_nil_zero = one INITIALIZATION cvUpdate_nil_zero_zero_nil_zero = zero INITIALIZATION cvUpdate_nil_one_nil_one_one = zero INITIALIZATION cvUpdate_one_one_nil_nil_one = zero INITIALIZATION cvUpdate_one_nil_one_one_one = one INITIALIZATION cvUpdate_nil_nil_nil_one_nil = nil INITIALIZATION cvUpdate_nil_nil_nil_zero_zero = nil INITIALIZATION cvUpdate_nil_zero_nil_zero_zero = one INITIALIZATION cvUpdate_nil_zero_nil_nil_zero = one INITIALIZATION cvUpdate_nil_nil_one_nil_nil = nil INITIALIZATION cvUpdate_one_one_one_one_nil = one INITIALIZATION cvUpdate_nil_nil_nil_nil_nil = nil INITIALIZATION cvUpdate_nil_nil_zero_zero_zero = one INITIALIZATION cvUpdate_one_nil_one_nil_one = zero INITIALIZATION cvUpdate_one_nil_nil_one_nil = zero INITIALIZATION cvUpdate_one_nil_nil_one_one = zero INITIALIZATION cvUpdate_zero_nil_zero_zero_nil = nil INITIALIZATION cvUpdate_nil_zero_zero_nil_nil = one INITIALIZATION cvUpdate_zero_nil_nil_nil_zero = zero INITIALIZATION cvUpdate_zero_zero_nil_nil_zero = one INITIALIZATION cvUpdate_nil_one_one_nil_nil = zero INITIALIZATION cvUpdate_nil_zero_nil_nil_nil = nil INITIALIZATION cvUpdate_nil_nil_one_one_nil = zero INITIALIZATION cvUpdate_zero_zero_zero_zero_nil = zero INITIALIZATION cvUpdate_one_nil_nil_nil_nil = nil INITIALIZATION cvUpdate_nil_nil_zero_nil_nil = nil INITIALIZATION cvUpdate_one_one_nil_nil_nil = nil INITIALIZATION cvUpdate_nil_zero_zero_zero_zero = zero INITIALIZATION cvUpdate_nil_one_nil_nil_one = zero INITIALIZATION cvUpdate_one_one_one_nil_nil = zero INITIALIZATION cvUpdate_nil_nil_nil_zero_nil = nil INITIALIZATION cvUpdate_zero_nil_nil_zero_nil = zero INITIALIZATION cvUpdate_one_one_one_nil_one = one INITIALIZATION cvUpdate_nil_one_nil_one_nil = zero TRANSITION [ TRUE --> ] END; system: MODULE = calculator || control || ( WITH OUTPUT consistencyVectors: ARRAY [1..N] OF ARRAY [1..N] OF CVInfoUnit WITH INPUT dataExchanges_1: ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit WITH INPUT dataExchanges_2: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit WITH INPUT dataExchanges_3: ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF ARRAY [1..N] OF CHInfoUnit (|| (i: Node): RENAME consistencyVector_i TO consistencyVectors[i], %input_i_1 TO dataExchanges_1[i], %input_i_2 TO dataExchanges_2[i], input_i_3 TO dataExchanges_3[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(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]))))); p1_syn: THEOREM system |- X(X(X( 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])))) ; l2: LEMMA system |- G(FORALL(i: Node): FORALL(j: Node): (consistencyVectors[i][j] /= nil2)); l1: LEMMA system |- G(cvUpdate_zero_zero_zero_zero_zero=zero AND cvUpdate_one_nil_one_one_nil=nil AND cvUpdate_one_one_nil_one_one=zero AND cvUpdate_nil_zero_nil_zero_nil=zero AND cvUpdate_zero_zero_nil_zero_zero=one AND cvUpdate_nil_one_one_one_one=one AND cvUpdate_nil_nil_nil_nil_zero=nil AND cvUpdate_nil_zero_zero_zero_nil=zero AND cvUpdate_nil_nil_one_nil_one=zero AND cvUpdate_zero_nil_nil_zero_zero=one AND cvUpdate_one_one_nil_one_nil=zero AND cvUpdate_zero_zero_zero_nil_nil=one AND cvUpdate_one_nil_one_nil_nil=zero AND cvUpdate_nil_nil_nil_nil_one=nil AND cvUpdate_zero_zero_nil_zero_nil=one AND cvUpdate_zero_nil_zero_nil_nil=one AND cvUpdate_zero_nil_zero_nil_zero=zero AND cvUpdate_one_one_one_one_one=one AND cvUpdate_zero_nil_zero_zero_zero=zero AND cvUpdate_nil_nil_one_one_one=zero AND cvUpdate_nil_nil_nil_one_one=nil AND cvUpdate_zero_zero_nil_nil_nil=nil AND cvUpdate_zero_nil_nil_nil_nil=nil AND cvUpdate_nil_one_one_nil_one=one AND cvUpdate_zero_zero_zero_nil_zero=zero AND cvUpdate_one_nil_nil_nil_one=zero AND cvUpdate_nil_one_nil_nil_nil=nil AND cvUpdate_nil_nil_zero_zero_nil=one AND cvUpdate_nil_one_one_one_nil=zero AND cvUpdate_nil_nil_zero_nil_zero=one AND cvUpdate_nil_zero_zero_nil_zero=zero AND cvUpdate_nil_one_nil_one_one=zero AND cvUpdate_one_one_nil_nil_one=zero AND cvUpdate_one_nil_one_one_one=one AND cvUpdate_nil_nil_nil_one_nil=nil AND cvUpdate_nil_nil_nil_zero_zero=nil AND cvUpdate_nil_zero_nil_zero_zero=one AND cvUpdate_nil_zero_nil_nil_zero=one AND cvUpdate_nil_nil_one_nil_nil=nil AND cvUpdate_one_one_one_one_nil=one AND cvUpdate_nil_nil_nil_nil_nil=nil AND cvUpdate_nil_nil_zero_zero_zero=one AND cvUpdate_one_nil_one_nil_one=zero AND cvUpdate_one_nil_nil_one_nil=zero AND cvUpdate_one_nil_nil_one_one=zero AND cvUpdate_zero_nil_zero_zero_nil=nil AND cvUpdate_nil_zero_zero_nil_nil=one AND cvUpdate_zero_nil_nil_nil_zero=zero AND cvUpdate_zero_zero_nil_nil_zero=one AND cvUpdate_nil_one_one_nil_nil=zero AND cvUpdate_nil_zero_nil_nil_nil=nil AND cvUpdate_nil_nil_one_one_nil=zero AND cvUpdate_zero_zero_zero_zero_nil=zero AND cvUpdate_one_nil_nil_nil_nil=nil AND cvUpdate_nil_nil_zero_nil_nil=nil AND cvUpdate_one_one_nil_nil_nil=nil AND cvUpdate_nil_zero_zero_zero_zero=zero AND cvUpdate_nil_one_nil_nil_one=zero AND cvUpdate_one_one_one_nil_nil=zero AND cvUpdate_nil_nil_nil_zero_nil=nil AND cvUpdate_zero_nil_nil_zero_nil=zero AND cvUpdate_one_one_one_nil_one=one AND cvUpdate_nil_one_nil_one_nil=zero); END % How to analyze? % First, check that there are no deadlocks % sal-deadlock-checker -v 10 test_final_4nodes_synth_simpler system % Second, bounded-model-check and make sure p1 is true, but p2 and p3 are not % sal-bmc -d 6 test_final_4nodes_synth p1|p2|p3 % FINALLY, Prove property p1 using % sal-bmc -i -d 5 -l l1 -l l2 test_final_4nodes_synth_simpler p1 % Note that we needed two lemmas, so prove them: % sal-bmc -i -d 2 -l l1 test_final_4nodes_synth_simpler l2 % sal-bmc -i -d 2 test_final_4nodes_synth_simpler l1