vessel_01.clingo

%% Inspired by example from Shanahan (1999)

timestep(0..30*P) :- precision(P).

% One world - vessel size = 10
max_level(10*P) :- precision(P), not max_level(16*P).
max_level(16*P) :- precision(P), not max_level(10*P).

initiates(tapOn,filling,T) :- timestep(T).
terminates(tapOff,filling,T) :- timestep(T).

initiates(overflow,spilling,T) :-
    timestep(T),
    max_level(Max),
    holdsAt(level(Max), T).

% Note that (S1.3) has to be a Releases formula instead of a
% Terminates formula, so that the Level fluent is immune from the
% common sense law of inertia after the tap is turned on.
releases(tapOn,level(0),T) :- timestep(T), happens(tapOn, T).

% Now we have the Trajectory formula, which describes the continuous
% variation in the Level fluent while the Filling fluent holds.
trajectory(filling,T1,level(X2),T2) :-
    timestep(T1), timestep(T2),
    T1 < T2,
    X2 = X + (4 * (T2 - T1)/3),
    max_level(Max),
    X2 <= Max,
    holdsAt(level(X),T1).
 trajectory(filling,T1,overlimit,T2) :-
     timestep(T1), timestep(T2),
     T1 < T2,
     X2 = X + (4 * (T2 - T1)/3),
     max_level(Max),
     X2 > Max,
     holdsAt(level(X),T1).

% Now we have the Trajectory formula, which describes the continuous
% variation in the Leaf fluent while the Spilling fluent holds.
trajectory(spilling,T1,leak(X),T2) :-
    timestep(T1), timestep(T2),
    holdsAt(filling, T2),
    T1 < T2,
    X = 4 * (T2 - T1) /3.

initiallyP(level(0)).

%% Actions
% The next formulae ensures the Overflow event is triggered when it
% should be.
happens(overflow,T) :- timestep(T).                            

% Here’s a simple narrative. The level is initially 0, and the tap is
% turned on at time 5.
happens(tapOn,5*P) :- precision(P).


%% Query
:- not query.