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
On Thu, Feb 27, 2020 at 10:33 AM Ranjana N <ranjana.nallamalli(a)gmail.com> wrote:
>
> The following website:
>
> spot.lrde.epita.fr
Thanks. Our sysadmin said he banned all non-french IPs two days ago
because of a DDOS attack that would fill the ram of our shared web
server in just 1sec. Unfortunately he had no time yesterday to work
on this.
He tried to lift the ban a few minutes ago, and the server went down
in a couple of seconds again. He is currently trying to look for a
smaller range of IPs to block.
--
Alexandre Duret-Lutz
Dear all,
I was wondering if there exists an option to disable the generation of
the documentation.
Thank you in advance,
Best,
Jaime
--
--------------------------------------------------------------
Jaime Arias https://lipn.univ-paris13.fr/~arias
CNRS Research Engineer (LoVe Team)
LIPN, CNRS UMR 7030
Institut Galilée - Université Paris 13
99 Avenue Jean-Baptiste Clément, F-93430 Villetaneuse, France
tel:[+33] 01 49 40 40 67
--------------------------------------------------------------
Have been trying to access the resources at your website but not getting
through. Is the site down?
Kindly throw some light.
Thanks & Regards
Ranjana
New Delhi
To whom it may concern,
I am having Ubuntu 16.04 and my python3 version is 3.5.2 (default version
from Ubuntu 16.04). After installing with the default configuration setting
(installing from a tarball), I am able to import spot in python3 but
"print(spot.version())" gives me this error: "AttributeError: module 'spot'
has no attribute 'version'".
Also, when trying "sudo apt-get install python3-spot", I am getting this
error: "The following packages have unmet dependencies:
python3-spot : Depends: python3 (>= 3.7~) but 3.5.1-3 is to be installed
E: Unable to correct problems, you have held broken packages."
I was wondering if you could help me with this issue. Thank you!
Best,
Yoon
--
*Yoonchang Sung*
Postdoctoral Associate
Massachusetts Institute of Technology
Computer Science and Artificial Intelligence Laboratory
32 Vassar St. / Room 32-335
Cambridge, MA 02139
USA
Hi Spot Team,
I am trying to compile Cyclist (cyclist-prover.org) against the latest
version (2.8.6) of Spot, and I am getting an error.
Cyclist is including spot/twa/twa.hh, and when compiling I get the
following error:
In file included from
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/twa/acc.hh:28:0,
from
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/twa/twa.hh:27,
from src/soundness/proof_aut.hpp:4,
from src/soundness/proof_aut.c:1:
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/misc/bitset.hh:
In constructor ‘spot::bitset<N>::bitset(spot::bitset<N>::word_t)’:
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/misc/bitset.hh:57:5:
error: constexpr constructor does not have empty body
}
^
In fact, I also get this error when trying to compile again versions
2.6.3 and 2.7.5 too.
When I try to compile against version 2.5.3, I get the error that there
is no such file spot/twa/twa.hh.
Is this a bug, or has the API changed? If the latter, how should I
update my code to use the newer versions?
Thanks,
Reuben
--
Lecturer, Dept of Computer Science
Royal Holloway, University of London
Egham
Surrey
TW20 0EX
Tel: +44 (0)1784 276827
