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

Re: MU.pvs

Hi Jean-François,

The mucalculus is part of the prelude as of PVS version 2.3, but the
library dump files have not all been converted yet.

Just comment out the importing of MU@ctlops and it should work.

Sam

> From:    Jean-François Molderez <jfm@cetic.be>
> Subject: MU.pvs
> Date:    Wed, 18 Sep 2002 16:31:07 +0200
> To:      <pvs-help@csl.sri.com>
> 
> [1  <text/plain; iso-8859-1 (quoted-printable)>]
> I don't find the file MU.pvs in my directory pvs/lib/ (when trying to reproduce example in
> chap 4 p54 State Transition Systems and SCR Requirements Specifications)
> 
>                                                         JF Molderez (jfm@cetic.be)
> [2  <text/html; iso-8859-1 (quoted-printable)>]
>