[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:
>> maybe(p) : bool
>> interrupted(p) : bool =
>> wanted_time(p) < timer_setting(p)) -> false,
>> wanted_time(p) > timer_setting(p)) -> true,
>> wanted_time(p) = timer_setting(p)) -> maybe(p)
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
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,