3%% Include the BASIC EVENT CALCULUS THEORY
    4#include '../bec_theory'.
    5
    6%% Inspired by example from Shanahan (1999)
    7
    8% One world - vessel size = 10
    9max_level(10) :- not max_level(16).
   10max_level(16) :- not max_level(10).
   11
   12initiates(tapOn,filling,T).
   13terminates(tapOff,filling,T).
   14
   15initiates(overflow,spilling,T) :-
   16    max_level(Max),
   17    holdsAt(level(Max), T).
   18
   19% Note that (S1.3) has to be a Releases formula instead of a
   20% Terminates formula, so that the Level fluent is immune from the
   21% common sense law of inertia after the tap is turned on.
   22releases(tapOn,level(0),T) :- happens(tapOn, T).
   23
   24% Now we have the Trajectory formula, which describes the continuous
   25% variation in the Level fluent while the Filling fluent holds.
   26trajectory(filling,T1,level(X2),T2) :-
   27    T1 #< T2,
   28    X2 #= X + 4/3 * (T2 - T1),
   29    max_level(Max),
   30    X2 #=< Max,
   31    holdsAt(level(X),T1).
   32trajectory(filling,T1,overlimit,T2) :-
   33    T1 #< T2,
   34    X2 #= X + 4/3 * (T2 - T1),
   35    max_level(Max),
   36    X2 #> Max,
   37    holdsAt(level(X),T1).
   38
   39% Now we have the Trajectory formula, which describes the continuous
   40% variation in the Leaf fluent while the Spilling fluent holds. 
   41trajectory(spilling,T1,leak(X),T2) :-
   42    holdsAt(filling, T2),
   43    T1 #< T2,
   44    X #= 4/3 * (T2 - T1).
   45
   46initiallyP(level(0)).

The next formulae ensures the Overflow event is triggered when it should be.

   51happens(overflow,T).                            
   52
   53% Here’s a simple narrative. The level is initially 0, and the tap is
   54% turned on at time 5.
   55happens(tapOn,5)