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

Re: COND and incomplete information

>>>>> "DK" == Darrell Kindred <dkindred@cmu.edu> writes:

DK> Robert P. Goldman writes:
>> 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.

DK> I think the problem you're going to have here is that it
DK> sounds like you want `interrupted' to be nondeterministic
DK> (in the third case).  PVS functions, being true functions,
DK> are never nondeterministic.  When you write

DK>    maybe(p) : bool

DK> you're defining a constant function that is either (LAMBDA x: FALSE)
DK> or (LAMBDA x: TRUE), but it's not nondeterministic.  It's
DK> fixed across all uses of `maybe'.  For instance, you can prove
DK> this:

DK>    FORALL p,q: maybe(p) = maybe(q)

I'm afraid I don't understand this.  I understand that I am defining a
function but, since p is a variable (of type process in this case),
why is maybe(p) a constant function?  Surely if p and q are different,
maybe(p) need not equal maybe(q).  Or have I misunderstood the syntax?

DK> If you really want nondeterminism, you'll need to model it
DK> differently.  The best way to do it will depend on the
DK> context in which you're using `interrupted'.  In general, if
DK> you're trying to define a state-transition function mapping
DK> state p to next-state q, you'll want instead to define a
DK> state-transition relation that contains all state pairs p,q
DK> which represent legal transitions.  

I should have been more clear.  I am not trying to define a state
transition function.  Instead, I am trying to define a formula (the
run time of the process) that is conditional on whether the process
simply runs to completion, or is stopped by the intervention of the
timer.  So the interrupted function is being used to select between
multiple definitions of the sum...  What I have done is to do the

run_time(p) : number =
  IF interrupted(p) THEN ....
  ELSE .....

This effectively means that interrupted is used in run_time.  If I
understand you correctly, you seem to be suggesting that it would be
better to use multiple, alternative formulations of run_time inside
interrupted, instead of vice versa....

But that wouldn't quite work, either, since run_time, being a
function, can't be nondeterministic, either.