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

Re: Real numbers

Thanks, Leslie.  I'm still looking and thinking about a path forward, and maybe I'll go that route.  As a backup, I'm considering SAL and Yices, and possibly translating PlusCal-generated TLA+ into SAL, or maybe using SAL directly.

John


On Saturday, October 11, 2014 5:37:19 PM UTC-4, Leslie Lamport wrote:
We have had no requests from industrial users for reasoning about real numbers, and we no plans to add support for it.  It shouldn't be too hard to implement, and we'd be happy to help anyone who wants to do it.

Leslie


On Saturday, October 11, 2014 1:04:11 PM UTC-7, John Baugh wrote:
The "Unsupported TLA+ features" page states:
  • None of the back-end provers support reasoning about real numbers.
Given that Z3 can be used as a back-end, I'm curious about whether plans for supporting reals in TLAPS might be in the works.

Thanks,
John