% Wang Yi et al.'s Brige Crossing Problem (See Examples in Uppaal package
% for the timed automata pictures.
% 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: 1 + Number of trains, 1 for the crossing
processnum(3).

% 0 for no symmetry, 1 for symmetry.
have_symmetry(1).

% Number 1 bigger than the biggest location number
saved_base(5).

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

% List of free variables
genvars([_, _, _, _, _]).

% Initial states
start_labels([0, 0, 0]).
start_mem([Y1, Y2, L1, L2, _Len]) :-
	Z >= 0, Y1 = Z, Y2 = Z, 
	L1 = 3, L2 = 3.
invariant([Y1, Y2, L1, L2, Len]) :-
	Y1 >= 0, Y2 >= 0, 
	L1 >= 1, L1 <= 3, L2 >= 1, L2 <= 3, 
	Len >= 0, Len <= 2.


% Transitions

trans([0, P1, P2], [1, P1, P2], [Y1, Y2, L1, L2, _Len], [Y11, Y21, L11, L21, Len1]) :-
	Len1 = 0, L11 = L1, L21 = L2, Z >= 0, Y11 = Y1 + Z, Y21 = Y2 + Z.
trans([2, 2, P2], [1, 0, P2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len = 1, Len1 = 0,
	Y1 >= 3, Y1 <= 5,
	L1 = 1, L11 = 3,
	L21 = L2, L2 = 3, 
	Z >= 0, Y11 = Z, Y21 = Y2 + Z.
trans([2, P1, 2], [1, P1, 0], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len = 1, Len1 = 0,
	Y2 >= 3, Y2 <= 5,
	L2 = 1, L21 = 3,
	L11 = L1, L1 = 3, 
	Z >= 0, Y11 = Y1 + Z, Y21 = Z.
trans([2, 2, 3], [2, 0, 4], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len <= 2, Len >= 2, Len1 <= 1, Len1 >= 1,
	Y1 >= 3, Y1 <= 5,
	L1 = 1, L11 = 3,
	Y2 <= 15,
	L2 = 2, L21 = 1,
	Z >= 0, Y11 = Z, Y21 = Z.
trans([2, 3, 2], [2, 4, 0], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len <= 2, Len >= 2, Len1 <= 1, Len1 >= 1,
	Y2 >= 3, Y2 <= 5,
	L2 = 1, L21 = 3,
	Y1 <= 15,
	L1 = 2, L11 = 1,
	Z >= 0, Y11 = Z, Y21 = Z.
trans([2, 0, P2], [2, 3, P2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len >= 0, Len <= 1, 
	Len1 >= 1, Len1 <= 2,
	L1 = 3, L11 = Len1,
	Z >= 0, Y11 = Z, Y21 = Y2 + Z.
trans([2, P1, 0], [2, P1, 3], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len >= 0, Len <= 1, 
	Len1 >= 1, Len1 <= 2,
	L2 = 3, L21 = Len1,
	Z >= 0, Y11 = Y1 + Z, Y21 = Z.
trans([1, 0, P2], [2, 1, P2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len = 0, Len1 = 1,
	Y11 <= 20,
	L1 = 3, L11 = 1,
	Z >= 0, Y11 = Z, Y21 = Y2 + Z.
trans([1, P1, 0], [2, P1, 1], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len = 0, Len1 = 1,
	Y21 <= 20,
	L2 = 3, L21 = 1,
	Z >= 0, Y11 = Y1 + Z, Y21 = Z.
trans([P0, 1, P2], [P0, 2, P2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len1 = Len, 	L11 = L1, 	L21 = L2, 	Y1 <= 20, Y1 >= 10, Y11 <= 5,
	Z >= 0, Y11 = Z, Y21 = Y2 + Z.
trans([P0, P1, 1], [P0, P1, 2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len1 = Len, 	L11 = L1, 	L21 = L2, 	Y2 <= 20, Y2 >= 10, Y21 <= 5,
	Z >= 0, Y11 = Y1 + Z, Y21 = Z.
trans([P0, 4, P2], [P0, 2, P2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len1 = Len, 	L11 = L1, 	L21 = L2, 	Y1 <= 7, Y1 >= 15, Y11 <= 5,
	Z >= 0, Y11 = Z, Y21 = Y2 + Z.
trans([P0, P1, 4], [P0, P1, 2], [Y1, Y2, L1, L2, Len], [Y11, Y21, L11, L21, Len1]) :-
	Len1 = Len, 	L11 = L1, 	L21 = L2, 	Y2 <= 7, Y2 >= 15, Y21 <= 5,
	Z >= 0, Y11 = Y1 + Z, Y21 = Z.

% Wrapper
run(Noise) :-
	ztime, processnum(N),
	mutex_violation(N - 1, [0, 0], [4, 4], 2, Cfg),
	gen_bounded_int(0, 2, X),
	cs(0, Noise, [y1, y2, l1, l2, len], [X|Cfg], [Y1, Y2, L1, L2, Len]),
	dump([Y1, Y2, L1, L2, Len], [y1, y2, l1, l2, len]).
run(_) :-
	ctime(T),
	counter_value(attempted_node, Anode),
	counter_value(unsubsumed_node, Unode),
	printf("Time % seconds, Unsubsumed % nodes, Tried % nodes\n", [T, Unode, Anode]).
separate_variables([Y1, Y2, L1, L2, Len], [Y1, Y2], [L1, L2], [Len]).


% Symmetry-related rules

sort_cfg(Ip, [CCfg|TCfg1], IpIdx1) :-
	Ip = [CCfg|TCfg],
	qsort1(TCfg, TCfg1),
	config_to_index([CCfg|TCfg1], 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 definition

symmetry(Ip1, V1, Ip2, V2) :-
	Ip1 = [X|TrainsCfg1],
	Ip2 = [X|TrainsCfg2],
	separate_variables(V1, Clocks1, List1, [Len1]),
	separate_variables(V2, Clocks2, List2, [Len2]),
	qsort(TrainsCfg1, Clocks1, List1, TrainsCfg2, Clocks2, List2),
	Len2 = Len1.

qsort(List, ListA, ListB, Sorted, SortedA, SortedB) :-
	qsort_aux(List,   ListA,   ListB,
                  [],     [],      [],
                  Sorted, SortedA, SortedB).

qsort_aux([],  [],   [], 
          Acc, AccA, AccB,
	  Acc, AccA, AccB).
qsort_aux([H|T],  [HA|TA], [HB|TB],
          Acc,    AccA,    AccB,
          Sorted, SortedA, SortedB) :-
	pivoting(H, T,  TA,  TB,
                    L1, L1A, L1B,
                    L2, L2A, L2B),
	qsort_aux(L1,      L1A,      L1B,
	          Acc,     AccA,     AccB,
	          Sorted1, Sorted1A, Sorted1B),
	qsort_aux(L2,          L2A,           L2B,
                  [H|Sorted1], [HA|Sorted1A], [HB|Sorted1B],
		  Sorted,      SortedA,       SortedB).

pivoting(_H, [], [], [],
             [], [], [],
             [], [], []).
pivoting(H, [X|T], [XA|TA], [XB|TB],
            [X|L], [XA|LA], [XB|LB],
            G,     GA,      GB) :-
	X >= H, pivoting(H, T, TA, TB,
                            L, LA, LB,
                            G, GA, GB).
pivoting(H, [X|T], [XA|TA], [XB|TB],
            L,     LA,      LB,
            [X|G], [XA|GA], [XB|GB]) :-
	X <= H, pivoting(H, T, TA, TB,
                           L, LA, LB,
                           G, GA, GB).

:- consult('u28b.clpr').