February 2018 - Spot

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

2 5

bug spot online
by MATTEO LUCCHI 22 Mar '18

22 Mar '18

Good afternoon, You are probably already aware of that, but the spot online translator is not working anymore. I am trying to translate a LTL formula into a Buchi Automaton. It was working until 2 days ago, but now i get this: Traceback (most recent call last): File "/var/www/html/cgi-bin/spotcgi.py", line 732, in <module> render_automaton(degen, dont_run_dot) File "/var/www/html/cgi-bin/spotcgi.py", line 318, in render_automaton render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname) File "/var/www/html/cgi-bin/spotcgi.py", line 305, in render_dot_maybe render_dot(autprefix, hoaname) File "/var/www/html/cgi-bin/spotcgi.py", line 237, in render_dot run_dot(basename, 'svg') File "/var/www/html/cgi-bin/spotcgi.py", line 230, in run_dot os.link(outname, tmpdir + "/" + ext) FileNotFoundError: [Errno 2] No such file or directory: '../spotimg/960f234ef7d2cd7d8fbab23c49603c6a66fc284d.svg' -> '../spotimg/0f33f8af71a0356e3d63971bc8a4a7e39e64b7d9-154/svg' Any fix to the problem? Thank you! Kind Regards, Matteo Lucchi

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