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

Re: [tlaplus] Displaying graphs on TLA Toolbox

Hi Amira,

You may also want to have a look at our tool ProB. It was initially developed for the B-Method but now you can also animate and model check (certain) TLA+ specifications.
Some details can be found here : http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA
With ProB you can visualize the state space out of the box; there are even several techniques to view the state space in reduced form (see also http://www.stups.uni-duesseldorf.de/ProB/index.php5/State_Space_Visualization).

Best regards,
Michael Leuschel

On 8 Feb 2013, at 09:37, Amira Methni <methni...@xxxxxxxxx> wrote:

Hello Stephan,
Thank you for your response.

Best Regards,

Le jeudi 7 février 2013 16:56:34 UTC+1, Stephan Merz a écrit :
Dear Amira,

there is no default way for displaying state graphs. For realistic specifications, these become too big to visualize entirely, although it might be useful to navigate around parts of the state space. For some partial answers to your question, check the discussion following a previous question in this group at https://groups.google.com/d/topic/tlaplus/34gmsa-u1-k/discussion.

Best regards,

On Thursday, February 7, 2013 4:50:53 PM UTC+1, Amira Methni wrote:
I'm new with tla+ and after writing and verifying the specification with TLC, on the TLA toolbox, the graph of states can not be displayed.
Should I install a feature to display graphs (I have also install xdot)


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.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.