[tlaplus] Re: TLA+ and Reals

[Chris Ortiz <zitroomega@xxxxxxxxx>]

Hi John,

I am also trying to follow that paper and trying to model check it. I encountered the same problem. What specifically did you do to make the example to work on TLC?

Thanks,

Zitro

On Tuesday, July 25, 2017 at 6:32:58 AM UTC-7 John Baugh wrote:

Thanks for the quick response, Leslie.

John

On Monday, July 24, 2017 at 8:43:51 PM UTC-4, Leslie Lamport wrote:

I don't remember the details of the paper, but its whole point was to do model checking over a set of integers rather than a set of real numbers.  A check of the models I used for those specs indicates that they substituted Nat for Real and .. for RealInterval.

Leslie

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a6e7fa4e-c185-4c1a-99ed-ed4a6e7a747dn%40googlegroups.com.