MURPHI2SMV(1)

💖 MURPHI2SMV(1) 💖

okay bestie, gather round, because this is the page for murphi2smv — a General Commands Manual classic, and she is so useful. ✨

---

🌸 NAME 🌸

murphi2smv — the lil translator that takes your Murphi model and turns it into SMV. like, it's giving "bilingual icon". 🦋

---

🎀 SYNOPSIS 🎀

murphi2smv [--output FILE | -o FILE] FILE

---

✨ DESCRIPTION ✨

so murphi2smv ships bundled with the model checker Rumur, and what she does is translate a Murphi model into the input format for the NuSMV model checker. 💅

if you want the whole backstory on Rumur or on Murphi itself, go read rumur(1) — she's got the lore. 📖

---

👑 OPTIONS 👑

• --help or -? — shows you the usage info. your lil "what do I even do here" button. 🫶
• --numeric-type [integer | word] or -n [integer | word] — sets the SMV type used for ranges, scalarsets and numeric literals. pick integer to use native integers, or word... no wait, word to use bit-vectors. if you don't pass this at all, one gets chosen automatically based on what's inside your input model. she just knows. 🔮
• --output FILE or -o FILE — tells her where to write the output SMV model. skip it and the output goes to standard out instead. classic. 🌈
• --quiet or -q — shhh. silences warning diagnostics. 🤫
• --verbose or -v — the opposite vibe: reports extra debugging information. she will yap (affectionately). 🗣️
• --version — displays version information and exits. periodt. 👑

---

⚠️ NOTES ⚠️

okay so real talk, bestie, because this part matters. 🚨

Translation to SMV is imprecise, because the semantics of model execution in SMV are significantly different from Murphi. like, different enough that you should not expect murphi2smv to hand you a ready-to-run SMV model. nope!

what she actually gives you is an initial rough translation — a starting point that you will need to edit before it becomes a runnable model. it's giving "first draft energy", not "final submission energy". ✍️

fr fr, do not skip the editing step. 🙈

---

💀 LIMITATIONS 💀

Murphi type declarations have no exact equivalent in SMV. so what happens? they get handled by propagating and expanding them inline. and this is done purely syntactically, which can lead to unexpected or incorrect results if your input model has symbols that shadow other symbols. no cap. 😭

and now, the big list. the following Murphi constructs have no equivalent in SMV and get emitted as a placeholder comment:

• alias declarations
• alias rules
• alias statements
• assume, cover, and liveness properties
• clear statements
• error statements
• exists expressions
• for loops
• forall expressions
• functions, procedures, and calls to these
• if statements
• isundefined statements
• property statements
• quantifiers
• record definitions
• simple rules
• rulesets
• switch statements
• undefine statements
• while statements

so basically you've got two paths, bestie: rephrase your input model to dodge all of these features, or edit the generated SMV after generation. pick your fighter. 🥊

---

Rumur supports integers up to 64-bit in width. SMV integers are only 32-bit. and there are no checks that the numbers or calculations in your input model actually fit in 32-bit. which means... yeah. constants or calculations in the generated SMV may overflow. 💥 be careful out there.

---

Murphi rule-local declarations and variables have no equivalent in SMV either. they get emitted using SMV syntax, but you'll need to move them to a valid location within the SMV output yourself. she did her part, you do yours. 💅

---

🌈 SEE ALSO 🌈

rumur(1)

---

🫶 AUTHOR 🫶

all comments, questions and complaints should be directed to Matthew Fernandez <matthew.fernandez@gmail.com>. 💌

(yes, complaints too. he said it, not me.)

---

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

---

okay that's the whole page, bestie!! 🎀 this was murphi2smv(1) from the General Commands Manual, and that's the whole vibe check. go translate something iconic. mwah. 💖✨👑