diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts index 3827183..69c5698 100644 --- a/examples/folio/sanderling/spec.ts +++ b/examples/folio/sanderling/spec.ts @@ -1,4 +1,5 @@ import { + DoubleTap, InputText, Tap, actions, @@ -95,7 +96,17 @@ const newAccountBalanceIsZero = always( }) ); -// Property 2: a newly-added ledger row changes the ledger balance by exactly its signed amount. +// Property 2: no single user action grows the ledger by more than one row. +// Reuses the existing ledgerRows extractor. +const noDuplicateTxnPerStep = always( + next(() => { + const prev = ledgerRows.previous?.length ?? 0; + const curr = ledgerRows.current.length; + return curr - prev <= 1; + }) +); + +// Property 3: a newly-added ledger row changes the ledger balance by exactly its signed amount. const newTxnChangesBalance = always( now(() => route.current === "ledger").implies( next(() => { @@ -165,8 +176,19 @@ const addTxn = whenRoute(route, ["home", "ledger", "add-transaction"], () => { return opts; }); +const doubleSubmitTxn = whenRoute(route, "add-transaction", () => { + const field = txnAmountField.current; + const submit = txnSubmit.current; + if (!field || !submit) return []; + return [ + InputText({ into: field, text: amounts.generate() }), + DoubleTap({ on: submit }), + ]; +}); + export const properties = { newAccountBalanceIsZero, + noDuplicateTxnPerStep, newTxnChangesBalance, }; @@ -176,9 +198,10 @@ export const setup = login; // adds breadth so the fuzzer wanders the whole app and types edge-case values // into every field, stressing the balance invariants above. export const actionsRoot = weighted( - [50, addAccount], - [40, addTxn], - [20, defaultActions], + [40, addAccount], + [30, addTxn], + [15, doubleSubmitTxn], + [15, defaultActions], ); (globalThis as { actions?: unknown; properties?: unknown; setup?: unknown }).actions = actionsRoot;