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