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

Re: [tlaplus] Temporal logic

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 leads-to and well-founded orderings, for realistic liveness properties. Full support for temporal reasoning, and then for ENABLED, is on the top of our to-do 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.


On 13 Nov 2014, at 02:49, chris...@xxxxxxxxx wrote:

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:


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.

Stephan Merz