Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
RUMUR(1)		    General Commands Manual		      RUMUR(1)

       rumur - Yet another explicit state model	checker

       rumur options --output FILE [FILE]

       Rumur  is a reimplementation of the model checker CMurphi with improved
       performance and a slightly different feature set.

       --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 en-
	      tire 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  transi-
	      tion  out	 of  a	state and raise	an error in this scenario. The
	      possible modes for this check are:

		     o off No deadlock checks are performed.

		     o stuck A deadlock	is reached when	arriving  at  a	 state
		       from which there	are no enabled transitions, and	an er-
		       ror is signaled in this case.

		     o stuttering A deadlock is	reached	in  the	 same  circum-
		       stances	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 sce-
		       nario 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

       --debug or -d
	      Enable  debugging	 options  in  the generated verifier. This in-
	      cludes enabling runtime assertions. This will also output	debug-
	      ging messages while generating the verifier.

	      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 er-
	      ror is encountered.  However, you	may wish to set	a higher value
	      to get multiple error traces from	a single run.

	      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 cur-
	      rent 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 ex-
	      pense of runtime.	That is, by default the	verifier will  try  to
	      minimise memory usage. If	your model is small enough to comfort-
	      ably 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.

       --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 de-
	      bugging purposes.

       --sandbox [on | off]
	      Control whether the generated verifier uses your operating  sys-
	      tem's  sandboxing	 facilities  to	 limit its own operations. The
	      verifier does not	intentionally perform any malicious or danger-
	      ous operations, but at the end of	the day	it is a	generated pro-
	      gram that	you are	going to execute. To safeguard against	a  bug
	      in the code generator, it	is recommended to constrain the	opera-
	      tions 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 val-
	      ues 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 iden-
	      tity  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	 intu-
	      itive  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 configu-
	      ration, 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 run-

       --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:

		     o off Do not use symmetry reduction. All scalarsets  will
		       be treated as if	they were range	types.

		     o 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  em-
		       pirically.  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.

		     o exhaustive Use a	symmetry reduction algorithm based  on
		       exhaustive permutation of the state data. This is guar-
		       anteed 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  ex-
		       pense 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 plat-
	      form 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:

		     o handle_reads Reads from variable	handles

		     o handle_writes Writes to variable	handles

		     o memory_usage Summary of memory allocation during	check-

		     o queue Events relating to	the pending state queue

		     o set Events relating to the seen state set

		     o symmetry_reduction  Events  related to the symmetry re-
		       duction optimisation

		     o 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	debug-
	      ging purposes.

       --value-type TYPE
	      Change  the C type used to represent scalar values in the	gener-
	      ated 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.

	      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 fol-
       lowing 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 de-
       scribed below to	instruct Rumur how to use them.	Note  that  Rumur  can
       only  use a single SMT solver and specifying the	--smt-path option mul-
       tiple 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 or-
	      der  listed.  E.g.  if  you  specify  --smt-arg=--tlimit	--smt-
	      arg=5000	the  solver will be called with	the command line argu-
	      ments --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  sup-
	      ported  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	execu-
	      tions. 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 environ-
	      ment'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-sim-
	      plification 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

       --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

       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  in-
	      stead. For example, --smt-prelude	AUFLIA.

       All  comments,  questions  and complaints should	be directed to Matthew
       Fernandez <>.

       This is free and	unencumbered software released into the	public domain.

       Anyone is free to copy, modify, publish,	use, compile,  sell,  or  dis-
       tribute	this software, either in source	code form or as	a compiled bi-
       nary, 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 soft-
       ware 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  per-
       petuity	of  all	present	and future rights to this software under copy-
       right law.


       For more	information, please refer to <>



Want to link to this manual page? Use this URL:

home | help