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

*To*: pvs-help@csl.sri.com*Subject*: what's the precise meaning of ...?*From*: Pu Zhang <zhangpu@cas.mcmaster.ca>*Date*: Thu, 22 Feb 2001 16:29:36 -0500*Sender*: pvs-help-owner@csl.sri.com

Hello, friends

I'm intended to prove the following formula: *subset?(g,v)* where
*g={closed}*,
*v={closed,open}*. I failed. The code is :

*valve: type = {closed,open}*
*va: type=setof[valve]*
*v: var va
% Do these statements correctly define v={closed, open} ?*
* *

*guan: type = {i:valve | i=closed}*
*gu: type =setof[guan]*
*g: var gu
% Do these statements correctly define g={closed} ?*

*try: formula subset?(g,v)*

The possible reasons might be sth relating to '*va: type=setof[valve]*'.
I'm very

confused by the precise meaning of variables defined by '*setof[T]*'.
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? How
to define a set like
*v={closed, open}* which contains 2 elements, one is '*closed*',
the other is '*open*'.

I've checked the manuals, but didn't find the answers. Could anybody help me with the 2 questions? Thank you very much.

Pu

- Prev by Date:
**Re: PVS questions** - Next by Date:
**Re: what's the precise meaning of ...?** - Prev by thread:
**Model-Checking** - Next by thread:
**Re: what's the precise meaning of ...?** - Index(es):