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

Re: COND and incomplete information


>  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)

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

The usual way to deal with this situation is to introduce an additional
parameter n that identifies *this* run/iteration/ivocation of p.  The
intepretation of n could be time, or round number, or whatever that makes
sense in the context.  Then an uninterpreted oracle function (like your
"maybe" function) tells what the outcome for this run will be in the third
case.  Depending on the model, you may want to remove the n argument from
"wanted_time" below, and/or add one to "timer_setting" (it depends whether
these are independent of the run).

  n: VAR nat

  oracle(p, n) : bool

  interrupted(p, n) : bool =
	  wanted_time(p, n) < timer_setting(p)) -> false,
	  wanted_time(p, n) > timer_setting(p)) -> true,
	  wanted_time(p, n) = timer_setting(p)) -> oracle(p, n)


PS.  Contrary to Darrell Kindred's note, "choose" and the other choice
functions are *functions* and always return the same value when given the
same argument (you just don't know what that value is).