[ 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-mcrl2(1) - generate a torx primer for mcrl2 using mcrl2

Table of Contents

Name

mkprimer-mcrl2 - generate a torx primer for mcrl2 using mcrl2

Synopsis

mkprimer [ options ... ] specification.mcrl2

Description

From the specification file mkprimer(1) generates a torx-primer(5) program. In this manual page we describe specific features of primers generated using the mcrl2 toolkit.

When mkprimer(1) is invoked on a specification file with a .mcrl2 suffix, or when the command line option --language MCRL2 is given, the specification file is interpreted as a mCRL2 specification file and translated to a .lpe file which is then accessed using explorer lpe2torx(1) using the `generic' primer(1).

Logfile

A mcrl2 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-mcrl(1) - generate a torx primer for mcrl using mcrl2 and mcrl		Appendix D: TorX Manual Pages: mkprimer-trojka(1) - generate a promela primer for torx using trojka