How to read the graph generated by TLC? Is there a way to specify its location?

[Ouiza]

Hi everyone,
I have 2 questions related to the graph generated by TLC in the states directory:
1) Is there any way to read it?
2) Is there a way to specify to TLC where to create the states directory, I am running it in a network environment with the "workers" option and I want it to write in the local space of the machine where it's being run, by default it's writing in my home directory.

Thanks and best regards,
Ouiza

[Stephan Merz]

Hello Ouiza,

I don't know the reply to your first question. In any case, there is no existing tool that would allow you to analyze the graph, so you'd have to look at the TLC code to interpret the data.

For the second question, you can specify the directory using the -metadir option of TLC when you run it from the command line. (You can download the command-line version from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html). There does not (yet) seem to be a way to pass such parameters to TLC from the Toolbox, but Leslie announced that this will come in a future version.

Hope this helps,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@googlegroups.com.
To unsubscribe from this group, send email to tlaplus+u...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
 
 

[Ouiza]

Hi Stephan,
Thank you very much for your answer.
I tried the -metadir option and it works.
Ouiza

[Markus]

On Friday, November 9, 2012 4:52:00 PM UTC+1, Ouiza wrote:

Hi everyone,
I have 2 questions related to the graph generated by TLC in the states directory:
1) Is there any way to read it?

Hi Ouiza,

https://tla.msr-inria.inria.fr/kuppe/org.lamport.tla.toolbox.tool.tlc.ui.trace.zip is the code I hacked a while ago to recreate a visual state graph from the .st file. That might serve as an inspiration.

HTH
Markus

[Ouiza]

Hi Markus!
Thank you very much, I really appreciate!
I will have a look at your code and be back if I have any question.
Best regards,
Ouiza

[Ouiza]

Hi Markus!
I am not used with plugins and to save time, I would like to know if I can run your code outside of Eclipse.
I had a look at it and saw that I need packages which I expect to be in the plugins directory under toolbox. When I tried to run javac on your java files, I got this as the first error:
org/lamport/tla/toolbox/tool/tlc/ui/trace/TLCTraceFileModelProvider.java:6: package org.lamport.tla.toolbox.util does not exist
import org.lamport.tla.toolbox.util.RCPNameToFileIStream

Thank you for your help.

 
Best regards,
Ouiza

On Friday, 9 November 2012 16:10:31 UTC-5, Markus wrote:

[Markus]

On Wednesday, November 14, 2012 5:22:33 PM UTC+1, Ouiza wrote:

Hi Markus!
I am not used with plugins and to save time, I would like to know if I can run your code outside of Eclipse.
I had a look at it and saw that I need packages which I expect to be in the plugins directory under toolbox. When I tried to run javac on your java files, I got this as the first error:
org/lamport/tla/toolbox/tool/tlc/ui/trace/TLCTraceFileModelProvider.java:6: package org.lamport.tla.toolbox.util does not exist
import org.lamport.tla.toolbox.util.RCPNameToFileIStream

Hi Ouiza,

no, you won't be able to run the code outside the Toolbox or Eclipse. And even running it in the Toolbox requires one to install additional dependencies (GEF zest).

I actually posted the code as a reference on how to parse/read the .st file, not for you to execute it (the UI part won't scale to more than ~10^2 states anyway). The interesting bits are in TLCTraceFileModelProvider.java. Btw. all tlc2.* and util.* imports are part of the Tools distribution [1].

Thanks
Markus

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html

[Ouiza]

Ok, thanks.
Ouiza

[Amira Methni]

Hi Markus,

I want to display graph generated by TLC but i don't understand how your plugin works.
Could you explain to me how can i execute it and what it takes as entry.

Thanks,

Amira

[Markus Alexander Kuppe]

On 09/27/2013 04:07 PM, Amira Methni wrote:
> Hi Markus,
> I want to display graph generated by TLC but i don't understand how your plugin
> works.
> Could you explain to me how can i execute it and what it takes as entry.

Hi Amira,

I have made a special build available [1] that comes with the TLC Trace
File Viewer installed. Just grab a zip for your architecture.

You can open the corresponding TLC Trace Viewer via "CTRL+3" and
typing "Trace File Viewer" [2]. The view that opens up has an "Open
Trace" in its view menu [3] where you are prompted for trace and spec.

The input it takes are the trace file (.st) with all (explored) states
and the original spec.

Do not expect the graph to scale beyond a few states though (I have
never tried it on more the 100 states).

HTH
Markus

PS: If there is demand, the trace viewer could easily be added to the
next toolbox release.

[1] https://tla.msr-inria.inria.fr/kuppe/traceviewer
[2]
https://tla.msr-inria.inria.fr/kuppe/traceviewer/OpenTLCTraceFileViewer.png
[3] https://tla.msr-inria.inria.fr/kuppe/traceviewer/OpenTraceAndSpec.png

[sawsan8...@gmail.com]

Hello
I am working on TLA in order to analyze the filters in Dynamic networks, how can I see the states and the results of TLC models checking if there no error trace>
Second question: I am working on windows not linux, is that a reason for not finding TLC Trace viewer? cause I dwonloaded the zip file but still I could not find a way to see the results or save it
Thank you in advance

[Stephan Merz]

TLC explores the entire graph of reachable states of the instance you give it to verify. If no error is found, the Toolbox displays some quantitative information, including how many states TLC visited and coverage information about the underlying specification. It does not visualize the entire state space, if that's what you mean.

Regards,
Stephan

> --
> 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...@googlegroups.com.

> To post to this group, send email to tla...@googlegroups.com.

> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Y2i]

I am working on TLA in order to analyze the filters in Dynamic networks, how can I see the states and the results of TLC models checking if there no error trace>

Sometimes I deliberately introduce an error in a spec, like a type invariant violation, to let Toolbox display the sequence of states that leads to the error.

Regards,

Yuri

[Leslie Lamport]

I have finally put a list of all TLC command-line options on the current TLA+ web site at:

     http://research.microsoft.com/en-us/um/people/lamport/tla/tlc-options.html

That page is reachable through a link on the TLC page, which is reachable by a link on the TLA+ Tools page.  You will find there a -dump option that writes all the states that TLC finds to a file. 

Leslie

[sawsan8...@gmail.com]

Dear Leslie Lamport
Thank you for your Reply, I will try that on the model
sawsan

[sawsan8...@gmail.com]

Hell Yuri
Thnak for your Reply, I do the same thing with the model I am working on it

[sawsan8...@gmail.com]

Hello Stephen .. Thanks a lot for your reply

[fl]

> Do not expect the graph to scale beyond a few states though (I have
> never tried it on more the 100 states).

 

There is a demand obviously and if you can give use a TLAPLUS specification

of your algorithm we can try to implement it using other tools using graphviz or another

tool.

 

--

FL

[Markus Alexander Kuppe]

On 16.12.2015 16:16, fl wrote:
> There is a demand obviously and if you can give use a TLAPLUS specification
> of your algorithm we can try to implement it using other tools using
> graphviz or another
> tool.

Hi Frederic,

I recently used graphviz to visualize the technical representation of
TLC's liveness graph (i.e. see [1] where the labels are
fingerprints/tableau ids). For a directed graph, I found though that
graphviz either doesn't handle more than a few dozen states or creates
an incomprehensible entangled mess (with its fast layout algorithm).

As for my prototype, there is no TLA+ specification or even an
implementation of a layout algorithm. It rather uses Eclipse Zest [2]
which implements similar algorithms to those in graphviz.

Besides the deficiencies of the graphing libraries, you will also have
to make TLC keep the actual states rather than fingerprints or you won't
be able to print the variable assignments (my prototype effectively
explores the state graph twice).

That said, you find the prototype's source code at Codeplex [3].


Does anybody know the number of states ProB's visualization can
realistically handle?

Cheers
Markus

[1]
http://tlaplus.codeplex.com/Download/AttachmentDownload.ashx?ProjectName=tlaplus&WorkItemId=8&FileAttachmentId=1441621
[2] https://www.eclipse.org/gef/zest/
[3] http://tlaplus.codeplex.com/SourceControl/latest

[Michael Leuschel]

Hi Markus,

ProB also uses DOT to render the state space, this puts a severe limit on how much states and transitions can be rendered within reasonable time (and how much this information is of use to users). When you exceed about 100 transitions the rendering time starts becoming very high, if I remember correctly.

The ProB tool displays a warning when the state space exceeds 250 nodes, asking the user to confirm whether dot should be launched.

What I find very useful, however, is the state space projection feature: basically, the user types an expression and ProB evaluates the expression over the state space and displays the projected graph. Below is an example for a TLA hour-minute-seconds clock.

The state space is too large to render with DOT, however, one can type in an expression like “hour” and obtain the projection.

The graph is attached below, dotted lines mean that the action is not always possible or does not always lead to the target equivalence class.

A solid line means the action is always possible and always leads to the same equivalence class.

This graph actually shows that the hour progression (0 -> 1 -> 2….) is correct, but also highlights a bug in the model: if the hour is 1..11, then the next state always increases the hour by one.

(I leave the task of correcting the model to the interested reader).

(I don’t know where the model is from; while typing this post I was looking for a TLA+ model to showcase the projection diagram and didn’t expect the model to be faulty ;-)).

I also attach another example below: the Sieve Prime number algorithm, with MAX=1000 and where the state space is projected onto s=Cardinality(N).

Other (B) examples, such as the ABZ’14 landing gear, are in an ICFEM’2015 paper, in case you are interested.

On 16 Dec 2015, at 17:04, Markus Alexander Kuppe <tlaplus-go...@lemmster.de> wrote:

Does anybody know the number of states ProB's visualization can
realistically handle?

Kind regards,

Michael

---------------------- MODULE clock_init0 ----------------------

EXTENDS Naturals

VARIABLES

  hours,

  minutes,

  seconds

Init  ==    hours = 0

               /\ minutes = 0

               /\ seconds = 0 

Next  ==    hours' = (IF minutes # 59 THEN hours ELSE (hours + 1) % 12)

               /\ minutes' = (IF seconds # 59 THEN minutes ELSE (minutes + 1) % 60)

               /\ seconds' = (seconds + 1) % 60

Clock  ==  Init /\ [][Next]_{seconds}

--------------------------------------------------------------

THEOREM  Hansen

==============================================================

---- MODULE Sieve_Full ----

EXTENDS Naturals, FiniteSets

CONSTANT MAX

VARIABLE cur, N, s

Init == /\ cur = 2

        /\ N = 2..MAX

        /\ s = Cardinality(N)

prime == /\ cur \in N

         /\ cur' = cur+1

         /\ N' = N \ {cur*n : n\in cur..(MAX \div cur) }

         /\ s' = Cardinality(N')

nprime == /\ cur \notin N

          /\ cur*cur < MAX

          /\ cur' = cur+1

          /\ UNCHANGED <<N,s>>

Next == prime \/ nprime

Spec == Init /\ [] [Next]_<<cur,N,s>>

===================

[fl]

 

Hi Markus,

> For a directed graph, I found though that
> graphviz either doesn't handle more than a few dozen states or creates
> an incomprehensible entangled mess (with its fast layout algorithm).

 

400 nodes here:

 

http://www.graphviz.org/Gallery/undirected/root.svg

 

Finding a good representation for a large graph is challenging

and needs more studies.

 

But they have technics to order the nodes or explore them  

just like "the fish eye view".

 

And those softwares deserve to be thought of.

 

--

FL

[Michael Leuschel]

I made a mistake while posting the clock example and accidentally replaced the Clock => []Init  theorem.

Below is the corrected model in case you want to try it out (and correct the bug ;-)).

---------------------- MODULE clock_init0 ----------------------

EXTENDS Naturals

VARIABLES

  hours,

  minutes,

  seconds

Init  ==    hours = 0

               /\ minutes = 0

               /\ seconds = 0 

Next  ==    hours' = (IF minutes # 59 THEN hours ELSE (hours + 1) % 12)

               /\ minutes' = (IF seconds # 59 THEN minutes ELSE (minutes + 1) % 60)

               /\ seconds' = (seconds + 1) % 60

Clock  ==  Init /\ [][Next]_<<hours, minutes, seconds>>

--------------------------------------------------------------

THEOREM  Clock => []Init

==============================================================

[fl]

> 400 nodes here:

> http://www.graphviz.org/Gallery/undirected/root.svg

 

This one is impressive.

 

http://www.hpcwire.com/2013/11/16/sc13-research-highlight-large-graph-processing-without-overhead/

 

The software used to render the graph is not provided but it shows at least that large graphs

are not out of reach. (Wen you think it is supposed to represent "A Protein Interaction Map of

Drosophila melanogaster" (a fly then) you are definitely convinced that "There are more things in

heaven and earth,  Horatio,  // Than are dreamt of in your philosophy."  Hamlet (1.5.167-8)

--

FL

[Michael Leuschel]

Hi Frederic,

On 17 Dec 2015, at 17:48, fl <freder...@laposte.net> wrote:

 

This one is impressive.

 

http://www.hpcwire.com/2013/11/16/sc13-research-highlight-large-graph-processing-without-overhead/

 

The software used to render the graph is not provided but it shows at least that large graphs

are not out of reach. (Wen you think it is supposed to represent "A Protein Interaction Map of

Drosophila melanogaster" (a fly then) you are definitely convinced that "There are more things in

heaven and earth,  Horatio,  // Than are dreamt of in your philosophy."  Hamlet (1.5.167-8)

—

Yes, that looks very impressive indeed.

Thanks to your posts, I have also found this link which also mentions the sfdp tool:

 http://stackoverflow.com/questions/13417411/laying-out-a-large-graph-with-graphviz

sdfp accepts dot files as input; so it could be used for Mark’s TLC visualization.

I have just updated ProB so that there is now the option to use sfdp instead of dot for rendering the state space.

It renders much faster for larger state spaces; but I am not really sure that it will be that useful for users yet. Probably one would have to add some custom colouring of the nodes, depending on some user-specified expression/property, to help a human make sense of the visualization.

I can publish some of the state space visualizations for TLC models on a website if you are interested (the size of the generated PDFs get larger; so I am not inclined to post them here on the mailing list).

Greetings,

Michael

[fl]

 

I can publish some of the state space visualizations for TLC models on a website if you are interested (the size of the generated PDFs get larger; so I am not inclined to post them here on the mailing list).

 

 

 

Hi Michael,

 

yes do that so that we can see  the result.

 

--

FL

[Michael Leuschel]

Hi Frederic,

I tried one TLA+ example, the MCAlternatingBit protocol example in the TLC distribution.

I have put a png of the visualization for about 2000 states and 11,000 transitions at this wiki page:

 http://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples

I can send you the full PDF (1.7 MB); rendering was fast.

Orange nodes satisfy the predicate RBit=1.

Greetings,

Michael

[fl]

> I have put a png of the visualization for about 2000 states and 11,000 transitions at this wiki page:
> http://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples

Hi, Michael,

the first one is difficult to interpret. And I don't know how people could take advantage of it (1). The second one

on the contrary can be useful.

(1) But maybe it is due to the idiosyncrasy of the alternating bit protocol. A more traditional algorithm would be

easier to make sense of it.

-- 

FL

[Michael Leuschel]

Hi,

FYI: I have added a few more examples to the web page (http://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples).

I agree and I also believe the projection diagrams to be the most useful; they have already enabled me to uncover various issues with several models.

But sometimes the visualization of the full state space can yield surprising results; see, e.g., the visualization of the Hanoi model.

Greetings,

Michael

[fl]

> FYI: I have added a few more examples to the web page .

Can you post an enalargement of the Rush Hour state space around the orange nodes. I'd like to be able to read
the labels to see if it can bring the user something.

> But sometimes the visualization of the full state space can yield surprising results; see, e.g., the visualization of the > Hanoi model.

Yes it is really curious the homorphism of the  state space and the Sierpinski Gasket.
 
--
FL

[jarjuk]

Hello,

I have made a small patch to TLC -dump option, which outputs state fingerprint and transition information to TLC -dump file,
and a ruby script 'tla2dot', which parses the dump file and outputs graphviz dot notation.

The patch, the pathced tla2tools.jar, and the ruby script are available in https://github.com/jarjuk/tla2dot under MIT licences.

I have used the tool only in small scale mainly to better understand state space generation, and to communicate, how tla2tool works.

Is it be possible to add the patch https://github.com/jarjuk/tla2dot/blob/master/tla2dot.patch to tlatools trunk?

BR,
Jukka