--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.
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.
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>
Visit the GSP FreeBSD Man Page Interface.