In the first step of designing a program, you roughly think of it, right? When you thought about the behavioral aspect of the design, you would sketch it as state-transition diagrams using events, for example. It is not better to draw them in detail because some of them could be redrawn, or even discarded.
After fixing the sketch and the course of the detailed design, you proceed to make a more detailed model. In this case, there is a trouble that you cannot compare the sketch with the detailed model directly because they are described in different abstract level. Specifically, they use events and channels in different level of abstraction. Roughly speaking, they should be in the correctness relation, and the comparison to check the relation is desired. You can achieve this by renaming.
Suppose, for example, we have a process shown below. It receives data and calculate some on the data, then send the result. It has two modes of operations. In one mode, it merely sends the result. In another mode, it reports the calculation through another channel in addition to sending the result. For brevity, we assume that the mode setting can be done only once at the start time of the process.
All of transitions use event synchronizations as abstract operations. This means we focus on rough behavior and ignore data on channels.
After fixing the rough behavior, we next make a detailed model. Receiving and send data are replaced with channel communications. Reporting is also replaced with channel sending. Additionally, mode setting is also realized as receiving through a channel. In contrast to the rough sketch, the mode setting is stored to a state variable and it will be used by guard. The result of calculation and the contents of the report is chosen to be simply the received data itself in this example.
The computation tree is as follows. You can see that the mode is selected properly as the sketch.
Unfortunately, the process IMP cannot be directly compared with the sketch process SPEC to check if IMP satisfies SPEC or not. Because they use different events and channels. However, if we translate the events and the channels used in IMP to ones in SPEC, we can compare them. This can be achieved by renaming.
As you can see, the channels used in the detailed model IMP are renamed into the events used in the sketch process SPEC. Since IMP uses the channel ch-mode for the mode setting, each channel event of the channel ch-mode is needed to be renamed to an individual event mode0 and mode1.
The renaming from a channel to an event is a many-to-one translation. This means that the renaming procedure is abstraction because the difference of channel arguments is ignored or dropped. In other words, the procedure adjusts the abstraction level of the detailed model to the level of the sketch.
(define-process IMP-ABS (rename `((,($ ch-mode 0) . ,mode0) (,($ ch-mode 1) . ,mode1) (,ch-in . ,in) (,ch-out . ,out) (,ch-report . ,report)) P0))
Now you can compare the abstract IMP and the sketch SPEC. The result shows that IMP actually satisfies SPEC.
Let's explore the renamed (abstract) process IMP-ABS. The computation tree of the process is as follows. Since renaming is just substitution of event labels on the computation tree, there are similar branches which corresponds to each of channel arguments. You can see the received data, which is stored in the state variable x, on the environment window.
Since the value of the state variable differs, you might think they are different states. However, please recall that the behavior of processes is determined by interactions which can be observed by the other party. These three paths has exactly the same sequence of events. This means they cannot be distinguished from the outside.
You can confirm this by seeing the process with Process Explorer in the trace mode. In order to explore a process in the trace mode, compare it with STOP (the check intentionally fails).
You can see that three states are put together.
Let's see another example. This process makes a branch using guard based on the received data through a channel c. If the process receives 0, it generates an event e. Otherwise it calculate some data on the received data and send the result through a channel d. (In this example, the calculation is just -1, for simplicity.)
The computation tree is as follows.
The process is abstracted by renaming the channel c and d to an event ca and da respectively.
(define-process P-ABS (rename `((,c . ,ca) (,d . ,da)) P0))
The computation tree of the abstracted process is as follows.
This time, in contrast to the previous example, there are different behaviors after the event ca. This means that the abstracted process P-ABS has nondeterminism. You can confirm this in the trace mode.
You can see that there are two minimal acceptances in the state after the event ca, which means the process has nondeterminism in the state.
The process P-ABS is actually the same as the following process, which is a typical process having a nondeterministic choice.
In general, nondeterminism may appear when you abstract a process using renaming. If the process has case distinctions on channel arguments and state variables, it could be turned into nondeterministic choices. The reason why this could happen is the abstraction drops the information of channel arguments and blurs whether the guard on them holds or not.
Conversely, if nondeterminism does not appear after renaming, it meas that the process does not depend on the channel arguments. For example, buffers, queues, and stacks we have seen in the user guide and the articles on this site do not depend on the arguments of channels they use. You can check this by renaming the channels into events. You can decide whether or not a process depends on channel arguments by renaming.
It is often the case that case distinctions are described using different events in the sketch-level specifications. In this case, you cannot compare the sketch and the abstracted process because the case distinctions in the detailed model before abstraction turns into nondeterministic choices.
This problem can be solved by renaming each channel event of the channels into different events. This correspondence is determined by guard.
In the above example, we can rename the channel event c.0 into an event ca0 and the others into an event ca. (We assume that the events ca and ca0 are used in the sketch for the case distinction.)
(define-process P-ABS2 (rename `((,($ c 0) . ,ca0) (,($ c 1) . ,ca) (,($ c 2) . ,ca) (,($ c 3) . ,ca) (,d . ,da)) P0))
The computation tree is as follows.
This time nondeterminism does not emerge. You can check this in the trace mode as follows:
That's all for abstraction by renaming, but I want to add something about channel events a little more.
As you saw, the expression of the rename-map looks clumsy. If the domain of the channel c is modified, the rename-map is also needed to be changed since it uses the elements of the domain directly. Additionally, the condition for the case distinction appears in two places, the guard and the rename-map. This could be trouble when you would modify the condition. This problem can be relaxed using channel event functions.
Firstly we define the predicate g? for the condition. The guard on the state-transition diagram is replaced with this. (Needless to say, you should use more descriptive name in models.)
(define (g? x) (= x 0))
You can get the list of all channel events belonging to the specified channel by the function channel-events. The order of the elements in the list does not matter.
In addition, you can get the argument list of the given channel event by the function channel-event-args. Note that the return value is always a list of values even though the channel has only one argument.
The strategy to make a rename-map is as follows: First the channel events are enumerated by channel-events. They are classified with the predicate g? into groups. And then, the elements in each group are paired with ca0 or ca, depending on the group.
(define-process P-ABS3 (rename `((,d . ,da) ,@(map (lambda (x) (if (g? (car (channel-event-args x))) (cons x ca0) (cons x ca))) (channel-events c))) P0))
This code is not needed to be modified even when the condition is changed, or the domain of the channel c is modified.