1% OBJECT-LEVEL DEFINITION OF THE ELECTRICAL DOMAIN, WITH DELAYABLES
    2% CILog code. Copyright David Poole, 1997.
    3
    4% Here "<=" is the object-level "if" and is a meta-level predicate.
    5% "&" is the object-level conjunction and is a meta-level function symbol.
    6
    7% lit(L) is true if light L is lit.
    8lit(L) <=
    9   light(L) &
   10   ok(L) &
   11   live(L).
   12
   13% live(W) is true if W is live (i.e., current will flow through it if grounded)
   14live(W) <=
   15   connectedto(W,W1) &
   16   live(W1).
   17
   18live(outside) <= true.
   19
   20% connectedto(W0,W1) is true if W0 is connnected to W1 such that current will
   21% flow from W1 to W0.
   22
   23connectedto(l1,w0) <= true.
   24connectedto(w0,w1) <= up(s2) & ok(s2).
   25connectedto(w0,w2) <= down(s2) & ok(s2).
   26connectedto(w1,w3) <= up(s1) & ok(s1).
   27connectedto(w2,w3) <= down(s1) & ok(s1).
   28connectedto(l2,w4) <= true.
   29connectedto(w4,w3) <= up(s3) & ok(s3).
   30connectedto(p1,w3) <= true.
   31connectedto(w3,w5) <= ok(cb1).
   32connectedto(p2,w6) <= true.
   33connectedto(w6,w5) <= ok(cb2).
   34connectedto(w5,outside) <= ok(outside_connection).
   35
   36% light(L) is true if L is a light
   37light(l1) <= true.
   38light(l2) <= true.
   39
   40% up(S) is true if switch S is up
   41% down(S) is true if switch S is down
   42
   43up(s2) <= true.
   44down(s1) <= true.
   45up(s3) <= true.
   46
   47% ok(G) is true if G is working
   48% ok is delayable
   49delay(ok(X)).
   50
   51% Example Queries:
   52% ask dprove(live(w6),[],D).
   53% ask dprove(live(p1),[],D).
   54% ask dprove(lit(l2),[],D).
   55% ask dprove(lit(l2)&live(p1),[],D).