Logistics 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: prob05.pddl

TIM: Domain analysis complete for logistics-strips

TIM: TYPES:

Type T0 = {bos-truck,la-truck,pgh-truck}

Type T1 = {bos-po,la-po,pgh-po}

Type T2 = {bos-airport,la-airport,pgh-airport}

Type T3 = {bos,la,pgh}

Type T4 = {package1,package2,package3,package4,package5,package6,package7,package8}

Type T5 = {airplane1,airplane2}

TIM: STATE INVARIANTS:

FORALL x:T0 U T4 U T5. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) => y1 = z1

FORALL x:T0 U T4 U T5. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1

FORALL x:T0 U T4 U T5. (Exists y1:T1 U T2. at(x,y1) OR Exists y1:T0 U T5. in(x,y1))

FORALL x:T0 U T4 U T5. NOT (Exists y1:T1 U T2. at(x,y1) AND Exists y1:T0 U T5. in(x,y1))

TIM: DOMAIN INVARIANTS:

|{x0: airplane(x0)}| = 2

|{x0: airport(x0)}| = 3

|{x0: city(x0)}| = 3

|{(x0,x1): in-city(x0,x1)}| = 6

|{x0: location(x0)}| = 6

|{x0: obj(x0)}| = 8

|{x0: truck(x0)}| = 3

TIM: ATTRIBUTE SPACES:

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

Objects, x, in T0 U T5 can have property:

Objects, x, in T5 all have property:

Objects, x, in T2 all have property:

Objects, x, in T3 all have property:

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

Objects, x, in T3 all have property:

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

Objects, x, in T4 all have property:

Objects, x, in T0 all have property:

TIM: OPERATOR PARAMETER RESTRICTIONS:

drive(x1:T0,x2:T1 U T2,x3:T1 U T2,x4:T3)

fly(x1:T5,x2:T2,x3:T2)

unload(x1:T0 U T4 U T5,x2:T0 U T5,x3:T1 U T2)

load-plane(x1:T4,x2:T5,x3:T1 U T2)

load-truck(x1:T4,x2:T0,x3:T1 U T2)

TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS:

FORALL x:T0. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) => y1 = z1

FORALL x:T0. (Exists y1:T1 U T2. at(x,y1))

FORALL x:T4. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) => y1 = z1

FORALL x:T4. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) => y1 = z1

FORALL x:T4. (Exists y1:T1 U T2. at(x,y1) OR Exists y1:T0 U T5. in(x,y1))

FORALL x:T4. NOT (Exists y1:T1 U T2. at(x,y1) AND Exists y1:T0 U T5. in(x,y1))

FORALL x:T5. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) => y1 = z1

FORALL x:T5. (Exists y1:T1 U T2. at(x,y1))