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

Re: COND and incomplete information




>>>>> "JR" == John Rushby <RUSHBY@csl.sri.com> writes:

JR> Robert,
>> maybe(p) : bool
>> 
>> interrupted(p) : bool =
>> COND
>> wanted_time(p) < timer_setting(p)) -> false,
>> wanted_time(p) > timer_setting(p)) -> true,
>> wanted_time(p) = timer_setting(p)) -> maybe(p)
>> ENDCOND

JR> As you and Darrell Kindred noted, the problem with this is that the outcome
JR> in the third case is always the same (you just don't know what it
JR> is).

Actually, I was thinking of p as being a single, unique process
invocation (the full theory makes this clear).  So the fact that

p = q -> maybe(p) = maybe(q)

doesn't bother me at all.

The thing that did bother me was that I was gooping up the global
namespace with this maybe function.

I suspect that the solution to the question I was asking is to simply
scope the function inside the definition of interrupted.

Best to all,
Robert