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

Re: Real numbers

I don't know what SAL is, but translating TLA+ into any backend prover is a formidable task.  You would probably wind up writing a possibly correct translation for a tiny subset of TLA+.  Since there already exists a TLA+ to Z3 translation, it would probably be easier to produce a complete translation to Z3 that can reason about reals.  I don't know if the Event-B prover handles reals.  If it does, another possible alternative is to modify their TLA+ to Event-B translator to allow you to do that.  However, that would probably be hard because I don't imagine that they translate proofs.  Hand translating to another prover seems to be the only reasonable alternative to modifying TLAPS.