Hello! As far as I can understand, the current version of TLAPS does not perform temporal reasoning and hence can't be used to prove liveness properties. Is support for temporal reasoning being developed? As one can currently observe from https://tlaps.codeplex.com/SourceControl/list/changesets TLAPS development is not a completely open process, the only commits are "version 1.2.1" and "push to version 1.4.3". What is the reason for this and will it change in the future? I found https://tlaps.codeplex.com/SourceControl/latest#todo.txt but what other means are there to track the status of TLAPS? Best Regards, Jaak Ristioja Cybernetica AS PS: http://www.msr-inria.fr/projects/tools-for-proofs/#downloads still states "The TLA+ proof system version 1.3.0 has been released!"
Attachment:
0x4FCA45E0.asc
Description: application/pgp-keys