RUMUR(1)

📦
version 2025.02.02 · 3 versions
, in debian trixie, ubuntu noble, ubuntu resolute, ubuntu stonking

💖 RUMUR(1) — General Commands Manual 💖

okay bestie, welcome to rumur — literally yet another explicit state model checker ✨ and no, we are not gonna be normal about it.

🌸 NAME 🌸

rumur — yet another explicit state model checker 🦋

✨ SYNOPSIS ✨

rumur options --output FILE [FILE]

like… that's it. that's the whole vibe. options go brrr, --output FILE is mandatory-ish, and [FILE] is the input, sitting there in brackets like it knows something.

💅 DESCRIPTION 💅

So Rumur is a reimplementation of the model checker CMurphi, except it's got improved performance and a slightly different feature set. that's the entire description bestie, we keep it short and iconic here.

👑 OPTIONS 👑

get comfy, there's a lot of them, but honestly each one is lowkey doing something useful so stay with me 💖

  • --bound STEPS — sets a limit for state space exploration. the verifier will stop checking beyond this depth, periodt. a bound of 0 (which is the default, by the way) means unlimited exploration — like, the verifier just won't stop until it's expanded every single state it's ever seen. no cap, it goes until it's done.
  • --colour [auto | off | on] — turns ANSI colour codes in the verifier's output on or off. default is auto, which auto-detects based on whether the verifier's stdout is a TTY 🎀. so like, pipes get no colour, terminals get the whole rainbow.
  • --counterexample-trace [diff | full | off] — decides how counterexample traces get printed when an error shows up during checking:
    • diff — the default! prints each state showing only the differences from the previous state. minimal, clean, slay.
    • full — shows the entire contents of each state. everything. all of it. 🫶
    • off — disables counterexample trace printing altogether. nothing to see here.
  • --deadlock-detection [off | stuck | stuttering] — enables or disables deadlock detection. Rumur can generate a verifier that notices when there's no valid transition out of a state and raises an error in that scenario. the modes are:
    • off — no deadlock checks are performed. we're living dangerously 💀
    • stuck — a deadlock is reached when you arrive 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 stuck, or additionally if there are enabled transitions but they all result in an identical state. for CMurphi users: this is the scenario CMurphi considers to be a deadlock.

This defaults to stuttering. BUT — and this is the important bit — whether such a deadlock actually represents a problem depends on the properties of the system you're modelling. so you might wanna change deadlock detection. your model, your rules ✨

  • --debug or -d — enables debugging options in the generated verifier, which includes enabling runtime assertions. it'll also output debugging messages while generating the verifier. chatty and proud of it.
  • --help — displays this information. hi, that's us. that's this page. 👋
  • --max-errors COUNT — number of errors the verifier should report before considering them fatal. by default this is 1, meaning it exits as soon as an error is encountered. but if you want multiple error traces from a single run, bump it up bestie 💅
  • --monopolise — assumes 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 😭. it's the same as passing --set-expand-threshold 100 and --set-capacity with the total amount of physical memory available on the current machine. greedy. iconic. main character energy.
  • --output FILE or -o FILE — sets the path to write the generated C verifier's code to. this is where the ✨magic✨ lands.
  • --output-format [machine-readable | human-readable] — changes the format the verifier displays its output in. by default it uses human-readable, which gives you progress output and then a final summary of the result. machine-readable instead generates output in an XML format, suitable for consumption by a following tool in an I/O pipeline 🔥.
  • --pack-state [on | off] — sets whether auxiliary state data is compressed in the generated verifier. compression (on, the default) saves memory at the expense of runtime — so by default the verifier tries to minimise memory usage. if your model is small enough to comfortably fit in available memory, you may wanna set this to off to speed up the checking process 🧚.
  • --pointer-bits [auto | BITS] — number of relevant (non-zero) bits in a pointer on the target platform where the verifier will be compiled. you can use this to tune pointer compression, which saves 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 with this option. for example: if you're compiling on an x86-64 platform you know is using 4-level paging, you can pass --pointer-bits 48 to tell Rumur the upper 16 bits of a pointer will always be zero. knowledge is power 💜
  • --quiet or -q — don't output any messages while generating the verifier. silent mode. stealth mode. 🤫
  • --reorder-fields [on | off] — controls whether access to state variables and record fields is optimised by reordering them. by default this is on, which causes 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 exists for debugging purposes. vintage bug energy 🙈
  • --sandbox [on | off] — controls 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's recommended to constrain the operations the verifier is allowed to perform if you're using a model you did not write yourself. by default this is off.
ngl bestie, if you're running someone else's model, turn this on. fr fr.
  • --scalarset-schedules [on | off] — enables or disables tracking of the permutation of scalarset values, for more comprehensible counterexample traces. the permuting of scalarset values 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 it 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. given in bytes, and interpreted to mean the desired size of the set when it's 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 is 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. don't do it unless you love waiting 💀
  • --symmetry-reduction [off | heuristic | exhaustive] — enables or disables 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's fast and performs reasonably well empirically. using this option you may explore more states than you need to, with the advantage that you'll 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 — specifies the number of threads the verifier should use. if you don't 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. parallel girlies rise up 🔥
  • --trace CATEGORY — enables tracing of specific events while checking. this option is for debugging Rumur itself, and lets you generate a verifier that writes events to stderr. the 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: enabling tracing will significantly slow the verifier and is only intended for debugging purposes 🐌

…and that's where part 1 leaves us, bestie. more options are coming in the next part, so don't go anywhere 💖

  • --value-type TYPE — okay so bestie, this one changes 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, which 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. Like, it's yapping but make it useful. ✨
  • --version — display version information and exit. Slay. 👑

✨ 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. 🔮

👑 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>. 🌸

And that's the page, bestie! RUMUR(1) — that's the source and version, and the date is whatever the manpage footer says, but we're not copying the line. It's giving iconic manual energy, periodt. 💅✨

📦 where this page comes from