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(a)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(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/spot