:- module(ta,[main/0,main/1]).

:- use_module(library(chr)).
:- use_module(library(lists)).

/*

	Timed automaton => Constraints

			=>

	 X := N			geq(X,N)
	-------->

	 X =< N			leq(X,N)
	-------->

	 X >= N			geq(X,N)
	-------->


n > 1,	1 ------> v		fincl(Xv,X1),
	...    /		...
	n ----/			fincl(Xv,Xn),
				fub_init(Xv,[])

n >= 1, v ------> 1		bincl(Xv,X1),
	  \     ...		...
	   \----> n		bincl(Xv,X1),
				bub_init(Xv,[])
*/

%% handler ta.

:- chr_constraint

	fincl/2,	% expresses that clock 1 includes clock 2 (union)
			% in the sense that clock 2 is forward of clock 1

	bincl/2,	% expresses that clock 1 includes clock 2 (union)
			% in the sense that clock 1 is forward of clock 2

	leq/2,		% expresses that clock 1 =< number 2

	geq/2,		% expresses that clock 1 >= number 2

	fub_init/2,	% collects the inital upper bounds
			% from incoming arrows for clock 1 in list 2

	fub/2,		% collects the upper bounds for clock 1
			% from incoming arrows in list 2

	flb_init/2,	% collects the inital lower bounds
			% from incoming arrows for clock 1 in list 2

	flb/2,		% collects the lower bounds for clock 1
			% from incoming arrows in list 2

	bub_init/2,	% collects the inital upper bounds
			% from backward arrows for clock 1 in list 2

	bub/2,		% collects the upper bounds for clock 1
			% from outgoing arrows in list 2
			% values of clock 1 cannot exceed all
			% values of the clocks in list 2

	blb_init/2,	% collects the inital lower bounds
			% from backward arrows for clock 1 in list 2

	blb/2,		% collects the lower bounds for clock 1
			% from outgoing arrows in list 2
			% not all values of clock 1 can exceed any
			% values of the clocks in list 2

	compl/1,	% indicate that all incoming arrows for clock 1
			% have been registerd

	dist/3,		% indicates that clock 1 - clock 2 =< number 3

	fdist_init/3,	% records initial distances for clock 1 and clock 2 from
			% incoming arrows in list 3

	fdist/3,	% records distances for clock 1 and clock 2 from
			% incoming arrows in list 3

	setdist/3.	% sets distance between clock 1 and clock 2, where
			% clock 1 is reset to value 3

/* More Constraints:

*/

leq(X,N1) \ leq(X,N2) <=> N1 =< N2 | true.

geq(X,N1) \ geq(X,N2) <=> N2 =< N1 | true.

dist(X,Y,D1) \ dist(X,Y,D2) <=> D1 =< D2 | true.

dist(X,Y,D), leq(Y,MY) \ leq(X,MX1) <=>
	MX2 is MY + D, MX2 < MX1 | leq(X,MX2).

dist(X,Y,D), geq(X,MX) \ geq(Y,MY1) <=>
	MY2 is MX - D, MY2 > MY1 | geq(Y,MY2).

fincl(X,Y), leq(Y,N) \ fub_init(X,L)
	<=> \+ memberchk_eq(N-Y,L) |
	    insert_ub(L,Y,N,NL),
	    fub_init(X,NL).

fincl(X,Y), geq(Y,N) \ flb_init(X,L)
	<=> \+ memberchk_eq(N-Y,L) |
	    insert_lb(L,Y,N,NL),
	    flb_init(X,NL).

dist(X1,Y1,D), fincl(X2,X1), fincl(Y2,Y1) \ fdist_init(X2,Y2,L)
	<=>
	\+ memberchk_eq(D-X1,L) |
	insert_ub(L,X1,D,NL),
	fdist_init(X2,Y2,NL).

bincl(X,Y), leq(Y,N) \ bub_init(X,L)
	<=>
	\+ memberchk_eq(N-Y,L) |
	insert_ub(L,Y,N,NL),
	bub_init(X,NL).

compl(X) \ fub_init(X,L) # ID
	<=>
	fub(X,L),
	val(L,M),
	leq(X,M)
	pragma passive(ID).

compl(X) \ flb_init(X,L) # ID
	<=>
	flb(X,L),
	val(L,M),
	geq(X,M)
	pragma passive(ID).

compl(X), compl(Y) \ fdist_init(X,Y,L) # ID
	<=>
	fdist(X,Y,L),
	val(L,D),
	dist(X,Y,D)
	pragma passive(D).

compl(X) \ bub_init(X,L) # ID
	<=>
	bub(X,L),
	val(L,M),
	leq(X,M)
	pragma passive(ID).

fincl(X,Y), leq(Y,N) \ fub(X,L)
	<=>
	\+ memberchk_eq(N-Y,L) |
	insert_ub(L,Y,N,NL),
	fub(X,NL),
	val(NL,M),
	leq(X,M).

fincl(X,Y), geq(Y,N) \ flb(X,L)
	<=>
	\+ memberchk_eq(N-Y,L) |
	insert_lb(L,Y,N,NL),
	flb(X,NL),
	val(NL,M),
	geq(X,M).

bincl(X,Y), leq(Y,N) \ bub(X,L)
	<=>
	\+ memberchk_eq(N-Y,L) |
	insert_ub(L,Y,N,NL),
	bub(X,NL),
	val(NL,M),
	leq(X,M).

fincl(X2,X1), fincl(Y2,Y1), dist(X1,Y1,D) \ fdist(X2,Y2,L)
	<=>
	\+ memberchk_eq(D-X1,L) |
	insert_ub(L,X1,D,NL),
	fdist(X2,Y2,NL),
	val(NL,MD),
	dist(X2,Y2,MD).

fincl(X,Y), leq(X,N) ==> leq(Y,N).

fincl(X,Y), geq(X,N) ==> geq(Y,N).

bincl(X,Y), geq(X,N) ==> geq(Y,N).

bincl(X1,X2), bincl(Y1,Y2), dist(X1,Y1,D1) \ dist(X2,Y2,D2) <=> D1 < D2 | dist(X2,Y2,D1).

setdist(X,Y,N), leq(Y,D1) ==> D2 is D1 - N, dist(Y,X,D2).
setdist(X,Y,N), geq(Y,D1) ==> D2 is N - D1, dist(X,Y,D2).

val([N-_|_],N).

insert_ub([],X,N,[N-X]).
insert_ub([M-Y|R],X,N,NL) :-
	( Y == X ->
		insert_ub(R,X,N,NL)
	; M > N ->
		NL = [M-Y|NR],
		insert_ub(R,X,N,NR)
	;
		NL = [N-X,M-Y|R]
	).

insert_lb([],X,N,[N-X]).
insert_lb([M-Y|R],X,N,NL) :-
	( Y == X ->
		insert_lb(R,X,N,NL)
	; M < N ->
		NL = [M-Y|NR],
		insert_lb(R,X,N,NR)
	;
		NL = [N-X,M-Y|R]
	).

couple(X,Y) :-
	dist(X,Y,10000),
	dist(Y,X,10000).

giri :-
	giri([x1,y1,x2,y2,x3,y3,x4,y4,x5,y5,x6,y6,x7,y7,x8,y8,x9,y9,x10,y10]).

giri(L) :-
	L = [X1,Y1,X2,Y2,X3,Y3,X4,Y4,X5,Y5,X6,Y6,X7,Y7,X8,Y8,X9,Y9,X10,Y10],
	clocks(L),

	% 1.
	couple(X1,Y1),
	geq(X1,0),
	geq(X2,0),
	dist(X1,Y1,0),
	dist(Y1,X1,0),

	% 2.
	couple(X2,Y2),

	fincl(X2,X1),
	fincl(X2,X8),
	fincl(X2,X10),
	fub_init(X2,[]),
	flb_init(X2,[]),

	fincl(Y2,Y1),
	fincl(Y2,Y8),
	fincl(Y2,Y10),
	fub_init(Y2,[]),
	flb_init(Y2,[]),

	bincl(X2,X3),
	bincl(X2,X4),
	bub_init(X2,[]),
	blb_init(X2,[]),

	bincl(Y2,Y3),
	bincl(Y2,Y4),
	bub_init(Y2,[]),
	blb_init(Y2,[]),

	fdist_init(X2,Y2,[]),
	fdist_init(Y2,X2,[]),

	% 3.
	couple(X3,Y3),
	leq(X3,3),

	bincl(X3,X9),
	bincl(X3,X5),
	bub_init(X3,[]),
	blb_init(X3,[]),

	bincl(Y3,Y9),
	bincl(Y3,Y5),
	bub_init(Y3,[]),
	blb_init(Y3,[]),

	%fdist_init(X3,Y3,[]),
	%fdist_init(Y3,X3,[]),

	% 4.
	couple(X4,Y4),
	geq(Y4,2),
	leq(Y4,5),

	% 5.
	couple(X5,Y5),
	geq(Y5,5),
	leq(Y5,10),

	% 6.
	couple(X6,Y6),

	fincl(X6,X4),
	fincl(X6,X5),
	fub_init(X6,[]),
	flb_init(X6,[]),

	fincl(Y6,Y4),
	fincl(Y6,Y5),
	fub_init(Y6,[]),
	flb_init(Y6,[]),

	bincl(X6,X7),
	bub_init(X6,[]),

	bincl(Y6,Y7),
	bub_init(Y6,[]),

	fdist_init(X6,Y6,[]),
	fdist_init(Y6,X6,[]),

	% 7.
	couple(X7,Y7),
	geq(Y7,15),
	leq(Y7,15),

	% 8.
	couple(X8,Y8),
	geq(X8,2),
	geq(Y8,2),
	dist(X8,Y8,0),
	dist(Y8,X8,0),

	% 9.
	couple(X9,Y9),
	geq(Y9,5),
	leq(Y9,5),


	% 10.
	couple(X10,Y10),
	geq(X10,0),
	geq(Y10,0),
	dist(X10,Y10,0),
	dist(Y10,X10,0),

	% finish
	compl(X2),
	compl(Y2),

	compl(X3),
	compl(Y3),

	compl(X6),
	compl(Y6).



clocks([]).
clocks([C|Cs]) :-
	clock(C),
	clocks(Cs).

clock(X) :-
	geq(X,0),
	leq(X,10000).

main :-
	main(100).

main(N) :-
	cputime(T1),
	loop(N),
	cputime(T2),
	T is T2 - T1,
	write(bench(ta ,N , T,0,hprolog)),write('.'),nl.


loop(N) :-
	( N =< 0 ->
		true
	;
		( giri, fail ; true),
		M is N - 1,
		loop(M)
	).