11# door
2- type d : t {
2+ type d : t, lockable {
33 predicates {
4- open(d);
5- closed(d);
6- locked(d);
7-
84 link(r, d, r);
5+
6+ north_of/d(r, d, r);
7+ west_of/d(r, d, r);
8+
9+ south_of/d(r, d, r') = north_of/d(r', d, r);
10+ east_of/d(r, d, r') = west_of/d(r', d, r);
11+
12+ reachable(d) = at(P, r) & link(r, d, r') & link(r', d, r);
913 }
1014
1115 rules {
12- lock/d :: $at(P, r) & $link(r, d, r') & $link(r', d, r ) & $in(k, I) & $match(k, d) & closed(d) -> locked(d);
13- unlock/d :: $at(P, r) & $link(r, d, r') & $link(r', d, r ) & $in(k, I) & $match(k, d) & locked(d) -> closed(d);
16+ lock(d, k) :: $reachable(d ) & $in(k, I) & $match(k, d) & closed(d) -> locked(d);
17+ unlock( d, k) :: $reachable(d ) & $in(k, I) & $match(k, d) & locked(d) -> closed(d);
1418
15- open/d :: $at(P, r) & $link(r, d, r') & $link(r', d, r ) & closed(d) -> open(d) & free(r, r') & free(r', r);
16- close/d :: $at(P, r) & $link(r, d, r') & $link(r', d, r ) & open(d) & free(r, r') & free(r', r) -> closed(d);
19+ open(d) :: $reachable(d ) & closed(d) -> open(d) & free(r, r') & free(r', r);
20+ close(d) :: $reachable(d ) & open(d) & free(r, r') & free(r', r) -> closed(d);
1721 }
1822
1923 reverse_rules {
20- lock/d :: unlock/d ;
21- open/d :: close/d ;
24+ lock(d, k) :: unlock(d, k) ;
25+ open(d) :: close(d) ;
2226 }
2327
2428 constraints {
25- d1 :: open(d) & closed(d) -> fail();
26- d2 :: open(d) & locked(d) -> fail();
27- d3 :: closed(d) & locked(d) -> fail();
28-
2929 # A door can't be used to link more than two rooms.
3030 link1 :: link(r, d, r') & link(r, d, r'') -> fail();
3131 link2 :: link(r, d, r') & link(r'', d, r''') -> fail();
@@ -35,7 +35,7 @@ type d : t {
3535
3636 # There cannot be more than four doors in a room.
3737 too_many_doors :: link(r, d1: d, r1: r) & link(r, d2: d, r2: r) & link(r, d3: d, r3: r) & link(r, d4: d, r4: r) & link(r, d5: d, r5: r) -> fail();
38-
38+
3939 # There cannot be more than four doors in a room.
4040 dr1 :: free(r, r1: r) & link(r, d2: d, r2: r) & link(r, d3: d, r3: r) & link(r, d4: d, r4: r) & link(r, d5: d, r5: r) -> fail();
4141 dr2 :: free(r, r1: r) & free(r, r2: r) & link(r, d3: d, r3: r) & link(r, d4: d, r4: r) & link(r, d5: d, r5: r) -> fail();
@@ -52,18 +52,19 @@ type d : t {
5252 definition :: "door is openable and lockable.";
5353 }
5454
55- predicates {
56- open(d) :: "The {d} is open";
57- closed(d) :: "The {d} is closed";
58- locked(d) :: "The {d} is locked";
59- }
60-
6155 commands {
62- open/d :: "open {d}" :: "opening {d}";
63- close/d :: "close {d}" :: "closing {d}";
56+ open(d) :: "open {d}" :: "opening {d}";
57+ close(d) :: "close {d}" :: "closing {d}";
6458
65- unlock/d :: "unlock {d} with {k}" :: "unlocking {d} with the {k}";
66- lock/d :: "lock {d} with {k}" :: "locking {d} with the {k}";
59+ unlock(d, k) :: "unlock {d} with {k}" :: "unlocking {d} with the {k}";
60+ lock(d, k) :: "lock {d} with {k}" :: "locking {d} with the {k}";
61+ }
62+
63+ predicates {
64+ north_of/d(r, d, r') :: "South of {r} and north of {r'} is a door called {d}";
65+ south_of/d(r, d, r') :: "North of {r} and south of {r'} is a door called {d}";
66+ east_of/d(r, d, r') :: "West of {r} and east of {r'} is a door called {d}";
67+ west_of/d(r, d, r') :: "East of {r} and west of {r'} is a door called {d}";
6768 }
6869 }
6970}
0 commit comments