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

FreeBSD Manual Pages

  
 
  

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

NAME
       murphi2murphi - preprocessor for	Murphi models

SYNOPSIS
       murphi2murphi options [--output FILE] [FILE]

DESCRIPTION
       Murphi2Murphi is	a utility bundled with the Rumur model checker.	It can
       be used for various source-to-source transformations of Murphi  models.
       It  supports  options  for  "desugaring"	Rumur-specific constructs into
       equivalent, more	widely supported Murphi	constructs. It is also	useful
       for reducing the	number of different constructs that appear in a	Murphi
       model, to simplify the job of downstream	model-consuming	tools.

       All transformations are off by default. I.e. Murphi2Murphi will	simply
       reproduce  the  source  model unmodified. Transformations can be	selec-
       tively enabled using the	options	described below.  Each	transformation
       option  below  has  an  inverse no-prefixed option (e.g.	--no-explicit-
       semicolons for --explicit-semicolons) for  disabling  that  transforma-
       tion.  Whichever	 occurs	last, the enabling option for a	transformation
       or the disabling	option for a transformation, will take precedence.

       See rumur(1) for	more information about Rumur or	Murphi.

OPTIONS
       --decompose-complex-comparisons
	      Rumur supports comparing values of complex type (records and ar-
	      rays) with each other using the =	and != operators. Other	Murphi
	      tools typically only support the comparison of values of	simple
	      type  (booleans,	ranges,	enums, scalarsets). This option	breaks
	      comparisons of complex typed values  into	 element-wise  compar-
	      isons of their members, for compatibility	with other tools.

       --explicit-semicolons
	      Rumur  allows  semi-colons to be omitted in some places within a
	      Murphi model.  E.g. the semi-colon following a  rule  definition
	      is  optional.  This option adds semi-colons where	they have been
	      omitted, to aid other Murphi tools that may require them.

       --output	FILE or	-o FILE
	      Set path to write	the resulting model to.	Without	 this  option,
	      the model	is written to stdout.

       --remove-liveness
	      Remove  any  liveness  properties	 from the model. These are not
	      supported	by other Murphi	tools.

       --switch-to-if
	      Transform	switch statements into if-then-else  statements.  This
	      can be useful for	downstream tools that then only	need to	handle
	      if-then-else statements, and not also switch statements.

       --to-ascii
	      Turn extended unicode operators into  their  ASCII  equivalents.
	      This  makes models that use these	extended characters compatible
	      with other Murphi	tools.

       --version
	      Display version information and exit.

SEE ALSO
       rumur(1)

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

       THE SOFTWARE IS PROVIDED	"AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
       OR IMPLIED, INCLUDING  BUT  NOT	LIMITED	 TO  THE  WARRANTIES  OF  MER-
       CHANTABILITY, 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>

							      MURPHI2MURPHI(1)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO | AUTHOR | LICENSE

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=murphi2murphi&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help