Automated Grading of DFA Constructions

1 Introduction

There has been a lot of interest recently in offering collegelevel education to students worldwide via information tech-

∗This research is partially supported by NSF Expeditions in Computing awards CCF 1138996, and CCF 1016989.

Dileep Kini, Mahesh Viswanathan

Department of Computer Science Univ. of Illinois at Urbana-Champaign

nology. Several websites such as EdX (https://www. edx.org/), Coursera (https://www.coursera.org/), and Udacity (http://www.udacity.com/) are increasingly providing online courses on numerous topics, from computer science to psychology. Several challenges arise with this new teaching paradigm. Since these courses, often referred to as massive open online courses (MOOCs), are typically taken by several thousands of students located around the world, it is particularly hard for the instruction staff to provide useful personalized feedback for practice problem sets and homework assignments.

Our focus in this paper is on the problem of deterministic finite automata (DFA) construction. The importance of DFA in computer science education hardly needs justification. Beside being part of the standardized computer science curriculum, the concept of DFA is rich in structure and potential applications. It is useful in diverse settings such as control theory, text editors and lexical analyzers, and models of software interfaces. We focus on grading assignments in which a student is asked to provide a DFA construction corresponding to a regular language description. Our main goal is that of automatically measuring how far off the student solution is from the correct answer. This measure can then be used for two purposes: assigning a partial grade, and providing feedback on why the answer is incorrect.

Figure 1 shows five solutions from the ones we collected as part of an experiment involving students at UIUC. The solutions are for the following regular language description:

L = {s | s contains the substring "ab" exactly twice} For this problem the alphabet is Σ = {a, b}. Current technologies for this kind of problem [Aut, 2010] simply check whether the DFA proposed by the student is semantically equivalent to the correct one. For this particular example such a technique would only point out that the first solution A1 is correct, while all the other ones are wrong. Such a feedback, however, does not tell us how wrong each solution is.

The four DFAs A2,A3,A4, and A5 in Figure 1 are representative of different mistakes. We first concentrate on A2. In this attempt the DFA accepts the language

L1 = {s | s contains the substring "ab" at least twice}

This example shows a common mistake in this type of assignments: the student misunderstood the problem. We need an automated technique that is able to recognize this kind of mistake. The necessary ingredient to address this task is a procedure that, given a DFA A, can synthesize a description of the language L(A) accepted by A. Here a question that immediately arises is: what should the description language for L(A) be? Ideally we would like to describe L(A) in English, but such a description cannot be easily subjected to automated analysis. A better option is a logical language that is not only efficient to reason about, but one which also provides a rich set of primitives at a level of abstraction that is close to how language descriptions are normally stated in English. For this purpose, we extend a well-known logic, called monadic-second order logic (MSO) [Thomas, 1996; B¨uchi and Landweber, 1969], that can describe regular languages, and we introduce MOSEL, an MSO-equivalent declarative logic enriched with syntactic sugar. In MOSEL, the languages L and L1 can be described by the formulas |indOf 'ab'| = 2 and |indOf 'ab'| ≥ 2 respectively. Thanks to this formal representation, we can compute how far apart two MOSEL descriptions are from each other and translate such a value into a grade. To compute the distance between two descriptions we use an algorithm for computing the edit distance between trees [Bille, 2005]. We design two algorithms: the first one computes the DFA corresponding to a MOSEL description, and conversely the second one computes the MOSEL description of the language accepted by a DFA. Despite the high computational complexity of such algorithms, through several optimizations, we were able to make them work on examples used to learn automata. We executed the first algorithm on all the DFA assignments appearing in [Hopcroft et al., 2006], achieving running times below 1 second. On the same set of assignments we were able to execute the second algorithm on 95% of the problems, achieving running times below 5 seconds.

The approach presented in the previous paragraph is able to capture a particular class of mistakes. However, several DFAs, such as A3 in Figure 1, do not fall in this class. A3 has the full structure of the correct DFA but state 5 is not marked as final. A possible MOSEL description of A3 is |indOf 'ab'| = 2 ∧ endWt 'b' where the second conjunct indicates that all strings must end with a b. This description is syntactically far from the description of L causing the corresponding grade to be too low. This example shows that there should be a metric that tells how far A2 is from a correct DFA. To address this class of mistakes we introduce a notion of DFA edit distance that given a DFA A and a regular language R computes how many states and transitions of A we need to modify in order to obtain a DFA A′ that accepts R. Such a computation naturally translates into a grade.

The previous techniques cover two broad classes of mistakes. However, in several cases they are still not enough. The language accepted by the DFA A4 in Figure 1 has a complicated MOSEL description and the number of operations needed to "fix" A4 is quite high (more than 5) because we need to add a new state and redirect several edges. However, this solution is on the right track and behaves correctly on most of the strings. The student just did not notice that in state 4 the machine does not necessarily read the symbol a causing strings such as ababb to be rejected. Hence, A4 correctly rejects all the strings that are not in L, but also rejects "few" more. Following this intuition we introduce a notion of language density and we use it to approximate the percentage of strings in Σ∗ on which a DFA A misbehaves. Again, such a quantity naturally translates into a grade. We finally combine the three techniques to compute a unique grade.

DFA A5, despite being syntactically different from A2, computes exactly the same language as A2. This similarity might be hard to notice for a human. While our tool, using the same approach as for A2, assigned the same grade to both the attempts, we observed in our experiments that the same human grader assigned different grades.

We evaluated our tool on DFAs submitted by students at UIUC and compared the grades generated by the tool to those provided by human graders. First, we identified several instances in which two identical DFAs were graded differently by the same grader, while this was not the case for the tool. Second, we observed that the tool produces grades comparable to those produced by humans. In order to check such properties, we used statistical metrics to compare the tool with two human graders, and manually inspected the cases in which there was a discrepancy between the grades assigned by the tool and by the human. The resulting data suggests that the tool grades as well as a human, and we often found that, in case of a discrepancy, the grade of the human was less fair than that of the tool.

2 MOSEL: Declarative Descriptions of Regular Languages

This section provides a preliminary background on DFAs, defines the language MOSEL, and presents algorithms for transforming MOSEL descriptions into DFAs and vice-versa.

2.1 Background on DFAs

A deterministic finite automaton (DFA) over an alphabet Σ is a tuple A = (Q, q0, δ, F) where Q is a finite set of states, q0 ∈ Q is the initial state, δ : Q × Σ ↦→ Q is the transition function, and F ⊆ Q is the set of accepting states. We define the transitive closure of δ as, for all a ∈ Σ, s ∈ Σ∗ ,

δ∗ (q, as) = δ∗ (q′ , s), if δ(q, a) = q′ , and δ∗ (q, ε) = q. The language accepted by A is L(A) = {s | δ∗ (q0, s) ∈ F}.

2.2 The Language MOSEL

MOSEL was designed with the goal to be (a) expressive enough to describe problems that arise in common assignments, (b) simple enough to have a close correspondence to natural language descriptions so that the syntactic distance between MOSEL descriptions reflects the distance between their English language descriptions, and (c) succinct enough to have small descriptions for common DFA assignments.

The syntax and semantics of MOSEL can be found in the full version of this paper [Alur et al., ]. We illustrate features of this language through some examples. The 5 languages described in the first column of Table 1 can be described by the following MOSEL formulas:

• L1 = begWt 'a' ∧ |indOf 'ab'|% 2 = 1: strings that start with an a and have and odd number of ab substrings;
• L2 = |indOf 'a'| ≥ 2 ∨ |indOf 'b'| ≥ 2: strings that contain at least two a's or at least two b's;
• L3 = a@{x | |psLe x|% 2 = 1}: strings where every odd position is labeled with an a;
• L4 = begWt 'ab' ∧ |all|% 3 ̸= 0: strings that start with ab and with length not divisible by 3;
• L5 = |indOf 'ab'| = 2: strings that contain the substring ab exactly twice; and
• L6 = |indOf 'aa'| ≥ 1 ∧ endWt 'ab': strings that contain the substring aa at least once and end with ab.

2.3 FromMOSEL to DFAs

Next, we describe how we transform a MOSEL formula φ over an alphabet Σ into the corresponding DFA Aφ, such that Aφ describes the same language as φ. Since MOSEL only adds syntactic sugar to Monadic Second Order Logic (MSO) over strings, MOSEL formulas can be transformed into equivalent MSO formulas. In the first step of our transformation we inductively transform φ into an MSO formula φ′ . Next, we use standard techniques to transform an MSO formula into the corresponding DFA [Henriksen et al., 1995]. Such techniques inductively generate the DFAs corresponding to each sub-formula of φ′ and then combine such DFAs using automata operations. In the transformation fromMSO to DFA, the alphabet is enriched with bitvectors that represent the values of the quantified variables, causing the alphabet to grow exponentially in the number of nested quantifiers.

We implemented the transformation using the Automata library [Veanes and Bjørner, 2012]. This library relies on BDDs to succinctly represent large alphabets, making our transformation efficient in practice. During the inductive transformation we always keep the minimized DFA in order to avoid a blow-up in the number of states. For every exercise E appearing in [Hopcroft et al., 2006], our tool generated the DFA from the corresponding MOSEL description of E in less than 1 second.

2.4 FromDFAs to MOSEL

While it is well known that every DFA can be transformed into an equivalent MSO formula, in the standard transformation from DFA to MSO, the distance between MSO representations is not meaningful as it directly reflects the DFA structure rather than the accepted language. Since our goal is to use MOSEL descriptions to capture the syntactic difference between two languages, we use a different approach. Given a DFA A, we use an iterative deepening search to enumerate all possible MOSEL formulas and find the one that describes L(A). As we showed in the previous subsection, MOSEL descriptions of common DFA assignments are succinct. Thanks to such succinctness the brute force approach works adequately for our purpose.

Since typical formulas have small size/width, we use an iterative deepening search on the width of a formula. We next describe some optimizations that make this approach feasible in practice. In order to check whether a formula φ is equivalent to the target language, the simplest approach would be that of using the algorithm of Section 2.3 to generate the automaton Aφ corresponding to φ and then run a DFA equivalence algorithm. Such a procedure does not scale in practice. In our implementation we first check whether φ behaves correctly on some selected inputs and, only if it passes this test, we compute the DFA for φ and perform the equivalence test.

Next, we describe the procedure for generating the input test set. Given the input DFA A = (Q, q0, δ, F), we compute two sets P and N of positive and negative examples respectively, that is, P ⊆ L(A), and N ∩ L(A) = ∅. For every two states q1, q2 ∈ Q, we add the string sq1 pq1 to P, and the string sq2 nq2 to N, where δ∗ (q0, sqi ) = qi and δ∗ (qi, pqi ) ∈ F and δ∗ (qi, nqi ) ̸∈ F. Similarly, for every two states q1, q2 ∈ Q, and for every a ∈ Σ, we add the string sq1 apδ(q1,a) to P and the string sq2 anδ(q2,a) to N. The sets P and N contain at most |Q|2 |Σ| strings. Finally, for every DFA B = (QB, qB 0 , , δB, FB) such that |QB| ≤ |QA|, it is enough to test QB on the test sets P and N in order to check whether L(A) ̸= L(B). Therefore, if the minimal DFA corresponding to φ has fewer states than A, we detect the inequivalence of φ and A by simply testing the formula on P and N. In our experiments this technique yields a 300X speed-up.

Next, we optimized the algorithm for common cases in which the target formula is a disjunction or a conjunction. When we come across formulas φ1, φ2 which pass the negative test set N during the enumeration, we check if φ1 ∨ φ2 passes the positive test set P and follow it with an equivalence check if needed. Conjunctions are handled in a similar manner. This optimization permits to identify formulas of big width early in the search. For example, the tool was able to synthesize the formula describing the language in Figure 2 in less than a second. Without this optimization it would have taken more than 5 minutes to reach the corresponding formula in the enumeration.

Finally, we implemented several pruning techniques. First, using syntactic properties of the input DFA we can avoid enumerating some formulas. For example, if the DFA has only loops of size 1, and 2, the formula | |% 3 = can be statically ruled out. Secondly, we statically remove several terms that are equivalent to other terms of smaller width (¬¬φ). These pruning techniques caused a 500X speed-up on our test set of 30 examples. We tested the algorithm on the exercises in [Hopcroft et al., 2006] for which the alphabet only contained two elements.. For each exercise, given the corresponding DFA solution A, we were able to generate a MOSEL description of A in less than 5 seconds for 95% of the problems. In few cases, the MOSEL description was too big and the tool was not able to generate it.

3 An Algorithm for Grading DFA Constructions

We next address the problem of grading a student attempt. Given a target language LT , and a student solution As, we need a metric that tells us how far As is from a correct solution. Based on our experience related to teaching and grading DFA constructions, we identified three classes of mistakes:

Problem Syntactic Mistake: the student gives a solution for a different problem (see (2) and (5) in Figure 1);

Solution Syntactic Mistake: the student omits a transition or a final state (see (3) in Figure 1); and

Problem Semantic Mistake: the solution is wrong on a small fraction of the strings (see (4) in Figure 1).

We investigated three approaches that try to address each class. First, we use the classic notion of tree edit distance [Gao et al., 2010] to compute the difference between two MOSEL formulas. Secondly, we introduce a notion of DFA edit distance to capture the distance between DFAs. Last, we use the concept of regular language density to compute the difference between two languages when viewed as sets.

3.1 Problem Syntactic Distance

The following metric captures the case in which the MOSEL description of the language corresponding to As is close to the MOSEL description of the target language LT . This metric computes how syntactically close two MOSEL descriptions are. We consider MOSEL formulas as the ordered trees induced by their parse trees. Given a MOSEL formula φ, we call Tφ its parse tree. Given two ordered trees t1 and t2, their tree edit distance TED(t1, t2) is defined as the minimum number of edits that can transform t1 into t2. Given a tree t, an edit is one of the following operations:

relabel: change the label of a node n;

node deletion: given a node n with parent n′ , 1) remove n,

2) place the children of n as children of n′ , inserting

• them in the "place" left by n; and

node insertion: given a node n, 1) replace a consecutive subsequence C of children of n with a new node n′ , and 2) let C be the children of n′ .

We use the algorithm in [Gao et al., 2010] to compute TED. Next, we compute the distance D(φ1, φ2) between two formulas φ1 and φ2 as TED(Tφ1 , Tφ2 ). Finally, we compute WTED(φ1, φ2) def= D(φ1, φ2)/|Tφ2 |, where |T| is the number of nodes in T. In this way, for the same number of edits, less points are deducted for languages with a bigger description. Since we are ultimately interested in grading DFAs, given a DFA As we use the procedure proposed in § 2.4 to compute the formula φAs corresponding to As.

Example 1 Consider the language L corresponding to φ def= |indOf 'ab'|% 2 = 1 ∧ begWt 'a' over the alphabet

Σ = {a, b}. Let's assume the student provides the DFA A′ that implements the language φ′ def= |indOf 'ab'|% 2 = 1 ∨ begWt 'a', where ∧ has been replaced by ∨. The problem syntactic distance will yield the following values: TED(φ′ , φ) = 1, and WTED(φ′ , φ) = 1/9. In this case applying one node relabeling is enough to "fix" Tφ′ . We omit the parse tree of φ which contains 9 nodes. □

3.2 Solution Syntactic Difference

The following metric captures the case in which the student DFA As is syntactically close to a correct one, by computing how many edits are needed to transform As to make it accept the correct language LT . We define the notion of DFA edit distance. Given two DFAs A1, A2, we say that the difference between A1 and A2, DFA-D(A1,A2) is the minimum number of edits that can transform A1 into some DFA A′1 such that L(A′1 ) = L(A2). Given a DFA A, an edit is one of the following operations:

transition redirection: given a state q and a symbol a ∈ Σ, update δ(q, a) = q′ to δ(q, a) = q′′ where q′ ̸= q′′ ;

state insertion: insert a new disconnected state q, with δ(q, a) = q for every a ∈ Σ; and

state relabeling: given a state q, add it or remove it from the set of final states.

To take into consideration the severity of a mistake based on the difficulty of the problem, we compute the quantity WDFA-D(A1,A2) def= DFA-D(A1,A2)/k + t, where k and t are, respectively, the number of states and transitions of A2.

Example 2 Consider the DFA A3 in Figure 1 where state 5 is mistakenly marked as non-final. A1 is the correct solution for the problem. In this case

In the tool we compute this metric by trying all the possible edits and checking for equivalence with a technique similar to the one presented in Section 2.3.

A similar distance notion graph edit distance [Bille, 2005]. However this metric does not take into account the language accepted by the DFA.

3.3 Problem Semantic Difference

The following metric captures the case in which the DFA As behaves correctly on most inputs, by computing what percentage of the input strings is correctly accepted/rejected by As. Given two languages L1 and L2, we define density difference to be

Σn denotes the set of strings in Σ∗ of length n. Informally, for every n, the expression E(n) inside the limit computes the number of strings of length n that are misclassified by L1 divided by the number of strings of length n in L2. The max in the denominator is used to avoid divisions by 0. Unfortunately, the density difference is not always defined, as the limit may not exist.

Example 3 Consider the languages LA corresponding to |all|% 2 = 0 and LB corresponding to true (i.e. Σ∗ ) over the alphabet Σ = {a, b}. The limit DEN-DIF(LA, LB) is not defined since it keeps oscillating between 0 and 1. □

In practice we compute the approximated density A-DEN-DIF(L1, L2) def= (∑2k n=0 E(n))/2k +1, where k is the number of states of the minimum DFA representing L2. This approximation is not precise, but it is very helpful for capturing the cases in which the student forgot a finite number of strings in its solution (for example only ε).

Example 4 Consider the DFAs A1 and A4 in Figure 1 and their respective languages L(A1) and L(A4). In this case A-DEN-DIF(L(A4), L(A1)) = 0.09. This value is the one used to compute the grade shown in Figure 1. □

Similar notions of density have been proposed in the literature [Bodirsky et al., 2004; Kozik, 2005]. These definitions have good theoretical foundations, but, unlike our metric, they are undefined for most DFAs.

3.4 Combining the Approaches

The aforementioned approaches need to be combined in order to compute the final grade. We are aware of the many machine learning techniques that could be used for combining the three features, but instead, we decide to use a simple combination function for the following reason : 1) in the future we would like to extract feedback information from the computed grade, and 2) in general, only one of the three feature succeeds in computing a positive grade.

Next, we provide the general schema of the combining function. First, each deduction v, which ranges between 0 and 1, is scaled to a new value v′ using a formula of the form v′ := (v +c)2 - c2 where c is a constant. We used a training set of 60 manually graded attempts to identify the constants c for the combining function. Finally, we pick the metric which awarded the highest score.

4 Experimental Evaluation

The aim of our experiment is to evaluate to what extent the grades given by our tool and those given by human instructors agree. To do so we collected around 800 attempts at DFA construction questions by students taking a theory of computation course for the first time. For each problem we had two instructors and our tool grade each attempt separately. In order to see how well the tool does we compare statistics that reveal variation between human graders and variation between a human grader and our tool. To measure the extent of agreement between two graders we employ Pearson's correlation coefficient. The correlation coefficient is a number between -1 and 1. A value of 1 indicates that the paired points are linearly related with a positive slope. When this quantity is closer to 1 it indicates that the two measurements being compared tend to vary together in the same direction.

In order to obtain a basis for comparing the correlation coefficients we also see how a naive grader would perform with respect to human graders. There could be many ways to define a naive grader. A simple one that we consider uses the following grading scheme: (i) it awards near maximum (9 or 10) marks to the correct solutions, and (ii) for incorrect solutions it deducts marks based on the number of states that are lacking or in excess and adds a small random noise. We summarize the resulting calculations in Table 1.

Detailed Analysis In the following we only consider the first problem where the language is L1 = {s | s starts with a and has odd number of ab substrings}. The first column in the averages reads 0.99 for H1-H2 meaning that H1 has awarded, on average, 1 point more than H2. The next two columns show that H1 is on average closer to the naive grader N and to the tool T than it is to H2. However, the standard deviation for H1-N (2.62) is greater than that for H1-T (1.99), which means that the grades given by our tool show a lot less variation, and are in fact closer to H1 more often than N. The Pearson correlation coefficients shows that the degree of correlation between the tool T and H1 (0.83) is clearly better than that between N and H1 (0.65), and at the same time comes very close to the degree of correlation between two human graders H1 and H2 (0.87).

We say that two graders agree on an attempt with a threshold of t if the grades given by the two graders do not differ by more than t. The plot on the right shows 3 curves.

Each curve compares two graders and displays how the percentage of problems on which they agree increases with the threshold varying from 0 to 10. The three curves compare T, H2 and N against H1, and it

is easy to see that our tool T comes to an agreement much faster than N. More surprisingly, the tool also comes to an agreement faster than H2.

Figure 2 shows five cases in which either the human graders and the tool have a discrepancy. In case (1) the computed language L′1 is described by the formula |indOf 'b'|% 2 = 1 ∧ begWt 'a'. Since the MOSEL descriptions of L1 and L′1 are similar, the tool gives a high grade for this attempt. However, L′1 has an easier construction than L1. We attenuate these "false high grades" by deducting extra points when the size of the minimal DFA corresponding to the student solution has less states than the target DFA. Case (2) shows a DFA for which the language density is low, causing the tool to award this attempt with 7 points. One can argue that this grade is too high for such a DFA. However, the same DFA as (2) was submitted by multiple students, and, while the tool always awarded 7 points, both human graders were inconsistent: H1 graded five identical attempts with 4,5,7,7, and 7 points, while H2 awarded 1,1,2,3, and 8 points. Case (3) shows a DFA for which the DFA edit distance yields a too "generous" grade. For this DFA it is enough to remove the transition δ(0, b) in order to obtain a DFA that accepts L1. However, in this case the mistake is deeper than a simple typo. Case (4) shows a DFA for which the human awarded too high a score. Even though this DFA has several syntactic mistakes, H1 awarded the same grade as for attempt (5), where only one final state is missing. For case (5), where state 3 was mistakenly marked as non-final, both H1 and H2 lacked in consistency. H1 awarded different grades from 8 to 10 for 7 identical attempts.

Strengths of the tool Inspecting the data for the 131 attempts for the language L1 we observed the following: 1) in 6 cases one of the human graders mistakenly assigned the maximum score to an incorrect attempt; 2) in more than 20 out of 34 cases in which T and H1 were disagreeing by at least 3 points, H1, after reviewing the attempt, agreed with the grade computed of T; and 3) in more than 20 cases at least one of the human graders was inconsistent: i.e. two syntactically equivalent attempts were graded differently by the same grader.

Limitations The tool suffers two types of limitations: behavioral and structural. The former type concerns the failure of the grading techniques on some particular examples. An example is the attempt (3) of Figure 2 where a small DFA edit distance did not reflect the severity of the mistake. As for the structural limitations, our techniques are crafted to perform well on problems appearing in theory of computation books [Sipser, 1996; Hopcroft et al., 2006]. Such techniques do not scale for DFAs with large alphabets or many states. Moreover the MOSEL edit distance fails when the language does not admit a succinct description. We do not believe these to be actual limitations, because such situations typically do not arise in undergraduate level DFA constructions. However, we plan on extending our tool to deal with these cases.

5 RelatedWork

JFLAP [Rodger and Finley, 2006] is a mature system used widely for teaching automata and formal language theory. To the best of our knowledge JFLAP does not offer an automatic grading of DFA constructions.

Benedikt et.al have proposed a notion of regular language repairing [Benedikt et al., 2011]. Their approach could also be used for defining a grading metric, however, we believe that such metric would not be a good fit for our purposes since it cannot be associated with any natural feedback.

Singh et.al. have proposed an automatic grading framework for programming problems [Singh et al., 2013]. Given a error model in the form of expression rewrite rules, their system uses SAT based techniques to find the minimal number of corrections that can fix the student solution. Our syntactic edit distance approach is similar to this proposal.

There has been a lot of work in the AI community for building automated tutors for helping novice programmers learn programming by providing feedback about semantic errors [Adam and Laurent, 1980; Murray, 1987]. Such technologies share similar ideas with our tool in the way they measure distance from a correct solution.

6 Conclusion

We investigated the problem of grading DFA constructions. First, we introduced MOSEL, a declarative logic able to provide succinct and natural descriptions of regular languages appearing in automata theory textbooks. Second, we provided algorithms for transforming MOSEL descriptions into DFAs and vice-versa. Last, we presented three grading techniques based on three different classes of mistakes.

We evaluated our tool on DFAs submitted by real students and compared the grades generated by the tool to those provided by human graders. The results are encouraging and show that the tool grades as well as a human. In fact we plan on further engineering our tool, deploy it, and soon use it in real courses. We also plan on storing problem solutions in a database in order to speed up the grading and fix the few cases in which the tool does not assign a fair grade. We believe our techniques can provide foundations for generating automated feedback for students, and can be also adapted for other types of constructions. In particular we are working on automatically generating an inductive proof that a given DFA accepts a given language. Finally, this tool will not replace the need for teaching assistants (TAs), but it automates a task that often consumes several TA-hours. Although we only address a small problem, once a satisfactory grading tool for this problem is constructed, it will be used for a long time, since the concept of DFA will be always taught as it is now.