1:- module(ta,[main/0,main/1]).
2
3:- use_module(library(chr)).
4:- use_module(library(lists)).
5
6/*
7
8	Timed automaton => Constraints
9
10			=>
11
12	 X := N			geq(X,N)
13	-------->
14
15	 X =< N			leq(X,N)
16	-------->
17
18	 X >= N			geq(X,N)
19	-------->
20
21
22n > 1,	1 ------> v		fincl(Xv,X1),
23	...    /		...
24	n ----/			fincl(Xv,Xn),
25				fub_init(Xv,[])
26
27n >= 1, v ------> 1		bincl(Xv,X1),
28	  \     ...		...
29	   \----> n		bincl(Xv,X1),
30				bub_init(Xv,[])
31*/
32
33%% handler ta.
34
35:- constraints
36
37	fincl/2, 	% expresses that clock 1 includes clock 2 (union)
38			% in the sense that clock 2 is forward of clock 1
39
40	bincl/2, 	% expresses that clock 1 includes clock 2 (union)
41			% in the sense that clock 1 is forward of clock 2
42
43	leq/2, 		% expresses that clock 1 =< number 2
44
45	geq/2, 		% expresses that clock 1 >= number 2
46
47	fub_init/2, 	% collects the inital upper bounds
48			% from incoming arrows for clock 1 in list 2
49
50	fub/2,		% collects the upper bounds for clock 1
51			% from incoming arrows in list 2
52
53	flb_init/2, 	% collects the inital lower bounds
54			% from incoming arrows for clock 1 in list 2
55
56	flb/2,		% collects the lower bounds for clock 1
57			% from incoming arrows in list 2
58
59	bub_init/2, 	% collects the inital upper bounds
60			% from backward arrows for clock 1 in list 2
61
62	bub/2,		% collects the upper bounds for clock 1
63			% from outgoing arrows in list 2
64			% values of clock 1 cannot exceed all
65			% values of the clocks in list 2
66
67	blb_init/2, 	% collects the inital lower bounds
68			% from backward arrows for clock 1 in list 2
69
70	blb/2,		% collects the lower bounds for clock 1
71			% from outgoing arrows in list 2
72			% not all values of clock 1 can exceed any
73			% values of the clocks in list 2
74
75	compl/1,	% indicate that all incoming arrows for clock 1
76			% have been registerd
77
78	dist/3,		% indicates that clock 1 - clock 2 =< number 3
79
80	fdist_init/3,	% records initial distances for clock 1 and clock 2 from
81			% incoming arrows in list 3
82
83	fdist/3,	% records distances for clock 1 and clock 2 from
84			% incoming arrows in list 3
85
86	setdist/3.	% sets distance between clock 1 and clock 2, where
87			% clock 1 is reset to value 3
88
89/* More Constraints:
90
91*/
92
93leq(X,N1) \ leq(X,N2) <=> N1 =< N2 | true.
94
95geq(X,N1) \ geq(X,N2) <=> N2 =< N1 | true.
96
97dist(X,Y,D1) \ dist(X,Y,D2) <=> D1 =< D2 | true.
98
99dist(X,Y,D), leq(Y,MY) \ leq(X,MX1) <=>
100	MX2 is MY + D, MX2 < MX1 | leq(X,MX2).
101
102dist(X,Y,D), geq(X,MX) \ geq(Y,MY1) <=>
103	MY2 is MX - D, MY2 > MY1 | geq(Y,MY2).
104
105fincl(X,Y), leq(Y,N) \ fub_init(X,L)
106	<=> \+ memberchk_eq(N-Y,L) |
107	    insert_ub(L,Y,N,NL),
108	    fub_init(X,NL).
109
110fincl(X,Y), geq(Y,N) \ flb_init(X,L)
111	<=> \+ memberchk_eq(N-Y,L) |
112	    insert_lb(L,Y,N,NL),
113	    flb_init(X,NL).
114
115dist(X1,Y1,D), fincl(X2,X1), fincl(Y2,Y1) \ fdist_init(X2,Y2,L)
116	<=>
117	\+ memberchk_eq(D-X1,L) |
118	insert_ub(L,X1,D,NL),
119	fdist_init(X2,Y2,NL).
120
121bincl(X,Y), leq(Y,N) \ bub_init(X,L)
122	<=>
123	\+ memberchk_eq(N-Y,L) |
124	insert_ub(L,Y,N,NL),
125	bub_init(X,NL).
126
127compl(X) \ fub_init(X,L) # ID
128	<=>
129	fub(X,L),
130	val(L,M),
131	leq(X,M)
132	pragma passive(ID).
133
134compl(X) \ flb_init(X,L) # ID
135	<=>
136	flb(X,L),
137	val(L,M),
138	geq(X,M)
139	pragma passive(ID).
140
141compl(X), compl(Y) \ fdist_init(X,Y,L) # ID
142	<=>
143	fdist(X,Y,L),
144	val(L,D),
145	dist(X,Y,D)
146	pragma passive(D).
147
148compl(X) \ bub_init(X,L) # ID
149	<=>
150	bub(X,L),
151	val(L,M),
152	leq(X,M)
153	pragma passive(ID).
154
155fincl(X,Y), leq(Y,N) \ fub(X,L)
156	<=>
157	\+ memberchk_eq(N-Y,L) |
158	insert_ub(L,Y,N,NL),
159	fub(X,NL),
160	val(NL,M),
161	leq(X,M).
162
163fincl(X,Y), geq(Y,N) \ flb(X,L)
164	<=>
165	\+ memberchk_eq(N-Y,L) |
166	insert_lb(L,Y,N,NL),
167	flb(X,NL),
168	val(NL,M),
169	geq(X,M).
170
171bincl(X,Y), leq(Y,N) \ bub(X,L)
172	<=>
173	\+ memberchk_eq(N-Y,L) |
174	insert_ub(L,Y,N,NL),
175	bub(X,NL),
176	val(NL,M),
177	leq(X,M).
178
179fincl(X2,X1), fincl(Y2,Y1), dist(X1,Y1,D) \ fdist(X2,Y2,L)
180	<=>
181	\+ memberchk_eq(D-X1,L) |
182	insert_ub(L,X1,D,NL),
183	fdist(X2,Y2,NL),
184	val(NL,MD),
185	dist(X2,Y2,MD).
186
187fincl(X,Y), leq(X,N) ==> leq(Y,N).
188
189fincl(X,Y), geq(X,N) ==> geq(Y,N).
190
191bincl(X,Y), geq(X,N) ==> geq(Y,N).
192
193bincl(X1,X2), bincl(Y1,Y2), dist(X1,Y1,D1) \ dist(X2,Y2,D2) <=> D1 < D2 | dist(X2,Y2,D1).
194
195setdist(X,Y,N), leq(Y,D1) ==> D2 is D1 - N, dist(Y,X,D2).
196setdist(X,Y,N), geq(Y,D1) ==> D2 is N - D1, dist(X,Y,D2).
197
198val([N-_|_],N).
199
200insert_ub([],X,N,[N-X]).
201insert_ub([M-Y|R],X,N,NL) :-
202	( Y == X ->
203		insert_ub(R,X,N,NL)
204	; M > N ->
205		NL = [M-Y|NR],
206		insert_ub(R,X,N,NR)
207	;
208		NL = [N-X,M-Y|R]
209	).
210
211insert_lb([],X,N,[N-X]).
212insert_lb([M-Y|R],X,N,NL) :-
213	( Y == X ->
214		insert_lb(R,X,N,NL)
215	; M < N ->
216		NL = [M-Y|NR],
217		insert_lb(R,X,N,NR)
218	;
219		NL = [N-X,M-Y|R]
220	).
221
222couple(X,Y) :-
223	dist(X,Y,10000),
224	dist(Y,X,10000).
225
226giri :-
227	giri([x1,y1,x2,y2,x3,y3,x4,y4,x5,y5,x6,y6,x7,y7,x8,y8,x9,y9,x10,y10]).
228
229giri(L) :-
230	L = [X1,Y1,X2,Y2,X3,Y3,X4,Y4,X5,Y5,X6,Y6,X7,Y7,X8,Y8,X9,Y9,X10,Y10],
231	clocks(L),
232
233	% 1.
234	couple(X1,Y1),
235	geq(X1,0),
236	geq(X2,0),
237	dist(X1,Y1,0),
238	dist(Y1,X1,0),
239
240	% 2.
241	couple(X2,Y2),
242
243	fincl(X2,X1),
244	fincl(X2,X8),
245	fincl(X2,X10),
246	fub_init(X2,[]),
247	flb_init(X2,[]),
248
249	fincl(Y2,Y1),
250	fincl(Y2,Y8),
251	fincl(Y2,Y10),
252	fub_init(Y2,[]),
253	flb_init(Y2,[]),
254
255	bincl(X2,X3),
256	bincl(X2,X4),
257	bub_init(X2,[]),
258	blb_init(X2,[]),
259
260	bincl(Y2,Y3),
261	bincl(Y2,Y4),
262	bub_init(Y2,[]),
263	blb_init(Y2,[]),
264
265	fdist_init(X2,Y2,[]),
266	fdist_init(Y2,X2,[]),
267
268	% 3.
269	couple(X3,Y3),
270	leq(X3,3),
271
272	bincl(X3,X9),
273	bincl(X3,X5),
274	bub_init(X3,[]),
275	blb_init(X3,[]),
276
277	bincl(Y3,Y9),
278	bincl(Y3,Y5),
279	bub_init(Y3,[]),
280	blb_init(Y3,[]),
281
282	%fdist_init(X3,Y3,[]),
283	%fdist_init(Y3,X3,[]),
284
285	% 4.
286	couple(X4,Y4),
287	geq(Y4,2),
288	leq(Y4,5),
289
290	% 5.
291	couple(X5,Y5),
292	geq(Y5,5),
293	leq(Y5,10),
294
295	% 6.
296	couple(X6,Y6),
297
298	fincl(X6,X4),
299	fincl(X6,X5),
300	fub_init(X6,[]),
301	flb_init(X6,[]),
302
303	fincl(Y6,Y4),
304	fincl(Y6,Y5),
305	fub_init(Y6,[]),
306	flb_init(Y6,[]),
307
308	bincl(X6,X7),
309	bub_init(X6,[]),
310
311	bincl(Y6,Y7),
312	bub_init(Y6,[]),
313
314	fdist_init(X6,Y6,[]),
315	fdist_init(Y6,X6,[]),
316
317	% 7.
318	couple(X7,Y7),
319	geq(Y7,15),
320	leq(Y7,15),
321
322	% 8.
323	couple(X8,Y8),
324	geq(X8,2),
325	geq(Y8,2),
326	dist(X8,Y8,0),
327	dist(Y8,X8,0),
328
329	% 9.
330	couple(X9,Y9),
331	geq(Y9,5),
332	leq(Y9,5),
333
334
335	% 10.
336	couple(X10,Y10),
337	geq(X10,0),
338	geq(Y10,0),
339	dist(X10,Y10,0),
340	dist(Y10,X10,0),
341
342	% finish
343	compl(X2),
344	compl(Y2),
345
346	compl(X3),
347	compl(Y3),
348
349	compl(X6),
350	compl(Y6).
351
352
353
354clocks([]).
355clocks([C|Cs]) :-
356	clock(C),
357	clocks(Cs).
358
359clock(X) :-
360	geq(X,0),
361	leq(X,10000).
362
363main :-
364	main(100).
365
366main(N) :-
367	cputime(T1),
368	loop(N),
369	cputime(T2),
370	T is T2 - T1,
371	write(bench(ta ,N , T,0,hprolog)),write('.'),nl.
372
373
374loop(N) :-
375	( N =< 0 ->
376		true
377	;
378		( giri, fail ; true),
379		M is N - 1,
380		loop(M)
381	).
382