SYNOPSIS

pins-open model.type [cc_options] app[.a|.c|.o] [app_options]

pins-open [OPTION]…

DESCRIPTION

pins-open provides the OPEN/CAESAR interface for state space generators which themselves provide a LTSmin PINS interface. Supporting PINS libraries which correspond to the type of model are linked to an OPEN/CAESAR application app[.a|.c|.o]. The resulting executable app is then executed.

pins-open follows the OPEN/CAESAR command line conventions.

OPTIONS

--version

Print version information of this tool.

-h, --help

Print help text.

EXAMPLES

Run the declarator test application (provided by CADP) with the mcrl(1) specification brp.tbf:

{manname} brp.tbf declarator

Output:

{manname}: running ``declarator'' for ``brp.tbf''

*** checking compatibility of ``./declarator''

declarator: loading model from brp.tbf
MCRL grey box: Start compiling ...
MCRL grey box: .... end compiling.
declarator: hiding the state.
declarator: creating a new string index
declarator: creating a new string index
declarator: model brp.tbf loaded
declarator: length is 21, there are 45 groups
declarator: There are 0 state labels and 1 edge labels
declarator: CAESAR_HINT_SIZE_STATE=84 CAESAR_HINT_SIZE_LABEL=4
*** general parameters

[...]

*** state #1

CAESAR_COPY_STATE : OK
CAESAR_COMPARE_STATE : OK

[...]

SEE ALSO

ltsmin(7), caesar.open(l), mcrl(1), CADP