FreeBSD Manual Pages
RUMUR(1) General Commands Manual RUMUR(1) 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 per- formance 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 un- limited 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 con- tents of each state. off disables counterexample trace printing al- together. --deadlock-detection [off | stuck | stuttering] Enable or disable deadlock detection. Rumur has the ability to gen- erate 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 en- abled 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 actu- ally 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 mes- sages 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 en- countered. However, you may wish to set a higher value to get mul- tiple 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 eventu- ally 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 de- fault, 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 ver- ifier. Compression (on, the default) saves memory at the expense of runtime. That is, by default the verifier will try to minimise mem- ory 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 plat- form 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 ex- ample, 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 opti- mised 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 ac- cesses, 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 de- fault 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 coun- terexample traces. The result is more intuitive and easily under- standable 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 alloca- tion 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. De- fault 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 opti- misation that decreases the state space that must be searched by de- riving 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 sort- ing the state data. This is not guaranteed to find a sin- gle, 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 in- dividual state much faster than with exhaustive. This is the default. * exhaustive Use a symmetry reduction algorithm based on ex- haustive permutation of the state data. This is guaranteed to find a single, canonical representation for each equiva- lent 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 cho- sen 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 signifi- cantly slow the verifier and is only intended for debugging pur- poses. --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 arith- metic 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 func- tionality 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 ar- gument 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. AUTHOR All comments, questions and complaints should be directed to Matthew Fer- nandez <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 ded- ication 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 CON- NECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. For more information, please refer to <http://unlicense.org> RUMUR(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SMT OPTIONS | AUTHOR | LICENSE
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=rumur&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>