//@ invariant dfa5.predict(input) > 0;
    protected DFA5 dfa5 = new DFA5(this);

    // the following dosen't play niece:
    //@invariant (input != null) ==> dfa5.predict(input) > 0;
    protected DFA5 dfa5 = new DFA5(this);