From: Vladimir Sipos (vlad_at_sipos-software.com)
Date: Tue Mar 23 2004 - 14:22:46 MST
Hi,
I ran ltl_to_aut given the following ltl formula:
i=0 * i =1 ;
I was not expecting to get any buechi automaton since the formula is contradiction.
However, the ltl_to_aut produced the following dot file:
digraph "(i=1 * i=0)" {
node [shape=ellipse];
size = "7.5,10"
center = true;
"title" [label="(i=1 * i=0)",shape=plaintext];
"n1" [label="n1\n{(i=1 * i=0)}\n()"];
"n2" [label="n2\n{}\n()"];
"init-n1" [style=invis]
"init-n1" -> "n1";
"n1" -> "n2";
"n2" -> "n2";
}
Why is this so?
Is there a way to set ltl_to_aut so that it does not create any automaton unless the formula is valid?
-VS
This archive was generated by hypermail 2.1.7 : Tue Mar 23 2004 - 14:25:05 MST