Problem class: node-ltl-bmc-partial-order-minimal-counterexample · Node.js 20
All artifacts are verified and saved. Below is the complete solution document (also written to /workspace/SOLUTION.md, with runnable sources at /workspace/ltlbmc.js, /workspace/test.js, /workspace/verify_canonical.js, /workspace/instance.json).
Problem class: node-ltl-bmc-partial-order-minimal-counterexample · Node.js 20
Artifacts: ltlbmc.js (checker + CLI), test.js (verification), verify_canonical.js (POR proof-check), instance.json (sample).
There is no pre-existing source to patch, so the "bug" to diagnose is the set of algorithmic traps that make a naive implementation fail the two hard acceptance criteria:
agree with brute-force enumeration on every instance, while exploring >= 5x fewer states on the reduction-friendly ones, and return the lexicographically shortest counterexample.
The traps, and their root causes:
X φ is false at the last position; G/F/U/R range over the remaining finite suffix.G/F/U need least/greatest fixpoints, not suffix folds.Picking one silently, or folding G over a finite suffix with a true tail (or X with a false tail) while the reference uses the other, produces off-by-one disagreements. Root cause: conflating the two evaluators.
Root cause of the state explosion: explicit unrolling of all action words up to depth k is O(|A|^k). The 5x reduction requirement can only be met by collapsing words equivalent modulo an independence relation.
Root cause of unsound "reduction": commuting independent actions is only legal when the property is invariant under that commutation.
X in general when independence is computed from read/write sets (X p can flip after a swap).It is not invariant for lasso loop detection, because the lasso closes on a state repetition in the concrete word, and a different representative of the same trace class may never repeat that state. A 20 000-instance stress run with canonical POR forced on under lasso semantics produced 26 divergences, including none vs. a real counterexample. Root cause: applying a trace-class reduction to a semantics whose acceptance is not trace-class invariant.
Root cause of non-minimal answers: finding a counterexample is easy; finding the lexicographically shortest one requires a search order. Depth-first or hash-visited exploration returns an arbitrary trace. The correct order is breadth-first by length, lexicographic within a length, and the reduction must canonically choose the lexicographically least word of each Mazurkiewicz class, otherwise the minimal class representative can be pruned away.
Root cause of spurious traces: guards, simultaneous (non-sequential) updates, and finite domains must be enforced; an out-of-domain successor is not a legal transition.
A single self-contained module with these decisions:
toNNF).evalLTLf — finite-suffix semantics (X false past the end).evalLasso — least/greatest fixpoints over the functional successor graph of an ultimately-periodic word. Handles all of X/F/G/U/R exactly.0..k. Counterexamples are tested on dequeue. Because the frontier is built at each depth in lexicographic action order, the first hit is the shortest, then lexicographically smallest, trace.a to history h, let h2 be the suffix after the last action in h dependent on a (all of h2 is independent of a). The append is allowed iff no action in h2 has a strictly greater rank than a. This enumerates exactly one word per trace class — its lexicographically least member. verify_canonical.js checks this against brute-force connected components of the "swap adjacent independent letters" graph (60 random independence relations × words up to length 5): exact match.X and independence is auto-computed from read/write sets → POR is disabled (or use an explicitly supplied, X-sound relation).semantics: "lasso" → POR is disabled, because it was proved by counterexample to be unsound there. Brute-force agreement is prioritized.[a,b] pairs when supplied, otherwise from read/write sets (writes(a) ∩ (reads(b) ∪ writes(b)) = ∅ both ways).{
"variables": [
{ "name": "x", "domain": { "type": "bool" } },
{ "name": "n", "domain": { "type": "int", "min": 0, "max": 5 } },
{ "name": "c", "domain": { "type": "enum", "values": ["a", "b"] } }
],
"actions": [
{ "name": "inc", "guard": "n < 5", "updates": { "n": "n + 1" } }
],
"propositions": { "p": "n >= 2" },
"formula": "G(p -> F q)",
"independence": [["a", "b"]],
"bound": 8,
"semantics": "ltlf"
}
ltlbmc.js'use strict';
/*
* ltlbmc.js — Bounded model checker for LTL/LTLf over a small imperative language.
*
* Public API (module.exports):
* parseExpr(text) -> expression AST
* parseFormula(text) -> LTL AST (general, not yet NNF)
* toNNF(ast) -> NNF AST
* normalizeSystem(obj) -> system {vars, actions, props, independence}
* checkBMC(system, opts) -> { result, trace, states, explored, loop }
* bruteForce(system, opts) -> same shape, no partial-order reduction
*/
/* ============================ Expressions ============================ */
function tokenizeExpr(input) {
const toks = [];
let i = 0;
const isDigit = (c) => c >= '0' && c <= '9';
const isAlpha = (c) => /[A-Za-z_]/.test(c);
const isAlnum = (c) => /[A-Za-z0-9_]/.test(c);
while (i < input.length) {
const c = input[i];
if (/\s/.test(c)) { i++; continue; }
if (isDigit(c)) {
let j = i; while (j < input.length && isDigit(input[j])) j++;
toks.push({ t: 'num', v: parseInt(input.slice(i, j), 10) });
i = j; continue;
}
if (isAlpha(c)) {
let j = i; while (j < input.length && isAlnum(input[j])) j++;
const id = input.slice(i, j);
if (id === 'true') toks.push({ t: 'bool', v: true });
else if (id === 'false') toks.push({ t: 'bool', v: false });
else toks.push({ t: 'id', v: id });
i = j; continue;
}
const two = input.slice(i, i + 2);
if (['&&', '||', '==', '!=', '<=', '>='].includes(two)) { toks.push({ t: 'op', v: two }); i += 2; continue; }
if ('!<>+-*/%()'.includes(c)) { toks.push({ t: 'op', v: c }); i++; continue; }
throw new Error('Unexpected character in expression: ' + c);
}
toks.push({ t: 'eof' });
return toks;
}
function parseExpr(input) {
const toks = typeof input === 'string' ? tokenizeExpr(input) : input;
let p = 0;
const peek = () => toks[p];
const isOp = (v) => { const t = toks[p]; return t.t === 'op' && t.v === v; };
const eat = (v) => { if (!isOp(v)) throw new Error('Expected "' + v + '"'); p++; };
function primary() {
const t = peek();
if (t.t === 'num') { p++; return { t: 'num', v: t.v }; }
if (t.t === 'bool') { p++; return { t: 'bool', v: t.v }; }
if (t.t === 'id') { p++; return { t: 'id', v: t.v }; }
if (t.t === 'op' && t.v === '(') { p++; const e = or(); eat(')'); return e; }
throw new Error('Unexpected token in expression: ' + JSON.stringify(t));
}
function unary() {
if (isOp('!')) { p++; return { t: 'un', op: '!', e: unary() }; }
if (isOp('-')) { p++; return { t: 'un', op: '-', e: unary() }; }
return primary();
}
function mul() { let l = unary(); while (isOp('*') || isOp('/') || isOp('%')) { const op = peek().v; p++; l = { t: 'bin', op, l, r: unary() }; } return l; }
function add() { let l = mul(); while (isOp('+') || isOp('-')) { const op = peek().v; p++; l = { t: 'bin', op, l, r: mul() }; } return l; }
function cmp() {
let l = add();
if (isOp('==') || isOp('!=') || isOp('<') || isOp('<=') || isOp('>') || isOp('>=')) {
const op = peek().v; p++; l = { t: 'bin', op, l, r: add() };
}
return l;
}
function and() { let l = cmp(); while (isOp('&&')) { p++; l = { t: 'bin', op: '&&', l, r: cmp() }; } return l; }
function or() { let l = and(); while (isOp('||')) { p++; l = { t: 'bin', op: '||', l, r: and() }; } return l; }
const e = or();
if (peek().t !== 'eof') throw new Error('Trailing tokens in expression');
return e;
}
function evalExpr(ast, state) {
switch (ast.t) {
case 'num': return ast.v;
case 'bool': return ast.v;
case 'id': return state[ast.v];
case 'un': {
const v = evalExpr(ast.e, state);
return ast.op === '!' ? !v : -v;
}
case 'bin': {
const a = evalExpr(ast.l, state), b = evalExpr(ast.r, state);
switch (ast.op) {
case '&&': return !!(a && b);
case '||': return !!(a || b);
case '==': return a === b;
case '!=': return a !== b;
case '<': return a < b;
case '<=': return a <= b;
case '>': return a > b;
case '>=': return a >= b;
case '+': return a + b;
case '-': return a - b;
case '*': return a * b;
case '/': return Math.trunc(a / b);
case '%': return a % b;
}
}
}
throw new Error('bad expr node');
}
function exprVars(ast, out) {
if (ast.t === 'id') out.add(ast.v);
else if (ast.t === 'un') exprVars(ast.e, out);
else if (ast.t === 'bin') { exprVars(ast.l, out); exprVars(ast.r, out); }
return out;
}
/* ============================ LTL formulas ============================ */
function tokenizeFormula(input) {
const toks = [];
let i = 0;
const isAlpha = (c) => /[A-Za-z_]/.test(c);
const isAlnum = (c) => /[A-Za-z0-9_]/.test(c);
while (i < input.length) {
const c = input[i];
if (/\s/.test(c)) { i++; continue; }
if (c === '(' || c === ')' || c === '!') { toks.push({ t: c }); i++; continue; }
if (c === '&' && input[i + 1] === '&') { toks.push({ t: '&&' }); i += 2; continue; }
if (c === '|' && input[i + 1] === '|') { toks.push({ t: '||' }); i += 2; continue; }
if (c === '-' && input[i + 1] === '>') { toks.push({ t: '->' }); i += 2; continue; }
if (isAlpha(c)) {
let j = i; while (j < input.length && isAlnum(input[j])) j++;
const id = input.slice(i, j);
if (id === 'true') toks.push({ t: 'true' });
else if (id === 'false') toks.push({ t: 'false' });
else if (['X', 'F', 'G', 'U', 'R'].includes(id)) toks.push({ t: id });
else toks.push({ t: 'id', v: id });
i = j; continue;
}
throw new Error('Unexpected character in formula: ' + c);
}
toks.push({ t: 'eof' });
return toks;
}
function parseFormula(input) {
const toks = typeof input === 'string' ? tokenizeFormula(input) : input;
let p = 0;
const peek = () => toks[p];
const is = (t) => toks[p].t === t;
const eat = (t) => { if (!is(t)) throw new Error('Expected ' + t + ', got ' + JSON.stringify(peek())); p++; };
function imp() {
const l = or();
if (is('->')) { p++; return { t: 'or', l: { t: 'not', c: l }, r: imp() }; }
return l;
}
function or() { let l = and(); while (is('||')) { p++; l = { t: 'or', l, r: and() }; } return l; }
function and() { let l = until(); while (is('&&')) { p++; l = { t: 'and', l, r: until() }; } return l; }
function until() {
let l = unary();
while (is('U') || is('R')) { const op = peek().t; p++; l = { t: op, l, r: unary() }; }
return l;
}
function unary() {
if (is('!')) { p++; return { t: 'not', c: unary() }; }
if (is('X') || is('F') || is('G')) { const op = peek().t; p++; return { t: op, c: unary() }; }
return primary();
}
function primary() {
if (is('true')) { p++; return { t: 'true' }; }
if (is('false')) { p++; return { t: 'false' }; }
if (is('id')) { const v = peek().v; p++; return { t: 'lit', name: v, neg: false }; }
if (is('(')) { p++; const e = imp(); eat(')'); return e; }
throw new Error('Unexpected token in formula: ' + JSON.stringify(peek()));
}
const e = imp();
if (!is('eof')) throw new Error('Trailing tokens in formula');
return e;
}
function toNNF(node, neg) {
switch (node.t) {
case 'true': return neg ? { t: 'false' } : { t: 'true' };
case 'false': return neg ? { t: 'true' } : { t: 'false' };
case 'lit': return { t: 'lit', name: node.name, neg: neg ? !node.neg : node.neg };
case 'not': return toNNF(node.c, !neg);
case 'and':
return neg ? { t: 'or', l: toNNF(node.l, true), r: toNNF(node.r, true) }
: { t: 'and', l: toNNF(node.l, false), r: toNNF(node.r, false) };
case 'or':
return neg ? { t: 'and', l: toNNF(node.l, true), r: toNNF(node.r, true) }
: { t: 'or', l: toNNF(node.l, false), r: toNNF(node.r, false) };
case 'X': return { t: 'X', c: toNNF(node.c, neg) };
case 'F': return neg ? { t: 'G', c: toNNF(node.c, true) } : { t: 'F', c: toNNF(node.c, false) };
case 'G': return neg ? { t: 'F', c: toNNF(node.c, true) } : { t: 'G', c: toNNF(node.c, false) };
case 'U':
return neg ? { t: 'R', l: toNNF(node.l, true), r: toNNF(node.r, true) }
: { t: 'U', l: toNNF(node.l, false), r: toNNF(node.r, false) };
case 'R':
return neg ? { t: 'U', l: toNNF(node.l, true), r: toNNF(node.r, true) }
: { t: 'R', l: toNNF(node.l, false), r: toNNF(node.r, false) };
}
throw new Error('bad formula node ' + JSON.stringify(node));
}
function formulaHasX(node) {
switch (node.t) {
case 'X': return true;
case 'F': case 'G': return formulaHasX(node.c);
case 'U': case 'R': return formulaHasX(node.l) || formulaHasX(node.r);
case 'and': case 'or': return formulaHasX(node.l) || formulaHasX(node.r);
default: return false;
}
}
/* ============================ Semantics ============================ */
// LTLf: evaluate on finite trace, return boolean at position 0.
function evalLTLf(root, states, propOf) {
const n = states.length;
const memo = new Map();
function ev(node, i) {
let arr = memo.get(node);
if (!arr) { arr = new Array(n); memo.set(node, arr); }
if (arr[i] !== undefined) return arr[i];
let v;
switch (node.t) {
case 'true': v = true; break;
case 'false': v = false; break;
case 'lit': { const p = propOf(node.name, states[i]); v = node.neg ? !p : p; break; }
case 'and': v = ev(node.l, i) && ev(node.r, i); break;
case 'or': v = ev(node.l, i) || ev(node.r, i); break;
case 'X': v = i + 1 < n ? ev(node.c, i + 1) : false; break;
case 'F': v = false; for (let j = i; j < n; j++) if (ev(node.c, j)) { v = true; break; } break;
case 'G': v = true; for (let j = i; j < n; j++) if (!ev(node.c, j)) { v = false; break; } break;
case 'U': {
v = false;
for (let j = i; j < n; j++) {
if (ev(node.r, j)) { v = true; break; }
if (!ev(node.l, j)) break;
}
break;
}
case 'R': {
v = true;
for (let j = i; j < n; j++) {
if (!ev(node.r, j)) { v = false; break; }
if (ev(node.l, j)) break;
}
break;
}
default: throw new Error('bad node');
}
arr[i] = v;
return v;
}
return ev(root, 0);
}
// LTL on an ultimately-periodic (lasso) trace. `states` = s_0..s_{m-1},
// succ(m-1) = loopStart. Evaluated by least/greatest fixpoints over the
// functional successor graph (exact for one infinite ultimately-periodic word).
function evalLasso(root, states, loopStart, propOf) {
const n = states.length;
const succ = (i) => (i + 1 < n ? i + 1 : loopStart);
const memo = new Map();
const allTrue = () => { const a = new Array(n).fill(true); return a; };
const allFalse = () => { const a = new Array(n).fill(false); return a; };
const shift = (a) => { const r = new Array(n); for (let i = 0; i < n; i++) r[i] = a[succ(i)]; return r; };
function ev(node) {
if (memo.has(node)) return memo.get(node);
let res;
switch (node.t) {
case 'true': res = allTrue(); break;
case 'false': res = allFalse(); break;
case 'lit': {
res = new Array(n);
for (let i = 0; i < n; i++) { const p = propOf(node.name, states[i]); res[i] = node.neg ? !p : p; }
break;
}
case 'and': { const a = ev(node.l), b = ev(node.r); res = a.map((v, i) => v && b[i]); break; }
case 'or': { const a = ev(node.l), b = ev(node.r); res = a.map((v, i) => v || b[i]); break; }
case 'X': { const a = ev(node.c); res = shift(a); break; }
case 'F': {
const a = ev(node.c); res = a.slice();
for (let iter = 0; iter < n; iter++) { const s = shift(res); let ch = false; for (let i = 0; i < n; i++) if (!res[i] && s[i]) { res[i] = true; ch = true; } if (!ch) break; }
break;
}
case 'G': {
const a = ev(node.c); res = a.slice();
for (let iter = 0; iter < n; iter++) { const s = shift(res); let ch = false; for (let i = 0; i < n; i++) if (res[i] && !s[i]) { res[i] = false; ch = true; } if (!ch) break; }
break;
}
case 'U': {
const a = ev(node.l), b = ev(node.r); res = b.slice();
for (let iter = 0; iter < n; iter++) { const s = shift(res); let ch = false; for (let i = 0; i < n; i++) if (!res[i] && a[i] && s[i]) { res[i] = true; ch = true; } if (!ch) break; }
break;
}
case 'R': {
const a = ev(node.l), b = ev(node.r); res = b.slice();
for (let iter = 0; iter < n; iter++) { const s = shift(res); let ch = false; for (let i = 0; i < n; i++) if (res[i] && !(a[i] || s[i])) { res[i] = false; ch = true; } if (!ch) break; }
break;
}
default: throw new Error('bad node');
}
memo.set(node, res);
return res;
}
return ev(root)[0];
}
/* ============================ Transition system ============================ */
function normalizeSystem(obj) {
const vars = (obj.variables || []).map((v) => {
const domain = v.domain || { type: v.type || 'bool' };
let init;
if (v.init !== undefined) init = v.init;
else if (domain.type === 'bool') init = false;
else if (domain.type === 'int') init = domain.min;
else init = (domain.values || [])[0];
return { name: v.name, domain, init };
});
const varIndex = new Map(vars.map((v, i) => [v.name, i]));
const actions = (obj.actions || []).map((a) => {
const guardText = a.guard === undefined ? 'true' : String(a.guard);
const guard = parseExpr(guardText);
let updates;
if (Array.isArray(a.updates)) {
updates = a.updates.map((u) => ({ name: u.var || u.name, expr: parseExpr(String(u.expr)) }));
} else {
updates = Object.entries(a.updates || a.effect || {}).map(([name, e]) => ({ name, expr: parseExpr(String(e)) }));
}
for (const u of updates) if (!varIndex.has(u.name)) throw new Error('update to unknown var ' + u.name);
const reads = exprVars(guard, new Set());
for (const u of updates) exprVars(u.expr, reads);
const writes = new Set(updates.map((u) => u.name));
return { name: a.name, guard, updates, reads, writes };
});
const props = {};
for (const [k, v] of Object.entries(obj.propositions || {})) props[k] = parseExpr(String(v));
const formula = toNNF(parseFormula(obj.formula), false);
let independence = null;
if (Array.isArray(obj.independence)) {
independence = new Set();
for (const [a, b] of obj.independence) { independence.add(a + '\u0000' + b); independence.add(b + '\u0000' + a); }
}
return { vars, varIndex, actions, props, formula, independence };
}
function initialState(sys) {
const s = {};
for (const v of sys.vars) s[v.name] = v.init;
return s;
}
function stateKey(sys, s) {
const a = new Array(sys.vars.length);
for (let i = 0; i < sys.vars.length; i++) a[i] = s[sys.vars[i].name];
return JSON.stringify(a);
}
function enabled(sys, action, s) {
if (!evalExpr(action.guard, s)) return false;
const next = applyAction(sys, action, s);
return next !== null;
}
function applyAction(sys, action, s) {
const next = Object.assign({}, s);
const pending = [];
for (const u of action.updates) pending.push([u.name, evalExpr(u.expr, s)]);
for (const [name, val] of pending) next[name] = val;
for (const v of sys.vars) {
const val = next[v.name];
const d = v.domain;
if (d.type === 'bool') { if (typeof val !== 'boolean') next[v.name] = !!val; }
else if (d.type === 'int') { if (typeof val !== 'number' || val < d.min || val > d.max) return null; }
else if (d.type === 'enum') { if (!d.values.includes(val)) return null; }
}
return next;
}
function isIndependent(sys, a, b) {
if (a.name === b.name) return false;
if (sys.independence) return sys.independence.has(a.name + '\u0000' + b.name);
for (const w of a.writes) if (b.reads.has(w) || b.writes.has(w)) return false;
for (const w of b.writes) if (a.reads.has(w) || a.writes.has(w)) return false;
return true;
}
/* ============================ Search ============================ */
function makePropEval(sys) {
const cache = new Map();
return function propOf(name, s) {
const ast = sys.props[name];
if (ast === undefined) throw new Error('unknown proposition ' + name);
const key = name + '@' + stateKey(sys, s);
if (cache.has(key)) return cache.get(key);
const v = !!evalExpr(ast, s);
cache.set(key, v);
return v;
};
}
// Is appending `a` to `history` the lexicographically least word in its
// Mazurkiewicz trace class? Every action after the last history action
// dependent on `a` is independent of `a`; swapping `a` left past a larger
// independent action would produce a smaller word, so forbid that.
function canonicalAppend(sys, rankOf, history, a) {
let lastDep = -1;
for (let i = history.length - 1; i >= 0; i--) {
if (!isIndependent(sys, history[i], a)) { lastDep = i; break; }
}
for (let i = lastDep + 1; i < history.length; i++) {
if (rankOf.get(history[i].name) > rankOf.get(a.name)) return false;
}
return true;
}
function counterexampleCheck(sys, propOf, semantics, states, history) {
if (semantics === 'ltlf') {
return !evalLTLf(sys.formula, states, propOf);
}
const last = stateKey(sys, states[states.length - 1]);
for (let l = 0; l < states.length - 1; l++) {
if (stateKey(sys, states[l]) === last) {
if (!evalLasso(sys.formula, states, l, propOf)) return { loop: l };
}
}
return false;
}
function search(sys, opts, usePor) {
const bound = opts.bound === undefined ? 8 : opts.bound;
const semantics = opts.semantics || 'ltlf';
const propOf = makePropEval(sys);
const actions = sys.actions.slice().sort((x, y) => x.name < y.name ? -1 : x.name > y.name ? 1 : 0);
const rankOf = new Map(actions.map((a, i) => [a.name, i]));
let por = !!usePor && opts.por !== false;
// Canonical-representative POR is provably sound for finite-trace (LTLf)
// properties. Under infinite-lasso semantics loop detection depends on the
// concrete state sequence, and commuting independent actions can destroy the
// repeat even though they preserve the trace class. POR is disabled for
// lasso mode; brute-force agreement wins.
if (semantics === 'lasso') por = false;
// X is not preserved by commuting independent actions in general; only
// auto-computed independence (not a supplied relation) is rejected here.
if (por && !opts.forcePor && formulaHasX(sys.formula) && !sys.independence) por = false;
const init = initialState(sys);
let frontier = [{ states: [init], history: [] }];
let explored = 0;
for (let depth = 0; depth <= bound; depth++) {
const next = [];
for (const node of frontier) {
explored++;
const ce = counterexampleCheck(sys, propOf, semantics, node.states, node.history);
if (ce) {
return { result: 'counterexample', trace: node.history.map((a) => a.name), states: node.states, explored, loop: ce.loop };
}
if (depth === bound) continue;
const s = node.states[node.states.length - 1];
for (const a of actions) {
if (!enabled(sys, a, s)) continue;
if (por && !canonicalAppend(sys, rankOf, node.history, a)) continue;
const s2 = applyAction(sys, a, s);
next.push({ states: node.states.concat([s2]), history: node.history.concat([a]) });
}
}
frontier = next;
if (frontier.length === 0) break;
}
return { result: 'none', trace: null, states: null, explored, loop: null };
}
function checkBMC(sys, opts = {}) { return search(sys, opts, true); }
function bruteForce(sys, opts = {}) { return search(sys, opts, false); }
/* ============================ CLI ============================ */
if (require.main === module) {
const fs = require('fs');
const argv = process.argv.slice(2);
const file = argv.find((a) => !a.startsWith('--'));
if (!file) {
console.error('usage: node ltlbmc.js instance.json [--bound N] [--semantics ltlf|lasso] [--no-por] [--brute]');
process.exit(2);
}
const inst = JSON.parse(fs.readFileSync(file, 'utf8'));
const get = (flag) => { const i = argv.indexOf(flag); return i >= 0 ? argv[i + 1] : undefined; };
const sys = normalizeSystem(inst);
const opts = {
bound: get('--bound') !== undefined ? Number(get('--bound')) : (inst.bound !== undefined ? inst.bound : 8),
semantics: get('--semantics') || inst.semantics || 'ltlf',
por: !argv.includes('--no-por'),
};
const run = argv.includes('--brute') ? bruteForce : checkBMC;
const r = run(sys, opts);
process.stdout.write(JSON.stringify({
result: r.result === 'counterexample' ? 'counterexample' : 'no-counterexample-up-to-k',
k: opts.bound,
semantics: opts.semantics,
trace: r.trace,
loopStart: r.loop,
exploredStates: r.explored,
}, null, 2) + '\n');
}
module.exports = {
parseExpr, parseFormula, toNNF, normalizeSystem,
evalLTLf, evalLasso, initialState, stateKey, enabled, applyAction,
isIndependent, formulaHasX, checkBMC, bruteForce, canonicalAppend,
};
node ltlbmc.js instance.json # POR, finite-trace semantics
node ltlbmc.js instance.json --brute # reference enumeration
node ltlbmc.js inst.json --semantics lasso # infinite ultimately-periodic
node ltlbmc.js inst.json --bound 6 --no-por
Programmatic:
const { normalizeSystem, checkBMC, bruteForce } = require('./ltlbmc.js');
const sys = normalizeSystem(instance);
const r = checkBMC(sys, { bound: 7, semantics: 'ltlf' });
// r = { result: 'counterexample' | 'none', trace, states, explored, loop }
test.js)$ node test.js
reduction-friendly: brute=97656 por=792 ratio=123.30x
counterexample: brute=32 por=22 trace=["inc0","inc0","inc0"]
lasso: brute=6 por=6 trace=["set","keep"] loop=1
26 passed, 0 failed
| # | Test | Result |
|---|---|---|
| 1 | LTLf hand semantics (X at end = false, p U q, G, lasso F/G) |
pass |
| 2 | Reduction-friendly, full bound, no counterexample | 123.30x fewer states |
| 3 | Counterexample + lexicographic minimality | brute = POR = ["inc0","inc0","inc0"] |
| 4 | Lasso semantics, loop recorded, brute = POR | pass |
| 5 | 400 randomized systems, brute vs. POR (finite trace) | 0 mismatches |
| 6 | 200 randomized systems, brute vs. checker (lasso) | 0 mismatches |
| 6b | Regression: lasso instance where forced POR diverges; shipped checker disables POR and agrees | pass |
verify_canonical.js)This is the load-bearing correctness property of the reduction:
$ node verify_canonical.js
canonical-representative verification: OK
It builds the graph whose edges swap adjacent independent letters, takes connected components (Mazurkiewicz classes), computes each class's lexicographically least word, and compares that set against the words produced by the incremental canonicalAppend rule — 60 random independence relations, word lengths 0..5, exact set equality.
Forcing canonical POR under lasso semantics gave 26 divergences in 20 000 random instances. Minimal reproducing instance:
variables: v0,v1,v2 : bool
actions: a0: v1:=!v1, v2:=true // a1: v0:=!v0
formula: G(p U !p) // p = v0, q = v1, r = v0||v1
["a0","a1","a0","a0"] (loop starts at index 2);none, because the unique lexicographically minimal representative never revisits the loop state.The shipped checker disables POR for semantics:"lasso", so its answer again equals brute force. This is the correct trade-off given "must agree with brute-force enumeration on every supplied instance".
$ node ltlbmc.js /tmp/ce.json
{
"result": "counterexample",
"k": 5,
"semantics": "ltlf",
"trace": ["inc0", "inc0", "inc0"],
"exploredStates": 4
}
| Defect | Fix | Evidence |
|---|---|---|
| Exponential enumeration | canonical Mazurkiewicz POR | 123.3x fewer states |
| LTLf/lasso semantics conflation | two exact evaluators (suffix fold / fixpoints) | semantic unit tests + randomized differential |
Unsound POR with X |
auto-disable unless supplied relation | guard in search() |
| Unsound POR for lasso loops | disable POR under lasso | 26/20000 divergence reproduced, regression test |
| Arbitrary/non-minimal trace | BFS by depth + lex order + least class rep | trace equality with brute force |
| Spurious transitions | simultaneous update + domain checks | applyAction |
# Evidence - Problem class: node-ltl-bmc-partial-order-minimal-counterexample - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-29T04:35:03.535Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Implement a bounded model checker for LTL over finite traces on a small imperative language: parse a transition system plus an LTL formula in NNF, unroll to bound k, search for lasso-shaped counterexamples, and apply partial-order reduction that is sound for the supplied independence relation. Output either no-counterexample-up-to-k together with the explored-state count, or the lexicographically shortest counterexample trace. The checker must agree with brute-force enumeration on every supplied instance while exploring at least 5x fewer states on the reduction-friendly ones.", "environment": "node20", "language": "js", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "node-ltl-bmc-partial-order-minimal-counterexample", "provider": "openrouter", "solved_at": "2026-09-29T04:35:03.535Z", "version": "20"}