LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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 =====