gistfile1.txt

%name P1;
%name P2;
%name P3;
%name P4;
%name P5;

%name F1;
%name F2;
%name F3;
%name F4;
%name F5;

%passive F : 1; # Fork-id
%passive P : 3; # Left-fork, Phil-id, Right-fork
%passive Q : 1; # Fork-id - placeholder

# Acquire a left fork
P[lf1,p1,rf1] || F[lf1] -> P[lf1,p1,rf1].F[lf1] || Q[lf1];
# Acquire a right fork
P[lf2,p2,rf2].F[lf2] || F[rf2] -> P[lf2,p2,rf2].(F[lf2] | F[rf2]) || Q[rf2];
# Drop left fork
P[lf3,p3,rf3].(F[lf3] | F[rf3]) || Q[lf3] -> P[lf3,p3,rf3].F[rf3] || F[lf3];
# Drop right fork
P[lf4,p4,rf4].F[rf4] || Q[rf4] -> P[lf4,p4,rf4] || F[rf4];

# The philosopher's table!

F[F1] | P[F1,P1,F2] | F[F2] | P[F2,P2,F3] | F[F3] | P[F3,P3,F4] | F[F4] | P[F4,P4,F5] | F[F5] | P[F5,P5,F1];

%property deadlock_free !terminal();

%check;

================================================================================================


> /usr/local/bigmc/bin/bigmc -m 1000 -r 50 /var/folders/Nc/Nc1H5h9TH14SM3+s7s-JhqO+ols/-Tmp-/bigmc_model8658463124795779775.bgm
[mc::report] [q: 94 / g: 144] @ 50
[mc::report] [q: 155 / g: 255] @ 100
[mc::report] [q: 218 / g: 368] @ 150
*** Found violation of property: deadlock_free
*** deadlock_free: !terminal()
#0  (Q[F4].nil | Q[F2].nil | Q[F3].nil | P[F3,P3,F4].F[F3].nil | P[F1,P1,F2].F[F1].nil | Q[F1].nil | P[F4,P4,F5].F[F4].nil | Q[F5].nil | P[F5,P5,F1].F[F5].nil | P[F2,P2,F3].F[F2].nil)   <- *** VIOLATION ***
 >> P[lf1,p1,rf1].nil || F[lf1].nil -> P[lf1,p1,rf1].F[lf1].nil || Q[lf1].nil

#1  (F[F2].nil | Q[F4].nil | Q[F3].nil | P[F3,P3,F4].F[F3].nil | P[F1,P1,F2].F[F1].nil | Q[F1].nil | P[F4,P4,F5].F[F4].nil | Q[F5].nil | P[F5,P5,F1].F[F5].nil | P[F2,P2,F3].nil)
 >> P[lf1,p1,rf1].nil || F[lf1].nil -> P[lf1,p1,rf1].F[lf1].nil || Q[lf1].nil

#2  (Q[F1].nil | P[F1,P1,F2].F[F1].nil | F[F2].nil | P[F2,P2,F3].nil | F[F3].nil | P[F3,P3,F4].nil | Q[F4].nil | P[F4,P4,F5].F[F4].nil | Q[F5].nil | P[F5,P5,F1].F[F5].nil)
 >> P[lf1,p1,rf1].nil || F[lf1].nil -> P[lf1,p1,rf1].F[lf1].nil || Q[lf1].nil

#3  (Q[F1].nil | P[F1,P1,F2].F[F1].nil | F[F2].nil | P[F2,P2,F3].nil | F[F3].nil | P[F3,P3,F4].nil | F[F4].nil | P[F4,P4,F5].nil | Q[F5].nil | P[F5,P5,F1].F[F5].nil)
 >> P[lf1,p1,rf1].nil || F[lf1].nil -> P[lf1,p1,rf1].F[lf1].nil || Q[lf1].nil

#4  (Q[F1].nil | P[F1,P1,F2].F[F1].nil | F[F2].nil | P[F2,P2,F3].nil | F[F3].nil | P[F3,P3,F4].nil | F[F4].nil | P[F4,P4,F5].nil | F[F5].nil | P[F5,P5,F1].nil)
 >> P[lf1,p1,rf1].nil || F[lf1].nil -> P[lf1,p1,rf1].F[lf1].nil || Q[lf1].nil

#5  (F[F1].nil | P[F1,P1,F2].nil | F[F2].nil | P[F2,P2,F3].nil | F[F3].nil | P[F3,P3,F4].nil | F[F4].nil | P[F4,P4,F5].nil | F[F5].nil | P[F5,P5,F1].nil)
 >> (root)
[mc::step] Counter-example found.