separate processes, so there is the opportunity for the ship action to be done either before, after, or during the redemption of the electronic money. That policy allows the store to get into a situation where it has already shipped the goods and then finds out the money was bogus.

The store starts out in state a. When the customer orders the goods by performing the pay action, the store enters state 6. In this state, the store begins both the shipping and redemption processes. If the good.s are shipped first, then the store enters state c, where it must still redeem the money from the bank and receive the transfer of an equivalent money file from the bank. Alternatively, the store may send the redeem message first, entering state d. From state d, the store might next ship, entering state c, or it might next receive the transfer of money from the bank, entering state /. From state /, we expect that the store will eventually ship, putting the store in state ,g, where the transaction is complete and nothing more will happen. In state e, the store is waiting for the transfer from the bank. Unfortunately, the goods have already been shipped, and if the transfer never occurs, the store is out of luck.

Last, observe the automaton for the customer, Fig. 2.1(b), This automaton has only one state, reflecting the fact that the customer can do anything, The customer can perform the pay and cancel actions any number of times, in any order, and stays in the lone state after each action.

2,1.3 Enabling the Automata to Ignore Actions

While the three automata of Fig. 2.1 reflect the behaviors of the three participants independently, there are certain transitions that are missing. For example, the store is not affected by a cancel message, so if the cancel action is performed by the customer, the store should remain in whatever state it is in. However, in the formal definition of a finite automaton, which we shall study in Section 2.2, whenever an input X is received by an automaton, the automaton must follow an arc labeled X from the state it is in to some new state. Thus, the automaton for the store n(*eds an additional arc from each state to itself, labeled cancel. Then, whenever the cancel action is executed, the store automaton can make a transition on tliat input, with the effect that it stays in the same state it was in. Without these additional arcs, whenever the caned action was executed the store automaton would die ; that is, the automaton would be in no state at all, and further actions by that automaton would be impossible.

Another potential problem is that one of the participants may, intentionally or erroneously, send an unexpected message, and we do not want this action to cause one of the automata to die. For instance, suppose the customer decided to execute the pay action a second time, while the store was in state e. Since that state has no arc out with label pay, the stores automaton would die before it could receive the transfer from the bank. In summary, we must add to the automata of Fig. 2.1 loops on certain states, with labels for all those actions that must be ignored when in that state; the complete automata are shown in Fig. 2.2. To save space, wc combine the labels onto one arc, rather than

showing several arcs with the same heads and tails bnt different labels. The two kinds of actions that must be ignored are:

cancel pay.cancel pay,cancel pay,cancel

(a) Store

ship, redeem, transfer, pay, cancel

redeem ship

redeem/

transfer ship

4transfer

ship

(i/transfer

pay,cancel pay.cancel pay.cancel pay, ship

Start

cancel

Start

pay,redeem, pay,redeem, cancel, ship cancel, ship

-Ki)-4i)

redeem transfer

(b) Customer

(c) Bank

Figure 2.2: The complete sets of transitions for the three automata

1. Actions that are irrelevant to the participant involved. As we saw, the only irrelevant action for the store is cancel, so each of its seven states has a loop labeled cancel. For the bank, both pay and ship are irrelevant, so we have put at each of the banks states an arc labeled pay, ship. For the customer, ship, redeem and transfer are all irrelevant, so we add arcs with these labels. In effect, it stays in its one state on any sequence of inputs, so the customer automaton has no effect on the operation of the overall system. Of course, the customer is still a participant, since it is the customer who initiates the pay and cancel actions. However, as we mentioned, the matter of who initiates actions has nothing to do with the behavior of the automata.

2. Actions that must not be allowed to kill an automaton. As mentioned, we must not allow the customer to kill the stores automaton by executing pay

again, so we liave added loops with label pay to all but state a (where the pay action is expected and relevant). We have also added loops with labels cancel to states 3 and 4 of the bank, in order to prevent the customer from killing the banks automaton by trying to cancel money that has already been redeemed. The bank properly ignores such a request. Likewise, states 3 and 4 have loops on redeem. The store should not try to redeem the same money twice, but if it does, the bank properly ignores the second request.

2Л .4 The Entire System as an Automaton

While we now have models for how the three participants behave, we do not yet have a representation for the interaction of the three participants. As mentioned, because the customer has no constraints on behavior, that automaton has only one state, and any sequence of events lets it stay in that state; i.e., it is not possible for the system as a whole to die because the customer automaton has no response to an action. However, both the store and bank behave in a complex way, and it is not immediately obvious in what combinations of states these two automata can be.

The normal way to explore the interaction of automata such as these is to construct the product automaton. That automatons states represent a pair of states, one from the store and one from the bank. For instance, the state (3,) of the product automaton represents the situation where the bank is in state 3, and the store is in state d. Since the bank has four states and the store has seven, the product automaton has 4 x 7 = 28 states.

We show the product automaton in Fig. 2.3. For clarity, we have arranged the 28 states in an array. The row corresponds to the state of the bank and the column to the state of the store. To save space, we have also abbrcjviated the labels on the arcs, with P, 5, C, Я, and T standing for pay, ship, cancel, redeem, and transfer, respectively.

To construct the arcs of the product automaton, we пксЛ to run the bank and store automata in paiallel, Each of the two components of the product automaton independently makes transitions on the various inputs, Ho\ever, it is important to notice that if an input action is received, and one of the two automata has no state to go to on that input, then the product automaton dies ; it has no state to go to.

To make this rule for state transitions precise, suppose the product automaton is in state {i,x). That state corresponds to the situation where the bank is in state г and the store in state x. Let Z be one of the input actions. We look at the automaton for the bank, and see whether there is a transition out of state i with label Z. Suppose there is, and it leads to state j (which might be the same as г if the bank loops on input Z). Then, we look at the store and see if there is an arc labeled Z leading to some state y. If both j and у exist, then the product automaton has an arc from state {i,x) to .state {jy), labeled Z. If either of states j or у do not exist (because the bank or store has no arc