--boundSTEPS
Set a limit for state space exploration. The verifier will stop checking beyond this depth. A
bound of 0, the default, indicates unlimited exploration. That is, the verifier will not stop
checking until it has expanded all seen states.
--colour [auto | off | on]
Enable or disable the use of ANSI colour codes in the verifier's output. The default is auto, to
auto-detect based on whether the verifier's stdout is a TTY.
--counterexample-trace [diff | full | off]
Set how counterexample traces are printed when an error is found during checking. diff, the
default, prints each state showing only the differences from the previous state. full shows the
entire contents of each state. off disables counterexample trace printing altogether.
--deadlock-detection [off | stuck | stuttering]
Enable or disable deadlock detection. Rumur has the ability to generate a verifier that notices
when there is no valid transition out of a state and raise an error in this scenario. The possible
modes for this check are:
• off No deadlock checks are performed.
• stuck A deadlock is reached when arriving at a state from which there are no enabled
transitions, and an error is signaled in this case.
• stuttering A deadlock is reached in the same circumstances as for the stuck option or
additionally if there are enabled transitions but these all result in an identical state.
For CMurphi users, this is the scenario that CMurphi considers to be a deadlock.
This defaults to stuttering. However, whether such a deadlock actually represents a problem
depends on the properties of the system you are modelling. Hence you may want to change deadlock
detection.
--debug or -d
Enable debugging options in the generated verifier. This includes enabling runtime assertions.
This will also output debugging messages while generating the verifier.
--help
Display this information.
--max-errorsCOUNT
Number of errors the verifier should report before considering them fatal. By default this is 1,
that is exit as soon as an error is encountered. However, you may wish to set a higher value to
get multiple error traces from a single run.
--monopolise
Assume that the machine the generated verifier will run on is the current host and that it will be
the only process running. This flag causes the verifier to upfront allocate a seen set that will
eventually occupy all of memory. That is, it is the same as passing --set-expand-threshold100 and
--set-capacity with the total amount of physical memory available on the current machine.
--outputFILE or -oFILE
Set path to write the generated C verifier's code to.
--output-format [machine-readable | human-readable]
Change the format in which the verifier displays its output. By default, it uses human-readable
which results in progress output and then a final summary of the result. Using machine-readable
generates output in an XML format suitable for consumption by a following tool in an I/O pipeline.
--pack-state [on | off]
Set whether auxiliary state data is compressed in the generated verifier. Compression (on, the
default) saves memory at the expense of runtime. That is, by default the verifier will try to
minimise memory usage. If your model is small enough to comfortably fit in available memory, you
may want to set this to off to accelerate the checking process.
--pointer-bits[auto | BITS]
Number of relevant (non-zero) bits in a pointer on the target platform on which the verifier will
be compiled. This option can be used to tune pointer compression, which can save memory when
checking larger models. With the default, auto, 5-level paging is assumed for x86-64, meaning
pointers can be compressed and stored in 56 bits. Other platforms currently have no auto-
detection, and will store pointers uncompressed at their full width. If you know a certain number
of high bits of pointers on your target platform are always zero, you can teach Rumur this
information with this option. For example, if you are compiling on an x86-64 platform that you
know is using 4-level paging you can pass --pointer-bits48 to tell Rumur that the upper 16 bits
of a pointer will always be zero.
--quiet or -q
Don't output any messages while generating the verifier.
--reorder-fields [on | off]
Control whether access to state variables and record fields is optimised by reordering them. By
default this is on, causing the order of a model's state variables and fields within record types
to be optimised to more likely result in naturally aligned memory accesses, which are assumed to
be faster. You should never normally have cause to turn this off, but this feature was buggy when
first implemented so this option is provided for debugging purposes.
--sandbox [on | off]
Control whether the generated verifier uses your operating system's sandboxing facilities to limit
its own operations. The verifier does not intentionally perform any malicious or dangerous
operations, but at the end of the day it is a generated program that you are going to execute. To
safeguard against a bug in the code generator, it is recommended to constrain the operations the
verifier is allowed to perform if you are using a model you did not write yourself. By default
this is off.
--scalarset-schedules [on | off]
Enable or disable tracking of the permutation of scalarset values for more comprehensible
counterexample traces. The permuting of scalarset values that is performed during symmetry
reduction leads to paths in the state space where a single scalarset identity does not have the
same value throughout the trace. When this option is on (the default), Rumur tracks these
permutations and takes them into account when printing scalarset values or reconstructing
counterexample traces. The result is more intuitive and easily understandable traces. Turning this
off may gain runtime performance on models that use scalarsets. However counterexample traces will
likely be confusing in this configuration, as scalarset variables will appear to have their values
change arbitrarily.
--set-capacitySIZE or -sSIZE
The size of the initial set to allocate for storing seen states. This is given in bytes and is
interpreted to mean the desired size of the set when it is completely full. That is, the initial
allocation performed will be for a number of "state slots" that, when all occupied, will consume
this much memory. Default value for this 8MB.
--set-expand-thresholdPERCENT or -ePERCENT
Expand the state set when its occupancy exceeds this percentage. Default is 75, valid values are 1
- 100. Setting a value of 100 will result in the set only expanding when completely full. This may
sound ideal, but will actually result in a much longer runtime.
--symmetry-reduction [off | heuristic | exhaustive]
Enable or disable symmetry reduction. Symmetry reduction is an optimisation that decreases the
state space that must be searched by deriving a canonical representation of each state. While two
states may not be directly equal, if their canonical representations are the same only one of them
need be expanded. To take advantage of this optimisation you must be using named scalarset types.
The available options are:
• off Do not use symmetry reduction. All scalarsets will be treated as if they were range
types.
• heuristic Use a symmetry reduction algorithm based on sorting the state data. This is not
guaranteed to find a single, canonical representation for each equivalent state, but it
is fast and performs reasonably well empirically. Using this option, you may explore more
states than you need to, with the advantage that you will process each individual state
much faster than with exhaustive. This is the default.
• exhaustive Use a symmetry reduction algorithm based on exhaustive permutation of the
state data. This is guaranteed to find a single, canonical representation for each
equivalent state, but is typically very slow. Use this if you want to minimise memory
usage at the expense of runtime.
--threadsCOUNT or -tCOUNT
Specify the number of threads the verifier should use. If you do not specify this parameter or
pass 0, the number of threads will be chosen based on the available hardware threads on the
platform on which you generate the model.
--traceCATEGORY
Enable tracing of specific events while checking. This option is for debugging Rumur itself, and
lets you generate a verifier that writes events to stderr. Available event categories are:
• handle_reads Reads from variable handles
• handle_writes Writes to variable handles
• memory_usage Summary of memory allocation during checking
• queue Events relating to the pending state queue
• set Events relating to the seen state set
• symmetry_reduction Events related to the symmetry reduction optimisation
• all Enable all of the above
More than one of these can be enabled at once by passing the --trace argument multiple times. Note
that enabling tracing will significantly slow the verifier and is only intended for debugging
purposes.
--value-typeTYPE
Change the C type used to represent scalar values in the generated verifier. Valid values are
auto and the C fixed-width types, int8_t, uint8_t, int16_t, uint16_t, int32_t, uint32_t, int64_t,
and uint64_t. The type you select is mapped to its fast equivalent (e.g. int_fast8_t) and then
used in the verifier. The default is auto that selects the narrowest type that can contain all the
scalar types in use in your model. It is possible that your model does some arithmetic that
temporarily exceeds the bound of any declared type in your model, in which case you will need to
use this option to select a wider type. However, this is not a common case.
--verbose or -v
Output informational messages while generating the verifier.
--version
Display version information and exit.
Install Now
PNG Icons
