Examples of TIM's analysis of benchmark domains. The domains are as published with the PDDL release.

TIM's output is divided into 5 components:

The types - these form a partition of the domain objects. The output only shows the basic types. These are in fact organised in a hierarchy in which supertypes are unions of basic types. These are denoted explicitly in the analysis which follows using set union notation.
The state invariants - these are logical formulae constraining the properties of objects of specified types.
Domain invariants - these are expressed as size invariants on sets of vectors of objects satisfying specified properties. For example, in a Blocksworld with fixed amount of space on the table, the number of clear surfaces is invariant - any goal set which requires more than this fixed number of clear surfaces can be eliminated without search.
Attribute spaces - TIM distinguishes between states of an object and attributes of an object.The distinction is important to infer correct invariants: attributes do not support the inference of invariants. The analysis lists collections of objects and associated lists of attributes which the objects either might have or must have.
Operator parameter types - this information restricts possible instantiations of operators to those which are well-typed according to the domain description. This information can significantly reduce the number of instantiations that are possible when the domain has potentially rich types but these are not explicit in the original domain definition.

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.

Sample Output for a Logistics Domain

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%

Sample Output for a Mystery 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: 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%

Sample Output for a Hanoi Domain

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%

Sample Output for a Blocks Domain

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%