e: {jacket red} post: (white,blue) (red.yellow) pre: (jacket white} {tie yellow}) post: {jacket grey} pre: (jacket grey} pre: {jacket grey} post: {jacket red} post: {jacket white} Fig. 7.44 An EFSM representation of the FSM diagram Since, however, transitions always go between states and not between sets of states, we must instead introduce a qualifying statement on each transition that can differentiate between different values of other state variables, in this case only the variable jacket. Such a qualification is a precondition (abbreviated to pre: in the diagram). From a mathematical point of view, a precondition is "a predicate on the state space", i.e. a logical statement that refers to entities, relations and properties of the resource model, and which must be true if the transition is going to happen. Since the state in which a transition terminates is also a set of states, a similar state- ment must be made for the termination point. This is the postcondition statement (abbreviated to post:). This discussions leads to the following definitions: An explicit state variable is a selected variable of the state space. An explicit state is a subset of states of the state space, where a particular state variable has the same value. In next figure, we focus instead on the state variable jacket, as the explicit state variable. The state symbols depicted in the EFSM diagram will then reflect differ- ent jacket values, depicting four state symbols in this case. Three of the state sym- bols will now represent two states of the state space, having different tie values. Obviously, this state diagram also describes exactly the same behaviour as the pre- vious one, though it looks very different. This discussions leads to the following definitions: Explicit state variables can be used to produce different EFSM diagrams, each diagram focusing on some particular state variable. 7.5 Behaviour Descriptions For a given state machine, there are as many EFSM diagrams based on explicit states as there are variables describing t