% 2-Processes Fischer's Mutual Exclusion Algorithm
% This is the looping algorithm: not just the entry protocol
% 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).

% Number of processes
processnum(2).

% A number 1 bigger than the greatest location number
saved_base(4).

% 1 = use symmetry routines, 0 = do not use symmetry
have_symmetry(0).

% Just leave it like this for all examples
which_table([X|_], X).

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

% Invariant to be enforced so that the engine
% won't search impossible region of state space.
invariant([X0, X1, _K]) :- X0 >= 0, X1 >= 0.

% Initial locations and state
start_labels([0, 0]).
start_mem([X0, X1, K]) :- K = room([1, 0, 0]), Z >= 0, X0 = Z, X1 = Z.

% Transitions
trans([0, P1], [1, P1], [X0, X1, K], [X01, X11, K1]) :-
	K = K1, K = room([1, 0, 0]),
	Z >= 0, X01 = Z, X11 = X1 + Z.
trans([P0, 0], [P0, 1], [X0, X1, K], [X01, X11, K1]) :-
	K = K1, K = room([1, 0, 0]),
	Z >= 0, X01 = X0 + Z, X11 = Z.
trans([1, P1], [2, P1], [X0, X1, K], [X01, X11, K1]) :-
	K1 = room([0, 1, 0]),
	X0 <= 2, Z >= 0, X01 = Z, X11 = X1 + Z.
trans([P0, 1], [P0, 2], [X0, X1, K], [X01, X11, K1]) :-
	K1 = room([0, 0, 1]),
	X1 <= 2, Z >= 0, X01 = X0 + Z, X11 = Z.
trans([2, P1], [3, P1], [X0, X1, K], [X01, X11, K1]) :-
	K = K1, K = room([0, 1, 0]),
	X0 >= 4, Z >= 0, X01 = X0 + Z, X11 = X1 + Z.
trans([P0, 2], [P0, 3], [X0, X1, K], [X01, X11, K1]) :-
	K = K1, K = room([0, 0, 1]),
	X1 >= 4, Z >= 0, X01 = X0 + Z, X11 = X1 + Z.
trans([3, P1], [0, P1], [X0, X1, K], [X01, X11, K1]) :-
	K1 = room([1, 0, 0]),
	Z >= 0, X01 = X0 + Z, X11 = X1 + Z.
trans([P0, 3], [P0, 0], [X0, X1, K], [X01, X11, K1]) :-
	K1 = room([1, 0, 0]),
	Z >= 0, X01 = X0 + Z, X11 = X1 + Z.
trans([2, P1], [0, P1], [X0, X1, K], [X01, X11, K1]) :-
	K = K1, K = room([_, 0, _]),
	X0 >= 4, Z >= 0, X01 = X0 + Z, X11 = X1 + Z.
trans([P0, 2], [P0, 0], [X0, X1, K], [X01, X11, K1]) :-
	K = K1, K = room([_, _, 0]),
	X1 >= 4, Z >= 0, X01 = X0 + Z, X11 = X1 + Z.


% Some wrapper to make running easier

run(Noise) :-
	ztime, processnum(Len),
	mutex_violation(Len, [0, 0], [3, 3], 3, Cfg),
	cs(0, Noise, [x0, x1, k], Cfg, [X0, X1, K]),
	dump([X0, X1, K], [x0, x1, k]).
run(_) :-
	ctime(T),
	counter_value(attempted_node, Anode),
	counter_value(unsubsumed_node, Unode),
printf("Time % seconds, Unsubsumed % nodes, Tried % nodes\n", [T, Unode, Anode]).


% Followings are symmetry-related predicates

separate_variables([X0, X1, K], [X0, X1], [K]).

sort_cfg(Ip, Ip1, IpIdx1) :-
	qsort1(Ip, Ip1),
	config_to_index(Ip1, IpIdx1), !.

qsort1(List, Sorted) :-
	qsort1_aux(List, [], Sorted).

qsort1_aux([], Acc, Acc).
qsort1_aux([H|T], Acc, Sorted) :-
	pivoting1(H, T, L1, L2),
	qsort1_aux(L1, Acc, Sorted1),
	qsort1_aux(L2, [H|Sorted1], Sorted).

pivoting1(_H, [], [], []).
pivoting1(H, [X|T], [X|L], G) :-
	X >= H, pivoting1(H, T, L, G).
pivoting1(H, [X|T], L, [X|G]) :-
	X < H, pivoting1(H, T, L, G).


symmetry(Ip1, V1, Ip2, V2) :-
	separate_variables(V1, Clocks1, [K1]), % not var(K1),
	separate_variables(V2, Clocks2, [K2]),
	K1 = room([H|K1T]),
	K2 = room([H|K2T]),
	sym_qsort1(Ip1, Clocks1, K1T, Ip2, Clocks2, K2T).
%symmetry(Ip1, V1, Ip2, V2) :-
%	separate_variables(V1, Clocks1, [K1]), var(K1),
%	separate_variables(V2, Clocks2, [K1]),
%	sym_qsort2(Ip1, Clocks1, Ip2, Clocks2).

sym_qsort1(List, ListA, ListB, Sorted, SortedA, SortedB) :-
	sym_qsort1_aux(List,   ListA,   ListB,
                  [],     [],      [],
                  Sorted, SortedA, SortedB).
sym_qsort1_aux([],  [],   [], 
          Acc, AccA, AccB,
	  Acc, AccA, AccB).
sym_qsort1_aux([H|T],  [HA|TA], [HB|TB],
          Acc,    AccA,    AccB,
          Sorted, SortedA, SortedB) :-
	sym_pivoting1(H, T,  TA,  TB,
                    L1, L1A, L1B,
                    L2, L2A, L2B),
	sym_qsort1_aux(L1,      L1A,      L1B,
	          Acc,     AccA,     AccB,
	          Sorted1, Sorted1A, Sorted1B),
	sym_qsort1_aux(L2,          L2A,           L2B,
                  [H|Sorted1], [HA|Sorted1A], [HB|Sorted1B],
		  Sorted,      SortedA,       SortedB).
sym_pivoting1(_H, [], [], [],
             [], [], [],
             [], [], []).
sym_pivoting1(H, [X|T], [XA|TA], [XB|TB],
            [X|L], [XA|LA], [XB|LB],
            G,     GA,      GB) :-
	X >= H, sym_pivoting1(H, T, TA, TB,
                            L, LA, LB,
                            G, GA, GB).
sym_pivoting1(H, [X|T], [XA|TA], [XB|TB],
            L,     LA,      LB,
            [X|G], [XA|GA], [XB|GB]) :-
	X <= H, sym_pivoting1(H, T, TA, TB,
                           L, LA, LB,
                           G, GA, GB).

sym_qsort2(List, ListA, Sorted, SortedA) :-
	sym_qsort2_aux(List,   ListA,
                       [],     [], 
                       Sorted, SortedA).
sym_qsort2_aux([],  [],
               Acc, AccA,
	       Acc, AccA).
sym_qsort2_aux([H|T],  [HA|TA],
               Acc,    AccA,
               Sorted, SortedA) :-
  	sym_pivoting2(H, T,  TA,
                         L1, L1A,
                         L2, L2A),
	sym_qsort2_aux(L1,      L1A,
	               Acc,     AccA,
	               Sorted1, Sorted1A),
	sym_qsort2_aux(L2,          L2A,
                       [H|Sorted1], [HA|Sorted1A],
	    	       Sorted,      SortedA).
sym_pivoting2(_H, [], [],
                  [], [],
                  [], []).
sym_pivoting2(H, [X|T], [XA|TA],
                 [X|L], [XA|LA],
                 G,     GA) :-
	X >= H, sym_pivoting2(H, T, TA,
                                 L, LA,
                                 G, GA).
sym_pivoting2(H, [X|T], [XA|TA],
                 L,     LA,
                 [X|G], [XA|GA]) :-
	X <= H, sym_pivoting2(H, T, TA,
                                 L, LA,
                                 G, GA).

:- consult('u28b.clpr').