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

Re: [tlaplus] Finite State Machine Visualization

On 28.06.19 22:07, Mike O'Shea wrote:
> One advantage I got to visualizing the FSM based on a specification (I
> did this by hand): I found some enabling conditions missing from two
> action definitions in the example model given in the video lectures for
> the TwoPhase spec which did not technically affect the correctness, but
> after filling them in reduced by 25% the number of states searched.
> Fairly significant reduction - but depends - since the BFS can generate
> potentially exponentially many state paths. That said, the additional
> conditions added made the model easier to understand - which is a positive.

Hi Mike,

not exactly a drawing of the FSM, but the upcoming TLC/Toolbox profiler
shows statistics for states found and distinct states at the action
level (see attached screenshot).  The profiler should be useful in
scenarios as described above.  It is part of all recent nightly toolbox
builds [1].


[1] https://nightly.tlapl.us/

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0aa88525-450f-5d3b-6de7-612c06536347%40lemmster.de.
For more options, visit https://groups.google.com/d/optout.

Attachment: Profiler.png
Description: PNG image