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