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

*To*: goldman@htc.honeywell.com*Subject*: Re: COND and incomplete information*From*: John Rushby <RUSHBY@csl.sri.com>*Date*: Tue 30 Jun 98 09:11:48-PDT*Cc*: pvs-help@csl.sri.com, alarson@htc.honeywell.com*In-Reply-To*: <13719.61044.893000.47689@MN65-ZERBINA>*Mail-System-Version*: <SUN-MM(229)+TOPSLIB(128)@csl.sri.com>

Robert, > maybe(p) : bool > > interrupted(p) : bool = > COND > wanted_time(p) < timer_setting(p)) -> false, > wanted_time(p) > timer_setting(p)) -> true, > wanted_time(p) = timer_setting(p)) -> maybe(p) > ENDCOND 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 = COND 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) ENDCOND John 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). -------

- Prev by Date:
**Re: COND and incomplete information** - Next by Date:
**Re: Why no TCC generated?** - Prev by thread:
**Re: COND and incomplete information** - Next by thread:
**Re: COND and incomplete information** - Index(es):