
| fly( X, Y , Z)   |
|------------------|
| Pre:             |
| Ad:              |
| Del:             |

| at (X, Y)   |
|-------------|
| at (X , Z)  |
| at (X, Y)   |

allows flying as a means of travel for any object that can be at a location, including packages, and other objects, as well as aircraft. Tim is capable of automatically inferring all types playing the restrictive role indicated in the typed drive operator. However, TIM cannot infer type information that is not implicit in the domain description. Thus, given the untyped fly schema, there are no grounds for TIM to infer any type restrictions. TIM will draw attention to unintended under-discrimination by making packages and aircraft indistinguishable at the type level, unless there is distinguishing information provided in other schemas. At the very least TIM will make explicit the fact that packages are amongst those objects that can fly.  This assists the domain designer in tracking errors and omissions in a domain description, but unstated intended distinctions cannot be enforced by TIM.

## 2.2 An Overview Of The Tim Algorithm

Figure 2 gives a broad outline of the TIM algorithm. A more detailed description is given in Appendix B. The role of each component of the algonthm is described, together with a commentary on discussing related issues and justifications, in Sections 2.3, 2.4 and 2.7.

Broadly, TIM begins with an analysis of the domain operatois, extracting transition rules that form the foundations of the property and attribute spaces described previously. These rules are used to separate properties into equivalence classes from which the property and attribute spaces are constructed. Tim then analyses the initial state in order to assign the domain objects to their appropriate spaces. This analysis also identifies the initial properties of individual objects and uses them to form states of the objects in the property spaces. The initial states in a property space are then extended by the application of the transition rules in that space to form complete sets of states accounting for all of the states that objects in that property space can possibly inhabit. As described in Section 2.4, attribute spaces do not behave like FSMs, as property spaces do, and the extension of these is carried out by a different procedure: one that can add new objects to these spaces, rather than new states.

TIM then assigns types to objects using the pattern of membership of the spaces it has constructed. Finally, TIM uses the spaces to determine invariants that govern the behaviour of the domain and the objects in it.

## 2.3 Constructing The Transition Rules

We begin by describing the process by which the transition rules are constructed. The following definitions are required.

Definition 8 A property is a predicate subscripted by a number between 1 and the arity of that predicate. Every predicate of arity n defines n properties.

Definition 9 A transition rule is an expression of the form:
pr opert y*

$$\begin{array}{r l r l}{r t y^{*}}&{}&{{}\quad p r o p e r t y^{*}}&{}&{{}\quad p r o p e r t y^{*}}\end{array}$$
