1%Code for modeling timed automata using CLP(R).
    2%Adapted from "A Constraint based Approach for 
    3%Specification and Verification for Real-time Systems"
    4%by G. Gupta and E. Pontelli. Realtime Systems Symposium.
    5%1997. 
    6
    7%Copyright Gopal Gupta and Enrico Pontelli 1997, 2003.
    8%Please leave the above message intact, if you modify
    9%this code. Please do not distribute without authors'
   10%permission.
   11
   12:- use_package(clpr).   13:- push_prolog_flag(quiet, on).   14
   15train(s0, approach, s1, T1, T2, T3) :-
   16    T3 .=. T1.
   17train(s1, inn, s2, T1, T2, T3) :-
   18    T1 .>. T2 + 2,
   19    T3 .=. T2.
   20train(s2, out,  s3, T1, T2, T3) :-
   21    T3 .=. T2.
   22train(s3, exit, s0, T1, T2, T3) :-
   23    T3 .=. T2,
   24    T1 .<. T2 + 5.
   25train(X, lower, X, T1, T2, T2).
   26train(X, down,  X, T1, T2, T2).
   27train(X, raise, X, T1, T2, T2).
   28train(X, up,    X, T1, T2, T2).
   29
   30gate(s0, lower, s1, T1, T2, T1).
   31gate(s1, down,  s2, T1, T2, T3) :-
   32    T3 .=. T2,
   33    T1 .<. T2 + 1.
   34gate(s2, raise, s3, T1, T2, T3) :-
   35    T3 .=. T1.
   36gate(s3, up, s0, T1, T2, T3) :-
   37    T3 .=. T2,
   38    T1 .>. T2 + 1,
   39    T1 .<. T2 + 2.
   40gate(X, approach, X, T1, T2, T2).
   41gate(X, inn,       X, T1, T2, T2).
   42gate(X, out,      X, T1, T2, T2).
   43gate(X, exit,     X, T1, T2, T2).
   44
   45
   46
   47contr(s0, approach, s1, T1, T2, T1).
   48contr(s1, lower,    s2, T1, T2, T3) :-
   49    T3 .=. T2,
   50    T1 .=. T2 + 1.
   51contr(s2, exit,  s3, T1, T2, T1).
   52contr(s3, raise, s0, T1, T2, T2) :-
   53    T1 .<. T2 + 1.
   54contr(X, inn,   X, T1, T2, T2).
   55contr(X, out,  X, T1, T2, T2).
   56contr(X, up,   X, T1, T2, T2).
   57contr(X, down, X, T1, T2, T2).
   58
   59
   60driver(N, S0, S1, S2, T, T0, T1, T2, [X|Rest], [f(X, T)|R]) :-
   61    train(S0, X, S00, T, T0, T00),
   62    gate(S1, X, S10, T, T1, T10),
   63    contr(S2, X, S20, T, T2, T20),
   64    TA .>. T,
   65    X = approach, N = 0,
   66    driver(1, S00, S10, S20, TA, T00, T10, T20, Rest, R).
   67
   68driver(N, S0, S1, S2, T, T0, T1, T2, [X|Rest], [f(X, T)|R]) :-
   69    N > 0,
   70    train(S0, X, S00, T, T0, T00),
   71    gate(S1, X, S10, T, T1, T10),
   72    contr(S2, X, S20, T, T2, T20),
   73    TA .>. T,
   74    X \= approach,
   75    driver(N, S00, S10, S20, TA, T00, T10, T20, Rest, R).
   76
   77driver(N, S0, S1, S2, T, T0, T1, T2, [X|Rest], [f(X, T)|R]) :-
   78    train(S0, X, S00, T, T0, T00),
   79    gate(S1, X, S10, T, T1, T10),
   80    contr(S2, X, S20, T, T2, T20),
   81    TA .>. T,
   82    X = approach, R = [], Rest = [], N > 0.
   83
   84
   85append([],    L, L).
   86append([X|A], B, [X|C]) :- append(A, B, C).
   87
   88%---------------------------------------------------------------
   89%Property 1: check that the gate will always be "down" when the
   90%train is "in" subject to the timing constraints. A call to
   91% "downbeforein" will produce the answer "no" since the property
   92% is negated in the query.
   93
   94downbeforein(X) :- driver(0, s0, s0, s0, 0, 0, 0, 0, X, R),
   95    append(A, [down|_], X), append(_, [inn|_], A).
   96%---------------------------------------------------------------
   97
   98
   99%---------------------------------------------------------------
  100%Property 2: check that the gate can never be up more than 10 units 
  101%of time.  A call to downmorethan10 will produce the answer "no" 
  102%since the property is negated in the query.
  103
  104downmorethan10 :- driver(0, s0, s0, s0, 0, 0, 0, 0, X, R),
  105    append(A, [f(up, T2)|_], R), append(_, [f(down, T1)|_], A),
  106    10 .<. T2 - T1.
  107%---------------------------------------------------------------
  108
  109
  110%---------------------------------------------------------------
  111%Property 3: Find the upper and lower bounds on the time the gate
  112%can be down (assuming there is only one train). Variables M and N 
  113%denote the Max time and the Min time. More precisely this query 
  114%will find the upper and lower bounds on the times at which 
  115%two approach signals can occur with no other intervening approach 
  116%signal. Calling "findrange(M,N)" on sicstus will produce:
  117%           N < 7,  M > 1, M > N
  118% This means that the largest value that difference of 
  119% T2 and T1 can have is 7, while the smallest value it can
  120% have is larger than 1.
  121
  122findrange(M, N, X) :- driver(0, s0, s0, s0, 0, 0, 0, 0, X, R),
  123    append(A, [f(up, T2)|_], R), append(_, [f(down, T1)|_], A),
  124    N .<. T2 - T1, T2 .<. T1 + M, M .>. 0, N .>. 0.
  125%---------------------------------------------------------------