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
http://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html