Tyre-world 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: 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:

Objects, x, in T3 can have property:

Objects, x, in T3 all have property:

Objects, x, in T4 all have property:

Objects, x, in T1 all have property:

Objects, x, in T7 all have property:

Objects, x, in T6 all have property:

Objects, x, in T5 all have property:

Objects, x, in T3 all have property:

Objects, x, in T1 U T2 all have property:

Objects, x, in T0 all have property:

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