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

Re: Real numbers

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.


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.