[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: MU library
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.
> 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?
> Aaron Ballard
- MU library
- From: Aaron Ballard <email@example.com>