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

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



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.

Thanks
Markus