:- use_module(library(scasp)).
:- style_check(-discontiguous).
:- style_check(-singleton).
:- set_prolog_flag(scasp_unknown, fail).

% BASIC EVENT CALCULUS (BEC) THEORY

% https://github.com/JanWielemaker/sCASP/blob/swipl/examples/benchmark_EventCalculus/lopstr19/event-calculus/bec_theory.pl

% I changed .<. to #<

% BEC1 - StoppedIn(t1,f,t2)
stoppedIn(T1, Fluent, T2) :-
    T1 #< T, T #< T2,
    terminates(Event, Fluent, T),
    happens(Event, T).

stoppedIn(T1, Fluent, T2) :-
    T1 #< T, T #< T2,
    releases(Event, Fluent, T),
    happens(Event, T).

% BEC2 - StartedIn(t1,f,t2)
startedIn(T1, Fluent, T2) :-
    T1 #< T, T #< T2,
    initiates(Event, Fluent, T),
    happens(Event, T).

startedIn(T1, Fluent, T2) :-
    T1 #< T, T #< T2,
    releases(Event, Fluent, T),
    happens(Event, T).

% BEC3 - HoldsAt(f,t)
holdsAt(Fluent2, T2) :-
    initiates(Event, Fluent1, T1),
    happens(Event, T1),
    trajectory(Fluent1, T1, Fluent2, T2),
    not stoppedIn(T1, Fluent1, T2).
% BEC4 - HoldsAt(f,t)
holdsAt(Fluent, T) :-
    0 #< T,
    initiallyP(Fluent),
    not stoppedIn(0, Fluent, T).

% BEC5 - not HoldsAt(f,t)
-holdsAt(Fluent, T) :-
    0 #< T,
    initiallyN(Fluent),
    not startedIn(0, Fluent, T).

% BEC6 - HoldsAt(f,t)
holdsAt(Fluent, T) :-
    T1 #< T,
    initiates(Event, Fluent, T1),
    happens(Event, T1),
    not stoppedIn(T1, Fluent, T).

% BEC7 - not HoldsAt(f,t)
-holdsAt(Fluent, T) :-
    T1 #< T,
    terminates(Event, Fluent, T1),
    happens(Event, T1),
    not startedIn(T1, Fluent, T).


% Include the BASIC EVENT CALCULUS THEORY

% https://github.com/JanWielemaker/sCASP/blob/swipl/examples/benchmark_EventCalculus/lopstr19/event-calculus/example-light/bec_light_01.pl

% #include '../bec_theory'.    % not necessary in SWISH due to previous cells

% changed .>. to #>=

% Inspired by example 4 from Mueller

% If a light is turned on, it will be on:
initiates(turn_on, light_on, T).

% If a light is turned on, whether it is red or green will be released
% from the commonsense law of inertia:
releases(turn_on, light_red, T).
releases(turn_on, light_green, T).

% If a light is turned off, it will not be on.
terminates(turn_off, light_on, T).

% After a light is turned on, it will emit red for up to two seconds
% and green after at least two seconds:
trajectory(light_on, T1, light_red, T2) :- T2 #>= T1, T2 #< T1 + 2.
trajectory(light_on, T1, light_green, T2) :- T2 #>= T1 + 2.

initiallyN(light_on).

% Actions
happens(turn_on, 1/2).
happens(turn_off, 4).
happens(turn_on, 6).


? holdsAt(light_on, 7).
