TIM's output is divided into 5 components:
It is important to notice that TIM can only infer type information and invariants which are implicit in the domain description. The analysis supports debugging of flawed domain descriptions by making the implicit type information apparent. However, TIM is not able to identify whether domain descriptions are well-typed with respect to some external type system (in the way that, for example, the type checkers of functional programming languages can determine the well-typedness of functional programs). This is because TIM infers the basic types from the domain description rather than being supplied with these as part of a context in which type checking is performed.
A detailed description of the TIM algorithm and its properties is currently in preparation.
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}
It will be noted that TIM produces invariants which, while correct, are slightly weaker than might be hoped since they imply that aircraft and trucks could be loaded into one another. We are currently working on a revision of TIM in which this weakness can be overcome by more precisely capturing the subtle nature of the state/attribute distinction.
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)
Time taken: 0.03u 0.07s 0:00.10 100.0%
TIM: Type Inference Mechanism - support for STAN: State Analysis Planner
D. Long and M. Fox, University of Durham
Reading domain file: domain02.pddl
Reading problem file: prob049.pddl
TIM: Domain analysis complete for mystery-strips
TIM: TYPES:
Type T0 = {arugula,bacon,baguette,beef,cantelope,chicken,chocolate,cod,endive,flounder, ham,hamburger,haroset,hotdog,lamb,lemon,lobster,muffin,papaya,pear,pepper,pork, rice,scallion,shrimp,snickers,sweetroll,tofu,turkey,wonderbread,yogurt}
Type T1 = {venus}
Type T2 = {abrasion,abrasion-1,abrasion-120,abrasion-36,abrasion-44,abrasion-59,abrasion-9, anger,anger-122,anger-127,anger-14,anger-20,anger-27,anger-48,angina,angina-11, angina-121,angina-26,angina-40,angina-54,angina-60,anxiety,anxiety-117,anxiety-15,anxiety-21, anxiety-34,anxiety-47,anxiety-57,boils,boils-118,boils-32,boils-33,boils-5,boils-50,boils-55,depression, depression-112,depression-16,depression-28,depression-38,depression-45,depression-64,dread, dread-116,dread-125,dread-17,dread-29,dread-3,dread-41,grief,grief-10,grief-39,grief-51,grief-63, grief-7,hangover,hangover-113,hangover-12,hangover-23,hangover-37,hangover-52, hangover-61,jealousy,jealousy-115,jealousy-128,jealousy-31,jealousy-46,jealousy-56,jealousy-8, laceration,laceration-114,laceration-25,laceration-35,laceration-53,laceration-58,laceration-6, loneliness,loneliness-111,loneliness-124,loneliness-18,loneliness-22,loneliness-4,loneliness-43, prostatitis,prostatitis-119,prostatitis-126,prostatitis-13,prostatitis-19,prostatitis-30,prostatitis-49, sciatica,sciatica-110,sciatica-123,sciatica-2, sciatica-24,sciatica-42,sciatica-62}
Type T3 = {saturn}
Type T4 = {aesthetics,entertainment,satisfaction}
Type T5 = {jupiter}
Type T6 = {goias}
TIM: STATE INVARIANTS:
FORALL x:T4. FORALL y1. FORALL z1. harmony(x,y1) AND harmony(x,z1) => y1 = z1
FORALL x:T4. (Exists y1:T1 U T3 U T5. harmony(x,y1))
FORALL x:T0. FORALL y1. FORALL z1. locale(x,y1) AND locale(x,z1) => y1 = z1
FORALL x:T0. (Exists y1:T6. locale(x,y1))
FORALL x:T2 U T4. FORALL y1. FORALL z1. fears(x,y1) AND fears(x,z1) => y1 = z1
FORALL x:T2 U T4. FORALL y1. FORALL z1. craves(x,y1) AND craves(x,z1) => y1 = z1
FORALL x:T2 U T4. (Exists y1:T0. craves(x,y1) OR Exists y1:T4. fears(x,y1))
FORALL x:T2 U T4. NOT (Exists y1:T0. craves(x,y1) AND Exists y1:T4. fears(x,y1))
TIM: DOMAIN INVARIANTS:
|{(x0,x1): attacks(x0,x1)}| = 0
|{(x0,x1): eats(x0,x1)}| = 78
|{x0: food(x0)}| = 31
|{(x0,x1): harmony(x0,x1)}| = 3
|{(x0,x1): locale(x0,x1)}| = 31
|{(x0,x1): orbits(x0,x1)}| = 2
|{x0: pain(x0)}| = 97
|{x0: planet(x0)}| = 3
|{x0: pleasure(x0)}| = 3
|{x0: province(x0)}| = 1
TIM: ATTRIBUTE SPACES:
Objects, x, in T1 U T3 U T5 can have property: Exists y1:T4. harmony(y1,x);
Objects, x, in T6 can have property: Exists y1:T0. locale(y1,x);
Objects, x, in T4 can have property: Exists y1:T4. fears(y1,x);
Objects, x, in T0 can have property: Exists y1:T2 U T4. craves(y1,x);
Objects, x, in (empty) all have property: Exists y1:(empty). attacks(x,y1);
Objects, x, in (empty) all have property: Exists y1:(empty). attacks(y1,x);
Objects, x, in T0 all have property: Exists y1:T0. eats(x,y1);
Objects, x, in T0 all have property: Exists y1:T0. eats(y1,x);
Objects, x, in T0 all have property: food(x);
Objects, x, in T1 U T3 all have property: Exists y1:T3 U T5. orbits(x,y1);
Objects, x, in T3 U T5 all have property: Exists y1:T1 U T3. orbits(y1,x);
Objects, x, in T2 all have property: pain(x);
Objects, x, in T1 U T3 U T5 all have property: planet(x);
Objects, x, in T4 all have property: pleasure(x);
Objects, x, in T6 all have property: province(x);
TIM: OPERATOR PARAMETER RESTRICTIONS:
succumb(x1:T2,x2:T4)
feast(x1:T4,x2:T0,x3:T0)
overcome(x1:T2,x2:T4)
Time taken: 0.16u 0.07s 0:00.24 95.8%
Sample Output for a Gripper Domain
TIM: Type Inference Mechanism - support for STAN: State Analysis Planner
D. Long and M. Fox, University of Durham
Reading domain file: domain02.pddl
Reading problem file: prob004.pddl
TIM: Domain analysis complete for gripper-strips
TIM: TYPES:
Type T0 = {rooma,roomb}
Type T1 = {left,right}
Type T2 = {ball1,ball2,ball3,ball4}
TIM: STATE INVARIANTS:
FORALL x:T2. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) => y1 = z1
FORALL x:T2. FORALL y1. FORALL z1. carry(x,y1) AND carry(x,z1) => y1 = z1
FORALL x:T2. (Exists y1:T0. at(x,y1) OR Exists y1:T1. carry(x,y1))
FORALL x:T2. NOT (Exists y1:T0. at(x,y1) AND Exists y1:T1. carry(x,y1))
FORALL x:T1. FORALL y1. FORALL z1. carry(y1,x) AND carry(z1,x) => y1 = z1
FORALL x:T1. (free(x) OR Exists y1:T2. carry(y1,x))
FORALL x:T1. NOT (free(x) AND Exists y1:T2. carry(y1,x))
TIM: DOMAIN INVARIANTS:
|{x0: at-robby(x0)}| = 1
|{x0: ball(x0)}| = 4
|{x0: gripper(x0)}| = 2
|{x0: room(x0)}| = 2
TIM: ATTRIBUTE SPACES:
Objects, x, in T0 can have property: Exists y1:T2. at(y1,x);
Objects, x, in T0 can have property: at-robby(x);
Objects, x, in T2 all have property: ball(x);
Objects, x, in T1 all have property: gripper(x);
Objects, x, in T0 all have property: room(x);
TIM: OPERATOR PARAMETER RESTRICTIONS:
drop(x1:T2,x2:T0,x3:T1)
pick(x1:T2,x2:T0,x3:T1)
move(x1:T0,x2:T0)
Time taken: 0.03u 0.03s 0:00.09 66.6%
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 hanoi
TIM: TYPES:
Type T0 = {huge,large,massive,medium,small,tiny}
Type T1 = {teeny}
Type T2 = {pega,pegb,pegc}
TIM: STATE INVARIANTS:
FORALL x:T0 U T1. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T0 U T1. (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 T1. on(y1,x))
FORALL x:T0 U T1 U T2. NOT (top(x) AND Exists y1:T0 U T1. on(y1,x))
TIM: DOMAIN INVARIANTS:
|{(x0,x1): on(x0,x1)}| = 7
|{(x0,x1): smaller(x0,x1)}| = 42
|{x0: top(x0)}| = 3
TIM: ATTRIBUTE SPACES:
Objects, x, in T0 U T1 all have property: Exists y1:T0 U T2. smaller(x,y1);
Objects, x, in T0 U T2 all have property: Exists y1:T0 U T1. smaller(y1,x);
TIM: OPERATOR PARAMETER RESTRICTIONS:
move(x1:T0 U T1,x2:T0 U T2,x3:T0 U T2)
0.02u 0.05s 0:00.09 77.7%
TIM: Type Inference Mechanism - support for STAN: State Analysis Planner
D. Long and M. Fox, University of Durham
Reading domain file: domain05.pddl
Reading problem file: prob12.pddl
TIM: Domain analysis complete for simple-blocks
TIM: TYPES:
Type T0 = {table}
Type T1 = {a,b,c}
TIM: STATE INVARIANTS:
FORALL x:T1. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) => y1 = z1
FORALL x:T1. (Exists y1:T0 U T1. on(x,y1))
TIM: DOMAIN INVARIANTS:
|{(x0,x1): on(x0,x1)}| = 3
|{x0: table(x0)}| = 1
TIM: ATTRIBUTE SPACES:
Objects, x, in T0 U T1 can have property: clear(x); Exists y1:T1. on(y1,x);
Objects, x, in T0 all have property: table(x);
TIM: OPERATOR PARAMETER RESTRICTIONS:
put(x1:T1,x2:T0 U T1,x3:T0 U T1,x4:T0)
puttable(x1:T1,x2:T0 U T1,x3:T0)
Time taken: 0.01u 0.04s 0:00.07 71.4%