- Spot - LRE

A bug in determinization procedure of Spot?
by Anton Pirogov 22 Mar '18

22 Mar '18

Hello, first I just want to say, thanks for creating Spot, it is immensely useful! And I think that I might have found a bug (or two). My inputs are classic state-based NBAs. I rely on Spot to compare and verify my determinized automata, i.e. I compare the automaton that my tool produces with the one I get from Spot using autfilt -D -S -p (to get a deterministic parity automaton). I use autfilt --equivalent-to=... for the equivalence test. Yesterday I noticed something strange. When I compare the original NBA and my DPA, it reports that they are equivalent. Same for the original NBA and the DPA I get from Spot. But when I compare my automaton with the one from Spot, it says that the languages are different! So the first thought was - something must be broken in the equivalence test. Apparently, at least one of the three answers I got is wrong. So I used a little Python script using the Spot API to get a word where two of the automata do not agree on. Let's call the original NBA A, my DPA B and the one from Spot C. There were no words found in A×¬B, ¬A×B, A×¬C, ¬A×C and also B×¬C. But there IS a word in ¬B×C. I used this word with autfilt --accept-word=... to check A, B and C. And it turned out that in fact A and B do not accept the word, but C does, i.e. C is incorrect. So, to conclude, there seems to be a bug in the determinization and the problem is not detected by the equivalence test between A and C. I don't know about Spot internals, but if the equivalence test is using the same determinization procedure to complement A for the required products, then the bug in the equivalence test is a consequence of the problem in the determinization (i.e., the equiv. test compares the wrong DPA with basically itself), so the issues might be related. It might be useful to know that I found the problem using Spot 2.4.4 and it is still present in the current version 2.5.1. I also attach the smallest automata A, B and C that illustrate the issue and the script I used to search for the counterexample. You can check that: cat aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 0 and autfilt -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 1. I hope this helps. Thanks and best regards, Anton Pirogov

2 1

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335478点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2229572857咨询
by 傅瑶 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【336248点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2300040163咨询
by 高俏秀 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335418点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2813339771咨询
by 孟荔娜 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【336478点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2810009279咨询
by 邱秋铭 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335648点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2415932228咨询
by 何世 10 Feb '18

10 Feb '18

1 0

Possible Bug in SPOT
by Yong Li 22 Jan '18

22 Jan '18

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

2 1

Bug in ltlcross manual
by František Blahoudek 28 Dec '17

28 Dec '17

Hi, I think there is a bug in the manual of ltlcross. There is the paragraph > If the translator produced a Streett or Rabin automaton, these columns > contains the size of a TGBA (or BA) produced by ltlcross from that > Streett or Rabin automaton. Check in_states, in_edges, in_transitions, and in_acc for statistics about the actual input automaton. which seems no longer to be valid as I have no such columns in the output files created by ltlcross v. 2.4.4. Best, Fanda Blahoudek

2 1

genaut --ks-nca error
by Florian Barta 18 Oct '17

18 Oct '17

Hi, when using genaut --ks-nca e.g. genaut --ks-nca=1..10 I get the following error: genaut: print_hoa(): automaton is complete but prop_complete()==false Is this a bug? What can I do to get the desired result? I am using spot version 2.4.1 on Ubuntu 16.04. Best regards, Florian Barta

2 1

is_tt and is_ff in Python bindings
by František Blahoudek 18 Oct '17

18 Oct '17

Hi, I have found out that is_tt and is_ff does nt work as expected in Python. See the attached notebook for details. Best, Fanda Blahoudek

2 1