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)
TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS:
FORALL x:T2. FORALL y1. FORALL z1. fears(x,y1) AND fears(x,z1) => y1 = z1
FORALL x:T2. FORALL y1. FORALL z1. craves(x,y1) AND craves(x,z1) => y1 = z1
FORALL x:T2. (Exists y1:T0. craves(x,y1) OR Exists y1:T4. fears(x,y1))
FORALL x:T2. NOT (Exists y1:T0. craves(x,y1) AND Exists y1:T4. fears(x,y1))
FORALL x:T4. FORALL y1. FORALL z1. craves(x,y1) AND craves(x,z1) => y1 = z1
FORALL x:T4. (Exists y1:T0. craves(x,y1))