22 Jan
2018
22 Jan
'18
12:30 p.m.
Hi Yong,
Thank you for the report. It seems that this bug, which I can reproduce with Spot 2.4.4, was fixed in Spot 2.5.
The bug disappears after commit bd739a5712, a major rewrite of the determinization algorithm.
Best regards,
--
Alexandre Duret-Lutz
On Tue, Jan 16, 2018 at 10:05 AM, Yong Li liyong@ios.ac.cn wrote:
> Hi all,
>
> I am using SPOT by following command
>
> autfilt --equivalent-to=A.hoa B.hoa
>
> to check the equivalence of two Buchi automata A.hoa and B.hoa (attached).
>
> It returns nothing and it means two automata are not equivalent.
>
> But actually I used GOAL and RABIT to check the equivalence, they said yes.
>
> I think you may want to have a look.
>
>
> Regards,
>
> Yong
>
> --
> Yong Li (李勇),
> State Key Lab. of Computer Science
> Institute of Software, Chinese Academy of Sciences
>
>
> _______________________________________________
> Spot mailing list
> Spot@lrde.epita.fr
> https://lists.lrde.epita.fr/listinfo/spot
>