Enhancement of sequential composition operator

[jgroote]

Issue migrated from trac ticket # 1120

component: General | priority: major

2012-12-07 16:08:45: @twillems created the issue

---

The inability of the sequential operator to pass on data values to the next process restricts large-scale modularity of processes.

Consider the following (erroneous) example specification of a Buffer (for the sake of brevity, the example is kept small; motivation comes from larger examples that are less trivial to solve with the current language):

act rec,snd : Nat;

proc Receive = sum n:Nat. rec(n);
proc Send(m:Nat) = snd(m);

proc Buffer = Receive. Send(n). Buffer;

init Buffer;

The idea is that Buffer behaves as a one-place buffer, reading values that must subsequently be sent. The problem is that the value n that is received in process Receive cannot be passed on to the next process using mCRL2 constructs.

LOTOS provides an elegant solution to this problem, by allowing processes to return values and offering a mechanism for using these values in the context of a sequential composition. A suggested syntax could be as follows:

act rec,snd : Nat;

proc Receive = sum n:Nat. rec(n).return(n);
proc Send(m:Nat) = snd(m);

proc Buffer = bind k:Nat in Receive. Send(k). Buffer;

init Buffer;

Obviously, details need to be worked out in case multiple variables are returned (a list?)

[jgroote]

2016-12-04 22:41:57: anonymous changed status from new to assigned

[jgroote]

2016-12-04 22:41:57: anonymous changed owner from jkeiren to jfg

[jgroote]

2016-12-04 22:41:57: anonymous

[jgroote]

2016-12-04 22:41:57: anonymous commented

---

This feature request has not theoretical support as it stands. An adequate theory on parameter passing and return value handover needs to be developed first. But admittedly, various people ran into this problem.