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