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. The Overflow event initiates a period during
   16% which the fluent Spilling holds.
   17
   18max_level(10).
   19
   20initiates(tapOn,filling,T).
   21terminates(tapOff,filling,T).
   22
   23initiates(overflow,spilling,T) :-
   24    max_level(Max),
   25    holdsAt(level(Max), T).
   26
   27releases(tapOn,level(0),T) :- happens(tapOn, T).
   28
   29% Note that (S1.3) has to be a Releases formula instead of a
   30% Terminates formula, so that the Level fluent is immune from the
   31% common sense law of inertia after the tap is turned on.
   32
   33% Now we have the Trajectory formula, which describes the continuous
   34% variation in the Level fluent while the Filling fluent holds. The
   35% level is assumed to rise at one unit per unit of time until it reach
   36% the maximum level of the vessel.
   37
   38trajectory(filling,T1,level(X2),T2) :-
   39    T1 #< T2,
   40    X2 #= X + T2 - T1,
   41    max_level(Max),
   42    X2 #=< Max,
   43    holdsAt(level(X),T1).
   44% trajectory(filling,T1,level(overlimit),T2) :-
   45%     T1 #< T2,
   46%     X2 #= X + T2 - T1,
   47%     max_level(Max),
   48%     X2 #> Max,
   49%     holdsAt(level(X),T1).
   50
   51% Now we have the Trajectory formula, which describes the continuous
   52% variation in the Leaf fluent while the Spilling fluent holds. The
   53% water is assumed to leak at one unit per unit of time since it reach
   54% the maximum level of the vessel.
   55
   56trajectory(spilling,T1,leak(X),T2) :-
   57    holdsAt(filling, T2),
   58    T1#<T2,
   59    X #= T2 - T1.
   60
   61% The next formulae ensures the Overflow event is triggered when it
   62% should be.
   63
   64happens(overflow,T).
   65
   66% Here’s a simple narrative. The level is initially 0, and the tap is
   67% turned on at time 5.
   68
   69initiallyP(level(0)).
   70happens(tapOn,5).
   71happens(tapOff,20).       %% Option A - the tap is on 15 seconds -> overflow
   72
   73
   74
   75
   76%% Queries (with the expected result)
   77%% Uncomment the querie you want to check...
   78
   79% ?- holdsAt(level(H),-1).     % -> no
   80% ?- holdsAt(level(H),4).      % -> H = 0
   81 ?- holdsAt(level(H),8).      % -> H = 3
   82% ?- holdsAt(level(H),14).     % -> H = 9
   83% ?- holdsAt(level(H),19).     % -> H = overlimit
   84% ?- holdsAt(level(7),T).      % -> T = 12s
   85% ?- holdsAt(level(12),T).     % -> no
   86% ?- holdsAt(spilling,T).      % -> T > 15s
   87% ?- holdsAt(leak(L),14).      % -> L = 0
   88% ?- holdsAt(leak(L),19).      % -> L = 4
   89% ?- holdsAt(leak(L),22).      % -> no