% Computational Intelligence: a logical approach. 
% CILog Code. 
% THE ELECTRICAL DOMAIN for abduction
% Copyright (c) 1998, Poole, Mackworth, Goebel and Oxford University Press.

% lit(L) is true if light L is lit.
lit(L) <-
   light(L) &
   ok(L) &
   live(L).

% dark(L) is true if light L isn't lit
dark(L) <-
  light(L) &
  broken(L).
dark(L) <-
  light(L) & ok(L) &
  dead(L).

% live(W) is true if W is live (i.e., current will flow through it if grounded)
live(W) <-
   connectedto(W,W1) &
   live(W1).

live(outside).

dead(W) <-
   connectedto(W,W1) &
   dead(W1).
dead(W) <-
   unconnected(W).

% connectedto(W0,W1) is true if W0 is connnected to W1 such that current will
% flow from W1 to W0.

connectedto(l1,w0).
connectedto(w0,w1) <- up(s2) & ok(s2).
connectedto(w0,w2) <- down(s2) & ok(s2).
connectedto(w1,w3) <- up(s1) & ok(s1).
connectedto(w2,w3) <- down(s1) & ok(s1).
connectedto(l2,w4).
connectedto(w4,w3) <- up(s3) & ok(s3).
connectedto(p1,w3).
connectedto(w3,w5) <- ok(cb1).
connectedto(p2,w6).
connectedto(w6,w5) <- ok(cb2).
connectedto(w5,outside).

unconnected(w0) <-
   broken(s2).
unconnected(w1) <-
   broken(s1).
unconnected(w1) <-
   down(s1).
unconnected(w2) <-
  up(s1).
unconnected(w2) <-
  broken(s1).
unconnected(w3) <-
   broken(cb1).
unconnected(w4) <-
   down(s3).
unconnected(w4) <-
   broken(s3).
unconnected(w6) <-
   broken(cb2).


% light(L) is true if L is a light
light(l1).
light(l2).


% ok(G) is true if G is working
% ok is delayable
assumable ok(_).
assumable broken(_).

% up(S) is true if switch S is up
% down(S) is true if switch S is down
askable up(_).
down(S) <- ~ up(S).

% integrity constraints
false <- up(S) & down(S).
false <- ok(X) & broken(X).

% Example Queries:
% ask lit(l1).
% ask dark(l2).
% ask dark(l2)&lit(l1).