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: prob03.pddl
TIM: Domain analysis complete for hanoi
TIM: TYPES:
Type T0 = {small}
Type T1 = {pega,pegb,pegc}
Type T2 = {huge,large,massive,medium}
TIM: STATE INVARIANTS:
FORALL x:T0 U T2. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T0 U T2. (Exists y1:T0 U T1 U T2. on(x,y1))
FORALL x:T0 U T1 U T2. FORALL y1. FORALL z1. on(y1,x) AND on(z1,x) => y1 = z1
FORALL x:T0 U T1 U T2. (top(x) OR Exists y1:T0 U T2. on(y1,x))
FORALL x:T0 U T1 U T2. NOT (top(x) AND Exists y1:T0 U T2. on(y1,x))
TIM: DOMAIN INVARIANTS:
|{(x0,x1): on(x0,x1)}| = 5
|{(x0,x1): smaller(x0,x1)}| = 25
|{x0: top(x0)}| = 3
TIM: ATTRIBUTE SPACES:
Objects, x, in T0 U T2 all have property:
Exists y1:T1 U T2. smaller(x,y1);
Objects, x, in T1 U T2 all have property:
Exists y1:T0 U T2. smaller(y1,x);
TIM: OPERATOR PARAMETER RESTRICTIONS:
move(x1:T0 U T2,x2:T1 U T2,x3:T1 U T2)
TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS:
FORALL x:T0. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T0. (Exists y1:T0 U T1 U T2. on(x,y1))
FORALL x:T2. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T2. (Exists y1:T0 U T1 U T2. on(x,y1))
FORALL x:T0. (top(x))
FORALL x:T1. FORALL y1. FORALL z1. on(y1,x) AND on(z1,x) => y1 = z1
FORALL x:T1. (top(x) OR Exists y1:T0 U T2. on(y1,x))
FORALL x:T1. NOT (top(x) AND Exists y1:T0 U T2. on(y1,x))
FORALL x:T2. FORALL y1. FORALL z1. on(y1,x) AND on(z1,x) => y1 = z1
FORALL x:T2. (Exists y1:T0 U T2. on(y1,x) OR top(x))
FORALL x:T2. NOT (Exists y1:T0 U T2. on(y1,x) AND top(x))