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