%------------------------------------------------------------------------------
% Dining Philosophers Example
% by Andrew E. Santosa
% To run: ?- run(X). where X = 0 (no noise), 1 (display states visited),
% 2 (display states visited, and stop for input at each state).
%------------------------------------------------------------------------------

% A table for 3 person
processnum(3).

% A number 1 bigger than the biggest program point
saved_base(3).

% 1 = run with symmetry, 
have_symmetry(1).

% Leave the following as is.
which_table([X|_], X).

% Free variables, same as number of program variables
genvars([_, _, _, _, _, _]).

% True
invariant([_, _, _, _, _, _]).

% Initial state
start_labels([0, 0, 0]).
start_mem([X0, X1, X2, Y0, Y1, Y2]) :- 
	Z >= 0,
	X0 = Z, X1 = Z, X2 = Z,
	Y0 = Z, Y1 = Z, Y2 = Z.

% This is to be applied in the transitions
trans_invariant([X0, X1, X2, Y0, Y1, Y2]) :-
	X0 >= 0, X1 >= 0, X2 >= 0,
	Y0 >= 0, Y1 >= 0, Y2 >= 0.

trans([0, 0, P2], [0, 0, P2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = Z, X11 = X1 + Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P2 < 2; P2 = 2, X21 < 2), 
	X0 < 1, X11 < 1,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([0, 1, P2], [0, 2, P2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = Z, X11 = Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P2 < 2; P2 = 2, X21 < 2), 
	X0 < 1, X11 < 2,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([0, P1, P2], [1, P1, P2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = X1 + Z, X21 = X2 + Z, 
	Y01 = Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P1 < 2; P1 = 2, X11 < 2), (P2 < 2; P2 = 2, X21 < 2),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([2, 0, P2], [0, 0, P2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = Z, X11 = X1 + Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P2 < 2; P2 = 2, X21 < 2), 
	X0 < 2, X11 < 1,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([2, 1, P2], [0, 2, P2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = Z, X11 = Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P2 < 2; P2 = 2, X21 < 2), 
	X0 < 2, X11 < 2,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([P0, 0, 0], [P0, 0, 0], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P0 < 2; P0 = 2, X01 < 2), 
	X1 < 1, X21 < 1,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([P0, 0, 1], [P0, 0, 2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = Z, X21 = Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P0 < 2; P0 = 2, X01 < 2), 
	X1 < 1, X21 < 2,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([P0, 0, P2], [P0, 1, P2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = X1 + Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Z, Y21 = Y2 + Z,
	(P0 < 2; P0 = 2, X01 < 2), (P2 < 2; P2 = 2, X21 < 2),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([P0, 2, 0], [P0, 0, 0], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P0 < 2; P0 = 2, X01 < 2), 
	X1 < 2, X21 < 1,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([P0, 2, 1], [P0, 0, 2], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = Z, X21 = Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P0 < 2; P0 = 2, X01 < 2), 
	X1 < 2, X21 < 2,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([0, P1, 0], [0, P1, 0], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = X1 + Z, X21 = Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P1 < 2; P1 = 2, X11 < 2), 
	X2 < 1, X01 < 1,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([1, P1, 0], [2, P1, 0], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = Z, X11 = X1 + Z, X21 = Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P1 < 2; P1 = 2, X11 < 2), 
	X2 < 1, X01 < 2,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([P0, P1, 0], [P0, P1, 1], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = X1 + Z, X21 = X2 + Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Z,
	(P0 < 2; P0 = 2, X01 < 2), (P1 < 2; P1 = 2, X11 < 2),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([0, P1, 2], [0, P1, 0], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = X0 + Z, X11 = X1 + Z, X21 = Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P1 < 2; P1 = 2, X11 < 2), 
	X2 < 2, X01 < 1,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).
trans([1, P1, 2], [2, P1, 0], [X0, X1, X2, Y0, Y1, Y2], [X01, X11, X21, Y01, Y11, Y21]) :-
	Z >= 0,
	X01 = Z, X11 = X1 + Z, X21 = Z, 
	Y01 = Y0 + Z, Y11 = Y1 + Z, Y21 = Y2 + Z,
	(P1 < 2; P1 = 2, X11 < 2), 
	X2 < 2, X01 < 2,
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]),
	trans_invariant([X0, X1, X2, Y0, Y1, Y2]).


%------------------------------------------------------------------------------
% Wrapper for running the program
%------------------------------------------------------------------------------

% Generator of violating configurations: two adjacent philosophers
% are eating at the same time.

gen_numbers(I, L) :-
	processnum(N),
	gen_numbers_aux(I, N, L).

gen_numbers_aux(0, 0, []).
gen_numbers_aux(0, N + 1, [2|R]) :-
	N >= 0,
	gen_numbers_aux(N, N, R).
gen_numbers_aux(I + 1, N + 1, [0|R]) :-
	I >= 0, N >= 0,
	gen_numbers_aux(I, N, R).
gen_numbers_aux(I + 1, N + 1, [1|R]) :-
	I >= 0, N >= 0,
	gen_numbers_aux(I, N, R).
gen_numbers_aux(I + 1, N + 1, [2|R]) :-
	I >= 0, N >= 0,
	gen_numbers_aux(I, N, R).

% Wrapper predicate

run(_) :-
	ztime, fail.
run(Noise) :-
	gen_numbers(0, Cfg), Y0 >= 6,
	cs(0, Noise, [x0, x1, x2, y0, y1, y2], Cfg, [X0, X1, X2, Y0, Y1, Y2]),
	dump([Y0], [y0]).
run(Noise) :-
	gen_numbers(1, Cfg), Y1 >= 6,
	cs(0, Noise, [x0, x1, x2, y0, y1, y2], Cfg, [X0, X1, X2, Y0, Y1, Y2]),
	dump([Y1], [y1]).
run(Noise) :-
	gen_numbers(2, Cfg), Y2 >= 6,
	cs(0, Noise, [x0, x1, x2, y0, y1, y2], Cfg, [X0, X1, X2, Y0, Y1, Y2]),
	dump([Y2], [y2]).
run(_) :-
	ctime(T),
	counter_value(attempted_node, Anode),
	counter_value(unsubsumed_node, Unode),
	printf("Time % seconds, Unsubsumed % nodes, Tried % nodes\n", [T, Unode, Anode]).

%------------------------------------------------------------------------------
% Rotational symmetry implementation
%------------------------------------------------------------------------------

symmetry(Ip1, V1, Ip2, V2) :-
	separate_variables(V1, X1, Y1),
	separate_variables(V2, X2, Y2),
	canon_form([Ip1, X1, Y1], [Ip2, X2, Y2]).

sort_cfg(Ip, Ip1, IpIdx1) :-
        canon_form([Ip], [Ip1]),
        config_to_index(Ip1, IpIdx1), !.


canon_form(L, L1) :-
	rotater(L, L2),
	rotatel(L2, L1).

rotatel([[H, I|R]|ListL], RotatedL) :-
	H > I,
	rotate_all_left([[H, I|R]|ListL], ListL1),
	rotatel(ListL1, RotatedL).
rotatel([[H, I|R]|ListL], [[H, I|R]|ListL]) :-
	H <= I.

rotater([L|ListL], RotatedL) :-
	last_two(L, [H, I]),
	H > I,
	rotate_all_right([L|ListL], ListL1),
	rotater(ListL1, RotatedL).
rotater([L|ListL], [L|ListL]) :-
	last_two(L, [H, I]),
	H <= I.

last_two([A, B], [A, B]).
last_two([_, B, C|R], T2) :-
	last_two([B, C|R], T2).

rotate_all_left([], []).
rotate_all_left([L|R], [L1|S]) :-
	shiftl(L, L1),
	rotate_all_left(R, S).

rotate_all_right([], []).
rotate_all_right([L|R], [L1|S]) :-
	shiftr(L, L1),
	rotate_all_right(R, S).

shiftr([X0, X1, X2], [X2, X0, X1]).
shiftl([X0, X1, X2], [X1, X2, X0]).

separate_variables([X0, X1, X2, Y0, Y1, Y2], [X0, X1, X2], [Y0, Y1, Y2]).

:- consult('u28b.clpr').