Up Readme Releases Todo

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

A utility to convert state space dump created by patched TLC tool in TLA toolbox of tlaplus 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 in directory model 'in files setup.tla, setup.cfg, and model.tla

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

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

Create a ../examples/customer1-patched.dump setup for the TLA model using the command

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

The patch adds fingerprint and transition information to the dump file created using -dump option.

For example, difference of non-patched dump file, and the patched dump file for a TLA model may show

1c1
< State 1:
---
> State 1/-2710668386619955114:
25c25
< State 2:
---
> State 2/-2906287262858016143:
60c60,62
< State 3:
---
> Transition -2710668386619955114 --> -2906287262858016143
> 
> State 3/-5306425081709262628:
84c86,88
< State 4:
---
> Transition -2906287262858016143 --> -5306425081709262628
> 
> State 4/3141097224850855796:
95a100,103
> 
> Transition -5306425081709262628 --> 3141097224850855796
> 
> Transition 3141097224850855796 --> 3141097224850855796

Create dot file

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

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

and to convert it to a graph

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

Command graph takes in a list of variables to include in state nodes. For example, in the example model show variables now,step use the command

bin/tla2dot.rb graph examples/customer1-patched.dump now,step  >tmp/dump.dot

State identity is referenced using variable name ID.

bin/tla2dot.rb graph examples/customer1-patched.dump ID,now,step  >tmp/dump.dot

and all variables can be show using value TRUE

bin/tla2dot.rb graph examples/customer1-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