Lipari Ring

Transition System

type state = {init, try, notry, leader}

in N : int where N > 1
in id : array [1..N] of [1..] where (Forall i,j : [1..N] . id[i] = id[j] --> i = j)

local tok : array [1..N] of int where Forall i : [1..N] . tok[i] = 0
local q : array [1..N] of state where Forall i : [1..N] . q[i] = init

macro next(i: [1..N]) = if i = N then 1 else i + 1
macro empty(i: [1..N]) = tok[i] = 0


Transition t1[i: [1..N]] : 
  enable q[i] = init
  assign q[i] := try, 
         tok[next(i)] := id[i]

Transition t2[i: [1..N]] :
  enable q[i] = init
  assign q[i] := notry

Transition t3[i: [1..N]] :
  enable q[i] = notry /\ !empty(i) /\ empty(next(i)) 
  assign tok[next(i)] := tok[i], 
         tok[i] := 0

Transition t4[i: [1..N]] :
  enable q[i] = try /\ !empty(i) /\ empty(next(i)) /\ tok[i] > id[i]
  assign tok[next(i)] := tok[i],
	 tok[i] := 0
	 
Transition t5[i: [1..N]] :
  enable q[i] = try /\ !empty(i) /\ tok[i] < id[i]
  assign tok[i] := 0

Transition t6[i: [1..N]] :
   enable q[i] = try /\ !empty(i) /\ tok[i] = id[i]
   assign q[i] := leader
     

SPEC

macro between (x: [1..N], i: [1..N], j: [1..N], l: bool, r: bool) =
   if i < j then ( 
      (if l then i <= x else i < x) /\ 
      (if r then x <= j else x < j)
   ) 
   else (
      ((if l then i <= x else i < x) /\ x <= N) \/ 
      (1 <= x /\ (if r then x <= j else x < j)) 
   )

macro active (i: [1..N]) = q[i] = try \/ q[i] = leader

% The program declarations 
%
AXIOM A1:
   Forall i, j: [1..N] . id[i] = id[j] ==> i = j

AXIOM A2:
   Forall i: [1..N] . 0 < id[i]
   
AXIOM A3:
   Forall i: [1..N] . 0 <= tok[i]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

CONJECTURE phi0:
   Forall i: [1..N] . q[i] = init ==> empty(next(i))

CONJECTURE phi1: 
   Forall i: [1..N] . (Exists j: [1..N] . tok[j] = id[i]) ==> active(i)

CONJECTURE phi2: 
   Forall i: [1..N] . q[i] = init ==> Forall j: [1..N] . tok[j] != id[i]

CONJECTURE phi3: 
   Forall i: [1..N] . !active(i) ==> Forall j: [1..N] . tok[j] != id[i]

CONJECTURE phi4: 
   [] Forall i: [1..N] . !empty(i) --> Exists j: [1..N] . tok[i] = id[j]

CONJECTURE phi5: 
   [] Forall i, j, k: [1..N] . tok[j] = id[i] /\ between (k, i, j, true, false) --> q[k] != init 

CONJECTURE phi6: 
   [] Forall i, j: [1..N] . !empty(i) /\ !empty(j) /\ tok[i] = tok[j] --> i = j

CONJECTURE phi7:
   [] Forall i, j: [1..N] . id[i] = tok[i] --> q[j] != init

CONJECTURE phi8: 
   [] Forall i, j: [1..N] . q[i] = leader --> q[j] != init

CONJECTURE psi1: 
   [] Forall i, j, k: [1..N] . tok[j] = id[i] /\ between (k, i, j, true, false) /\ active (k) --> id[i] >= id[k]

CONJECTURE psi2: 
   [] Forall i: [1..N] . q[i] = leader --> tok[i] = id[i]

CONJECTURE psi3:
   [] Forall i, j: [1..N] . q[i] = leader /\ active(j) --> id[i] >= id[j]

CONJECTURE psi4:
   [] Forall i, j: [1..N] . q[i] = leader /\ q[j] = leader --> i = j