motteler@umbc3.UMBC.EDU (Howard E. Motteler) (09/08/89)
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