LPSCONFCHECK(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 LPSCONFCHECK(1) — the lpsconfcheck girlies' guide 💅

okay so bestie, welcome to lpsconfcheck(1) ✨ this is the mCRL2 toolset page for it, and i'm gonna walk you through it like we're texting at 2am 🫶

🌸 NAME 🌸

lpsconfcheck — mark confluent tau-summands of an LPS 🎀

like, it goes through your LPS and finds the tau-summands that are confluent, and it marks them. that's the whole job. iconic honestly 💅

✨ SYNOPSIS ✨

lpsconfcheck [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

so here's the vibe: lpsconfcheck checks which tau-summands of the mCRL2 LPS in INFILE are confluent, marks them by renaming them to ctau, and writes the result to OUTFILE. no cap, that's it 🌈

  • if INFILE is not present, stdin is used 🍓
  • if OUTFILE is not present, stdout is used ⭐

like, it just picks up whatever you give it. lowkey flexible of it tbh 😌

💖 OPTIONS 💖

OPTION can be any of the following, and yes bestie we're listing every single one because i would never do you like that 🙈

  • -a, --check-all — check the confluence of tau-summands regarding all other summands, instead of continuing with the next tau-summand as soon as a summand is encountered that is not confluent with the current tau-summand. so like, thorough mode. main character energy 👑
  • -x[CONDITIONS], --conditions[=CONDITIONS] — use the confluence conditions specified by individual characters. here's the cheat sheet:
    • c / C: commutative confluence with / without disjointness check
    • d: commutative confluence with disjointness check only
    • T: triangular confluence
    • Z: trivial confluence
  • -c, --counter-example — display a valuation for which the confluence condition does not hold, in case the encountered condition is neither a contradiction nor a tautology. it's giving "here's exactly where it went wrong" 🔥
  • -g, --generate-invariants — try to prove that the reduced confluence condition is an invariant of the LPS, in case the confluence condition is not a tautology 🧚
  • -o, --induction — apply induction on lists 📋
  • -iINVFILE, --invariant=INVFILE — use the boolean formula (an mCRL2 data expression of sort Bool) in INVFILE as invariant 💜
  • -n, --no-check — do not check if the invariant holds before checking for confluence. yep, it literally says "for for" in the original and i'm keeping the facts, not fixing the typo, that's not my job 😭
  • -m, --no-marking — do not mark the confluent tau-summands; since there are no changes made to the LPS, nothing is written to OUTFILE 💀 like genuinely nothing, don't go looking for output that isn't there
  • -u, --no-sums — do not rewrite summands with a sum operator and prove their confluence formula 🙅‍♀️
  • -pPREFIX, --print-dot=PREFIX — save a .dot file of the resulting BDD in case two summands cannot be proven confluent; 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) ⭐
  • -rNAME, --rewriter=NAME — use rewrite strategy NAME:
    • 'jitty' — jitty rewriting (default)
    • 'jittyc' — compiled jitty rewriting
  • -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
  • -sNUM, --summand=NUM — eliminate or simplify the summand with number NUM only 🎯
  • -tLIMIT, --time-limit=LIMIT — spend at most LIMIT seconds on proving a single formula ⏳
  • --timings[=FILE] — append timing measurements to FILE. measurements are written to standard error if no FILE is provided 📊

🌟 Standard options 🌟

the classics, the essentials, the little black dress of CLI flags 💅

  • -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 👀 iykyk

👑 AUTHOR 👑

Written by Luc Engelen. 🫡

🐛 REPORTING BUGS 🐛

Report bugs at <http://www.mcrl2.org/issuetracker> — bestie if it's broken, tell them, not me 😭

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. fr fr, no warranty, read the license 🌸

🌈 SEE ALSO 🌈

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/lpsconfcheck.html> ✨

and that's the whole page babes 🎀 this was lpsconfcheck from the mCRL2 toolset, version 202..., dated October 2026 — go check your confluence, slay, and remember: mark those tau-summands 💅💖🦋

📦 where this page comes from