These are all good questions.
> I was stymied by the fact TLA was not reaching every legal next state I thought possible.
I've struggled with this too, and I don't have many tips to suggest.
>
How/can we ask TLA to tell us legal next states from a specified label?
I don't know a straightforward way to list them, but you can easily ask the model checker whether a particular label-to-label transition is possible. For instance, to detect if a process can transition from label "la" to label "lb", you could check the temporal property:
[][~\E pid \in ProcSet: pc[pid] = "la" /\ pc'[pid] = "lb"]_vars
A "violation" of this property would be a trace where some process takes a step from label "la" to label "lb". I often do things like this to check whether certain events are possible in my specifications.
>
How/can we ask TLA to tell us about non-reachable labels?
TLC's "coverage" feature, as you've noted, is supposed to cover this use case. It's always worked quite well for me, although you have to know where to look in the toolbox for the info. If you have a case where the toolbox doesn't show it to you, it might be a bug.
> TLA doesn't bother to name [which liveness property failed]. Why?
There is a workaround, but it is quite tedious to carry out by hand.
Regarding this question:
>* A more operational question: I run TLA with a single LTL _expression_ entered in Property section. The _expression_ reads "LogSizeConsistent == <>([](LogSize=MessageIndex))". Only it is enabled. >When TLA stops it reports "1 Error" under model checking results tab. The console shows,
>--------
>Checking temporal properties for the complete state space with 132 total distinct states at (2020-11-18 20:28:27)
>Temporal properties were violated.
>The following behavior constitutes a counter-example:
<39 states elided>
>----------
Again while I claim or hoped the TLA IDE would be more forthcoming about which property was violated with the last evaluation that made it fail, the TLA tool was of course correct. For some properties, stuttering means that a valid state path may end at a legal state, but the process may not make more progress. The failed property is defined in terms of variables which the trackback does included so one in fact assess why the property failed e.g. failure to make more progress means other code wasn't run hence the property fails to verify. In my case, adding the modifier ``fair" to the processes resolved the violation.
Still I remain confused by the IDE: prior to the fair process modification, it reported two warnings and 1 error. It was sort of clear what the error was (e.g. read the console output), but I never found what the warnings were even though the warnings appears a link in the IDE. Clicking on it reveals nothing additional.On Wednesday, November 18, 2020 at 8:56:37 PM UTC-5 recepient recepient wrote:
Calvin, thank you taking time to respond. Was not aware of PlusCal Manual, section 3.2.8; noted. Just like printf can never replace a symbolic debugger, static analysis, and so on in regular programming languages, print can't be any bottom line in model checking. Agreed.
Still to write LTL expressions right one has to have a sense of what states are reachable, when, and in what format. In my earlier work I was stymied by the fact TLA was not reaching every legal next state I thought possible. `print` helped me see what went wrong because I could at least get a hint of what TLA was up to - what it was running - and places it never seemed to get to. Sometimes variables will have same values but in different states ... making print tough to interpret right ... motivating my earlier question.
Anyway, ... engaging question on better mechanisms than printf()-debugging" to learn about a system's behavior generalizing away from print,
* How/can we ask TLA to tell us legal next states from a specified label? Partial answer? the DOT diagram generator or error trace might be helpful here. The former eats memory on large state but otherwise spot on and the latter I do not understand.
* How/can we ask TLA to tell us about non-reachable labels? Periodically I see TLA pointing out unreachable code, however, not consistently. In my earlier case there was indeed code that was never hit, therefore my loop never continued, and therefore state I wanted to make never happened. Having TLA point out "hey, your label is never hit" would be a plus.
* A more operational question: I run TLA with a single LTL _expression_ entered in Property section. The _expression_ reads "LogSizeConsistent == <>([](LogSize=MessageIndex))". Only it is enabled. When TLA stops it reports "1 Error" under model checking results tab. The console shows,
---------
Checking temporal properties for the complete state space with 132 total distinct states at (2020-11-18 20:28:27)
Temporal properties were violated.
The following behavior constitutes a counter-example:
<39 states elided>
----------
Now as LogSizeConsistent is the only one enabled, I know which property failed. TLA doesn't bother to name it. Why? Finally, no where in the counter example does TLA tell me the value of LogSize, which is a defined function. Nor does it refer to or name LogSizeConsistent in the counter example. Clicking on the hyperlink "1 Error" shows nothing new. TLA is probably right; but I am a lot perplexed about why.
Regards
On Monday, November 16, 2020 at 8:10:00 PM UTC-5 Calvin Loncaric wrote:
No.
Let me defend Markus's response though, which I think actually adds much more value than mine.
PlusCal's print statement is much less useful and much more confusing than you are probably imagining. I believe PlusCal should never have been given a print statement in the first place! Did you know that "TLC may print the value even if the step containing the print statement is not executed" [PlusCal Manual, section 3.2.8]? Did you know that consecutive printed lines are probably not from consecutive states of execution? It is quite reasonable for the first answer to be one that discourages you from such a bizarre language primitive. :)
The good news: TLA+ has much better mechanisms than "printf()-debugging" to learn about a system's behavior. Markus is not suggesting that you have failed to write good correctness properties; he is suggesting that the same TLA+ mechanisms that let you check correctness properties can also be used to explore other properties as well! So let's pop up a level... what properties are you interested in?
--
Calvin
Programmers unlike other engineers tend to comment on questions not asked ... then not answer the question as asked ... thereby adding no value. The rule is: answer the question as-is, then of course, continue on to other thoughts.
In this case this comment,
>TLC check suitable properties
is fully implied to using a model checker in the first place.
I asked the question I did because I still continue to find TLA+'s interpretation of PlusCal code (see the issue elsewhere in this group) weird. Print helps me understand how TLA thinks in small corner cases.
On Monday, November 16, 2020 at 3:13:16 PM UTC-5 Markus Alexander Kuppe wrote:
On 16.11.20 09:28, recepient recepient wrote:
> ... to do something like,
>
> print << __state_num__, msgQueue >>; (* perhaps state_num is hash on
> current state *)
>
> to help disambiguate msgQueue in different states which have the same valu?
You don't give much detail or context, but you appear to be relying on
TLC's print operator to understand your spec. Don't do this! Instead,
have TLC check suitable properties for which it produces useful
error-traces.
Markus
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.