MONA(1)

💖 MONA(1) 💖

okay bestie, sit down, hydrate, because we're about to talk about mona — a decision procedure for the logics WS1S and WS2S. yes it's giving very much "niche academic flex" and yes I'm obsessed 🫶

---

✨ NAME ✨

mona — a decision procedure for the logics WS1S and WS2S 💅

---

🌸 SYNOPSIS 🌸

mona [ options ] mona-file

that's it. that's the whole vibe. options in, file in, magic out ✨

---

🦋 DESCRIPTION 🦋

MONA is a tool that translates formulas in the logics WS1S or WS2S into finite-state automata represented by BDDs. like, it takes your fancy logic formula and turns it into automata. no cap. 🎀

the formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc. so basically whatever you're trying to say, if it fits in WS1S or WS2S, MONA's got you 💖

MONA also analyses the automaton resulting from the compilation, and determines whether the formula is valid and, if the formula is not valid, generates a counter-example. so she doesn't just build the thing, she reads the thing and tells you if it's true. main character energy fr fr 👑

The MONA project is a research project at Department of Computer Science, Aarhus University. 🏛️

Full documentation, GPL source code, and related research papers are available from the MONA project home page at http://www.brics.dk/mona — go read, it's iconic 🌈

---

💅 OPTIONS 💅

every single one. I do not skip. we do not skip. periodt.

• -w — Output whole automaton. Default is to only output its size. like, show me the whole thing, not just the measurements 📏
• -n — Don't analyze automaton. Default is to analyze for validity and unsatisfiability and to generate a satisfying example and counter-example. so if you're like "girl just build it, don't judge me", this is your flag 🙈
• -t — Print elapsed time for each phase. If -s is also used, the time for each automaton operation is also printed. clocking the tea ⏱️
• -s — Print statistics. Prints information for each automaton operation and a summary. numbers girlies rise 📊
• -i — Print intermediate automata (implies -s). the behind-the-scenes lore ✨
• -d — Dump AST, symboltable, and code DAG. Useful for debugging. debug girlies, this one's for you 🐛
• -q — Quiet, don't print progress. shy mode 🤫
• -e — Enable separate compilation. (See the MONALIB environment variable below.) ⚙️
• -oN — Code optimization level N (0=none, 1=safe, 2=heuristic) (default 1). glow-up levels, honestly 💖
• -r — Disable BDD index reordering, use order of declaration as index ordering. Default is to reorder BDD indices heuristically. so default = she rearranges, this flag = she does NOT rearrange 🔥
• -f — Force normal tree-mode output style. Only applicable for WSRT mode. 🌳
• -m — Alternative M2L-Str emulation (v1.3 style). throwback era 💀
• -h — Enable inherited acceptance analysis. 🧬
• -u — Unrestrict output automata. Create conventional automata by converting "don't-care" states to "reject" states and minimizes. she's cleaning up the place 🧹
• -gw — Output whole automaton in Graphviz format (implies -n -q). (Graphviz is available at http://www.graphviz.org/) 🎨
• -gs — Output satisfying example tree in Graphviz format (implies -q). 🌲
• -gc — Output counter-example tree in Graphviz format (implies -q). 💀
• -gd — Dump code DAG in Graphviz format (implies -n -q). 🕸️
• -xw — Output whole automaton in external format (implies -n -q). "External format" is the format used by dfalib and gtalib, see the source package. 📦

---

🌈 ENVIRONMENT 🌈

• MONALIB — Defines the directory used for separate-compilation automata (default is current directory). so if you don't set it, she's just hanging out wherever you are 🏠

---

😭 BUGS 😭

Please send bug reports to <amoeller@cs.au.dk> — email the girl, she wants to know 🫶

---

👑 AUTHORS 👑

Anders Moeller, Nils Klarlund, Jacob Elgaard, Theis Rauhe, and Morten Biehl. legends, all of them 💜

---

bestie this is BRICS tools era, dated MARCH 2016, and honestly? she still slays. mwah 💋✨🌸🎀🦋