Think Stitch


The Uses of Sequential Compositions

I will introduce two ways to use the sequential compositions in modeling.

Reuses of processes

You can reuse processes by the sequential compositions, like functions, procedures, or subroutines in programs.

Suppose, for example, we have a process P which needs to notify processes Q, R, and S in the middle of processing from time to time. We assume that the process P notifies Q, R, and S through channels chq, chr, and chs respectively. One of the definitions for the process P could be as follows:

(define-process P
  process1
  (! chq (notif1)
     (! chr (notif1)
        (! chs (notif1)
           process2
           (! chq (notif2)
              (! chr (notif2)
                 (! chs (notif2)
                    process3)))))))

This cannot be said to be a good description because the code for notifications is scattered over the whole definition of P and the codes of the same structure are repeated. You can define the process P more elegantly by using the sequential composition with an auxiliary process NOTIF as follows:

(define-process (NOTIF n)
  (! chq (n)
     (! chr (n)
        (! chs (n)
           SKIP))))

(define-process P
  (seq
    process1'
    (NOTIF notif1)
    process2'
    (NOTIF notif2)
    process3))

where process1' and process2' are modified versions of process1 and process2 respectively in which SKIP is placed at the tail position of the process in order for seq to enable the argument processes shift to the next process.

Confluences of Branches

It is often the case that when you make a branch by "if", the process after the proper process on each branch is the same. In other words, it is the case that you want to make the process confluent again.

If you don't make the confluence, you have to write the same process twice.

(define-process (P x)
  (if (pred x)
      (! a (? c (x) (! d (x) Q)))
      (! b (? c (x) (! d (x) Q))) ))

One of the ways to solve this problem is to define an auxiliary process with a name.

(define-process (P x)
  (if (pred x)
      (! a (P2 x))
      (! b (P2 x))))

(define-process (P2 x)
  (? c (y) (! d (x y) Q)))

This seems, however, to be exaggerated since the code fragment is small. In this case, we can describe the process using the sequential composition as follows:

(define-process (P x)
  (seq
    (if (pred x)
        (! a SKIP)
        (! b SKIP))
    (? c (y) (! d (x y) Q))))
31 July, 2013