mkprimer-cadp(1) - generate a torx primer for lotos, bcg, fc2 or aut using

Name

Synopsis

Description

When mkprimer(1) is invoked on a specification file with a .lot, .bcg, or .fc2 suffix, or when the command line option --language LOTOS, --language BCG, or --language FC2 is given, the specification file is interpreted as a LOTOS, BCG resp. FC2 specification file, adapted for use with TorX and CADP. The command line option --language AUT-CADP can be given to generate a CADP primer for Aldebaran (.aut) files -- by default, when given a file with a .aut suffix mkprimer(1) generates a primer using autexp(1).

Logfile

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. In the state-list, monotonic increasing sequences of the form m,m+1,...,n are abbreviated as m-n

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. In the state-list, monotonic increasing sequences of the form m,m+1,...,n are abbreviated as m-n

The STATS torx-log(4) line generated by a CADP Primer consists of a number of whitespace separated ``name value'' tuples.

#statesini nr

number of states in stateset (representing current state) reached by direct action (``visible'' transition) from the last menu, before expanding (by following internal steps)

#statesall nr

number of states in stateset (representing current state), reached by direct action from the last menu, after expanding (by following internal steps)

#statesexp nr

number of states added during expansion (by following internal steps)

#statesmaxrun nr

maximum number of states reported in #statesall during this test run

#statesmatchini nr

number of states matched from the states in #statesini

#statesmatchexp nr

number of states matched during expansion (following internal steps)

#statesmatchall nr

number of states matched from those in #statesall

#sinkstates nr

number of sink states (without outgoing edges)

#events nr

number of different actions possible (after expansion)

#eventsmax nr

max number of different actions possible in individual state

#eventsexp nr

number of different actions encountered during analysis of the states in the stateset

See Also

Contact

Version

Table of Contents

• Name
• Synopsis
• Description
• Logfile
• See Also
• Contact
• Version

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