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
49delay(ok(X)).
50