Actions with Results

Sometimes actions produce results of interest to the external observer. When I query my checking account balance, I expect the result to be displayed on the ATM screen or printed on a piece of paper.

Here's a Register with read and write actions. Read returns the value of the register; write takes an argument and modifies the register's state. Its initial value is the integer value 0.

Here are the specifications of the actions:

1

 readĒ()/ok(int)

            		pre true

            		post result = x

write(i: int)/ok()

            		pre true

            		post x' = i  

The first thing to notice is that I've introduced the word ``ok'' in the header. I've done this for two reasons. The first is that I want to set myself up so that I can have a convenient way to distinguish normal termination from exceptional termination of a procedure, a feature supported by most advanced programming languages. More on this later. The second is a trivial point: For symmetry, I prefer writing read()/ok(1) instead of read()/1. Think of the instance of an action as a procedure call. Then the state transition labeled read()/ok(1) corresponds to calling the read procedure and getting the integer 1 back.

What I am doing is adding more structure to actions. In general, a state transition is an action instance, which is a pair of an invocation event and response event. An invocation event is the name of the action plus the values of its input arguments; a response event is the name of the termination condition (e.g., ok) plus the value of its result.

An execution of a state machine is a sequence of alternating states and action instances. Some executions of the Register machine are:

For the above executions, I have the following (event-based) traces:

What would I have for a state-based definition of trace?

The second thing to notice in the above specification is that I've given in parentheses the type of the result, if any, of each action. The read action returns an int value; write doesn't return anything.

The third thing to notice is that in the post-condition I use a special reserved word result to stand for the return value. This trick works fine as long as an action produces only one result. It generalizes in the obvious way in case an action produces more than one result.

Technical Aside 1: There is a subtle difference between an action, which is a member of the finite set A, and an action instance, which is a member of the possibly infinite set of state transitions, as defined by . This difference is analogous in programming to the difference between the definition (declaration) of a procedure and a call (invocation) of it.

Technical Aside 2: There are state machine models that treat invocation events and response events as separate kinds of actions. Invocation events could be viewed as input actions; response events, as output actions (see the handout on State Machine Basics.) These models are mainly used for modeling classes of concurrent and distributed systems. For now, there is no compelling reason to treat them separately.