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

Re: [tlaplus] How to build Codeplex Tlaplus Tools?

Hi Marc and everyone else reading this,

When I discovered the problem, it seemed to me that liveness checking
simply didn't work in simulation mode and I didn't bother recording
the examples on which I tried it.  Now, we've been unable to reproduce
the problem.  We'd appreciate it if people could try using simulation
mode to check a model specifying a liveness property and let us know
what happens.