Quelle  allen_interval.pvs

%% allen_interval.pvs
allen_interval : THEORY
BEGIN
  IMPORTING interval
  
  s, t: VAR StrictInterval

  ;<(t, s): bool = t`ub < s`lb
  ;>(t, s): bool = s < t

  ;=(t, s): bool = t`lb = s`lb AND t`ub = s`ub

  overlaps(t, s): bool = t`lb < s`lb AND
                         t`ub > s`lb AND
                         t`ub < s`ub

  ;o(t, s): bool = overlaps(t, s)

  oi(t, s): bool = o(s, t)

  meets(t, s): bool = t`ub = s`lb;
  m(t, s): bool = meets(t, s)
  mi(t, s): bool = m(s, t)

  during(t, s): bool = ((t`lb > s`lb) AND (t`ub < s`ub))
  d(t, s): bool = during(t, s)
  di(t, s): bool = d(s, t)

  starts(t, s): bool = t`lb = s`lb AND t`ub < s`ub
  s(t, s): bool = starts(t, s)
  si(t, s): bool = s(s, t)

  finishes(t, s): bool = t`ub = s`ub AND t`lb > s`lb
  f(t, s): bool = finishes(t, s)
  fi(t, s): bool = f(s, t)

  dur(t, s): bool = d(t, s) OR s(t, s) OR f(t, s)
  con(t, s): bool = di(t, s) OR si(t, s) OR fi(t, s)

  AUTO_REWRITE+ <, >, =, overlaps, o, oi, meets, m, mi, during, d, di, 
                starts, s, si, finishes, f, fi, dur, con

END allen_interval