(AND/IF_1.0 % This spec violates rule Y in state 0 (NFA (NAME Non-Y) (INTERPRETATION Verhoeff/XDI) (SYMBOLS (a INPUT) (b OUTPUT) (c OUTPUT) ) (STATES (0 INITIAL TRANSIENT) (1 TRANSIENT) (2 BOX) (3 BOX) (4 TRANSIENT) ) (TRANSITIONS (0 1 a) (1 2 b) (0 3 b) (3 4 a) (4 2 c) ) ) )