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

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


Some time ago I realized about the problem: https://groups.google.com/forum/#!searchin/tlaplus/liveness$20simulation/tlaplus/MBjAaNbNMMc/qvp4wtoi9pEJ

I have not further investigated the issue. 

Marc Magrans de Abril

On Wed, Mar 18, 2015 at 12:16 PM, Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:
On 09.03.2015 09:32, marc magrans de abril wrote:
> I'm not sure if I will have the time or the skill to make it happen.
> However, If I had both, I would like to fix the simulation issue with
> Liveness. Simulation is pretty useful when the state space is too big,
> even if incomplete.
> If I had even more time, I would like to have Floats (!= Reals). I'm
> aware that floats imply an awful explosion in sate space. However, I
> think that it could still be useful to use simulation in this case. As I
> said, just a wish, and I can even imagine that it is not even possible.
> In summary just ideas and a small amount of time.
> In any case, thanks for the instructions!

Hi Marc,

can you elaborate on the issues you have with Liveness in simulation
mode? As I said, I'm working on Liveness right now and might have a
chance to address your problems with simulation mode too.


You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/XLAfgMVAu38/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.