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

Re: MU library

Hi Aaron,

The MU library is now a part of the PVS prelude.  You can use
M-x view-prelude-file or M-x view-prelude-theory to see the
relevant theories.  Note that the connectives theory is no
longer included, as built-in conversions do the necessary
lifting of the connectives for predicates.

Regards,
Sam Owre

> Hello,
> I have recently begun using PVS to develop a specification for a
> communications protocol.  I have been able to prove an invariant using 
> the PVS prover, but would also like to explore model checking with
> ctl.  However, PVS cannot find the MU library, and neither can I.  Is
> such a thing still available?
> 
> Sincerely,
> Aaron Ballard