two_rules_general: CONTEXT = BEGIN N: NATURAL = 4 ; % Number of nodes/processes Node: TYPE = [1..N]; % Nodes are named 1..N UpdateStateValue: TYPE = {xSref, upSref, xLref, upLref, xRref, upRref, trueref, falseref, xSrefneg, upSrefneg, xLrefneg, upLrefneg, xRrefneg, upRrefneg, truerefneg, falserefneg}; get_bool_val(val:UpdateStateValue, xS:BOOLEAN, upS:BOOLEAN, xL:BOOLEAN, upL:BOOLEAN, xR:BOOLEAN, upR:BOOLEAN): BOOLEAN = IF val = xSref THEN xS ELSIF val = upSref THEN upS ELSIF val = xLref THEN xL ELSIF val = upLref THEN upL ELSIF val = xRref THEN xR ELSIF val = upRref THEN upR ELSIF val = trueref THEN TRUE ELSIF val = falseref THEN FALSE ELSIF val = xSrefneg THEN NOT xS ELSIF val = upSrefneg THEN NOT upS ELSIF val = xLrefneg THEN NOT xL ELSIF val = upLrefneg THEN NOT upL ELSIF val = xRrefneg THEN NOT xR ELSIF val = upRrefneg THEN NOT upR ELSIF val = truerefneg THEN FALSE ELSIF val = falserefneg THEN TRUE ELSE xS ENDIF; element[i: Node]: MODULE = BEGIN % Each machine state is represented by two booleans xS and upS (A and B in the paper) OUTPUT xS_i: BOOLEAN OUTPUT upS_i: BOOLEAN % priv_enabled_i[j] is true if the jth rule of ith node is enabled OUTPUT priv_enabled_i: ARRAY [1..2] OF BOOLEAN % Input of the ith node INPUT xL_i: BOOLEAN INPUT upL_i: BOOLEAN INPUT xR_i: BOOLEAN INPUT upR_i: BOOLEAN %c_xS_1_1 c_upS_1_1 v_xS_1_1 v_upS_1_1 c_xS_2_1 c_upS_2_1 v_xS_2_1 v_upS_2_1 c_xS_1_2 c_upS_1_2 v_xS_1_2 v_upS_1_2 c_xS_2_2 c_upS_2_2 v_xS_2_2 v_upS_2_2 c_xS_1_3 c_upS_1_3 v_xS_1_3 v_upS_1_3 c_xS_2_3 c_upS_2_3 v_xS_2_3 v_upS_2_3 c_xS_1_4 c_upS_1_4 v_xS_1_4 v_upS_1_4 c_xS_2_4 c_upS_2_4 v_xS_2_4 v_upS_2_4 % Variables whose value will be synthetised encoding guards and assignments of each of the 2 rule for each node. INPUT c_xS_1_1, c_upS_1_1, v_xS_1_1, v_upS_1_1: UpdateStateValue INPUT c_xS_2_1, c_upS_2_1, v_xS_2_1, v_upS_2_1: UpdateStateValue INPUT c_xS_1_2, c_upS_1_2, v_xS_1_2, v_upS_1_2: UpdateStateValue INPUT c_xS_2_2, c_upS_2_2, v_xS_2_2, v_upS_2_2: UpdateStateValue INPUT c_xS_1_3, c_upS_1_3, v_xS_1_3, v_upS_1_3: UpdateStateValue INPUT c_xS_2_3, c_upS_2_3, v_xS_2_3, v_upS_2_3: UpdateStateValue INPUT c_xS_1_4, c_upS_1_4, v_xS_1_4, v_upS_1_4: UpdateStateValue INPUT c_xS_2_4, c_upS_2_4, v_xS_2_4, v_upS_2_4: UpdateStateValue % Privilege (node and rule) selected by the daemon INPUT selected_node: [0..N] INPUT selected_rule: [0..2] % The initial state of the machines is arbitrary INITIALIZATION priv_enabled_i[1] = FALSE; priv_enabled_i[2] = FALSE; TRANSITION xS_i' = IF (i = selected_node AND 1 = selected_rule) THEN get_bool_val(IF i = 1 THEN v_xS_1_1 ELSIF i = 2 THEN v_xS_1_2 ELSIF i = 3 THEN v_xS_1_3 ELSE v_xS_1_4 ENDIF, xS_i, upS_i, xL_i, upL_i, xR_i, upR_i) ELSIF (i = selected_node AND 2 = selected_rule) THEN get_bool_val(IF i = 1 THEN v_xS_2_1 ELSIF i = 2 THEN v_xS_2_2 ELSIF i = 3 THEN v_xS_2_3 ELSE v_xS_2_4 ENDIF, xS_i, upS_i, xL_i, upL_i, xR_i, upR_i) ELSE xS_i ENDIF; upS_i' = IF (i = selected_node and 1 = selected_rule) THEN get_bool_val(IF i = 1 THEN v_upS_1_1 ELSIF i = 2 THEN v_upS_1_2 ELSIF i = 3 THEN v_upS_1_3 ELSE v_upS_1_4 ENDIF, xS_i, upS_i, xL_i, upL_i, xR_i, upR_i) ELSIF (i = selected_node AND 2 = selected_rule) THEN get_bool_val(IF i = 1 THEN v_upS_2_1 ELSIF i = 2 THEN v_upS_2_2 ELSIF i = 3 THEN v_upS_2_3 ELSE v_upS_2_4 ENDIF, xS_i, upS_i, xL_i, upL_i, xR_i, upR_i) ELSE upS_i ENDIF; priv_enabled_i'[1] = (xS_i' = get_bool_val(IF i = 1 THEN c_xS_1_1 ELSIF i = 2 THEN c_xS_1_2 ELSIF i = 3 THEN c_xS_1_3 ELSE c_xS_1_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i') AND upS_i' = get_bool_val(IF i = 1 THEN c_upS_1_1 ELSIF i = 2 THEN c_upS_1_2 ELSIF i = 3 THEN c_upS_1_3 ELSE c_upS_1_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i') AND ((xS_i' /= get_bool_val(IF i = 1 THEN v_xS_1_1 ELSIF i = 2 THEN v_xS_1_2 ELSIF i = 3 THEN v_xS_1_3 ELSE v_xS_1_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i')) OR (upS_i' /= get_bool_val(IF i = 1 THEN v_upS_1_1 ELSIF i = 2 THEN v_upS_1_2 ELSIF i = 3 THEN v_upS_1_3 ELSE v_upS_1_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i')) )); priv_enabled_i'[2] = (xS_i' = get_bool_val(IF i = 1 THEN c_xS_2_1 ELSIF i = 2 THEN c_xS_2_2 ELSIF i = 3 THEN c_xS_2_3 ELSE c_xS_2_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i') AND upS_i' = get_bool_val(IF i = 1 THEN c_upS_2_1 ELSIF i = 2 THEN c_upS_2_2 ELSIF i = 3 THEN c_upS_2_3 ELSE c_upS_2_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i') AND ((xS_i' /= get_bool_val(IF i = 1 THEN v_xS_2_1 ELSIF i = 2 THEN v_xS_2_2 ELSIF i = 3 THEN v_xS_2_3 ELSE v_xS_2_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i')) OR (upS_i' /= get_bool_val(IF i = 1 THEN v_upS_2_1 ELSIF i = 2 THEN v_upS_2_2 ELSIF i = 3 THEN v_upS_2_3 ELSE v_upS_2_4 ENDIF, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i')) )) END; daemon: MODULE = BEGIN INPUT priv_enabled: ARRAY Node OF ARRAY[1..2] OF BOOLEAN OUTPUT selected_node: [0..N] OUTPUT selected_rule: [0..2] INITIALIZATION selected_node = 0; selected_rule = 0 TRANSITION [ (EXISTS(x: Node):EXISTS(y:[1..2]): priv_enabled'[x][y]) --> selected_node' IN {x: Node | EXISTS(y:[1..2]):priv_enabled'[x][y]}; selected_rule' IN {y: Node | priv_enabled'[selected_node'][y]} [] (FORALL(x: Node):FORALL(y:[1..2]): NOT priv_enabled'[x][y]) --> selected_node' = 0; selected_rule' = 0 ] END; control: MODULE = BEGIN %c_xS_1_1 c_upS_1_1 v_xS_1_1 v_upS_1_1 c_xS_2_1 c_upS_2_1 v_xS_2_1 v_upS_2_1 c_xS_1_2 c_upS_1_2 v_xS_1_2 v_upS_1_2 c_xS_2_2 c_upS_2_2 v_xS_2_2 v_upS_2_2 c_xS_1_3 c_upS_1_3 v_xS_1_3 v_upS_1_3 c_xS_2_3 c_upS_2_3 v_xS_2_3 v_upS_2_3 c_xS_1_4 c_upS_1_4 v_xS_1_4 v_upS_1_4 c_xS_2_4 c_upS_2_4 v_xS_2_4 v_upS_2_4 OUTPUT c_xS_1_1, c_upS_1_1, v_xS_1_1, v_upS_1_1: UpdateStateValue OUTPUT c_xS_2_1, c_upS_2_1, v_xS_2_1, v_upS_2_1: UpdateStateValue OUTPUT c_xS_1_2, c_upS_1_2, v_xS_1_2, v_upS_1_2: UpdateStateValue OUTPUT c_xS_2_2, c_upS_2_2, v_xS_2_2, v_upS_2_2: UpdateStateValue OUTPUT c_xS_1_3, c_upS_1_3, v_xS_1_3, v_upS_1_3: UpdateStateValue OUTPUT c_xS_2_3, c_upS_2_3, v_xS_2_3, v_upS_2_3: UpdateStateValue OUTPUT c_xS_1_4, c_upS_1_4, v_xS_1_4, v_upS_1_4: UpdateStateValue OUTPUT c_xS_2_4, c_upS_2_4, v_xS_2_4, v_upS_2_4: UpdateStateValue TRANSITION [ TRUE --> ] END; system: MODULE = daemon || control || ( WITH OUTPUT xS: ARRAY Node OF BOOLEAN WITH OUTPUT upS: ARRAY Node OF BOOLEAN WITH OUTPUT priv_enabled: ARRAY Node OF ARRAY [1..2] OF BOOLEAN (|| (i: Node): RENAME xS_i TO xS[i], upS_i TO upS[i], priv_enabled_i TO priv_enabled[i], xL_i TO xS[IF i=1 THEN N ELSE i-1 ENDIF], upL_i TO upS[IF i=1 THEN N ELSE i-1 ENDIF], xR_i TO xS[IF i=N THEN 1 ELSE i+1 ENDIF], upR_i TO upS[IF i=N THEN 1 ELSE i+1 ENDIF] IN element[i])); exactly_one_has_privilege(priv_enabled: ARRAY Node OF ARRAY [1..2] OF BOOLEAN): BOOLEAN = (EXISTS(i:Node):EXISTS(j:[1..2]): (priv_enabled[i][j] AND FORALL(k:Node):FORALL(l:[1..2]):(l/=j => NOT(priv_enabled[k][l])))); stabilizes: THEOREM system |- X(X(X(X(X(exactly_one_has_privilege(priv_enabled)))))); preserves_stability: THEOREM system |- X(exactly_one_has_privilege(priv_enabled) => X(exactly_one_has_privilege(priv_enabled))); END %home/agascon/sri/projects/sal-3.2/bin/sal-bmc -d 9 dijkstra_4_states_symmetric.sal p0 %time python dijkstra_bounded_syn.py synt2014_asymmetric_2_rules.sal -c _xS_1_1 c_upS_1_1 v_xS_1_1 v_upS_1_1 c_xS_2_1 c_upS_2_1 v_xS_2_1 v_upS_2_1 c_xS_1_2 c_upS_1_2 v_xS_1_2 v_upS_1_2 c_xS_2_2 c_upS_2_2 v_xS_2_2 v_upS_2_2 c_xS_1_3 c_upS_1_3 v_xS_1_3 v_upS_1_3 c_xS_2_3 c_upS_2_3 v_xS_2_3 v_upS_2_3 c_xS_1_4 c_upS_1_4 v_xS_1_4 v_upS_1_4 c_xS_2_4 c_upS_2_4 v_xS_2_4 v_upS_2_4 -d 6 -v -a stabilizes