Up Readme Releases Todo

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

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

 https://github.com/jarjuk/tla2dot

and change the working directory

 cd tla2dot

Running the patced TLC version to create state dump

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

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

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

Run the 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 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 diagran, run

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

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

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

State identity is referenced using 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 variable list

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

Installation

Add following lines to Gemfile

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

and to get help on using tla2tools

bundle exec tla2dot.rb help

Development

See RELEASES

License

MIT