This article introduces an operator called 'rename' which translates the events and channels specified in the definitions of processes into the other events and channels specified with the operator without chaging the definitions.
The operator 'rename' has the following format:
is a process expression to be renamed. is an association list (a.k.a. A-list) consisting of events and channels, which specifies which event or channel is translated into what event or channel.
The renaming rule is a little bit complicated to be explained in words. Instead, it will be explained through examples.
We firstly define events and channels used in the definitions of processes to be renamed.
(define-event a) (define-event b) (define-event c) (define-channel ch (x) '((0) (1) (2)))
We also define additional events and channels used in the definitions of processes in order to make sure which branch is selected after renaming.
(define-event xa) (define-event xb) (define-event xc) (define-channel xch (x) '((0) (1) (2)))
We define the target process of renaming as follows:
(define-process P (alt (! a (! xa STOP)) (! b (! xb STOP)) (! c (! xc STOP)) (? ch (x) (! xch (x) STOP))))
The computation tree of the process P is as follows:
Nextly, we prepare events and channel which are the targets of renaming. Note that the channel wch has smaller domain compared to ch, xch, and uch. It does not have 2 in the domain.
(define-event d) (define-event e) (define-channel uch (x) '((0) (1) (2))) (define-channel wch (x) '((0) (1)))
Most simple case is that an event is translated into another event. We define a process R which renames the process P. In this case, we translate the event a into the event e.
(define-process R (rename `((,a . ,e)) P))
If you are not familiar to the backquote notations, the following part:
(rename `((,a . ,e))
can be described as follows:
(rename (list (cons a e))
Becauseis evaluated, you can specify any expression which evaluates to an association list consisting of events and channels. You can also use functions to construct rename-maps.
The computation tree of the process R is as follows:
The transition of the event a disappeared and instead the transition of the event e is on the tree. You can check this transition certainly corresponds to the transition of the event a of the process P by seeing the second event is labelled with the event xa.
You can also rename more than one event at a time.
(define-process R (rename `((,a . ,e) (,b . ,d)) P))
You can also rename channels like events. Pairs of channels can be specified in.
(define-process R (rename `((,ch . ,uch)) P))
Each transition of the channel ch is translated into a transition of the channel uch.
When you rename a channel to another channel, the domain of the target channel of renaming must incliude all element of the domain of the source channel. In other words, the domain of the source channel must be a subset of the domain of the target channel.
In the next exmaple, renaming from the channel ch to the channel wch causes an error because the channel wch does not have 2 in the domain which is an element of the domain of the channel ch.
(define-process R (rename `((,ch . ,wch)) P))
When you specify a pair consisting of an event and a channel in, the transition of the event spreads to multiple transitions which correspond to the channel events of the channel.
(define-process R (rename `((,a . ,uch)) P))
The transition of the event a disappeared and instead there are three transitions for the channel uch. Each transition corresponds to each channel event of the channel uch.
When you conversely specify a pair of a channel and an event in, all of the transitions for the channel are translated into transitions with the event. It is nondeterministically decided which transition of them is selected when the event occurs.
(define-process R (rename `((,ch . ,e)) P))
You can rename only part of transitions for a channel using channel events of the channel. Recall that channel events can be obtained by the function $. In the next example, only a channel event ch.1 is renamed to the event e. You can see that the other transitions are not affected.
(define-process R (rename `((,($ ch 1) . ,e)) P))
You can also rename channel events to channels like atomic events.
(define-process R (rename `((,($ ch 1) . ,wch)) P))