Shown below is a ProofChecker screen shot of a student's incorrect DFA for the language
L2 = {w over {a,b} | w contains aa and ends with ab} followed by a screen shot of the
correct DFA.
Note that the student correctly entered
the language for the accepting state, q3, as
endsWith("ab") && numberOf("aa")>=1.
ProofChecker determined that the student's DFA was indeed correct for all strings over the alphabet up to length 6, the number of states plus 2. However, when ProofGrader was used to compare the student's DFA with the correct DFA, they were not equivalent. A string of length 7 ("aabbbab") was found to be the shortest string in the language that was NOT accepted by the student's DFA.