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