[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

RE: Call for help on CSPM

Hi Larry,

If it is just variables holding you back this is pretty simple.  You can look at Jeremy and Peter's CSP for JCSP for example, and Matt and I used this as a basis for some things we are working on.

Basic idea, you need to declare your variables and channels to allow a process to manage them.  For example:

VARIABLES = { x, y} -- variable names
VALUES = { 0, 1, 2} -- possible values of x and y: need to keep a small set.
datatype Operations = get | set -- get and set operators
channel var_chans = VARIABLES.Operations.VALUES

X_VAR(val) = (x.get!val -> X_VAR(val)) [] (x.set?val -> X_VAR(val))
Y_VAR(val) = (y.get!val -> Y_VAR(val)) [] (y.set?val -> Y_VAR(val))
VARS = X_VAR(0) ||| Y_VAR(0)

Or you can abstract further by passing the channel in to the process:

VAR(chan, val) = (chan.get!val -> VAR(chan, val)) [] (chan.set?val -> VAR(chan, val))
VARS = VAR(var_chans.x, 0) ||| VAR(var_chans.y, 0)

In either case, you can get and set the variable via:
x.get?n
x.set!2

Really just depends what you are trying to do.

Kevin

-----Original Message-----
From: occam-com-request@xxxxxxxxxx <occam-com-request@xxxxxxxxxx> On Behalf Of Larry Dickson
Sent: 15 February 2019 18:45
To: Matt Jadud <matt@xxxxxxxxx>; Carl Ritson <C.G.Ritson@xxxxxxxxxx>; P.H.Welch <P.H.Welch@xxxxxxxxxx>; Fred Barnes <F.R.M.Barnes@xxxxxxxxxx>; Martin, Jeremy <Jeremy.Martin@xxxxxxxxxx>; Bill Roscoe <awroscoe@xxxxxxxxx>
Cc: lindsay spacesciencescorp.com <lindsay@xxxxxxxxxxxxxxxxxxxxx>; rob spacesciencescorp.com <rob@xxxxxxxxxxxxxxxxxxxxx>; Occam Family <occam-com@xxxxxxxxxx>
Subject: Call for help on CSPM

Hello all,

I need help in translating two simple FIFO implementations into CSPM and then feeding them into programs (like FDR and Deadlock Checker) that take CSPM. We can pay a reasonable stipend.

One is the standard bunch-of-buffers-in-parallel and the other is the indexed circular buffer (shelf/store implementation to avoid output ALT). Each varies packet size (one bit or 4096 bits) and depth (5 or 256).

We need to demonstrate practical usability in data-flow problems - no state explosion - or else find a path to it. It has to be possible (Bill Roscoe and C.A.R.  Hoare, "The Laws of occam Programming," 1986; and I did it using "Ground Truth" at CPA2017), but I am wondering if anyone is still working on CSPM? There has to be some way to translate functional language into real computing; or else, I heard a rumor you could do variables as processes?

If anyone is interested I can provide the SHORT documentation.

Larry Dickson




This message and its attachment(s) are intended for the addressee(s) only and should not be read, copied, disclosed, forwarded or relied upon by any person other than the intended addressee(s) without the permission of the sender. If you are not the intended addressee you must not take any action based on this message and its attachment(s) nor must you copy or show them to anyone. Please respond to the sender and ensure that this message and its attachment(s) are deleted.

It is your responsibility to ensure that this message and its attachment(s) are scanned for viruses or other defects. Edinburgh Napier University does not accept liability for any loss or damage which may result from this message or its attachment(s), or for errors or omissions arising after it was sent. Email is not a secure medium. Emails entering Edinburgh Napier University's system are subject to routine monitoring and filtering by Edinburgh Napier University.

Edinburgh Napier University is a registered Scottish charity. Registration number SC018373