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

Re: [PVS-Help] Simple PVS setup question


Did you start PVS from within directory 
/home/<user>/pvs-3.2/Examples/ ?  If not, you need to explicitly tell 
PVS what is the current working directory (context).  The way to do 
this is via the M-x cc (change-context) command.

At 11:59 PM 6/6/2006, Ari Wilson wrote:
>I followed all of the instructions to install PVS on
>my machine and am running into the following problem
>(I haven't modified the pvs script or anything):
>I have a file, ex1.pvs that consists of the following:
>ex1: THEORY
>END ex1
>I do M-x tc and get the following message:
>/home/<user>/pvs-3.2/Examples/ex1.pvs is not in the
>current context
>Any suggestions? Thanks a lot.
>Do You Yahoo!?
>Tired of spam?  Yahoo! Mail has the best spam protection around

| Paul S. Miner, Ph.D.                      | phone: (757) 864-6201
| Senior Research Engineer                  | fax:   (757) 864-4234
| Safety-Critical Avionics Systems Branch  | mailto:paul.s.miner@nasa.gov
| NASA Langley Research Center      | http://shemesh.larc.nasa.gov/people/psm/
| Hampton, Virginia 23681-2199
The contents herein do not necessarily reflect the positions of the 
United States Government.