{"_id":"@botiroff/pnueli","_rev":"2-10151bed94d65f0138a4434d6d046504","name":"@botiroff/pnueli","dist-tags":{"latest":"0.2.0"},"versions":{"0.1.0":{"name":"@botiroff/pnueli","version":"0.1.0","keywords":["model-checking","formal-methods","partial-order-reduction","symmetry-reduction","liveness","temporal-logic","verification","state-space","concurrency"],"author":{"name":"BOTIROFF-D"},"license":"MIT","_id":"@botiroff/pnueli@0.1.0","maintainers":[{"name":"botiroff","email":"thebotiroff@gmail.com"}],"homepage":"https://github.com/BOTIROFF-D/pnueli#readme","bugs":{"url":"https://github.com/BOTIROFF-D/pnueli/issues"},"dist":{"shasum":"90b8f92ef0a457ca9bfcbd1c94a32acfd663a840","tarball":"https://registry.npmjs.org/@botiroff/pnueli/-/pnueli-0.1.0.tgz","fileCount":7,"integrity":"sha512-qY20d7Zwa36Gb+J/mQ6g3BDYefUhR4gWP9yR5JSWIID/SFNykOpTlovcP0HhbdM4FAOSBpezUrwyjiFsny6ZzQ==","signatures":[{"sig":"MEUCIDHZvLbRDmfZX2gw7lWIvBEr49rkCqvLLtBCGErAIvujAiEAi3UDu45o1Ux+k833jIA+lIb9evdPYVLoNeNlmDnwwCE=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":61813},"main":"./dist/index.cjs","type":"module","types":"./dist/index.d.ts","module":"./dist/index.js","engines":{"node":">=18"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js","require":"./dist/index.cjs"}},"gitHead":"395880d9fc27e4942e24e283b6c6972e3fac0dc9","scripts":{"test":"vitest run","bench":"vitest run test/reduction","build":"tsup","prepare":"npm run build","typecheck":"tsc --noEmit","test:watch":"vitest","prepublishOnly":"npm run typecheck && npm run test && npm run build"},"_npmUser":{"name":"botiroff","email":"thebotiroff@gmail.com"},"repository":{"url":"git+https://github.com/BOTIROFF-D/pnueli.git","type":"git"},"_npmVersion":"11.11.0","description":"An explicit-state model checker: exhaustive search with symmetry reduction, partial-order reduction and liveness under weak fairness, validated against unreduced ground truth.","directories":{},"sideEffects":false,"_nodeVersion":"25.8.1","publishConfig":{"access":"public"},"_hasShrinkwrap":false,"devDependencies":{"tsup":"^8.3.5","vitest":"^2.1.8","typescript":"^5.7.2","@types/node":"^22.10.2"},"_npmOperationalInternal":{"tmp":"tmp/pnueli_0.1.0_1786795563166_0.35611390071068394","host":"s3://npm-registry-packages-npm-production"}},"0.2.0":{"name":"@botiroff/pnueli","version":"0.2.0","description":"An explicit-state model checker: exhaustive search with symmetry reduction, partial-order reduction and liveness under weak fairness, validated against unreduced ground truth.","keywords":["model-checking","formal-methods","partial-order-reduction","symmetry-reduction","liveness","temporal-logic","verification","state-space","concurrency"],"license":"MIT","author":{"name":"BOTIROFF-D"},"repository":{"type":"git","url":"git+https://github.com/BOTIROFF-D/pnueli.git"},"homepage":"https://github.com/BOTIROFF-D/pnueli#readme","bugs":{"url":"https://github.com/BOTIROFF-D/pnueli/issues"},"type":"module","sideEffects":false,"publishConfig":{"access":"public"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js","require":"./dist/index.cjs"}},"main":"./dist/index.cjs","module":"./dist/index.js","types":"./dist/index.d.ts","engines":{"node":">=18"},"scripts":{"build":"tsup","typecheck":"tsc --noEmit","test":"vitest run","test:watch":"vitest","bench":"vitest run test/reduction","prepare":"npm run build","prepublishOnly":"npm run typecheck && npm run test && npm run build"},"devDependencies":{"@types/node":"^22.10.2","tsup":"^8.3.5","typescript":"^5.7.2","vitest":"^2.1.8"},"gitHead":"9a2797dac593a8b0e074b5281ad3c2de3097771c","_id":"@botiroff/pnueli@0.2.0","_nodeVersion":"25.8.1","_npmVersion":"11.11.0","dist":{"integrity":"sha512-AH+0cMdlDOH3x95nHWuuHSSE9ZTzMglOpBFqCunkvzKjC6ImKcsJuSejJv4ibkr2/QXsMqd5D343CcQjcUHR+Q==","shasum":"8c8747f335cd9378eb1519ad6b1871203ebf3272","tarball":"https://registry.npmjs.org/@botiroff/pnueli/-/pnueli-0.2.0.tgz","fileCount":7,"unpackedSize":64984,"signatures":[{"keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U","sig":"MEUCIC7UijSA5N7YfmvNVsAEVEnnrqzDkoyObLYIjdUJMt/jAiEAzp2bnk8dd7LP0NQjiORAlxepfkG5AkRNZ7TwlKzSH3c="}]},"_npmUser":{"name":"botiroff","email":"thebotiroff@gmail.com"},"directories":{},"maintainers":[{"name":"botiroff","email":"thebotiroff@gmail.com"}],"_npmOperationalInternal":{"host":"s3://npm-registry-packages-npm-production","tmp":"tmp/pnueli_0.2.0_1786895248855_0.05193079836014558"},"_hasShrinkwrap":false}},"time":{"created":"2026-08-15T12:06:02.933Z","modified":"2026-08-16T15:47:29.161Z","0.1.0":"2026-08-15T12:06:03.313Z","0.2.0":"2026-08-16T15:47:28.992Z"},"bugs":{"url":"https://github.com/BOTIROFF-D/pnueli/issues"},"author":{"name":"BOTIROFF-D"},"license":"MIT","homepage":"https://github.com/BOTIROFF-D/pnueli#readme","keywords":["model-checking","formal-methods","partial-order-reduction","symmetry-reduction","liveness","temporal-logic","verification","state-space","concurrency"],"repository":{"type":"git","url":"git+https://github.com/BOTIROFF-D/pnueli.git"},"description":"An explicit-state model checker: exhaustive search with symmetry reduction, partial-order reduction and liveness under weak fairness, validated against unreduced ground truth.","maintainers":[{"name":"botiroff","email":"thebotiroff@gmail.com"}],"readme":"# pnueli\n\n**An explicit-state model checker.** Exhaustive search, symmetry reduction, partial-order reduction and liveness under weak fairness — with every reduction validated against the unreduced search it is supposed to replace.\n\n[![CI](https://github.com/BOTIROFF-D/pnueli/actions/workflows/ci.yml/badge.svg)](https://github.com/BOTIROFF-D/pnueli/actions/workflows/ci.yml)\n[![npm](https://img.shields.io/npm/v/%40botiroff%2Fpnueli)](https://www.npmjs.com/package/@botiroff/pnueli)\n![node](https://img.shields.io/badge/node-%E2%89%A518-blue)\n![license](https://img.shields.io/badge/license-MIT-blue)\n\nNamed for [Amir Pnueli](https://amturing.acm.org/award_winners/pnueli_4725172.cfm), who won the Turing Award for introducing temporal logic to program verification and gave the field the language to ask whether something *always* holds or *eventually* happens.\n\n---\n\nThis exists because of a sentence in [unflake](https://github.com/BOTIROFF-D/unflake)'s limits section:\n\n> Hundreds of seeds is hundreds of schedules from an astronomically larger space. It is a very good fuzz run, not a theorem.\n\nSampling schedules finds bugs and can never prove their absence. Proving absence means visiting every reachable state — which is exponential, which is why the interesting part of a model checker is not the search but everything done to avoid searching.\n\n## The reductions, measured\n\n```\nspec               none  symmetry    both  factor\nworkers(4)          625        70      17     37×\nworkers(6)        15625       210      25    625×\n```\n\n**Symmetry reduction.** When processes are interchangeable, states differing only by permuting them are the same state. Six workers each in one of five phases is 5⁶ = 15,625 assignments but only 210 multisets, and the checker never needs to know which worker is which.\n\n**Partial-order reduction.** When two actions touch nothing in common they commute, so exploring both orders reveals nothing exploring one does not. This is done with ample sets, whose four conditions each earn their place — drop C2 and the checker will confidently miss violations. They are spelled out in [`explore.ts`](./src/explore.ts).\n\nAnd on a specification where processes read and write each other's variables constantly, the reduction correctly does nothing at all:\n\n```\npeterson             20        20      20      1×\n```\n\nThat row is in the test suite as an assertion. A tool that claimed a reduction there would be claiming something false.\n\n## Why there are two searches\n\nA partial-order reduction that drops the wrong states produces exactly the same output as one that works. Both say *no violation found*. One of them is a lie, and nothing inside the reduced search can tell you which you are holding.\n\nSo the exhaustive search is kept — slow, complete, and unable to be wrong — and **every specification here is run through both, with the reduced verdict required to match**. The reduction is trusted because it agrees with something that cannot be mistaken, on every case small enough to run both. That check is [`test/reduction.test.ts`](./test/reduction.test.ts) and it is the file the rest of the project rests on.\n\n## Specifications with settled answers\n\nThe other way to find out whether a checker works is to point it at problems the literature already decided.\n\n| Specification | Expected | Found |\n| --- | --- | --- |\n| Peterson's algorithm | mutual exclusion holds | holds, 20 states |\n| Peterson, check-then-set | mutual exclusion fails | fails, 4-step counterexample |\n| Plain spinlock | safe but starves | safe; starvation counterexample |\n| Dining philosophers | deadlocks | deadlocks at n = 3, 4, 5 |\n| Philosophers, one lefty | no deadlock | none at n = 3, 4, 5 |\n\nThe counterexamples are the output that matters, and breadth-first search makes them shortest by construction:\n\n```\n✗ peterson (check then set) — invariant \"at most one process in the critical section\"\n\n  trace\n    (initial)                    pc=00 flag=00\n    p0: check the other flag     pc=10 flag=00\n    p1: check the other flag     pc=11 flag=00\n    p0: raise flag and enter     pc=31 flag=10\n    p1: raise flag and enter     pc=33 flag=11\n```\n\nBoth look, both see a lowered flag, both walk in. That is the whole reason the flag has to go up first.\n\n## Proving what the other repositories sample\n\n[bulwark](https://github.com/BOTIROFF-D/bulwark) tests Raft's Election Safety by running the implementation under seeded partitions, crashes and reordered messages. [adya](https://github.com/BOTIROFF-D/adya) finds write skew by generating concurrent transactions and looking for dependency cycles in the histories. Both work, and both say plainly that a clean result means *not found*, not *impossible*.\n\nHere are the same two properties on instances small enough for *impossible* to be available.\n\n| Property | Sampled | Proven here |\n| --- | --- | --- |\n| Election Safety, 3 nodes, terms ≤ 3 | hundreds of schedules | **2,428 states**, exhaustive |\n| Election Safety, 5 nodes, terms ≤ 2 | hundreds of schedules | **148,318 states**, exhaustive |\n| Election Safety, 5 nodes, terms ≤ 3 | hundreds of schedules | **6,801,084 states**, exhaustive |\n| Write skew under snapshot isolation | found at seed 25 of 300 | reachable in **5 steps**, shortest |\n\nAnd the failure modes line up with the ones bulwark had to construct by hand. Its unpersisted-vote exhibit crashes a node in the one-tick window between granting a vote and writing it down — a window a random search never lands in, so bulwark builds that scenario directly. Take the same rule out of the specification and it is simply a reachable state:\n\n```\n✗ raft election (3 nodes, terms ≤ 2, one-vote-per-term OFF)\n  invariant \"at most one leader per term\" does not hold\n\n  trace\n    (initial)                 n0:f0 n1:f0 n2:f0\n    n0: stand for election    n0:c1→0 n1:f0   n2:f0\n    n1: stand for election    n0:c1→0 n1:c1→1 n2:f0\n    n0: vote for n1           n0:c1→1 n1:c1→1 n2:f0\n    n1: take office           n0:c1→1 n1:l1→1 n2:f0\n    n1: vote for n0           n0:c1→1 n1:l1→0 n2:f0\n    n0: take office           n0:l1→1 n1:l1→0 n2:f0\n```\n\nTwo candidates in term 1, each collecting the other's vote. One vote per term is the only thing standing between that and a split brain — and this is what \"only thing\" means, stated over every reachable configuration rather than over the ones a seed happened to produce.\n\nThe specifications are [`specs/raft-election.ts`](./specs/raft-election.ts) and [`specs/write-skew.ts`](./specs/write-skew.ts); the checks are [`test/portfolio.test.ts`](./test/portfolio.test.ts).\n\n**What this does not prove.** The specification is not the implementation. bulwark's Raft has message loss, duplication, reordering, crash-restart and persistence; this model has none of them, and voting is atomic. A proof about the model is a proof that the *algorithm* is sound at that level of abstraction — it says nothing about whether the code implements the algorithm. That is what the sampling is for, and why both exist.\n\n## Liveness\n\nSafety asks whether a bad state is reachable, and breadth-first search answers it. Liveness asks whether something good always eventually happens, and it is violated by an infinite run that never gets there — in a finite state space, a lasso: a path into a cycle, then the cycle forever.\n\nMost such cycles are absurd, though. They require a process that could run to simply never be scheduled. **Weak fairness** rules those out: a continuously enabled process must eventually move. So a cycle is a real counterexample only if every process either moves inside it or is blocked inside it. Without that condition every concurrent program \"fails\" liveness and the checker is useless.\n\nThe difference shows up exactly where it should — between a lock and Peterson's algorithm:\n\n```\n✗ spinlock — can loop forever without process 0 reaching its critical section\n  The cycle is fair: process 1 keeps moving; process 0 is blocked\n\n  then forever\n    p1: acquire   pc=03 lock=1\n    p1: release   pc=00 lock=-1\n```\n\nPeterson passes the same check. The turn variable exists for no other reason.\n\n## Usage\n\n```bash\nnpm install @botiroff/pnueli\n```\n\n```ts\nimport { checkExhaustive, checkReduced, checkLiveness, formatResult } from \"@botiroff/pnueli\";\n\nconst spec = {\n  name: \"counter\",\n  processes: 2,\n  init: [{ n: 0 }],\n  actions: [\n    {\n      name: \"p0: increment\",\n      process: 0,\n      reads: [\"n\"],\n      writes: [\"n\"],\n      step: (s) => (s.n < 3 ? [{ n: s.n + 1 }] : []),\n    },\n  ],\n  invariants: [{ name: \"n stays small\", reads: [\"n\"], holds: (s) => s.n <= 3 }],\n  terminal: (s) => s.n === 3,\n};\n\nconsole.log(formatResult(checkExhaustive(spec)));\n```\n\nAn action returns its successor states; an empty array means it is disabled, so a guard and its effect cannot drift apart. `reads` and `writes` are what the partial-order reduction needs, and `symmetry` is what the symmetry reduction needs — declared rather than guessed, for the same reason TLA+ asks you to declare symmetry sets. A wrong declaration is then a bug in the specification, not a silent unsoundness in the tool.\n\n## Limits\n\n**TLC and SPIN are better at this.** They have decades of work behind them, disk-backed state storage, distributed checking, full LTL, and specification languages designed for the job. This is a few hundred lines you can read in an afternoon, which is the only thing it offers that they do not.\n\n**Reductions are sound with respect to what you declare.** If an action writes a variable it did not list, the partial-order reduction may drop states that mattered. There is no analysis here that recovers dependencies from a closure — the declaration is the contract.\n\n**The C1 check is conservative.** It asks structurally whether any action of another process is dependent on the candidate set, rather than reasoning about which of them can actually run next. That rejects some legal ample sets and so reduces less than it could. Conservative is the correct direction to be wrong in.\n\n**Only invariants and one liveness form.** State predicates that must always hold, and \"eventually P\" under weak fairness. No nested temporal operators, no strong fairness, no LTL.\n\n**Everything is in memory.** State spaces here are thousands of states, not billions. There is no disk-backed store and no symbolic representation.\n\n**No predicate abstraction, no counterexample-guided refinement.** The model you write is the model that is checked.\n\n## Prior art\n\nThe algorithms are standard and old, and pretending otherwise would be silly. Partial-order reduction and the ample-set conditions are from [Clarke, Grumberg and Peled's *Model Checking*](https://mitpress.mit.edu/9780262038836/model-checking/); the persistent-set idea is Godefroid's, the stubborn-set variant Valmari's. Symmetry reduction is Clarke, Filkorn and Jha, and Emerson and Sistla. Weak fairness and the temporal framing are Pnueli's, by way of Lamport.\n\n[TLA+ and TLC](https://lamport.azurewebsites.net/tla/tla.html) and [SPIN](https://spinroot.com/) are where this is done properly.\n\nPart of a set: [unflake](https://github.com/BOTIROFF-D/unflake) samples schedules, [bulwark](https://github.com/BOTIROFF-D/bulwark) tests consensus with them, [adya](https://github.com/BOTIROFF-D/adya) tests transaction isolation — and this proves small instances outright instead of sampling.\n\n## Who wrote this\n\n[Doniyor Botirov](https://dbit.one/en/founder), founder of [dbit.one](https://dbit.one/en). The reasoning behind this repository at length — why a green suite says \"not found\" rather than \"not there\", and what closes that gap: [Tests do not prove the absence of a bug](https://dbit.one/en/blog/model-checking-proving-absence-of-bugs).\n\n## License\n\nMIT\n","readmeFilename":"README.md"}