[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...

Any suggestions?