single_rule_BR: 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 OUTPUT has_priv_enabled_i: BOOLEAN % Input of the ith node INPUT xL_i: BOOLEAN INPUT upL_i: BOOLEAN INPUT xR_i: BOOLEAN INPUT upR_i: BOOLEAN INPUT c_xS, c_upS, v_xS, v_upS: UpdateStateValue INPUT selected_privilege: [0..N] %Initializations INPUT ini_xS_1, ini_upS_1: BOOLEAN INPUT ini_xS_2, ini_upS_2: BOOLEAN INPUT ini_xS_3, ini_upS_3: BOOLEAN INPUT ini_xS_4, ini_upS_4: BOOLEAN % The initial state of the machines is arbitrary INITIALIZATION has_priv_enabled_i = FALSE; xS_i = IF i=1 THEN ini_xS_1 ELSIF i=2 THEN ini_xS_2 ELSIF i=3 THEN ini_xS_3 ELSE ini_xS_4 ENDIF; upS_i = IF i=1 THEN ini_upS_1 ELSIF i=2 THEN ini_upS_2 ELSIF i=3 THEN ini_upS_3 ELSE ini_upS_4 ENDIF; TRANSITION xS_i' = IF (i = selected_privilege) THEN get_bool_val(v_xS, xS_i, upS_i, xL_i, upL_i, xR_i, upR_i) ELSE xS_i ENDIF; upS_i' = IF i = (selected_privilege) THEN get_bool_val(v_upS, xS_i, upS_i, xL_i, upL_i, xR_i, upR_i) ELSE upS_i ENDIF; has_priv_enabled_i' = (xS_i' = get_bool_val(c_xS', xS_i', upS_i', xL_i', upL_i', xR_i', upR_i') AND upR_i' AND ( (xS_i' /= get_bool_val(v_xS, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i')) OR (upS_i' /= get_bool_val(v_upS, xS_i', upS_i', xL_i', upL_i', xR_i', upR_i')) )) END; daemon: MODULE = BEGIN INPUT priv_enabled: ARRAY [1..N] OF BOOLEAN OUTPUT selected_privilege: [0..N] INITIALIZATION selected_privilege = 0 TRANSITION [ (EXISTS(x: Node): priv_enabled'[x]) --> selected_privilege' IN {x: Node | priv_enabled'[x]} [] (FORALL(x: Node): NOT priv_enabled'[x]) --> selected_privilege' = 0 ] END; control: MODULE = BEGIN % c__xS_i v_xS_i v_upS_i OUTPUT c_xS, v_xS, v_upS: UpdateStateValue OUTPUT ini_xS_1, ini_upS_1: BOOLEAN OUTPUT ini_xS_2, ini_upS_2: BOOLEAN OUTPUT ini_xS_3, ini_upS_3: BOOLEAN OUTPUT ini_xS_4, ini_upS_4: BOOLEAN TRANSITION [ TRUE --> ] INITIALIZATION ini_upS_1 = TRUE; ini_upS_4 = FALSE END; system: MODULE = control || ( WITH OUTPUT xS: ARRAY [1..N] OF BOOLEAN WITH OUTPUT upS: ARRAY [1..N] OF BOOLEAN WITH OUTPUT has_priv_enabled: ARRAY [1..N] OF BOOLEAN (RENAME priv_enabled TO has_priv_enabled IN daemon) || (|| (i: Node): RENAME xS_i TO xS[i], upS_i TO upS[i], has_priv_enabled_i TO has_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(has_priv_enabled: ARRAY [1..N] OF BOOLEAN): BOOLEAN = (EXISTS(i:Node): (has_priv_enabled[i] AND FORALL(j:Node):(j/=i => NOT(has_priv_enabled[j])))); stabilizes: THEOREM %system |- X(X(X(X(X(X(X(X(X(X(X(X(X(X(X(X(X(exactly_one_has_privilege(has_priv_enabled)))))))))))))))))); system |- X(X(X(X(X(exactly_one_has_privilege(has_priv_enabled)))))); preserves_stability: THEOREM system |- X(exactly_one_has_privilege(has_priv_enabled) => X(exactly_one_has_privilege(has_priv_enabled))); if_stable_then_fair: THEOREM system |- X( EXISTS(i:Node):( (has_priv_enabled[i] AND FORALL(j:Node):(i/=j => NOT(has_priv_enabled[j]))) => (EXISTS(k:Node): k/=i AND X(has_priv_enabled[k])) ) ); if_stable_then_fair_2: THEOREM system |- X( (has_priv_enabled[1] AND NOT(has_priv_enabled[4] OR has_priv_enabled[2] OR has_priv_enabled[3])) => X(NOT(has_priv_enabled[1]) AND has_priv_enabled[4] OR has_priv_enabled[2] OR has_priv_enabled[3]) ); END %time python dijkstra_bounded_syn.py single_rule_BR.sal -c c_xS v_xS v_upS -d 6 -v -a stabilizes