Running rbsc¶

Basic usage¶

rbsc can be run from the command line and must be invoked with the path to a role-based model file:

rbsc my_model.rbl

The model will then be translated into a standard PRISM model. By default, the PRISM file will be written to out.prism. The -o option can be used to specify a different path:

rbsc my_model.rbl -o my_model.prism

If the model defines more than one system instance, one PRISM file for each instance is generated and an index is added to each output file. For instance, if my_model.rbl defines two system instances, the command shown above will generate the files my_model_0.prism and my_model_1.prism.

Options¶

rbsc provides a number of command line options listed below.

-m or --multi-actions

Translates the model into a PRISM model with multi-actions.

-c or --const

Defines the value of a constant defined in the model, for example:

rbsc my_model.rbl -c x=2

Multiple constant value can be specified by repeating the -c option:

rbsc my_model.rbl -c x=2 -c y=5

Any valid RBL expression can be specified after the = sign. However, it may be necessary to quote the expression, since some of the contained symbols may have a special meaning in the shell:

rbsc my_model.rbl -c 'x=[5*y, z+2]'

--export-systems <FILE>

Exports the completed system definition to the given file. If multiple systems have been instantiated, an index is added to the file name automatically.

--export-diagrams <FILE>

Exports a diagram that shows all component instances defined in the model, with arrows for the role bindings. Roles belonging to a compartment are drawn in the same box as the compartment. The diagram is exported in the Graphviz DOT format. If multiple systems have been instantiated, an index is added to the file name automatically.

--print-consts

Prints out the values of all constants defined in the model.

--recursion-depth <INT>

Sets the maximum number of recursive calls when evaluating functions. The default limit is 100.

--page-width <INT>

Sets the number of columns that is used for pretty printing the PRISM model. The pretty printer will try to stay below the specified page width by inserting newlines into the source code. The default is 120.

--no-color

Disables the use of color in error messages and warnings.

--no-warn

Silences all warnings.

--warn-no-sync

Shows a warning for all actions in the model that are only used in a single module, i.e., actions that never synchronize.

-v or --verbose

Enables verbose output.