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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Wed, 27 Apr 2022 17:56:57 -0700*References*: <09b97d68-4ce2-44a9-b5f3-a4556259dc96n@googlegroups.com>

Hi Hillel, in a nutshell, you're seeing TLC's internal representation of what "Temporal Verification of Reactive Systems: Safety" [1] and “How to verify temporal formulas in TLA” [2] call the "behavior graph" (cross product of the state graph and the tableaux). Unless others have found this graph useful outside of debugging TLC, I suggest we change TLC not to dump `outfile_liveness` by default (with the Toolbox nobody ever noticed because the file is well hidden). Markus [1] https://link.springer.com/book/10.1007/978-1-4612-4222-2 [2] http://www.wischik.com/lu/research/verify-tla-report.html > On Apr 26, 2022, at 6:26 PM, hwa...@xxxxxxxxx <hwayne@xxxxxxxxx> wrote: > > When you run TLC from the command line with the flag option -dump dot outfile and you check a temporal property, then TLC makes two files, `outfile` and `outfile_liveness`. The graphviz for `outfile` is self-descriptive, but I'm having a hard time understanding the `outfile_liveness` graph. First image is a regular state space, second is the liveness dotfile. > > <Xa_image-KYR.png> > > <Xa_image-KYR_liveness.png> > > 1. Why don't all four states appear in the liveness graph? > 2. What do the [t] and [f] labels on the edges mean? > 3. Does the #number.0# mean anything? > > Thanks! > H -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1D61DB69-2FEC-4784-B64A-41146768FCF3%40lemmster.de.

- Prev by Date:
**Re: [tlaplus] Questions about TLA+ formula.** - Next by Date:
**[tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator"** - Previous by thread:
**Re: [tlaplus] Questions about TLA+ formula.** - Next by thread:
**[tlaplus] "Level error in applying operator $Tuple: The level of argument 2 exceeds the maximum level allowed by the operator"** - Index(es):