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

*To*: Robert Goldman <goldman@htc.honeywell.com>*Subject*: Re: COND and incomplete information*From*: Darrell Kindred <dkindred@cmu.edu>*Date*: Mon, 29 Jun 98 18:26:12 EDT*Cc*: pvs-help@csl.sri.com, Aaron Larson <alarson@htc.honeywell.com>*In-Reply-To*: <13720.2205.330000.434831@MN65-ZERBINA>*Organization*: Carnegie Mellon University Computer Science Department*References*: <13719.61044.893000.47689@MN65-ZERBINA><199806292052.PAA08500@harpo.htc.honeywell.com><13720.2205.330000.434831@MN65-ZERBINA>*Sender*: dkindred@snooze.adsl.net.cmu.edu

Robert P. Goldman writes: > 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? You're right, I misspoke. The function `maybe' may have different values given different arguments. Its value at any fixed argument, however, is fixed. That may or may not make sense in your example; I don't know what p represents. If the value of p uniquely identifies a single execution of a process, then it may be reasonable to use your `maybe' approach. (Or the `choose' equivalent I describe below.) In this case, you could prove things like wanted_time(p) = timer_setting(p) IMPLIES (run_time(p) = 123 OR run_time(p) = 345) If p's value only specifies the values of certain parameters of the process, then you probably want run_time to be nondeterministic, since you want to allow two processes with the same parameters to choose different paths. If that's the case, you'll probably want run_time to return a set or range of possible runtimes. By the way, an equivalent expression to maybe(p), which won't require defining extra functions, is choose({b:bool|true}) That has the added advantage that you can use it several times and each occurrence may have a different value. - Darrell

**References**:**COND and incomplete information***From:*"Robert P. Goldman" <goldman@htc.honeywell.com>

**Re: COND and incomplete information***From:*"Robert P. Goldman" <goldman@htc.honeywell.com>

- Prev by Date:
**Re: COND and incomplete information** - Next by Date:
**Re: COND and incomplete information** - Prev by thread:
**Re: COND and incomplete information** - Next by thread:
**Re: COND and incomplete information** - Index(es):