3%% Include the BASIC EVENT CALCULUS THEORY
    4#include  'bec_theory.incl'.
    5
    6% The domain comprises a TapOn event, which initiates a flow of liquid
    7% into the vessel.  The fluent Filling holds while water is flowing
    8% into the vessel, and the fluent Level(x) represents holds if the
    9% water is at level x in the vessel, where x is a real number. The
   10% fluent Leak(x) represents holds if x liter of water are leaked,
   11% where x is a real number. Level(x) finishes when the maximum level of
   12% the vessel is reached and the Leak(x) starts.
   13
   14% An Overflow event occurs when the water reaches the rim of the
   15% vessel at level 10 or 16. The Overflow event initiates a period during
   16% which the fluent Spilling holds.
   17
   18max_level(10) :- not max_level(16).      %% The even loop
   19max_level(16) :- not max_level(10).
   20
   21initiates(tapOn,filling,T).
   22terminates(tapOff,filling,T).
   23
   24initiates(overflow,spilling,T) :-
   25    max_level(Max),
   26    holdsAt(level(Max), T).
   27
   28releases(tapOn,level(0),T) :- happens(tapOn, T).
   29
   30% Note that (S1.3) has to be a Releases formula instead of a
   31% Terminates formula, so that the Level fluent is immune from the
   32% common sense law of inertia after the tap is turned on.
   33
   34% Now we have the Trajectory formula, which describes the continuous
   35% variation in the Level fluent while the Filling fluent holds. The
   36% level is assumed to rise at one unit per unit of time until it reach
   37% the maximum level of the vessel.
   38
   39trajectory(filling,T1,level(X2),T2) :-
   40    T1 #< T2,
   41    X2 #= X + T2 - T1,
   42    max_level(Max),
   43    X2 #=< Max,
   44    holdsAt(level(X),T1).
   45% trajectory(filling,T1,level(overlimit),T2) :-
   46%     T1 #< T2,
   47%     X2 #= X + T2 - T1,
   48%     max_level(Max),
   49%     X2 #> Max,
   50%     holdsAt(level(X),T1).
   51
   52% Now we have the Trajectory formula, which describes the continuous
   53% variation in the Leaf fluent while the Spilling fluent holds. The
   54% water is assumed to leak at one unit per unit of time since it reach
   55% the maximum level of the vessel.
   56
   57trajectory(spilling,T1,leak(X),T2) :-
   58    holdsAt(filling, T2),
   59    T1#<T2,
   60    X #= T2 - T1.
   61
   62% The next formulae ensures the Overflow event is triggered when it
   63% should be.
   64
   65happens(overflow,T).
   66
   67% Here’s a simple narrative. The level is initially 0, and the tap is
   68% turned on at time 5.
   69
   70initiallyP(level(0)).
   71happens(tapOn,5).
   72happens(tapOff,20).         

   73                        

   81% ?- holdsAt(level(H),15/2).   % From paper
   82?- holdsAt(level(5/2), T).  % From paper
   83% ?- holdsAt(level(7),T).   % -> T = 12s / 12s "
   84% ?- holdsAt(level(12),T).  % -> no      / 17s "
   85% ?- holdsAt(spilling,T).   % -> T > 15s / no  "
   86% ?- holdsAt(leak(L),13).   % -> no      / no  "
   87% ?- holdsAt(leak(L),16).   % -> L = 1   / no  "
   88% ?- holdsAt(level(H),19), max_level(Max).   %  ->  H = overlimit, Max = 10 / H = 14, Max = 16"