Download MONA Version 1.4 User Manual

MONA 1.4
Boolean function
a1 ∧ a2
a1 ∨ a2
a1 ⇒ a2
a1 ⇔ a2
mode
dfaAND
dfaOR
dfaIMPL
dfaBIMPL
Figure 14: Product operation modes
DFA *dfaProject(DFA *a, unsigned index ) - projects away track index from a and determinizes the resulting automaton.
void dfaRightQuotient(DFA *a, unsigned index ) - performs the right-quotient operation described in Section 3.1.
DFA *dfaMinimize(DFA *a ) - minimizes a , that is, constructs an automaton with the minimal number of states and BDD nodes accepting and rejecting the same languages as
the original automaton.
Analysis and printing
The following functions generate information about automata:
char *dfaMakeExample(DFA *a, int kind, int num, unsigned indices [])
generates a shortest satisfying example (if kind = +1) or a counter-example (if kind =
−1) to the formula represented by a using the technique described in Section 2.3. The
array indices of length num contains the free variables. The resulting char array is
the concatenation of the rows of ’0’s, ’1’s, and ’X’s of the example string.
void dfaAnalyze(DFA *a, int num, char *names [],
unsigned indices [], char orders [], int treestyle )
analyzes the automaton a and prints the results as shown in Section 2.3. The arrays
names , indices , and orders are for the free variables. These arrays have length num .
The array orders contains 0s, 1s, and 2s representing boolean, first-order, and secondorder respectively. If treestyle is non-zero, examples are written in GTA style.
void dfaPrintVitals(DFA *a ) - prints the number of states and BDD nodes in a .
void dfaPrint(DFA *a, int num, char *names [], unsigned indices []) - prints a textual description of a as shown in Section 2.4. The arguments num , names , and indices
are the number of free variables, their names, and their indices, respectively.
void dfaPrintGraphviz(DFA *a, int num, unsigned indices []) - prints a in dot format as illustrated in Figure 3.
void dfaPrintVerbose(DFA *a ) - prints a verbose textual description of a as illustrated
in Section 5.1.
65