Spot July 2017

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

can't compile spot
by Pedro Marquez 19 Jul '17

19 Jul '17

I downloaded the spot tar package and tried to compile it using ./configure, make, sudo make install. However, make reports the error: make: *** No targets specified and no makefile found. Stop. and sudo make install reports: make: *** No rule to make target 'install'. Stop. What's happening, what can I do? Thank you in advance, -Pedro Marquez, Prof.

2 1

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot July 2017