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]. Markus [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
