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

Re: Conflicting Priorities in occam



Michael Goldsmith wrote:
> 
> I've not kept fully (at all?) up to date with the development of CSPP, but I
> have to say that my intuitions all view any formalism in which
> 
> > ((a --> STOP)[<] (b --> STOP)) \ {b}  = a --> STOP
> 
> is true, with the deepest suspicion.  Maybe Adrian would like to discuss it
> over a pint sometime (or a stein, if you're headed to FEmSys)...

Excellent! You are there and listening. Yes, I had guessed that you
would be on the FS stand at FEmSys.

Have you printed the postscript of the page that covers the above?
It discusses this. The reason is that CSPP does not model an environment
that
can modify its offer between events. You can of course add sampling
events
like a tocking clock to overcome that. Or use a timed
theory.                                                                         

So if the event a is on offer initially, then priority operates and it
is
selected over the hidden event b. a wins. Otherwise, a is not on offer.
But then nothing further happens, apparently. Ok, internally the hidden
event
b occurs, but we can't see that. But that is the behaviour of (a -->
STOP).
If a is never offered, it do does absolutely nothing. QED.

I understand your suspicion, but the semantics of CSPP is subtlely
different from the failures model. And I would say superior :-)

Adrian
--
Dr A E Lawrence (from home)