Benchmarks/ta.chr

   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
  22 n > 1,  1 ------> v             fincl(Xv,X1),
  23         ...    /                ...
  24         n ----/                 fincl(Xv,Xn),
  25                                 fub_init(Xv,[])
  26
  27 n >= 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
  93 leq(X,N1) \ leq(X,N2) <=> N1 =< N2 | true.
  94
  95 geq(X,N1) \ geq(X,N2) <=> N2 =< N1 | true.
  96
  97 dist(X,Y,D1) \ dist(X,Y,D2) <=> D1 =< D2 | true.
  98
  99 dist(X,Y,D), leq(Y,MY) \ leq(X,MX1) <=>
 100         MX2 is MY + D, MX2 < MX1 | leq(X,MX2).
 101
 102 dist(X,Y,D), geq(X,MX) \ geq(Y,MY1) <=>
 103         MY2 is MX - D, MY2 > MY1 | geq(Y,MY2).
 104
 105 fincl(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
 110 fincl(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
 115 dist(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
 121 bincl(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
 127 compl(X) \ fub_init(X,L) # ID
 128         <=>
 129         fub(X,L),
 130         val(L,M),
 131         leq(X,M)
 132         pragma passive(ID).
 133
 134 compl(X) \ flb_init(X,L) # ID
 135         <=>
 136         flb(X,L),
 137         val(L,M),
 138         geq(X,M)
 139         pragma passive(ID).
 140
 141 compl(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
 148 compl(X) \ bub_init(X,L) # ID
 149         <=>
 150         bub(X,L),
 151         val(L,M),
 152         leq(X,M)
 153         pragma passive(ID).
 154
 155 fincl(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
 163 fincl(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
 171 bincl(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
 179 fincl(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
 187 fincl(X,Y), leq(X,N) ==> leq(Y,N).
 188
 189 fincl(X,Y), geq(X,N) ==> geq(Y,N).
 190
 191 bincl(X,Y), geq(X,N) ==> geq(Y,N).
 192
 193 bincl(X1,X2), bincl(Y1,Y2), dist(X1,Y1,D1) \ dist(X2,Y2,D2) <=> D1 < D2 | dist(X2,Y2,D1).
 194
 195 setdist(X,Y,N), leq(Y,D1) ==> D2 is D1 - N, dist(Y,X,D2).
 196 setdist(X,Y,N), geq(Y,D1) ==> D2 is N - D1, dist(X,Y,D2).
 197
 198 val([N-_|_],N).
 199
 200 insert_ub([],X,N,[N-X]).
 201 insert_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
 211 insert_lb([],X,N,[N-X]).
 212 insert_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
 222 couple(X,Y) :-
 223         dist(X,Y,10000),
 224         dist(Y,X,10000).
 225
 226 giri :-
 227         giri([x1,y1,x2,y2,x3,y3,x4,y4,x5,y5,x6,y6,x7,y7,x8,y8,x9,y9,x10,y10]).
 228
 229 giri(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
 354 clocks([]).
 355 clocks([C|Cs]) :-
 356         clock(C),
 357         clocks(Cs).
 358
 359 clock(X) :-
 360         geq(X,0),
 361         leq(X,10000).
 362
 363 main :-
 364         main(100).
 365
 366 main(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
 374 loop(N) :-
 375         ( N =< 0 ->
 376                 true
 377         ;
 378                 ( giri, fail ; true),
 379                 M is N - 1,
 380                 loop(M)
 381         ).