Writing a liveness check for multiple processes

[tlab...@gmail.com]

Hi All,

Given a pluscal specification, I would like to write a liveness check that says if any process is not in the "Done" state, it eventually gets to the "Done" state.

 

The pluscal c manual has this example on page 40:

            (\E i \in 1..N : pc[i] \notin {"ncs", "cs", "I11", "I12"})

                        ~> (\E i \in 1..N : pc[i] = "cs")

 

This is similar to what I'm looking to write, but I'd like to make it stronger by ensuring that the same process that is not "Done" eventually gets to "Done".

(This is in contrast to the above expression that says if *any* process is not in an interesting state, *any* process eventually gets to that interesting state.)

 

If I were to unroll it explicitly, I could write clear liveness checks:

 

            pc[0] # "Done" ~> pc[0] = "Done"

            pc[1] # "Done" ~> pc[1] = "Done"

 

My initial thought was that this expression should do what I want:

            \A i \in 1..N : (pc[i] # "Done" ~> pc[i] = "Done")

 

But I'm not certain if TLC expands that as I expect in the context of a temporal check.  Another possibility is to use the existential operator instead:

 

            \E i \in 1..N : (pc[i] # "Done" ~> pc[i] = "Done")

 

But then it seems that it could be satisfied if one process gets to Done while another never gets to Done.

 

Is there a recommended way of doing this for all processes?

Thanks.

-Tom

[Stephan Merz]

Hello,

            \A i \in 1..N : (pc[i] # "Done" ~> pc[i] = "Done")

is what you want to write, for the reasons that you give (I'm assuming that N is a constant). Note that this formula is equivalent to

\A i \in 1 .. N : []<>(pc[i] = "Done")

and that, as long as processes remain at "Done" when they reach it (as in PlusCal), the latter can be further simplified to

\A i \in 1 .. N : <>(pc[i] = "Done")

Regards,

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e0db34df-ba74-4af3-8298-6642628e0be4%40googlegroups.com.

[tlab...@gmail.com]

Excellent!

Thanks Stephan!

Hello,

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.