Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ames!haven!umbc3!motteler
From: motteler@umbc3.UMBC.EDU (Howard E. Motteler)
Newsgroups: comp.sys.transputer
Subject: an occam/CSP question
Keywords: ALT, determinism, channel histories
Message-ID: <2277@umbc3.UMBC.EDU>
Date: 8 Sep 89 06:05:37 GMT
Organization: Univ of Maryland Baltimore County
Lines: 16


Suppose we restrict a "self contained" occam program (no external
input or output) so that componants of an ALT have mutually exclusive
guards---every input has a guard, and at most one guard is true at any
given time in any given ALT.

It would then seem that the sequences of values passed along channels
(the histories of the channels, to borrow a dataflow term) would be
the same for any trace of the program.

Is there an easy proof of this, using CSP?  (Or a counterexample, if
I'm missing something obvious...)

-- 
Howard E. Motteler       |  Dept. of Computer Science
motteler@umbc3.umbc.edu  |  UMBC, Catonsville, MD 21228