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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 12 Oct 2014 01:18:46 -0700 (PDT)*References*: <7c4fd2f4-f223-4642-8ace-d0eb49b378d7@googlegroups.com>

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.

Leslie

**Follow-Ups**:**Re: [tlaplus] Real numbers***From:*Stephan Merz

**References**:**Real numbers***From:*John Baugh

- Prev by Date:
**Re: Real numbers** - Next by Date:
**Re: [tlaplus] Real numbers** - Previous by thread:
**Re: Real numbers** - Next by thread:
**Re: [tlaplus] Real numbers** - Index(es):