MURPHI2UCLID(1)

💖 murphi2uclid(1) 💖

okay so bestie, this is a page straight out of the General Commands Manual — section 1, the commands section, the iconic one — and it's all about a little tool called murphi2uclid. sit down, grab a strawberry, we're doing a whole translation vibe today 🍓

---

🌸 NAME 🌸

murphi2uclid — translate a Murphi model to Uclid5 ✨

---

🎀 SYNOPSIS 🎀

murphi2uclid [--output FILE | -o FILE] FILE

---

💅 DESCRIPTION 💅

so murphi2uclid ships bundled with the model checker Rumur, and its whole job is the glow-up: it takes a Murphi model and translates it into a Uclid5 model 🦋

want the tea on Rumur or on Murphi itself? go read rumur(1), it's all in there.

---

✨ OPTIONS ✨

• --help, -? — shows you the usage info. the "help me help you" button 🫶
• --module NAME, -m NAME — sets the name for the generated Uclid5 module. if you don't pass this, it just defaults to main. no thoughts, head empty, main it is 💀
• --numeric-type TYPER, -n TYPE — sets the Uclid5 type used for ranges, scalarsets and numeric literals. it can be either integer or a bit-vector type, like, for example, bv8 🎀 if you leave this option out entirely, the tool picks either integer or bv64 automatically, based on whatever's inside your input model. it's giving psychic, honestly 🔮
• --output FILE, -o FILE — sets the path where the output Uclid5 model gets written. omit it and the output just goes to standard out, casual 🌈
• --quiet, -q — silences warning diagnostics. shhh, not now 😌
• --verbose, -v — reports extra debugging information. the yapper mode, we love her 🔥
• --version — displays version information and exits. bye bestie 👋

---

🧚 NOTES 🧚

ngl, translation to Uclid5 is imprecise whenever there's no direct Uclid5 equivalent for some Murphi concept. for example: an undefine statement in Murphi has no equivalent in Uclid5, so it gets translated into a havoc statement. and obviously, that is not exactly equivalent 💀

but the hope is that in real world models it achieves a similar effect. namely, any read of an undefined variable makes the verifier explore unintended behavior. so to get reasonable utility out of translating a model that uses undefine, you will likely need an assertion-heavy model. or, put another way: defensive programming is advised. periodt 👑

---

😭 LIMITATIONS 😭

these Murphi concepts have no translation to Uclid5 at all, and murphi2uclid straight up rejects them:

• Aliases, in the form of declaration statements or rules
• The isundefined operator
• The modulo operator, %
• The left and shift shift operators, << and >>
• Early return statements, with or without an expression
• Cover properties
• Liveness properties inside rulesets
• Cover and liveness statements
• A clear statement with a value of complex type as its argument
• Step sizes other than 1 in exists or forall expressions

---

also, heads up: function calls within expressions get translated as if they were calls to uninterpreted functions. Uclid5 does not support calling interpreted functions — procedures, in Uclid5 terminology — that way 🙈 the desirable mapping (uninterpreted function vs rephrasing the call site) cannot be determined automatically. so it's left to you, the user, to tweak or post-process the output, because Uclid5 will not accept it as-is. no cap.

---

🫶 SEE ALSO 🫶

rumur(1)

---

💌 AUTHOR 💌

all comments, questions and complaints should be directed to Matthew Fernandez <matthew.fernandez@gmail.com> — he's the main character here 👑

---

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

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. they make this dedication for the benefit of the public at large and to the detriment of their heirs and successors. they intend this dedication to be an overt act of relinquishment in perpetuity of all present and future rights to this software under copyright law. iconic behavior, honestly 💅

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 murphi2uclid(1) from the General Commands Manual — that's the manual name, that's the section, that's the whole footer energy right there. stay translated, stay iconic 💖✨