Provided by: rumur_2020.02.17-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.
--quiet or -q
Don't output any messages while generating the verifier.
--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.
--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)