[Tlaplus-users] First impressions using TLAPS
Stephan.Merz at loria.fr
Lun 31 Mai 16:30:40 CEST 2010
thanks for your report. This is indeed the type of feedback we were hoping for when we released the tool, except that we didn't expect users to be so kind with us. :-)
> I've been trying TLAPS on a small example (proof of critical section
> using a Compare-and-swap based spinlock) and things go well so far.
> Proving type invariants was trivial, and I'm half-way proving the
> "interesting" invariants. The proof language is natural and easy, the
> tools avoid entering into too much details (e.g. the proof of type
> invariant only takes 5 lines) and I believed that writing formal proof
> would have been much harder, so thanks!
Great. If it's not too secret, we'd be interested in collecting examples that could serve as introduction of the system to new users.
> Anyway I wanted to share some initial thoughts and minor nitpicks I
> found (before I get used to the system :)). I hope that this will be
> useful to you.
> 1. Tabs are no longer allowed in TLA+, but pressing tab kept inserting
> them (even if they were displayed in red). The following trivial
> patch makes so that pressing the Tab key directly insert spaces
> instead of tabs.
Thanks for pointing this out. I didn't see the patch you were referring to, but anyway I guess all of us have disabled tabs in emacs, and we should note this in the documentation. Our plan is to move pretty soon to an Eclipse-based interface, which is already used for the other TLA+ tools.
> 2. When the module does not have the same name than the file (e.g.
> MODULE SpinLocke in SpinLock.tla), the parser fails with that error:
> make proof
> ../tools/tlaps-0.9.2010_04_06_03/bin/tlapm SpinLock.tla
> File "./SpinLock.tla", line 1, character 17
> [Internal] <?>
> File "<unknown>":
> Error: Could not parse "./SpinLock.tla" successfully.
> Tlapm ending abnormally with Failure("Module.Parser.parse_file")
> make: *** [proof] Error 1
Not very helpful, indeed.
> 3. (Maybe normal) I tried to prouve the same theorem using two
> different proofs, the first proof was normal, and the second proof
> was incomplete. When I commented out the first proof, the system
> rightly complained, but not when it was present. I think this
> behaviour might be surprising.
I am not sure I completely understand. Do you mean you stated two theorems (with their proofs) in your module that asserted the same statement? TLAPS would not be clever enough to detect this. Or just one THEOREM followed by two proofs?
> 4. When there are no proof for a theorem, the system does not
> complain. This is interesting when writing proofs incrementally,
> (because some steps may be omitted), but I think it would be
> interesting to have an option that checks that there exists a proof
> for every theorem (I've been wondering for some time why a proof
> worked because I forgot to write a proof for a QED). Maybe I did
> not see it?
Hmmm, I'm pretty sure I have seen messages to this effect printed by the proof manager. Maybe that happens only when one asks for checking proofs with Isabelle (-C flag), when it prints the region(s) that have been checked? I let the front-end gurus fill in the details on this one.
Thanks again, and keep asking if you run into problems!
More information about the Tlaplus-users