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

*To*: Pu Zhang <zhangpu@cas.mcmaster.ca>*Subject*: Re: what's the precise meaning of ...?*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Sun, 04 Mar 2001 19:30:10 -0800*cc*: pvs-help@csl.sri.com*In-Reply-To*: Message from Pu Zhang <zhangpu@cas.mcmaster.ca> of "Thu, 22 Feb 2001 16:29:36 EST." <3A9584C0.C7D8060A@cas.mcmaster.ca>*Sender*: pvs-help-owner@csl.sri.com

> I'm intended to prove the following formula: subset?(g,v) where What you probably intended is this: test: THEORY BEGIN valve : TYPE = {closed,open} va : TYPE = setof[valve] v : va = fullset[valve] guan : TYPE = {i : valve | i = closed} gu : TYPE = setof[guan] g : va = fullset[guan] try: formula subset?(g,v) END test The proof of "try" is then simply (grind). > I'm very confused by the precise meaning of variables defined by > 'setof[T]'. setof[T] defines a type, not a variable. > For instance, 'va: type=setof[valve]'. Since 'v: var va ', so, what's > the value of 'v'? v={closed,open} or {open} or {closed} or {closed, > open, {closed,open}} or all of these are possible? In your example, v is a variable which can take any possible value of the type va, including the emptyset, i.e. v={}. > How to define a set like v={closed, open} which contains 2 elements, one > is 'closed', the other is 'open'. Two ways. The first is how I did it above, to say v is a "fullset" of valve, ie contains every element of the set. Another approach would be to enumerate the elements: v : va = {i : valve | i = open OR i = closed} Hope that helps, Dave --- Dr Dave Stringer-Calvert, Senior Project Manager, Computer Science Lab SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com

**References**:**what's the precise meaning of ...?***From:*Pu Zhang <zhangpu@cas.mcmaster.ca>

- Prev by Date:
**what's the precise meaning of ...?** - Next by Date:
**Model-Checking** - Prev by thread:
**what's the precise meaning of ...?** - Next by thread:
**Question on writing a strategy** - Index(es):