Spot January 2018

spot@lrde.epita.fr

2 participants
2 discussions

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

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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot January 2018