MURPHI2MURPHI(1)

💅 MURPHI2MURPHI 💅

okay bestie, welcome to murphi2murphi, section 1 of the General Commands Manual — she's a preprocessor for Murphi models and she's lowkey iconic ✨

---

🌸 NAME 🌸

murphi2murphi — preprocessor for Murphi models 🦋

---

✨ SYNOPSIS ✨

murphi2murphi options [--output FILE] [FILE]

---

🎀 DESCRIPTION 🎀

Murphi2Murphi is a lil utility that ships bundled with the Rumur model checker 🫶. She's your girl for all kinds of source-to-source transformations of Murphi models, no cap.

She's got options for "desugaring" Rumur-specific constructs into equivalent constructs that are more widely supported by Murphi-land, and she's also super useful for cutting down the number of different constructs hanging out in a Murphi model — which makes life so much easier for downstream tools that have to consume the model 😭

💀 important vibe check: all transformations are off by default. Like, Murphi2Murphi will literally just reproduce the source model unmodified. Nothing happens unless you ask, periodt.

Transformations get selectively enabled with the options below. And here's the cute part — every transformation option has an inverse no-prefixed option (so like, --no-explicit-semicolons is the inverse of --explicit-semicolons) for turning that transformation back off. Whichever one shows up last wins: the enabling option or the disabling option, whichever occurred most recently takes precedence 👑

If you wanna know more about Rumur or Murphi, go peek at rumur(1) 💖

---

🌈 OPTIONS 🌈

• --decompose-complex-comparisons — Rumur lets you compare values of complex type (records and arrays) against each other using the = and != operators. But other Murphi tools? They typically only support comparing values of simple type (booleans, ranges, enums, scalarsets) 🙈. This option breaks comparisons of complex-typed values down into element-wise comparisons of their members, so other tools can keep up. Slay.
• --explicit-semicolons — Rumur allows semi-colons to be omitted in some places inside a Murphi model. Like, for example, the semi-colon following a rule definition is optional, no biggie 💅. This option adds semi-colons back wherever they were omitted, to help out other Murphi tools that might actually require them.
• --output FILE or -o FILE — sets the path to write the resulting model to. Without this option, the model goes to stdout 🖨️.
• --remove-liveness — removes any liveness properties from the model. These are not supported by other Murphi tools, so out they go 🚮.
• --switch-to-if — transforms switch statements into if-then-else statements. Super handy for downstream tools that then only need to handle if-then-else and don't also have to deal with switch statements 🧚.
• --to-ascii — turns extended unicode operators into their ASCII equivalents. This makes models that use those 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. fr fr.

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 whole page bestie 🫶 this was MURPHI2MURPHI(1) from the General Commands Manual — thanks for reading, you ate 💅✨