LPSUNTIME(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💖 lpsuntime(1) 💖

okay bestie, welcome to User Commands — this is the lpsuntime(1) page, and she is literally here to remove time from an LPS. no cap. 🕰️✨

🎀 NAME 🎀

lpsuntime — remove time from an LPS. that's the whole assignment. 💅

🌈 SYNOPSIS 🌈

lpsuntime [OPTION]... [INFILE [OUTFILE]]

✨ DESCRIPTION ✨

Remove time from the linear process specification (LPS) in INFILE and write the result to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used. literally that simple, bestie. 🦋

💅 OPTIONS 💅

OPTION can be any of the following:

🫶 lpsuntime options 🫶

  • -e, --eliminate-sumvars — when possible, eliminate summation variables of type Real using the Fourier Motzkin algorithm. This can significantly change the structure of the conditions. iykyk, she can really rearrange the vibe. 😭
  • -i, --invariant — add invariants for parameters of type Real to the output. cute and useful. 🎀
  • -QNUM, --qlimit=NUM — limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited). the limits are limiting, periodt. 🫶
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME: 'jitty' jitty rewriting (default), 'jittyc' compiled jitty rewriting, 'jittyp' jitty rewriting with prover. pick your fighter. 👑
  • --timings[=FILE] — append timing measurements to FILE. Measurements are written to standard error if no FILE is provided. timing tea, served hot. ☕✨

🌸 standard options 🌸

  • -q, --quiet — do not display warning messages. shhh, she's quiet. 🙈
  • -v, --verbose — display short log messages. a little chatty, but make it useful. 💬
  • -d, --debug — display detailed log messages. detective mode activated. 🔍
  • --log-level=LEVEL — display log messages up to and including level; either warn, verbose, debug or trace. choose your level of drama. 💀
  • -h, --help — display help information. bestie needs a map sometimes. 🗺️
  • --version — display version information. who are you, icon? 👑
  • --help-all — display help information, including hidden and experimental options. the secret menu is real. 🧚

👑 AUTHOR 👑

Written by Jeroen Keiren. slay. 💜

🐛 REPORTING BUGS 🐛

Report bugs at <http://www.mcrl2.org/issuetracker>. do not suffer in silence, bestie. 😭📣

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. real ones know. ⭐

🦋 SEE ALSO 🦋

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/lpsuntime.html>. go read, she ate. 💅✨

mwah 💋 — this lpsuntime(1) page is from the mCRL2 toolset 202507..., dated October 2026. bye bestie! 🌈💖

📦 where this page comes from