[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
COND and incomplete information
This is a question about how best to represent incomplete information.
Here is the case I am concerned about. I want to write a theory about
a process running that is being monitored by a timer. If the timer
goes off, then the process will be interrupted, otherwise the process
will run to completion.
There are three salient cases:
1. The timer is set for more than the time the process wants. The
process will not be interrupted;
2. The timer is set for less time than the process wants. The
process will be interrupted;
3. The timer is set for EXACTLY the time the process wants. The
process may or may not be interrupted.
I could use a IF-THEN-ELSE form, if it weren't for the nasty third
case above. The best I can come up with for this case is the
following, and I don't like it at all:
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)
I've had to add a senseless maybe function (perhaps this could be
locally scoped), to capture my ignorance about the third case. I
believe I could split the above into a couple of axioms, but I don't
want to lose track of the fact that I've completely characterized the
set of possibilities...