LPSSUMINST(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 LPSSUMINST — like, the manual page, bestie

okay so this is lpssuminst, a User Commands girlie from the mCRL2 toolset, section 1 of the manual. she instantiates summation variables and she does it flawlessly. no cap.

✨ NAME ✨

lpssuminst — instantiate summation variables of an LPS. that's it, that's the whole job, and she ate 💅

🦋 SYNOPSIS 🦋

lpssuminst [OPTION]... [INFILE [OUTFILE]]

🌸 DESCRIPTION 🌸

so basically? lpssuminst goes and instantiates the summation variables of the linear process specification (LPS) that lives in INFILE, and then writes the result to OUTFILE. iconic behavior honestly.

and like, the inputs are super chill about it:

  • if INFILE isn't there? no problem, stdin is used 🫶
  • if OUTFILE isn't there? also fine, stdout is used ✨

🎀 OPTIONS 🎀

OPTION can be literally any of the following, bestie, take your pick:

  • -f, --finite — only instantiate variables whose sorts are finite. keeps things cute and finite 💖
  • -QNUM, --qlimit=NUM — caps how many iterations we're doing when enumerating universal and existential quantifiers in data expressions. default is NUM=10, and NUM=0 means unlimited (go off, no limits, main character energy 🔥)
  • -rNAME, --rewriter=NAME — picks your rewrite strategy NAME, and your girl has range:
    • 'jitty' — jitty rewriting, the default ⭐
    • 'jittyc' — compiled jitty rewriting
    • 'jittyp' — jitty rewriting with prover
  • -s[NAME], --sorts[=NAME] — select which sorts need to be expanded (it's a comma separated list, iykyk). examples: Bool; Bool, List(Nat)
  • -t, --tau — only instantiate variables in tau summands. tau-only, very exclusive 💅
  • --timings[=FILE] — append timing measurements to FILE. and if you don't give a FILE? the measurements go to standard error instead. she'll tell you how long she took either way 🙈

⭐ Standard options ⭐

like the basic everyday essentials, fr fr:

  • -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; it's 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, lowkey)

👑 AUTHOR 👑

Written by Jeroen Keiren. we stan 💜

😭 REPORTING BUGS 😭

found a bug? don't suffer in silence bestie, report it at <http://www.mcrl2.org/issuetracker>. tell them everything 🫶

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 genuinely none, so don't come for her if something breaks 💀

🧚 SEE ALSO 🧚

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/lpssuminst.html>. it's giving required reading, but make it cute 📖✨

so yeah, that's the whole page 💖 this is lpssuminst from the mCRL2 toolset, version 20250..., dated October 2026, and she's out here serving manual section 1 energy. no cap, periodt. 🎀🦋⭐

📦 where this page comes from