Provided by: rumur_2023.05.21-1_amd64 bug

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.

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)