tla2dot

[Up](../index.php) [Readme](README.html) [Releases](RELEASES.html) [Todo](TODO.html)

tladot - Utility to convert tlc/tlaplus state space to graphviz - $Release:0.0.6$

A utility to convert state space dump created by patched tlaplus TLC in TLA toolbox to graphviz dot format.

Usage

Obtain the patched TLC version

Clone github model

 git clone https://github.com/jarjuk/tla2dot

and change the working directory

cd tla2dot

Run Ruby bundler

The tool uses Ruby 2, and to have the required Gems installed run

bundle install

Running the patced TLC version to create state dump

The example below uses TLA model in files DieHard.tla, and DieHard.cfg under directory model.

Set up an environment variable CP to poinnt the patched tla2tools.jar found in directory java

export CP=$(pwd)/java/org.lamport.tlatools-1.0.1-SNAPSHOT.jar

Run TLA model, and generate a dump file ../examples/DieHard-patched.dump using the command

 (cd model; java -cp $CP tlc2.TLC -dump ../examples/DieHard-patched.dump DieHard)

The patched TLC command adds fingerprint and transition information to the dump file. For example, to show the difference of non-patched dump file, and the patched dump file use the command

diff examples/DieHard-orig.dump examples/DieHard-patched.dump

and observe diff output starting

1c1
< State 1:
---
> State 1/1721042995228635026:
5c5
< State 2:
---
> State 2/8981770525750446274:
9c9,11
< State 3:
---
> Transition 1721042995228635026 --> 8981770525750446274
> 
> State 3/-7007095103426876375:
13c15,27
< State 4:
---
> Transition 1721042995228635026 --> -7007095103426876375
> 
> Transition 1721042995228635026 --> 1721042995228635026
> 
> Transition 1721042995228635026 --> 1721042995228635026

Create dot file

To create a dot file for a patched state-dump in examples/customer1-patched.dump, run

bin/tla2dot.rb graph examples/DieHard-patched.dump >tmp/dump.dot

and to convert it to a svg picture, run

dot -T svg tmp/dump.dot >tmp/dump.svg

Command graph accepts optionally a list of variables to show in state nodes. For example, to show model variables big,small in the DieHard example, use the command

bin/tla2dot.rb graph examples/DieHard-patched.dump  big,small >tmp/dump.dot

State identity may be included a pseudo variable ID:

bin/tla2dot.rb graph examples/DieHard-patched.dump  ID,big,small  >tmp/dump.dot

and all variables can be included in the graph using value TRUE for the variable list

bin/tla2dot.rb graph examples/DieHard-patched.dump  TRUE  >tmp/dump.dot

Installation

Add following the lines to Gemfile

source 'https://rubygems.org'
gem 'tla2dot'

and run

bundle install

To validate that installation was successful, and to get help on using tla2dot.rb run

bundle exec tla2dot.rb help

Development

See RELEASES

License

MIT