construct a separate space for each equivalence class of properties;
{Assign transition rules (Section 2.4)}
for each rule, r, in Ts place r in the space associated with the equivalence class containing the properties in the start (and finish) of r, s; if r is an increasing or decreasing rule then mark s as an attribute space;
{A nalyse initial state (Section 2.4)}
for each object, o, in the domain identify the bag of initial properties of o, I(o);
for cach space, s ,
construct the bag of properties from I(o) which belong to the equivalence class associated with s, b, if b is non empty then add o to the space s if s is not an attribute space then add b as a state in s;
{Extend property spaces ( Section 2.4 )}
for each property space, p.

while there is an unextended state in p, s, mark s as extended; ncwgcn := {};
for each rule in p, r, if the start of r is included in s then add the state snew = (s ominus start oplus end) to newgen; if snewis a superset of any state in newgen then mark p is an attribute space and exit the analysis of p; add newgen to the states in p;
{Extend attribute spaces (Section 2.4)}
changes := TRUE;
while changes, changes := FALSE ;
for each unmarked attribute space, a, extend a where to extend a:
mark a; for each rule in a, r, for each property in enablers of r, p, if p's equivalence class is associated with an unmarked attribute space, a',
then extend a';
add all objects that appear in every space associated with an enabling property for r to a; if objects are added then   changes := TRUE;
{Identify types (Section 2.6)}
for each object in the domain, or identify the pattern of membership of spaces for o, tt; associate the type pattern, tt, with o; for each operator schema, O,
for each argument of O, x, identify the pattern of membership of spaces for x implied by the properties of x in the preconditions of O, tt; associate type pattern, tt, with x in O;
{Construct invariants ( Section 2.7 )}
for each property space, P,
for each property in P, p, construct an identity invariant for p; construct a state membership invariant for P;
construct a uniqueness invariant for P;