Hanoi Analysis

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))