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:
Exists y1:T0 U T4 U T5. at(y1,x);
Objects, x, in T0 U T5 can have property:
Exists y1:T0 U T4 U T5. in(y1,x);
Objects, x, in T5 all have property:
airplane(x);
Objects, x, in T2 all have property:
airport(x);
Objects, x, in T3 all have property:
city(x);
Objects, x, in T1 U T2 all have property:
Exists y1:T3. in-city(x,y1);
Objects, x, in T3 all have property:
Exists y1:T1 U T2. in-city(y1,x);
Objects, x, in T1 U T2 all have property:
location(x);
Objects, x, in T4 all have property:
obj(x);
Objects, x, in T0 all have property:
truck(x);
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))