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).