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  selectively  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  transformation.
       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  arrays)  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 comparisons 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 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>

                                                                                 MURPHI2MURPHI(1)