TIM: Type Inference Mechanism - support for STAN: State Analysis Planner
D. Long and M. Fox, University of Durham
Reading domain file: domain01.pddl
Reading problem file: prob01.pddl
TIM: Domain analysis complete for flat-tire-strips
TIM: TYPES:
Type T0 = {wrench}
Type T1 = {wheel2}
Type T2 = {wheel1}
Type T3 = {trunk}
Type T4 = {the-hub}
Type T5 = {pump}
Type T6 = {nuts}
Type T7 = {jack}
TIM: STATE INVARIANTS:
FORALL x:T4. (on-ground(x) OR lifted(x))
FORALL x:T4. NOT (on-ground(x) AND lifted(x))
FORALL x:T3. (closed(x) OR open(x))
FORALL x:T3. NOT (closed(x) AND open(x))
FORALL x:T1 U T2. (deflated(x) OR inflated(x))
FORALL x:T1 U T2. NOT (deflated(x) AND inflated(x))
FORALL x:T4. FORALL y1. FORALL z1. on(y1,x) AND on(z1,x) => y1 = z1
FORALL x:T4. (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. on(y1,x) OR free(x))
FORALL x:T4. NOT (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. on(y1,x) AND free(x))
FORALL x:T4. FORALL y1. FORALL z1. tight(y1,x) AND tight(z1,x) => y1 = z1
FORALL x:T4. FORALL y1. FORALL z1. loose(y1,x) AND loose(z1,x) => y1 = z1
FORALL x:T4. ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. tight(y1,x) AND fastened(x)) OR (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. loose(y1,x) AND fastened(x)) OR unfastened(x))
FORALL x:T4. NOT ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. tight(y1,x) AND fastened(x)) AND (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. loose(y1,x) AND fastened(x)))
FORALL x:T4. NOT ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. tight(y1,x) AND fastened(x)) AND unfastened(x))
FORALL x:T4. NOT ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. loose(y1,x) AND fastened(x)) AND unfastened(x))
TIM: DOMAIN INVARIANTS:
|{x0: container(x0)}| = 1
|{x0: hub(x0)}| = 1
|{x0: intact(x0)}| = 1
|{x0: jack(x0)}| = 1
|{x0: nut(x0)}| = 1
|{x0: pump(x0)}| = 1
|{x0: unlocked(x0)}| = 1
|{x0: wheel(x0)}| = 2
|{x0: wrench(x0)}| = 1
TIM: ATTRIBUTE SPACES:
Objects, x, in T0 U T1 U T2 U T5 U T6 U T7 can have property:
Exists y1:T3. in(x,y1);
Exists y1:T4. on(x,y1);
Exists y1:T4. tight(x,y1);
Exists y1:T4. loose(x,y1);
have(x);
Objects, x, in T3 can have property:
Exists y1:T0 U T1 U T2 U T5 U T6 U T7. in(y1,x);
Objects, x, in T3 all have property:
container(x);
Objects, x, in T4 all have property:
hub(x);
Objects, x, in T1 all have property:
intact(x);
Objects, x, in T7 all have property:
jack(x);
Objects, x, in T6 all have property:
nut(x);
Objects, x, in T5 all have property:
pump(x);
Objects, x, in T3 all have property:
unlocked(x);
Objects, x, in T1 U T2 all have property:
wheel(x);
Objects, x, in T0 all have property:
wrench(x);
TIM: OPERATOR PARAMETER RESTRICTIONS:
inflate(x1:T1)
put-on-wheel(x1:T1 U T2,x2:T4)
remove-wheel(x1:T1 U T2,x2:T4)
put-on-nuts(x1:T6,x2:T4)
remove-nuts(x1:T6,x2:T4)
jack-down(x1:T4)
jack-up(x1:T4)
tighten(x1:T6,x2:T4)
loosen(x1:T6,x2:T4)
put-away(x1:T0 U T1 U T2 U T5 U T6 U T7,x2:T3)
fetch(x1:T0 U T1 U T2 U T5 U T6 U T7,x2:T3)
close-container(x1:T3)
open-container(x1:T3)
cuss()
TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS:
FORALL x:T1. (deflated(x) OR inflated(x))
FORALL x:T1. NOT (deflated(x) AND inflated(x))
FORALL x:T2. (deflated(x))
FORALL x:T0. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1
FORALL x:T0. (Exists y1:T3. in(x,y1) OR have(x))
FORALL x:T0. NOT (Exists y1:T3. in(x,y1) AND have(x))
FORALL x:T1. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1
FORALL x:T1. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T1. (Exists y1:T3. in(x,y1) OR have(x) OR Exists y1:T4. on(x,y1))
FORALL x:T1. NOT (Exists y1:T3. in(x,y1) AND have(x))
FORALL x:T1. NOT (Exists y1:T3. in(x,y1) AND Exists y1:T4. on(x,y1))
FORALL x:T1. NOT (have(x) AND Exists y1:T4. on(x,y1))
FORALL x:T2. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1
FORALL x:T2. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T2. (Exists y1:T4. on(x,y1) OR have(x) OR Exists y1:T3. in(x,y1))
FORALL x:T2. NOT (Exists y1:T4. on(x,y1) AND have(x))
FORALL x:T2. NOT (Exists y1:T4. on(x,y1) AND Exists y1:T3. in(x,y1))
FORALL x:T2. NOT (have(x) AND Exists y1:T3. in(x,y1))
FORALL x:T5. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1
FORALL x:T5. (Exists y1:T3. in(x,y1) OR have(x))
FORALL x:T5. NOT (Exists y1:T3. in(x,y1) AND have(x))
FORALL x:T6. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1
FORALL x:T6. FORALL y1. FORALL z1. tight(x,y1) AND tight(x,z1) => y1 = z1
FORALL x:T6. FORALL y1. FORALL z1. loose(x,y1) AND loose(x,z1) => y1 = z1
FORALL x:T6. (Exists y1:T4. tight(x,y1) OR Exists y1:T4. loose(x,y1) OR have(x) OR Exists y1:T3. in(x,y1))
FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND Exists y1:T4. loose(x,y1))
FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND have(x))
FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND Exists y1:T3. in(x,y1))
FORALL x:T6. NOT (Exists y1:T4. loose(x,y1) AND have(x))
FORALL x:T6. NOT (Exists y1:T4. loose(x,y1) AND Exists y1:T3. in(x,y1))
FORALL x:T6. NOT (have(x) AND Exists y1:T3. in(x,y1))