[ Home | What's New | Contents | Overview | Contributors | Distribution | Examples | Documentation | Manual | Publications | Mailing List Archive | Problems ] This page was last updated by Axel Belinfante on 2006-06-30
TorX Test Tool Information
Prev   Next

mkprimer-ltsa(1) - generate an fsp primer for torx using ltsa

Table of Contents

Name

mkprimer-ltsa - generate an fsp primer for torx using ltsa

Synopsis

mkprimer [ options ... ] specification.lts

Description

When mkprimer(1) is invoked on a specification file with a .lts suffix, or when the --language fsp command line option is given, the specification file is interpreted as an FSP specification file, by the FSP (LTSA) explorer ltsaexp(1), using the `generic' primer(1). From the specification file mkprimer(1) generates a torx-primer(5) program: a shell-script that invokes the primer(1) and via it the LTSA explorer ltsaexp(1). In this manual page we describe specific features of primers generated by ltsa from FSP specifications.

Logfile

An LTSA Primer generates a STATEID torx-log(4) line containing the following whitespace-separated name value pairs:
super nr
where nr is just an integer number representing a superstate state set
init state-list
where state-list is a list of comma-separated state numbers, of the states that are present in the superstate state set, by the last transition done.
trans state-list
is a list of comma-separated state numbers, of the states that are present in the superstate state set, by expansion of the state-list given in the init field.

See Also

torx-intro(1), mkprimer(1), torx-primer(5), torx-adaptor(5), torx-log(4)

Contact

By Email: <torx_support@cs.utwente.nl>

Version

This manual page documents version 3.9.0 of torx.


Table of Contents


Prev Table of Contents Next
Appendix D: TorX Manual Pages: mkprimer-jararaca(1) - generate a torx primer using jararaca Valid HTML 4.01! Appendix D: TorX Manual Pages: mkprimer-mcrl(1) - generate a torx primer for mcrl using mcrl2 and mcrl