%% circuit.lp -- Chapter 10 (Code in Appendix D.3)
%% Last Modified: 2/4/14
%% Diagnosing the problem in a simple circuit.
%% We assume that switches s1 and s2 are mechanical components which
%% cannot become damaged.  Relay r is a magnetic coil. If not damaged,
%% it is activated when s1 is closed, causing s2 to close. An
%% undamaged bulb b emits light if s2 is closed.
%% The agent is aware of two exogenous actions relevant
%% to its work: break, which causes the circuit bulb
%% to become faulty, and surge, which damages the relay and
%% also the bulb if the latter is not protected.

%% ----------------------------------------------------
%% circuit.lp
%% ----------------------------------------------------

%% ----------
%% Signature:
%% ----------

%% Components:
comp(r).  %% relay
comp(b).  %% bulb

%% Switches:
switch(s1).
switch(s2).

%% Fluents:

fluent(inertial, prot(b)).  %% prot stands for "protected"
fluent(inertial, closed(SW)) :- switch(SW).  
fluent(inertial, ab(C)) :- comp(C).
fluent(defined, active(r)).  
fluent(defined, on(b)).      

%% Actions:

action(agent, close(s1)).
action(exogenous, break).
action(exogenous, surge).

action(X) :- action(agent, X).
action(X) :- action(exogenous, X).

%% Steps:

#const n = 1.
step(0..n).

%% -------------------
%% System Description:
%% -------------------

%% Causal laws:

%% close(s1) causes closed(s1)
holds(closed(s1), I+1) :- occurs(close(s1),I),
                          I < n.

%% break causes ab(b)
holds(ab(b), I+1) :- occurs(break,I),
                     I < n.

%% surge causes ab(r)
holds(ab(r), I+1) :- occurs(surge,I),
                     I < n.

%% surge causes ab(b) if -prot(b)
holds(ab(b), I+1) :- occurs(surge,I),
                     -holds(prot(b),I),
                     I < n.


%% State constraints:

%% active(r) if closed(s1), -ab(r)
holds(active(r), I) :- holds(closed(s1),I),
                       -holds(ab(r),I).

%% closed(s2) if active(r)
holds(closed(s2), I) :- holds(active(r),I).

%% on(b) if closed(s2), -ab(b)
holds(on(b), I) :- holds(closed(s2),I),
                   -holds(ab(b),I).


%% Executability conditions:

%% impossible close(s1) if closed(s1)
-occurs(close(s1), I) :- holds(closed(s1),I).


%% CWA for Defined Fluents:

-holds(F,I) :- fluent(defined,F),
               step(I),
               not holds(F,I).

%% General Inertia Axiom:

holds(F,I+1) :- fluent(inertial,F),
                holds(F,I),
                not -holds(F,I+1),
                I < n.

-holds(F,I+1) :- fluent(inertial,F),
                 -holds(F,I),
                 not holds(F,I+1),
                 I < n.
                 
%% CWA for Actions:

-occurs(A,I) :- action(A), step(I),
                not occurs(A,I).

%% --------
%% History:
%% --------

obs(closed(s1), false, 0).
obs(closed(s2), false, 0).
obs(ab(b), false, 0).
obs(ab(r), false, 0).
obs(prot(b), true, 0).

hpd(close(s1), 0).

obs(on(b), false, 1).

%% -------
%% Axioms:
%% -------

%% Full Awareness Axiom:
holds(F,0) | -holds(F,0) :- fluent(inertial, F).

%% Take what actually happened into account:
occurs(A,I) :- hpd(A,I).

%% Reality Check:
:- obs(F,true,I), -holds(F,I).
:- obs(F,false,I), holds(F,I).


%% -----------------------
%% Explanation Generation:
%% -----------------------

{occurs(A,K) : action(exogenous,A)} :- step(K),
                                       K >= 0, K < n.


expl(A,I) :- action(exogenous,A),
             occurs(A,I),
             not hpd(A,I).

#show expl/2.