Provided by: rumur_2020.12.20-1_amd64 
NAME
rumur - Yet another explicit state model checker
SYNOPSIS
rumur options --output FILE [FILE]
DESCRIPTION
Rumur is a reimplementation of the model checker CMurphi with improved performance and a slightly
different feature set.
OPTIONS
--bound STEPS
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-errors COUNT
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-threshold 100 and
--set-capacity with the total amount of physical memory available on the current machine.
--output FILE or -o FILE
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-bits 48 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-capacity SIZE or -s SIZE
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-threshold PERCENT or -e PERCENT
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.
--threads COUNT or -t COUNT
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.
--trace CATEGORY
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-type TYPE
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.
SMT OPTIONS
If you have a Satisfiability Modulo Theories (SMT) solver installed, Rumur can use it to optimise your
model while generating a verifier. This functionality is not enabled by default, but you can use the
following options to configure Rumur to find and use your SMT solver. Some examples of solver
configuration:
# for Z3 with a 5 second timeout
rumur --smt-path z3 --smt-arg=-smt2 --smt-arg=-in --smt-arg=-t:5000 ...
# for CVC4 with a 5 second timeout
rumur --smt-path cvc4 --smt-prelude "(set-logic AUFLIA)" --smt-arg=--lang=smt2 --smt-
arg=--rewrite-divk --smt-arg=--tlimit=5000 ...
For other solvers, consult their manpages or documentation to determine what command line parameters they
accept. Then use the options described below to instruct Rumur how to use them. Note that Rumur can only
use a single SMT solver and specifying the --smt-path option multiple times will only retain the last
path given.
--smt-arg ARG
A command line argument to pass to the SMT solver. This option can be given multiple times and
arguments are passed in the order listed. E.g. if you specify --smt-arg=--tlimit --smt-arg=5000
the solver will be called with the command line arguments --tlimit 5000.
--smt-bitvectors [off | on]
Select whether simple types (enums, ranges, and scalarsets) are translated to bitvectors or
unbounded integers when passed to the solver. By default, unbounded integers are used (--smt-
bitvectors off). If you turn this option on, 64-bit vectors are used instead. Whether integers,
bitvectors, or both are supported will depend on your solver as well as the SMT logic you are
using.
--smt-budget MILLISECONDS
Total time allotted for running the SMT solver. That is, the time the solver will be allowed to
run for over multiple executions. This defaults to 30000, 30 seconds. So if the solver runs for 10
seconds the first time it is called, then 5 seconds the second time it is called, then 20 seconds
the third time it is called, it will not be called again. Note that Rumur trusts the SMT solver to
limit itself to a reasonable timeout per run, so its final run can exceed the budget. You may want
to use the --smt-arg option to pass the SMT solver a timeout limit if it supports one.
--smt-path PATH
Command or path to the SMT solver. This will use your environment's PATH variable, so if the
solver is in one of your system directories you can simply provide the name of its binary. Note
that this option has no effect unless you also pass --smt-simplification on.
--smt-prelude TEXT
Text to emit when communicating with the solver prior to sending the actual problem itself. You
can use this to set a solver logic or other options. This option can be given multiple times and
each argument will be passed to the solver on a separate line.
--smt-simplification [off | on]
Disable or enable using the SMT solver to simplify the input model. By default, this is automatic,
in that it is turned on if you use any of the other SMT options or off if you do not use them.
LEGACY OPTIONS
The following options should no longer be used but are documented here for completeness.
--smt-logic LOGIC
Set the target logic used for communication with the SMT solver. This option is deprecated and you
should use --smt-prelude instead. For example, --smt-prelude AUFLIA.
AUTHOR
All comments, questions and complaints should be directed to Matthew Fernandez
<matthew.fernandez@gmail.com>.
LICENSE
This is free and unencumbered software released into the public domain.
Anyone is free to copy, modify, publish, use, compile, sell, or distribute this software, either in
source code form or as a compiled binary, for any purpose, commercial or non-commercial, and by any
means.
In jurisdictions that recognize copyright laws, the author or authors of this software dedicate any and
all copyright interest in the software to the public domain. We make this dedication for the benefit of
the public at large and to the detriment of our heirs and successors. We intend this dedication to be an
overt act of relinquishment in perpetuity of all present and future rights to this software under
copyright law.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT
LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN
NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF
CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
DEALINGS IN THE SOFTWARE.
For more information, please refer to <http://unlicense.org>
RUMUR(1)