Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:using_automata_to_decide_ws1s [2012/05/15 15:11] vkuncak |
sav08:using_automata_to_decide_ws1s [2012/05/15 15:38] vkuncak |
||
---|---|---|---|
Line 101: | Line 101: | ||
* if $q$ is a final state and $zero_x \in \Sigma$ is such that $zero_x(v)=0$ for all $x \neq v$, and if $\delta(q',zero_x)=q$, then set $q'$ also to be final | * if $q$ is a final state and $zero_x \in \Sigma$ is such that $zero_x(v)=0$ for all $x \neq v$, and if $\delta(q',zero_x)=q$, then set $q'$ also to be final | ||
- | **Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. | + | **Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. MONA syntax: |
+ | var2 Y; | ||
+ | ex2 X: ~(X sub Y); | ||
+ | Command to produce dot file: | ||
+ | mona -gw $1 | dot -Tps > output.ps | ||
**Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. Also compute the automaton for the formula $\exists X. (X < Y)$. | **Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. Also compute the automaton for the formula $\exists X. (X < Y)$. | ||
+ | |||
+ | Define less-than relation in MONA and encode this example. | ||
===== References ===== | ===== References ===== |