LPSREACH(1)

📦 version 202507, in nixos 26.05, nixpkgs unstable

💅 LPSREACH(1) 💅

okay bestie, welcome to lpsreach from the User Commands girlies — this is the manual page, and yes it's giving "I'm a tool that does symbolic reachability on an LPS" ✨

🎀 NAME 🎀

lpsreach — bestie, it applies a symbolic reachability algorithm to an LPS. that's the whole vibe. no cap. 💅

✨ SYNOPSIS ✨

lpsreach [OPTION]... [INFILE [OUTFILE]]

🦋 DESCRIPTION 🦋

So here's the tea, fr fr: it reads an LPS from INFILE and writes a symbolic labelled transition system to OUTFILE. 🌸

  • if OUTFILE isn't there? no symbolic LTS gets written, periodt. it's giving "no output, no problem."
  • if INFILE isn't there? bestie it just uses stdin. iconic. 🫶

👑 OPTIONS 👑

OPTION can be literally any of the following, iykyk:

  • --cached — uses transition group caching to speed up state space exploration. it's lowkey a glow-up for your runtime ✨
  • --chaining — reduces the amount of breadth-first iterations by applying the transition groups consecutively. fewer laps, same destination 🏃‍♀️💨
  • --deadlock — reports the number of deadlocks (i.e. states with no outgoing transitions). 💀 and yes that's exactly what it sounds like
  • --groups[=GROUPS] — summand grouping time, bestie! the drama of GROUPS:
    • 'none' (default) — no summand groups. we're all individuals here 💅
    • 'used' — summands with the same variables are joined. matching outfits = matching groups 🎀
    • 'simple' — summands with the same read/write variables are joined. the read/write equivalent of matching outfits 🦋
    • a user defined list of summand groups separated by semicolons, e.g. '0; 1 3 4; 2 5' — YOU pick the friend groups, main character energy fr
  • --info — prints read/write information of the summands. receipts on what each summand reads and writes 🧾
  • --initial-ratio[=NUM] — power-of-two ratio of initial and maximum table size (default 16). bigger ratio, bigger table, bigger blahaj energy 🦈
  • --lace-dqsize[=NUM] — sets the length of the Lace task queue (default 1024*1024*4). that's the queue, not the vibe check
  • --lace-stacksize[=NUM] — sets the size of the program stack in kilobytes (0 = default stack size). 0 means "whatever the default is," not "zero kilobytes," don't come for me 😭
  • --max-iterations[=NUM] — limits the number of breadth-first iterations to NUM. it's giving "we're stopping here whether you like it or not"
  • -m[NUM], --memory-limit[=NUM] — Sylvan memory limit in gigabytes (default 3). girlies, don't go overboard, RAM isn't free 😭
  • --print-exact — prints the sizes of LDDs exactly when within the representable range, and in scientific notation otherwise. exact when it can be, fancy 1.2e+07 core when it can't 🔥
  • --print-nodesize — prints the number of LDD nodes in addition to the number of elements represented as 'elements[nodes]'. two numbers, one flex 💅
  • -QNUM, --qlimit=NUM — limits enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited). so -Q0 = no limits, live your truth ⭐
  • --reorder[=ORDER] — variable reordering, and the options are very choose-your-own-adventure:
    • 'none' (default) — no variable reordering. chaotic neutral ✨
    • 'random' — variables are put in a random order. audacious. respect. 🎲
    • 'weighted' — variables are put in an order defined by their connectivity weight. meritocracy arc 🏆
    • a user defined permutation, e.g. '1 3 2 0 4' — you're the director of this lineup 🎬
  • --replace-dont-care — replaces parameters assignments to don't care variables by assignments to the parameter itself. "don't care" gets promoted to main character 🫶
  • -rNAME, --rewriter=NAME — uses rewrite strategy NAME:
    • 'jitty' — jitty rewriting (default) 👑
    • 'jittyc' — compiled jitty rewriting ⚡
    • 'jittyp' — jitty rewriting with prover. she brought backup 🔍
  • --saturation — reduces the amount of breadth-first iterations required by applying the transition groups until a fixed point is reached. we go till it stops changing, periodt ♻️
  • --table-ratio[=NUM] — power-of-two ratio of node table and cache table (default 1). one for one, balanced queen 🧚
  • --threads=NUM — runs with NUM threads (default=1). > ⚠️ heads up bestie: with multiple threads the stack size on a Mac is limited, which can lead to bus errors. it's giving "we don't do that here" on Mac with threads 😭💀
  • --timings[=FILE] — appends timing measurements to FILE. measurements are written to standard error if no FILE is provided. receipts, but make them timed ⏱️

🌈 Standard options 🌈

  • -q, --quiet — do not display warning messages. ignorance is bliss bestie 🙈
  • -v, --verbose — display short log messages. snack-sized info 🍓
  • -d, --debug — display detailed log messages. the full meal deal 🔍
  • --log-level=LEVEL — display log messages up to and including level; either warn, verbose, debug or trace. pick your volume level 📢
  • -h, --help — display help information. bestie asks and bestie receives 💖
  • --version — display version information. the "who is she" option 💅
  • --help-all — display help information, including hidden and experimental options. the VIP backstage pass 👑✨

🌸 AUTHOR 🌸

Written by Wieger Wesselink. we stan a legend 🫶

😭 REPORTING BUGS 😭

Report bugs at <http://www.mcrl2.org/issuetracker>. please do, the girlies want the tool to slay 🐛🔫

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. ngl if it breaks, that's on the universe 🌌

🧚 SEE ALSO 🧚

See also the manual at <http://www.mcrl2.org/web/user_manual/tools/release/lpsreach.html>. that's the deep lore, go read it 💖

okay that's the whole page bestie, ily, go reach some states 🦋✨

— lpsreach mCRL2 toolset 202507.... October 2026 💅 and that's the sign-off, mwah 🫶

📦 where this page comes from