Library

NWA · Weak ω-regular

Never two a's, with a needless guess

@thethinkmachine·version 1·CC BY 4.0·added 28 Sept 2026

A nondeterministic weak automaton for the same safety property as the DWA, with a redundant branch that leaves the SCC constraint intact.

Open in AutomataStudio
More
Open in the desktop app Download the .automaton file Source on GitHub
okjust saw…ok (copy)deadbabaa, bbba
The machine as drawn — 4 states, 9 transitions.

The author’s examples, run

(b) → accept(ab) → acceptb(ab) → acceptba(b) → accept(a) → rejectaa(b) → reject(aab) → reject