Hi Chris,
reasoning about ENABLED is still not supported by TLAPS, unfortunately. For the moment you'll have to assert statements like step <1>2 in your proof of z1_liveness. Moreover, temporal reasoning beyond propositional temporal logic is not yet possible, and you will typically need more complex temporal reasoning, such as combining leadsto and wellfounded orderings, for realistic liveness properties. Full support for temporal reasoning, and then for ENABLED, is on the top of our todo list.
Concerning your first question, proving type correctness for your MergeSort algorithm should not be difficult in principle. Of course, you'll need type assertions for the complete state space – for a recursive function, this includes a suitable type correctness predicate for the call stack (which contains the return address from a recursive call). I'm afraid I cannot be more specific without seeing the spec.
Best, Stephan
Hi, two questions:
Firstly I implemented a model for MergeSort, based on the BubbleSort example. It is a recursive function so I am using PlusCal procedure and calling it recursively. It model checks OK with TLC.
I am having trouble proving my TypeOK properties I assume this is because following the data flow into the function call requires some proof using temporal properties. For example, in states which return, I cannot prove pc \in ValidPC. Is this expected to be a hard problem? I can't find any examples that use recursive function calls, and very few that involve this type of temporal proof.
Secondly, I am finding it harder than expected to prove temporal properties. I have traced it down and it seems that I sometimes need to assert ENABLED without proof. I notice a comment in one of the Paxos proofs that TLAPS cannot reason about ENABLED, is this currently true?
My test example follows, note z1_liveness <1>2:
VARIABLE z1
z1_init == z1 = 1 z1_next == z1' = z1 + 1 z1_spec == z1_init /\ [][z1_next]_z1 /\ WF_z1(z1_next)
z1_inv == z1 \in Int
THEOREM z1_safety == z1_spec => []z1_inv <1>1. z1_init => z1_inv BY SMT DEF z1_spec, z1_init, z1_inv <1>2. z1_inv /\ [z1_next]_z1 => z1_inv' BY SMT DEF z1_inv, z1_next <1> QED BY <1>1, <1>2, PTL DEF z1_spec THEOREM z1_liveness == z1_spec => (<> <<z1_next>>_z1) <1> SUFFICES ASSUME z1_spec PROVE (<> <<z1_next>>_z1) BY PTL <1>1. []z1_inv BY z1_safety, PTL <1>2. [](ENABLED <<z1_next>>_z1) (**** BY SMT DEF z1_spec, z1_init, z1_next ****) PROOF OMITTED <1>3. []([]ENABLED <<z1_next>>_z1 => (<> <<z1_next>>_z1)) BY PTL DEF z1_spec <1> QED BY <1>1, <1>2, <1>3, PTL DEF z1_spec, z1_inv, z1_next, z1_init

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, 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.
