From: Chao Wang (Wangc_at_colorado.edu)
Date: Thu Mar 25 2004 - 15:27:00 MST
Hi VS,
In the current VIS release, there is no option (of ltl_to_aut) that can
detect that.
This is because "ltl_to_aut" currently relies only on syntex
transformations -- it does not do much semantic checking (against a Model
or a Kripke structure). As a result, each "atomic proposition" is treated
as an atom.
Part of the reason that "ltl_to"aut" does not do semantic checking is
that, VIS allows multi-valued variables to be used in the LTL formula,
which complicated things: for example, it is not always true that (i=0 +
i=1) equals TRUE --- it is valid only if variable is a Boolean variable.
However, you raised a very good point; some semantic checking may
actually be done with the partial information. We will see how much
we can improve it in the next release.
Thanks,
Chao
On Tue, 23 Mar 2004, Vladimir Sipos wrote:
> 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 : Thu Mar 25 2004 - 15:29:48 MST