Symmetry in the Bakery Algorithm¶
Description of the Case Study¶
Lamport’s Bakery algorithm is a mutual exclusion protocol for concurrent processes. The symmetry property states that no specific process is privileged in terms of a faster access to the critical section, which is a desirable property because it implies that concrete process ids are not relevant for faster accesses. Symmetry is a hyperproperty that can be expressed with different HyperLTL formulas
\[\begin{split}\varphi_{S1} = \forall \pi_A . \forall \pi_B . \left(
\neg \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \lor
\neg(pause_{\pi_A} = pause_{\pi_B})
\right) \mathcal{R} \\
\left(
(pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land
(pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B})
\right)\end{split}\]
\[\begin{split}\varphi_{S2} =\ & \forall \pi_A . \forall \pi_B . \big( \neg \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \lor
\neg(pause_{\pi_A} = pause_{\pi_B}) \lor \\
&\quad \neg(select_{\pi_A} < 3) \lor
\neg(select_{\pi_B} < 3) \big) \ \mathcal{R} \\
&\quad \big( (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land
(pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \big)\end{split}\]
\[\begin{split}\varphi_{S3} =\ & \forall \pi_A . \forall \pi_B . \big(\neg \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \lor
\neg(pause_{\pi_A} = pause_{\pi_B}) \lor \\
&\quad \neg(select_{\pi_A} < 3) \lor
\neg(select_{\pi_B} < 3) \lor \\
&\quad \neg \mathsf{sym}(sym\_break_{\pi_A}, sym\_break_{\pi_B}) \big)
\ \mathcal{R} \\
&\quad \big( (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land
(pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B}) \big)\end{split}\]
\[\begin{split}\varphi_{\text{sym}_1} =\ & \forall \pi_A . \exists \pi_B . \Box \mathsf{sym}(select_{\pi_A}, select_{\pi_B})
\land (pause_{\pi_A} = pause_{\pi_B}) \land \\
&\quad (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B})\end{split}\]
\[\begin{split}\begin{aligned}
\varphi_{\text{sym}_2} =\ & \forall \pi_A . \exists \pi_B . \Box \mathsf{sym}(select_{\pi_A}, select_{\pi_B}) \land (pause_{\pi_A} = pause_{\pi_B}) \land \\
&\quad (select_{\pi_A} < 3) \land (select_{\pi_B} < 3) \land \\
&\quad (pc(P_0)_{\pi_A} = pc(P_1)_{\pi_B}) \land (pc(P_1)_{\pi_A} = pc(P_0)_{\pi_B})
\end{aligned}\end{split}\]
In these formulas, each process \(P_{n}\) has a program counter \(pc(P_{n})\); select indicates which process is selected to process next; \(\text{pause}\) if both processes are not selected; \(\text{sym_break}\) is which process is selected after a tie; and sym(\(\text{select}\pi_{A}\) , \(\text{select}\pi_{B}\) ) indicates if two traces exchange the process ids of which processes proceeds. The basic Bakery algorithm does not satisfy symmetry (i.e. \(\varphi_{sym_{1}}\)), because when two or more processes are trying to enter the critical section with the same ticket number, the process with the smaller process ID has priority and process ID is statically fixed attribute. HyperQB returns SAT using the \(\text{pessimistic}\) semantics, indicating that there exists a counterexample to symmetry in the form of a falsifying witness to \(\pi_{A}\) in formula \(\varphi_{sym_{1}}\). The tool returns an observable witness within finite bound using the the pessimistic semantics. Therefore, we conclude that all future observations violate the property
Benchmarks¶
The Model(s)
--BAKERY ALGORITHM
--(adopted from the Bakery algorithm from: Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV’19))
MODULE main
VAR
p1_ticket: 0..3; -- the ticket number of p1
p2_ticket: 0..3; -- the ticket number of p2
p3_ticket: 0..3; -- the ticket number of p3
MAX_ticket: 0..3; -- let's say max ticket number is 3
p1_line: 0..4;
p2_line: 0..4;
p3_line: 0..4;
ASSIGN
init(p1_ticket) := 3; -- set to MAX
init(p2_ticket) := 3; -- set to MAX
init(p3_ticket) := 3; -- set to MAX
init(p1_line) := 0;
init(p2_line) := 0;
init(p3_line) := 0;
init(MAX_ticket):= 0;
next(MAX_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1 | p2_line=1 | p3_line=1): MAX_ticket+1;
TRUE: MAX_ticket;
esac;
next(p1_line) :=
case
(p1_line=0) : {0,1}; -- stay, or proceed
(p1_line=1) : {2}; -- draw ticket
(p1_line=2 & !p1-TOKEN) : {2}; -- check TOKEN
(p1_line=2 & p1-TOKEN) : {3}; -- check TOKEN
(p1_line=3) : {4}; -- stay in critical section, or leave
(p1_line=4) : {0}; -- back to starting point
TRUE: p1_line;
esac;
next(p1_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1): MAX_ticket+1;
TRUE: p1_ticket;
esac;
next(p2_line) :=
case
(p2_line=0) : {0,1}; -- stay, or proceed
(p2_line=1) : {2};
(p2_line=2 & !p2-TOKEN): {2}; -- check TOKEN
(p2_line=2 & p2-TOKEN): {3}; -- check TOKEN
(p2_line=3) : {4}; -- stay in critical section, or leave
(p2_line=4) : {0}; -- back to starting point
TRUE: p2_line;
esac;
next(p2_ticket):=
case
(MAX_ticket=3): 0; --reset
(p2_line=1): MAX_ticket+1;
TRUE: p2_ticket;
esac;
next(p3_line) :=
case
(p3_line=0) : {0}; -- stay, or proceed
(p3_line=1) : {2};
(p3_line=2 & !p3-TOKEN) : 2 ; -- check TOKEN
(p3_line=2 & p3-TOKEN) : 3 ; -- check TOKEN
(p3_line=3) : {4}; -- stay in critical section, or leave
(p3_line=4) : {0}; -- back to starting point
TRUE: p3_line;
esac;
next(p3_ticket):=
case
(MAX_ticket=3): 0; --reset
(p3_line=1): MAX_ticket+1;
TRUE: p3_ticket;
esac;
DEFINE
STARTED := (p1_line!=0 | p2_line!=0 | p3_line!=0);
p1-TOKEN := STARTED & (p1_line=2) & ((p1_ticket <= p2_ticket) & (p1_ticket <= p3_ticket));
p2-TOKEN := STARTED & (p2_line=2) & ((((p2_ticket <= p1_ticket) & (p2_ticket <= p3_ticket))) | !p1-TOKEN);
p3-TOKEN := STARTED & (p3_line=2) & ((((p3_ticket <= p1_ticket) & (p3_ticket <= p2_ticket))) | !p1-TOKEN & !p2-TOKEN);
Formula
forall A. exists B.
(G
(
((p1-TOKEN[A] <-> p2-TOKEN[B])
/\(p2-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p2_line[B]*)
/\(*p2_line[A] = p1_line[B]*))
/\((p1-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p3_line[B]*)
/\(*p3_line[A] = p1_line[B]*))
/\ ((p2-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p2-TOKEN[B])
/\(*p2_line[A] = p3_line[B]*)
/\(*p3_line[A] = p2_line[B]*))
)
)
The Model(s)
--BAKERY ALGORITHM
--(adopted from the Bakery algorithm from: Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV’19))
MODULE main
VAR
p1_ticket: 0..3; -- the ticket number of p1
p2_ticket: 0..3; -- the ticket number of p2
p3_ticket: 0..3; -- the ticket number of p3
MAX_ticket: 0..3; -- let's say max ticket number is 3
p1_line: 0..4;
p2_line: 0..4;
p3_line: 0..4;
ASSIGN
init(p1_ticket) := 3; -- set to MAX
init(p2_ticket) := 3; -- set to MAX
init(p3_ticket) := 3; -- set to MAX
init(p1_line) := 0;
init(p2_line) := 0;
init(p3_line) := 0;
init(MAX_ticket):= 0;
next(MAX_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1 | p2_line=1 | p3_line=1): MAX_ticket+1;
TRUE: MAX_ticket;
esac;
next(p1_line) :=
case
(p1_line=0) : {0,1}; -- stay, or proceed
(p1_line=1) : {2}; -- draw ticket
(p1_line=2 & !p1-TOKEN) : {2}; -- check TOKEN
(p1_line=2 & p1-TOKEN) : {3}; -- check TOKEN
(p1_line=3) : {4}; -- stay in critical section, or leave
(p1_line=4) : {0}; -- back to starting point
TRUE: p1_line;
esac;
next(p1_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1): MAX_ticket+1;
TRUE: p1_ticket;
esac;
next(p2_line) :=
case
(p2_line=0) : {0,1}; -- stay, or proceed
(p2_line=1) : {2};
(p2_line=2 & !p2-TOKEN): {2}; -- check TOKEN
(p2_line=2 & p2-TOKEN): {3}; -- check TOKEN
(p2_line=3) : {4}; -- stay in critical section, or leave
(p2_line=4) : {0}; -- back to starting point
TRUE: p2_line;
esac;
next(p2_ticket):=
case
(MAX_ticket=3): 0; --reset
(p2_line=1): MAX_ticket+1;
TRUE: p2_ticket;
esac;
next(p3_line) :=
case
(p3_line=0) : {0}; -- stay, or proceed
(p3_line=1) : {2};
(p3_line=2 & !p3-TOKEN) : 2 ; -- check TOKEN
(p3_line=2 & p3-TOKEN) : 3 ; -- check TOKEN
(p3_line=3) : {4}; -- stay in critical section, or leave
(p3_line=4) : {0}; -- back to starting point
TRUE: p3_line;
esac;
next(p3_ticket):=
case
(MAX_ticket=3): 0; --reset
(p3_line=1): MAX_ticket+1;
TRUE: p3_ticket;
esac;
DEFINE
STARTED := (p1_line!=0 | p2_line!=0 | p3_line!=0);
p1-TOKEN := STARTED & (p1_line=2) & ((p1_ticket <= p2_ticket) & (p1_ticket <= p3_ticket));
p2-TOKEN := STARTED & (p2_line=2) & ((((p2_ticket <= p1_ticket) & (p2_ticket <= p3_ticket))) | !p1-TOKEN);
p3-TOKEN := STARTED & (p3_line=2) & ((((p3_ticket <= p1_ticket) & (p3_ticket <= p2_ticket))) | !p1-TOKEN & !p2-TOKEN);
Formula
forall A. exists B.
(G
(
(p1-TOKEN[A] <-> p2-TOKEN[B])
/\(p2-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p2_line[B]*)
/\(*p2_line[A] = p1_line[B]*)
/\(p1-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p3_line[B]*)
/\(*p3_line[A] = p1_line[B]*)
/\(p2-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p2-TOKEN[B])
/\(*p2_line[A] = p3_line[B]*)
/\(*p3_line[A] = p2_line[B]*)
/\(p1-TOKEN[A] /\ p2-TOKEN[A] /\ p3-TOKEN[A])
/\(p1-TOKEN[B] /\ p2-TOKEN[B] /\ p3-TOKEN[B])
)
)
The Model(s)
--BAKERY ALGORITHM
--(adopted from the Bakery algorithm from: Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV’19))
MODULE main
VAR
p1_ticket: 0..3; -- the ticket number of p1
p2_ticket: 0..3; -- the ticket number of p2
p3_ticket: 0..3; -- the ticket number of p3
p4_ticket: 0..3; -- the ticket number of p4
p5_ticket: 0..3; -- the ticket number of p5
MAX_ticket: 0..3; -- let's say max ticket number is 3
p1_line: 0..4;
p2_line: 0..4;
p3_line: 0..4;
p4_line: 0..4;
p5_line: 0..4;
ASSIGN
init(p1_ticket) := 0;
init(p2_ticket) := 0;
init(p3_ticket) := 0;
init(p4_ticket) := 0;
init(p5_ticket) := 0;
init(p1_line) := 0;
init(p2_line) := 0;
init(p3_line) := 0;
init(p4_line) := 0;
init(p5_line) := 0;
init(MAX_ticket):= 0;
next(MAX_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1 | p2_line=1 | p3_line=1): MAX_ticket+1;
TRUE: MAX_ticket+1;
esac;
next(p1_line) :=
case
(p1_line=0) : {0,1}; -- stay, or proceed
(p1_line=1) : {2}; -- draw ticket
(p1_line=2 & !p1-TOKEN) : {2}; -- check TOKEN
(p1_line=2 & p1-TOKEN) : {3}; -- check TOKEN
(p1_line=3) : {4}; -- stay in critical section, or leave
(p1_line=4) : {0}; -- back to starting point
TRUE: p1_line;
esac;
next(p1_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1): MAX_ticket+1;
TRUE: p1_ticket;
esac;
next(p2_line) :=
case
(p2_line=0) : {0,1}; -- stay, or proceed
(p2_line=1) : {1};
(p2_line=2 & !p2-TOKEN): {2}; -- check TOKEN
(p2_line=2 & p2-TOKEN): {3}; -- check TOKEN
(p2_line=3) : {4}; -- stay in critical section, or leave
(p2_line=4) : {0}; -- back to starting point
TRUE: p2_line;
esac;
next(p2_ticket):=
case
(MAX_ticket=3): 0; --reset
(p2_line=1): MAX_ticket+1;
TRUE: p2_ticket;
esac;
next(p3_line) :=
case
(p3_line=0) : {0,1}; -- stay, or proceed
(p3_line=1) : {2};
(p3_line=2 & !p3-TOKEN) : 2 ; -- check TOKEN
(p3_line=2 & p3-TOKEN) : 3 ; -- check TOKEN
(p3_line=3) : {4}; -- stay in critical section, or leave
(p3_line=4) : {0}; -- back to starting point
TRUE: p3_line;
esac;
next(p3_ticket):=
case
(MAX_ticket=3): 0; --reset
(p3_line=1): MAX_ticket+1;
TRUE: p3_ticket;
esac;
next(p4_line) :=
case
(p4_line=0) : {0,1}; -- stay, or proceed
(p4_line=1) : {2};
(p4_line=2 & !p4-TOKEN) : 2 ; -- check TOKEN
(p4_line=2 & p4-TOKEN) : 3 ; -- check TOKEN
(p4_line=3) : {4}; -- stay in critical section, or leave
(p4_line=4) : {0}; -- back to starting point
TRUE: p4_line;
esac;
next(p4_ticket):=
case
(MAX_ticket=3): 0; --reset
(p4_line=1): MAX_ticket+1;
TRUE: p4_ticket;
esac;
next(p5_line) :=
case
(p5_line=0) : {0}; -- stay, or proceed
(p5_line=1) : {2};
(p5_line=2 & !p5-TOKEN) : 2 ; -- check TOKEN
(p5_line=2 & p5-TOKEN) : 3 ; -- check TOKEN
(p5_line=3) : {4}; -- stay in critical section, or leave
(p5_line=4) : {0}; -- back to starting point
TRUE: p5_line;
esac;
next(p5_ticket):=
case
(MAX_ticket=3): 0; --reset
(p5_line=1): MAX_ticket+1;
TRUE: p5_ticket;
esac;
DEFINE
p1-TOKEN := ((p1_ticket <= p2_ticket) & (p1_ticket <= p3_ticket)
& (p1_ticket <= p4_ticket)& (p1_ticket <= p5_ticket));
p2-TOKEN := ((((p2_ticket <= p1_ticket) & (p2_ticket <= p3_ticket)
& (p2_ticket <= p4_ticket) & (p2_ticket <= p5_ticket))) | !p1-TOKEN);
p3-TOKEN := ((((p3_ticket <= p1_ticket) & (p3_ticket <= p2_ticket)
& (p3_ticket <= p4_ticket) & (p3_ticket <= p5_ticket))) | !p1-TOKEN & !p2-TOKEN);
p4-TOKEN := ((((p4_ticket <= p1_ticket) & (p4_ticket <= p2_ticket)
& (p4_ticket <= p3_ticket) & (p4_ticket <= p5_ticket))) | !p1-TOKEN & !p2-TOKEN & !p3-TOKEN);
p5-TOKEN := ((((p5_ticket <= p1_ticket) & (p5_ticket <= p2_ticket)
& (p5_ticket <= p3_ticket) & (p5_ticket <= p4_ticket))) | !p1-TOKEN & !p2-TOKEN & !p3-TOKEN & !p4-TOKEN);
Formula
forall A. exists B.
(G
(
(p1-TOKEN[A] <-> p2-TOKEN[B])
/\(p2-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p2_line[B]*)
/\(*p2_line[A] = p1_line[B]*)
/\(p1-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p3_line[B]*)
/\(*p3_line[A] = p1_line[B]*)
/\(p1-TOKEN[A] <-> p4-TOKEN[B])
/\(p4-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p4_line[B]*)
/\(*p4_line[A] = p1_line[B]*)
/\(p1-TOKEN[A] <-> p5-TOKEN[B])
/\(p5-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p5_line[B]*)
/\(*p5_line[A] = p1_line[B]*)
)
)
The Model(s)
--BAKERY ALGORITHM
--(adopted from the Bakery algorithm from: Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV’19))
MODULE main
VAR
p1_ticket: 0..3; -- the ticket number of p1
p2_ticket: 0..3; -- the ticket number of p2
p3_ticket: 0..3; -- the ticket number of p3
p4_ticket: 0..3; -- the ticket number of p4
p5_ticket: 0..3; -- the ticket number of p5
MAX_ticket: 0..3; -- let's say max ticket number is 3
p1_line: 0..4;
p2_line: 0..4;
p3_line: 0..4;
p4_line: 0..4;
p5_line: 0..4;
ASSIGN
init(p1_ticket) := 0;
init(p2_ticket) := 0;
init(p3_ticket) := 0;
init(p4_ticket) := 0;
init(p5_ticket) := 0;
init(p1_line) := 0;
init(p2_line) := 0;
init(p3_line) := 0;
init(p4_line) := 0;
init(p5_line) := 0;
init(MAX_ticket):= 0;
next(MAX_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1 | p2_line=1 | p3_line=1): MAX_ticket+1;
TRUE: MAX_ticket+1;
esac;
next(p1_line) :=
case
(p1_line=0) : {0,1}; -- stay, or proceed
(p1_line=1) : {2}; -- draw ticket
(p1_line=2 & !p1-TOKEN) : {2}; -- check TOKEN
(p1_line=2 & p1-TOKEN) : {3}; -- check TOKEN
(p1_line=3) : {4}; -- stay in critical section, or leave
(p1_line=4) : {0}; -- back to starting point
TRUE: p1_line;
esac;
next(p1_ticket):=
case
(MAX_ticket=3): 0; --reset
(p1_line=1): MAX_ticket+1;
TRUE: p1_ticket;
esac;
next(p2_line) :=
case
(p2_line=0) : {0,1}; -- stay, or proceed
(p2_line=1) : {1};
(p2_line=2 & !p2-TOKEN): {2}; -- check TOKEN
(p2_line=2 & p2-TOKEN): {3}; -- check TOKEN
(p2_line=3) : {4}; -- stay in critical section, or leave
(p2_line=4) : {0}; -- back to starting point
TRUE: p2_line;
esac;
next(p2_ticket):=
case
(MAX_ticket=3): 0; --reset
(p2_line=1): MAX_ticket+1;
TRUE: p2_ticket;
esac;
next(p3_line) :=
case
(p3_line=0) : {0,1}; -- stay, or proceed
(p3_line=1) : {2};
(p3_line=2 & !p3-TOKEN) : 2 ; -- check TOKEN
(p3_line=2 & p3-TOKEN) : 3 ; -- check TOKEN
(p3_line=3) : {4}; -- stay in critical section, or leave
(p3_line=4) : {0}; -- back to starting point
TRUE: p3_line;
esac;
next(p3_ticket):=
case
(MAX_ticket=3): 0; --reset
(p3_line=1): MAX_ticket+1;
TRUE: p3_ticket;
esac;
next(p4_line) :=
case
(p4_line=0) : {0,1}; -- stay, or proceed
(p4_line=1) : {2};
(p4_line=2 & !p4-TOKEN) : 2 ; -- check TOKEN
(p4_line=2 & p4-TOKEN) : 3 ; -- check TOKEN
(p4_line=3) : {4}; -- stay in critical section, or leave
(p4_line=4) : {0}; -- back to starting point
TRUE: p4_line;
esac;
next(p4_ticket):=
case
(MAX_ticket=3): 0; --reset
(p4_line=1): MAX_ticket+1;
TRUE: p4_ticket;
esac;
next(p5_line) :=
case
(p5_line=0) : {0}; -- stay, or proceed
(p5_line=1) : {2};
(p5_line=2 & !p5-TOKEN) : 2 ; -- check TOKEN
(p5_line=2 & p5-TOKEN) : 3 ; -- check TOKEN
(p5_line=3) : {4}; -- stay in critical section, or leave
(p5_line=4) : {0}; -- back to starting point
TRUE: p5_line;
esac;
next(p5_ticket):=
case
(MAX_ticket=3): 0; --reset
(p5_line=1): MAX_ticket+1;
TRUE: p5_ticket;
esac;
DEFINE
p1-TOKEN := ((p1_ticket <= p2_ticket) & (p1_ticket <= p3_ticket)
& (p1_ticket <= p4_ticket)& (p1_ticket <= p5_ticket));
p2-TOKEN := ((((p2_ticket <= p1_ticket) & (p2_ticket <= p3_ticket)
& (p2_ticket <= p4_ticket) & (p2_ticket <= p5_ticket))) | !p1-TOKEN);
p3-TOKEN := ((((p3_ticket <= p1_ticket) & (p3_ticket <= p2_ticket)
& (p3_ticket <= p4_ticket) & (p3_ticket <= p5_ticket))) | !p1-TOKEN & !p2-TOKEN);
p4-TOKEN := ((((p4_ticket <= p1_ticket) & (p4_ticket <= p2_ticket)
& (p4_ticket <= p3_ticket) & (p4_ticket <= p5_ticket))) | !p1-TOKEN & !p2-TOKEN & !p3-TOKEN);
p5-TOKEN := ((((p5_ticket <= p1_ticket) & (p5_ticket <= p2_ticket)
& (p5_ticket <= p3_ticket) & (p5_ticket <= p4_ticket))) | !p1-TOKEN & !p2-TOKEN & !p3-TOKEN & !p4-TOKEN);
Formula
forall A. exists B.
(G
(
(p1-TOKEN[A] <-> p2-TOKEN[B])
/\(p2-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p2_line[B]*)
/\(*p2_line[A] = p1_line[B]*)
/\(p1-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p1-TOKEN[B])
/\(*p1_line[A] = p3_line[B]*)
/\(*p3_line[A] = p1_line[B]*)
/\(p2-TOKEN[A] <-> p3-TOKEN[B])
/\(p3-TOKEN[A] <-> p2-TOKEN[B])
/\(*p2_line[A] = p3_line[B]*)
/\(*p3_line[A] = p2_line[B]*)
/\
(
(~p1-TOKEN[A] /\ ~p2-TOKEN[A] /\ ~p3-TOKEN[A])
\/
(p1-TOKEN[B] \/ p2-TOKEN[B] \/ p3-TOKEN[B])
)
)
)