Solution set 3
Problem 3:
In all of the atoms below "K" is to be replaced by one of k1, k2, k3, k4;
"B" by one of b1, b2; "T" by a time instance between 0 and some maximum M.
Since the "fit" relations are given and fixed over time, they can be
compiled into the action description by allowing only two "lock"
actions and two "unlock" actions: Locking/unlocking b1 with k1 and
locking / unlocking b2 with k2. Alternatively, one can define
atemporal atoms "FIT_K_B" (e.g. FIT_k3_b1) and put these appropriately
into the precondition axioms.
Fluents: IN_K_B_T (e.g. IN_k3_b1_2)
OUTSIDE_K_T (e.g. OUTSIDE_k2_0)
LOCKED_B_T (e.g. LOCKED_b1_2)
Actions: LOCK_b1_k1_T, LOCK_b2_k2_T.
UNLOCK_b1_k1_T, UNLOCK_b2_k2_T.
PUTIN_K_B_T
REMOVE_K_B_T.
WAIT_T
Axioms:
Domain constraints:
1. For each K,T: OUTSIDE_K_T iff [not IN_K_b1_T and not IN_K_b2_T)
(Definition of OUTSIDE)
2. For each K,T: not(IN_K_b1_T and IN_K_b2_T)
(A key is in at most one box.)
Effect axioms: For each T, let T1=T+1.
3. For each T: LOCK_b1_k1_T implies LOCKED_b1_T1.
4. For each T: LOCK_b2_k2_T implies LOCKED_b2_T1.
5. For each T: UNLOCK_b1_k1_T implies not LOCKED_b1_T1.
6. For each T: UNLOCK_b2_k2_T implies not LOCKED_b2_T1.
7. For each K,B,T: PUTIN_K_B_T implies IN_K_B_T1
8. For each K,B,T: REMOVE_K_B_T implies OUTSIDE_K_T1
Precondition axioms:
9. For each T: LOCK_b1_k1_T implies OUTSIDE_k1_T and UNLOCKED_b1.
10. For each T: LOCK_b2_k2_T implies OUTSIDE_k2_T and UNLOCKED_b2.
11. For each T: UNLOCK_b1_k1_T implies OUTSIDE_k1_T and LOCKED_b1.
12. For each T: UNLOCK_b2_k2_T implies OUTSIDE_k2_T and LOCKED_b2.
13. For each K,B,T: PUTIN_K_B_T implies OUTSIDE_K_T and UNLOCKED_B_T.
14. For each K,B,T: REMOVE_K_B_T implies IN_K_B_T and UNLOCKED_B_T.
Frame axioms: There are two forms of frame axioms, either of which
will work. (A) For each action, enumerate the fluents that remain the same.
(B) For each fluent, enumerate the actions needed to change them.
As above T1 will designate T+1.
Style A:
16. (LOCK_b1_k1_T implies
[(IN_K_B_T iff IN_K_B_T1) and (LOCKED_b2_T iff LOCKED_b2_T1)]
(The non-effect of LOCK on OUTSIDE follows from its non-effect on IN.)
17. LOCK_b2_k2_T implies
[(IN_K_B_T iff IN_K_B_T1) and (LOCKED_b1_T iff LOCKED_b1_T1)]
18. UNLOCK_b1_k1_T implies
[(IN_K_B_T iff IN_K_B_T1) and (LOCKED_b2_T iff LOCKED_b2_T1)]
19. UNLOCK_b2_k2_T implies
[(IN_K_B_T iff IN_K_B_T1) and (LOCKED_b1_T iff LOCKED_b1_T1)]
20. For each K1 != K:
PUTIN_K_B_T implies (IN_K1_B_T iff IN_K1_B_T1)
21. PUTIN_K_B_T implies (LOCKED_B_T iff LOCKED_B_T1)]
22. For each K1 != K:
REMOVE_K_B_T implies (IN_K1_B_T iff IN_K1_B_T1)
23. REMOVE_K_B_T implies (LOCKED_B_T iff LOCKED_B_T1)]
24. For all fluents F: WAIT_T implies (F_T iff F_T1)
Style B:
22. (LOCKED_b1_T and not LOCKED_b1_T1) implies UNLOCK_b1_k1_T.
23. (LOCKED_b2_T and not LOCKED_b2_T1) implies UNLOCK_b2_k2_T.
24. (not LOCKED_b1_T and LOCKED_b1_T1) implies LOCK_b1_k1_T.
25. (not LOCKED_b2_T and LOCKED_b2_T1) implies LOCK_b2_k2_T.
26. (IN_K_B_T and not IN_K_B_T1) implies REMOVE_K_B_T.
27. (not IN_K_B_T and IN_K_B_T1) implies PUTIN_K_B_T.
One action at a time.
28. For each T:
LOCK_b1_k1_T or LOCK_b2_k2_T or UNLOCK_b1_k1_T or LOCK_b2_k2_T or
PUTIN_k1_b1_T or ... or PUTIN_k4_b2_T or
REMOVE_k1_b1_T or ... or REMOVE_k4_b2_T or WAIT_T.
29. For each T, and pair of actions A1 != A2
not(A1_T and A2_T).