LPSINVELM(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 lpsinvelm — check invariants & simplify summands of an LPS ✨

okay so this is the lpsinvelm page from the User Commands corner of the mCRL2 toolset manual, section 1, and bestie it's literally about proving your LPS behaves itself 🎀

🦋 NAME

lpsinvelm — check invariants and use these to simplify or eliminate summands of an LPS. that's the whole vibe, no cap 💖

🌸 SYNOPSIS

lpsinvelm [OPTION]... --invfile=INVFILE [INFILE [OUTFILE]]

like, options first, then the invariant file is basically mandatory, and then INFILE and OUTFILE are optional besties 🫶

✨ DESCRIPTION ✨

So what it does is: it checks whether the boolean formula (an mCRL2 data expression of sort Bool) that you handed over as your invariant is actually, truly an invariant of the linear process specification (LPS) sitting in INFILE. vibe check passed or failed, we'll find out 🔥

If it is an invariant, the tool eliminates all summands of the LPS whose condition violates the invariant, and writes the result to OUTFILE. slay 💅

  • if INFILE is present… wait, no, careful: if INFILE is not present, stdin is used 🍓
  • if OUTFILE is not present, stdout is used 🌈

Also! the tool can be used to simplify the conditions of the summands of the given LPS. so it's not just a bouncer, it's also a glow-up artist ✨

👑 OPTIONS 👑

OPTION can be any of the following, and yes we're listing every single one because we don't skip 💜

  • -y, --all-violations — don't terminate as soon as a single violation of the invariant is found; instead, report all violations. the completionist option, we love her 🙈
  • -c, --counter-example — display a valuation indicating why the invariant could possibly be violated, for when it's uncertain whether a summand violates the invariant. receipts, basically 🧾
  • -o, --induction — apply induction on lists. lists get the induction treatment, periodt 🎀
  • -iINVFILE, --invariant=INVFILE — use the boolean formula (an mCRL2 data expression of sort Bool) in INVFILE as the invariant. note the short form is glued right onto the value: -iINVFILE 💖
  • -n, --no-check — do not check if the invariant holds before applying the invariant. living dangerously, honestly 💀
  • -e, --no-elimination — do not eliminate or simplify summands, but add the invariant to each condition. this implies setting the flag --simplify-all. iykyk ⭐
  • -pPREFIX, --print-dot=PREFIX — save a .dot file of the resulting BDD if it's impossible to determine whether a summand violates the invariant; PREFIX will be used as prefix of the output files 🦋
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited). yes, zero means unlimited, not zero, iconic 🌸
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME: 'jitty' jitty rewriting (default), 'jittyc' compiled jitty rewriting. pick your fighter 💅
  • -l, --simplify-all — simplify the conditions of all summands, instead of just eliminating the summands whose conditions in conjunction with the invariant are contradictions ✨
  • -zSOLVER, --smt-solver=SOLVER — use SOLVER to remove inconsistent paths from the internally used BDDs (by default, no path elimination is applied): 'cvc' the SMT solver CVC3, 'z3' the SMT solver Z3 🔥
  • -tLIMIT, --time-limit=LIMIT — spend at most LIMIT seconds on proving a single formula. time is a social construct but LIMIT is real 🕐
  • --timings[=FILE] — append timing measurements to FILE. measurements are written to standard error if no FILE is provided 🎀

💜 Standard options 💜

  • -q, --quiet — do not display warning messages 🤫
  • -v, --verbose — display short log messages 🗣️
  • -d, --debug — display detailed log messages 🔍
  • --log-level=LEVEL — display log messages up to and including level; either warn, verbose, debug or trace 👑
  • -h, --help — display help information 🫶
  • --version — display version information ⭐
  • --help-all — display help information, including hidden and experimental options. the secret menu 🌈

🧚 AUTHOR

Written by Luc Engelen. give her her flowers 💐

😭 REPORTING BUGS

Report bugs at <http://www.mcrl2.org/issuetracker>. please do, they're not gonna fix themselves, fr fr 🍓

Copyright © 2025 Technische Universiteit Eindhoven.

This is free software. You may redistribute copies of it under the terms of the Boost Software License <http://www.boost.org/LICENSE_1_0.txt>. There is NO WARRANTY, to the extent permitted by law. like, none. zero. don't come for them 💀

⭐ SEE ALSO

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/lpsinvelm.html>. go read it bestie, it's giving documentation 💖

ngl this one's from the mCRL2 toolset, version string 202507..., dated October 2026, and it lives in section 1 of the manual under LPSINVELM(1). that's the whole page, mwah 💋✨
📦 where this page comes from