LPSCONSTELM(1)

πŸ“¦ version 202507, in nixos 26.05, nixpkgs unstable

πŸ’– NAME πŸ’–

Hey bestie! This is lpsconstelm, aka the LPSCONSTELM(1) manual page, from section 1 (User Commands). Its whole thing is that it removes constant parameters from an LPS. That’s the lewk. πŸ’…

✨ SYNOPSIS ✨

lpsconstelm [OPTION]... [INFILE [OUTFILE]]

πŸ¦‹ DESCRIPTION πŸ¦‹

Okay so here’s the vibe: lpsconstelm removes constant process parameters from the LPS in INFILE and writes the result to OUTFILE. If INFILE is not present, standard input is used. If OUTFILE is not present, standard output is used. Flexible icon behavior, honestly. πŸ’–

πŸŽ€ OPTIONS πŸŽ€

OPTION can be any of the following:

  • -c, --ignore-conditions β€” ignore conditions by assuming they evaluate to true.
  • -f, --instantiate-free-variables β€” allow free variables to be instantiated as a side effect of the algorithm. ⚠️ Heads up, bestie: this functionality is untested!
  • -QNUM, --qlimit=NUM β€” limit enumeration of universal and existential quantifiers in data expressions to NUM iterations. Default is NUM=10; NUM=0 means unlimited. πŸŒ€
  • -s, --remove-singleton-sorts β€” remove parameters with single element sorts.
  • -t, --remove-trivial-summands β€” remove summands with condition false.
  • -rNAME, --rewriter=NAME β€” use rewrite strategy NAME: 'jitty' = jitty rewriting (the default), 'jittyc' = compiled jitty rewriting, 'jittyp' = jitty rewriting with prover.
  • --timings[=FILE] β€” append timing measurements to FILE. If no FILE is provided, measurements are written to standard error.

🌈 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; LEVEL is 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.

πŸ‘‘ AUTHOR πŸ‘‘

Written by Wieger Wesselink; Frank Stappers. Iconic duo, fr fr. 🫢

πŸ’€ REPORTING BUGS πŸ’€

Report bugs at <http://www.mcrl2.org/issuetracker>. Please do, bestieβ€”bugs are not the vibe. 😭

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. ⚠️

πŸ”­ SEE ALSO πŸ”­

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/lpsconstelm.html>. Go read it, iykyk. 🌟


πŸ’– Cute lil sign-off: this page is for lpsconstelm from the mCRL2 toolset 2025..., dated October 2026. Mwah! πŸ’…

πŸ“¦ where this page comes from