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

[tlaplus] Re: TLA+ and Reals

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?


On Tuesday, July 25, 2017 at 6:32:58 AM UTC-7 John Baugh wrote:
Thanks for the quick response, Leslie.


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.


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.