![[A sample labelled
state transition system]](affect.png)
TVT (Tampere Verification Tool) was developed by the Verification Algorithm Research Group (VARG) at Tampere University of Technology.
While the tool itself was not publicly available until November 16, 2001, we were provided with an interface library of the tool in late July 2001. This C++ library implements textual input and output of labelled state transition systems in the TVT format. The library is now distributed as part of the toolset, which is covered by the Nokia Open Source License.
The current version of Maria supports the
command lsts, which allows execution paths or complete
reachability graphs of Maria models to be output in a format that the
TVT interface library recognises. For various reasons, this output
option does not make any use of the interface library.
The TVT format—as of July 2001—cannot be generated truly incrementally, since the TVT parser requires that the input be grouped in a certain way and that the size of the input be specified in advance. This problem can partly be solved by making use of the file inclusion feature of the TVT parser.
Maria generates TVT output in three files. The main file specifies
the size of the system and contains directives for including LSTS
action names (which correspond to transition instances in the Petri
net) and LSTS transitions (arcs in the reachability graph) from
separate files, whose names carry the suffixes -act and
-trans.
Unfortunately the file inclusion feature has not been implemented on the lexical analysis level, but it has been defined in the grammar. Because of this, the blocks that specify the states in which the specified state propositions hold, cannot be attached to the output LSTS via a file inclusion mechanism. Instead, the blocks are first written to temporary files and then copied to the main file.
The LSTS output option consumes main memory in proportion to the
amount of generated LSTS action names. A memory-based look-up
structure for generated action names is needed, since TVT identifies
actions by index numbers instead of names. Whenever an arc of the
reachability graph is added to the LSTS, Maria encodes the transition
instance to a bit string and converts it to a TVT action number using
the look-up structure. Whenever an action is added to the structure,
it is also written to the -act file. The
-trans file refers to the actions by numbers.
The TVT to Maria translator, which translates a set of labelled
state transition systems to a Petri net model that computes the
parallel composition of these systems, was designed and implemented by
Kimmo Varpaaniemi and improved by
Marko Mäkelä. The translator,
called lsts2pn, is available under the conditions of the
GNU General Public
License (GNU GPL).
Due to the simple nature of this converter, we distribute it as two
files: lsts2pn.C (the program code) and Makefile (the compiling commands). You may want
to alter some variable definitions in the Makefile.
Non-alphanumeric characters in identifiers are transformed both by
lsts2pn and by Maria. To reverse these transformations,
Marko Mäkelä wrote the Perl script
lsts-demangle.pl, which is in the
public domain. The script can be invoked on Maria-generated LSTS
files that contain names of actions or state propositions, to convert
the names in the output LSTS files to a format that is equivalent with
the names in the input LSTS files.
TVT contains a visualisation tool, but it (as far as we know) has
problems with larger systems and only produces multi-coloured bitmap images.
In order to produce the images for this document, Marko Mäkelä wrote
lsts2dot, a translator from TVT LSTS files to the input
language of GraphViz, a graph
visualisation library developed at AT&T.
The translator uses the same identifier transformation algorithm as
lsts2pn. Please note that there are bugs in GraphViz
that affect the display of labels containing backslash characters.
The compilation of this translator, lsts2dot.C, is controlled by the same Makefile as lsts2pn.C.
Typical usage is lsts2dot file.lsts | dotty
-" or "lsts2dot file.lsts | dot -Tps >
file.eps.
The figures on this page were created with the command
lsts2dot file.lsts | dot -Nfontname=Verdana
-Nfontsize=10 -Efontname=Verdana -Efontsize=7 -Tpng >
file.png.
The input file affect.lsts describes the following system:
This system can be transformed to Maria format by executing the
command lsts2pn affect.lsts > affect.pn. A more
interesting exercise is to synchronise the system with itself by
writing something like lsts2pn affect.lsts affect.lsts >
affect2.pn. Note that this example assumes that
lsts2pn has been compiled with the option
RELABEL_PROPS enabled. Alternatively, the second
argument affect.lsts could be replaced with a file that
contains different names for state propositions.
The parallel composition of the two systems can be computed with
the command maria -m affect2.pn -e 'lsts
"affect2.lsts";breadth;exit'. The resulting system, affect2.lsts (which we have slightly modified
for illustration purposes to eliminate file inclusions), has more
branches than the original system:
![[The sample system
synchronised with itself]](affect2.png)
Kimmo Varpaaniemi decomposed the PROD
system dekref.net to a set of LSTS
components. The system is otherwise identical to the dekker.net
distributed with PROD, but a #verify formula has been
removed.
In the following, we use a copy of lsts2pn that has
been compiled with the option RELABEL_PROPS disabled.
Without this option, the names of state propositions must be globally
unique in the composed system, and no prefixes are added to the
proposition names in the parallel composition.
lsts2pn dek*.lsts > dekker.pn
The decomposition was verified to be equivalent with the original PROD model by generating a labelled transition system in the ARA format (precursor of TVT) from the PROD model and by comparing the LTS with the Maria-generated composition of the LSTS components:
prod dekref.init
./dekref -A
maria -wm dekker.pn -e'lsts "dekker.lsts";breadth;exit'
"dekker.pn": 474 states, 666 arcs
lsts-demangle.pl dekker.lsts-act
tvt_27_july_01/Src/AraFormats/fftool --ara --force dekker.lsts dekker.lts
aracompu dekref.lts dekker.lts
ARA LTS Comparator 1.0 (c) VTT Electronics 1992-1994
ARA LTS to minimal AG Converter v1.54 (c) VTT Electronics 1992-94
Memory available: 10000000
Reading file dekref.lts
Lts to Ag start.
Lts to det-Lts in progress...
[...]
474 nodes
666 arcs
Det-Lts to Ag in progress...
Lts to Ag end.
Ag to minimized Ag start.
Initial blocks created
[...]
Ag to minimized Ag end.
Writing file tmp1.ag
Memory available: 10000000
Total time used for processing = 0.0 seconds
ARA LTS to minimal AG Converter v1.54 (c) VTT Electronics 1992-94
Memory available: 10000000
Reading file dekker.lts
Lts to Ag start.
Lts to det-Lts in progress...
[...]
474 nodes
666 arcs
Det-Lts to Ag in progress...
Lts to Ag end.
Ag to minimized Ag start.
Initial blocks created
[...]
Ag to minimized Ag end.
Writing file tmp2.ag
Memory available: 10000000
Total time used for processing = 0.0 seconds
ARA AG Comparator v1.54 (c) VTT Electronics 1992-94
tmp1.ag compared to tmp2.ag
Memory available: 10000000
Reading file tmp1.ag
Memory available: 10000000
Reading file tmp2.ag
AGs are equivalent.
End of comparison.
Verifying the progress property that both processes always eventually obtain the resource once they have requested it fails:
maria -p lbt -wb dekker.pn -e 'lsts "dekker.lsts";
[]((wait_set_b_i_1=> <>wait_set_k_1) && (wait_set_b_i_2=><>wait_set_k_2));exit'
"dekker.pn": 474 states, 666 arcs
(command line):1:constructing counterexample
shortest path from @0 to loop (35 nodes):
@0 @2 @4 @7 @10 @14 @19 @24 @31 @38 @47 @57 @71 @83 @101 @113 @131 @142 @158
@168 @180 @192 @205 @218 @234 @251 @267 @284 @299 @314 @327 @339 @351 @358
@351
The error trace was also output in LSTS format, which we converted to a file dekker.pdf using the following commands:
lsts-demangle.pl dekker.lsts-act
lsts2dot dekker.lsts > dekker.dot
dot -Tps dekker.dot > dekker.eps
epstopdf dekker.eps
Before running dot, we slightly edited the GraphViz
input file dekker.dot to divide the error
trace on several lines.
When the property is extended with the fairness assumption that each of the two processes is infinitely often chosen by the scheduler, the property holds:
maria -p lbt -wb dekker.pn -e 'lsts "dekker.lsts";
([](<>scheduler_1 && <>scheduler_2))=>
[]((wait_set_b_i_1=> <>wait_set_k_1) && (wait_set_b_i_2=><>wait_set_k_2));exit'
"dekker.pn": 474 states, 666 arcs
(command line):1:property holds