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
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
participants (2)
-
Alexandre Duret-Lutz -
Yong Li