This is the cgi-function for the automaton constructions.

write Automaton to a dot file to output stream ostr using statePrefix as name prefix of the states, and lblFun as optional function to give states an additional label (otherwise their name defined by statePrefix and their index is is used as the only label). The parameter "bundle" draws only one transition between a state pair that contains then the bundled list of input/output pairs instead of single transitions for each input and output combination between the same states.

convert Automaton to a corresponding Kripke structure

This function applies the Breakpoint construction to construct a deterministic automaton whose states are pairs of sets of states of the given automaton such that ((q,qf),a,(q',qf')) is a transition iff there were states s,s' in q and q', respectively with (s,a,s'), and qf is the subset of states of q where since the last breakpoint only accepting states could be used to reach these states. In addition to the automaton, the function also returns a mapping from new states to the state sets they represent.

Check some consistency properties of an automaton record. It is checked that all transitions are appropriate and that the

ComputeReachableStates computes the reachable states of an automaton which is given by the set of its state variables, its initial condition on the state variables, and the transition relation where the state variables and input variables (atoms) occur as well as BoolNext occurrences of the state variables (but not of the inputs). The procedure makes use of BDDs in that the transition relation is constructed with the variable ordering Xq1;...;XqN;q1;...;qN;a1;...;aM. Then, the inputs are existentially quantified in that the disjunction of the subtrees that start with (next) state variables is computed. Then, the reachable states are computed in a fixpoint computation where the conjunction with the modified transition relation and the so far computed reachable states is computed. The next states are then obtained by the disjunction of the subtrees starting with next state variables, but of course, that BDD must then be relabeled so it is expressed with the corresponding now state variables instead of the next state vars. Finally, the satisfying cubes are computed from the BDD of the reachable states, and these cubes are then extended to minterms which are encoded as sets of sets of state variables, so that a minterm corresponds with the state variables that have positive occurrences in the minterm. The function makes use of several computed tables to avoid computations on the same shared subtrees of the BDDs.

encode a deterministic Mealy machine by boolean state variables and compute the required boolean functions for output and state variables. Given an automaton, the function returns (sVars,iVars,oVars,sVars') which are the lists of state/input/output/next state variables, boolTransRel which is a list of transitions (qv,xv,yv,qv') where each component is a bitvector encoding a state, input, output and next state, a boolean expression transRel that is the transition relation even for nondeterministic automata, a boolean expression careSet on state and input variables careSet which denotes the care set and minBoolFun which is a map that maps variables in oVars and sVars' to corresponding boolean expression that define them in terms of state and input variables in case the given automaton is deterministic.

Check whether two given FSAs (on finite words) are equivalent to each other. The function returns a pair (isEqual,equal) where isEqual holds iff the two automata are equivalent, and equal is a boolean matrix that shows which states of the first automaton are equivalent to which states of the second automaton. Note that both automata have to be deterministic otherwise the result may not be correct.

This function compute for SR-, JK- and T-flipflops the control logic. These functions are stored in a map that maps next state variables to the control logic functions.

Minimize a given FSA (on finite words): Note that the given automaton has to be deterministic.

parsing an automaton from a string; the syntax is explained by the following example: inputs a,b; outputs c,d; init 0,1; transitions (0,a,c,1); (0,b,d,0); (1,a,d,1); (1,b,c,0); accept 1;

print input text for teaching tool

print the equivalence relation of EquivalentFSA or MinimalFSA

print the truth table for the output and next state variables

This function applies the Rabin-Scott subset construction to construct a deterministic automaton whose states are sets of states of the given automaton such that (q,a,q') is a transition iff there were states s,s' in q and q', respectively with (s,a,s'). In addition to the automaton, the function also returns a mapping from new states to the state sets they represent.

Convert a symbolic automaton to an explicit one where also the inputs are fully enumerated.

Convert a symbolic automaton to an explicit one where the input is kept as a formula on the input/output variables.

This is the cgi-function for converting symbolic automata to explicitly defined ones

This function computes a symbolic representation of a deterministic automaton for a given nondeterministic automaton using the breakpoint construction. The deterministic automaton is computed similarly to the one of SymbolicRabinScott, but adds additional state variables b[i] that denote if the corresponding states p[i] belongs to the breakpoint set.

This function computes a symbolic representation of a deterministic automaton for a given nondeterministic automaton. The nondeterministic automaton is given by its state variables, its initial condition, its transition relation, its acceptance condition, and the explicitly enumerated set of its reachable states in terms of minterms which are sets of state variables that contain those state variables that have positive occurrences in the minterm, i.e. which hold on the state. The latter can be computed by function ComputeReachableStatesByBdds. The determinization function associates then each reachable state (minterm, set of state variables) with a new state variable of the deterministic automaton whose name starts with the prefix "qDet". This way, a minterm on the new state variables corresponds with a set of sets of states of the nondeterministic automaton, since a minterm on the new state variables corresponds with a set of new state variables which is therefore a set of set of minterms of the old state variables, i.e., a set of set of states of the nondeterministic automaton. Details on the construction are given in MoSL08. Note that the transition equations are of the form next(pi) <-> p1&phi[i,1] | ... | pN&phi[i,N] where phi[i,j] is the set of inputs that trigger a transition from state pj to state pi in the nondeterministic automaton. This corresponds with the existential successor computation where pi is added to a successor state if one state pj can reach pi with input phi[i,j].

This function computes the transition monoid of the given automaton with further information: For every input symbol, we consister the state transitions induced by that input symbol as a boolean matrix and compute the closure of these boolean matrices under matrix multiplication. The resulting matrices form the transition monoid and partition all words of the input language into equivalence classes that lead to the same state transitions (considering all states). The result (matrix,transTable,assocInputs,aperiodic,period) of the function contains the matrices matrix[0..] of the monoid, their product table (where transTable[i,j] = p encodes that matrix[p] is the product of matrices matrix[i] and matrix[j]), assocInputs[i] is the set of inputs that induce matrix[i] (if the matrix is induced by inputs), period[i] is a pair ([i1,...,iN],p) such that p is the period of matrix[i] and [i1,...,iN] is the sequence obtained by computing exponents of that matrix. Finally, aperiodic holds if all periods are 1 which means that the automaton is noncounting, i.e., its monoid has only trivial subgroups, i.e., the automaton can also be expressed as a temporal logic formula.