[ 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

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.

Contact

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

Version

This manual page documents version 3.9.0 of torx.

Table of Contents

Name
Synopsis
Description
Logfile
See Also
Contact
Version

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