Hello,
I am trying to convert a LTL formula to Buchi automata in MATLAB. I want to
know if you have any script or library that can help me do this?
Thank you and best regards,
Alina Popa
--
Fourth-year Student | Automatic Control and Applied Informatics | Systems
Engineering
Faculty of Automatic Control and Computer Engineering
“Gheorghe Asachi” Technical University of Iasi, Romania
www.ac.tuiasi.ro
<http://www.ac.tuiasi.ro/> | www.tuiasi.ro <http://www.tuiasi.ro/>
Dear Spot Team,
I'm a master's student at Technical University of Munich and I'm currently writing my Master's Thesis in the research field of path planning for autonomous cars.
I came across Spot on the internet and I think it's a very nice tool that fits exactly my needs: I've got a discrete finite automaton (with certain attributes/APs per node) and I want to check, if this automaton satisfies a certain LTL specification. Especially, my intention is to find all path in my automaton, that satisfy a LTL specification. I've already installed Spot on my computer and tried to implement this with Python. Now I've got the following two questions:
1. What is the most simple and fastest way of defining a spot kripke graph, based on my own automaton (which is basically just a dictionary with nodes, that hold certain attributes and parent/child relations) ? Is there a possibility of including my nodes and transitions step by step into a spot kripke graph or do I have to convert my automaton at first into e.g. the HOA format and afterwards import this HOA-string as a kripke graph?
2. Building the product of a LTL formula (resp. the Büchi automaton) with the kripke graph leads to a object of the class twa_product. Is there a possibility of transforming this product back into a kripke structure or exporting it as a simple dictionary, so that I can make further computations on this "reduced" graph?
I hope you can help me with my questions and maybe provide some simple code examples. Thank you very much in advance!
Yours sincerely,
Patrick Halder
Hello,
I have noticed two types of errors that seem to occur when telling ltl2tgba to output unambiguous Büchi automata (UBA).
One seems to be some kind of assertion triggering and happens only in combination with the flag „—low“. That is,
on running:
ltl2tgba —low -U -B -f $FRML
the tool occasionally exits with exit code 2 and:
„ltl2tgba: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true“
This happens for example for the formula:
(G(!(G("2")))) & (("1") | (F("2")))
In some cases the UBA generated by ltl2tgba seem to be incorrect as well, and I don’t think this has to do with the „—low“
flag. An example formula is
(("2") W (G("1"))) -> (G("1"))
To reproduce these behaviors you can run ltlcross on the attached file „error“, as follows:
cat error | ltlcross —-lbt-input ‚ltl2tgba -U -B —-low -f %f >%O' 'ltl2tgba -f %f >%O'
Best regards,
Simon
Hello,
I'm new to spot and a bit of a novice with coding in general but I've been
running into an issue related to one of the modules that comes with spot
when attempting to run python code using the spot python bindings:
File "/usr/lib/python3.6/importlib/__init__.py", line 126, in
import_module
return _bootstrap._gcd_import(name[level:], package, level)
ModuleNotFoundError: No module named '_impl'
I understand if it is too difficult to diagnose with the limited output,
but I didn't want to bombard anyone with lengthy output. I am running
Ubuntu 18.04 (Bionic Beaver) and have successfully installed spot using
./configure, make, make install. Prior to installing spot, I also installed
the latest version of swig. I've also verified that the relevant .so files
are located within my .local/lib/python3.6/site-packages/spot directory.
If this issue with using import_module to locate the _impl package looks
familiar, any information would be much appreciated.
Thank you!
Best,
Lonnie
--
"But as for you, promote the kind of living that promotes right teaching."
--Titus 2:1
The web page https://spot.lrde.epita.fr/ipynb/stutter-inv.html shows how to use Spot to highlight the states in a Büchi automaton which have a stutter invariant language. It says "Such a procedure gives us map of where POR can be enabled when model checking using such an automaton.” Does anyone know a reference for this technique? I mean specifically the idea that POR is something that can be turned on or off depending on the current state of the property automaton. I feel I’ve seen that somewhere, but don’t remember where.
Thanks!
-Steve
Hello,
I am trying to set up a automated build for Spot in a docker like environment. The build errored during the `make` step. I have been able to run it fine on my machine, so I hope it is just a dependency/version issue. Do you have any idea what dependency I could be missing?
I did not installed anything besides python3-dev and got provided with an alpine linux distribution with gcc 7 already installed, this is the configuration I have:
Configuration:
OS: Alpine Linux
Gcc --version: gcc (GCC) 7.1.0
G++ --version : g++ (GCC) 7.1.0
Clang --version: clang version 6.0.1
Spot source:
https://gitlab.lrde.epita.fr/spot/spot/-/jobs/21303/artifacts/download
(spot 2.6.3 dev)
The build script :
apk add python3-dev
cd $WORKSPACE/srcdir
unzip download
tar -xzf spot-2.6.3.dev.tar.gz
cd spot-2.6.3.dev
./configure --prefix=$prefix --host=${target}
make -j${nproc}
make install
Extract of the log :
make[3]: Entering directory '/workspace/srcdir/spot-2.6.3.dev/spot/misc'
/bin/bash ../../libtool --tag=CXX --mode=compile /opt/x86_64-linux-gnu/bin/x86_64-linux-gnu-g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib -W -Wall -Werror -Wzero-as-null-pointer-constant -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Wmissing-declarations -Wnoexcept -Woverloaded-virtual -Wmisleading-indentation -Wimplicit-fallthrough -Wlogical-op -Wduplicated-cond -Wnull-dereference -Wsuggest-override -Wpedantic -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O -MT tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c -o tmpfile.lo tmpfile.cc
libtool: compile: /opt/x86_64-linux-gnu/bin/x86_64-linux-gnu-g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib -W -Wall -Werror -Wzero-as-null-pointer-constant -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Wmissing-declarations -Wnoexcept -Woverloaded-virtual -Wmisleading-indentation -Wimplicit-fallthrough -Wlogical-op -Wduplicated-cond -Wnull-dereference -Wsuggest-override -Wpedantic -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O -MT tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c tmpfile.cc -fPIC -DPIC -o .libs/tmpfile.o
tmpfile.cc: In function 'const char* spot::{anonymous}::get_tmpdir()':
tmpfile.cc:38:25: error: 'secure_getenv' was not declared in this scope
const char* res = secure_getenv("SPOT_TMPDIR");
^~~~~~~~~~~~~
tmpfile.cc:38:25: note: suggested alternative: '__secure_getenv'
const char* res = secure_getenv("SPOT_TMPDIR");
^~~~~~~~~~~~~
__secure_getenv
tmpfile.cc: In destructor 'virtual spot::temporary_file::~temporary_file()':
tmpfile.cc:91:32: error: 'secure_getenv' was not declared in this scope
static bool must_unlink = !secure_getenv("SPOT_TMPKEEP");
^~~~~~~~~~~~~
tmpfile.cc:91:32: note: suggested alternative: '__secure_getenv'
static bool must_unlink = !secure_getenv("SPOT_TMPKEEP");
^~~~~~~~~~~~~
__secure_getenv
make[3]: *** [Makefile:1284: tmpfile.lo] Error 1
make[3]: Leaving directory '/workspace/srcdir/spot-2.6.3.dev/spot/misc'
make[2]: *** [Makefile:1357: all-recursive] Error 1
make[2]: Leaving directory '/workspace/srcdir/spot-2.6.3.dev/spot'
make[1]: *** [Makefile:1274: all-recursive] Error 1
make[1]: Leaving directory '/workspace/srcdir/spot-2.6.3.dev'
make: *** [Makefile:1194: all] Error 2
Hi,
I'm attempting to compile under cygwin.
Calling configure (with --disable-python) succeeds, but make fails (with
error message as below).
The problem would appear to be the absence of 'secure_getenv', though FWIW
the generated makefile contains 'HAVE_SECURE_GETENV = 0'.
Any pointers on how I might get this to compile (preferably with minimum
disruption to the source or build process)?
Thanks and best wishes,
Jerry.
===============================
Error message:
/bin/sh ../../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I.
-I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib
-DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD
-std=c++14 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT
tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c -o tmpfile.lo tmpfile.cc
libtool: compile: g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../..
-I../../buddy/src -I../../lib -I../../lib -DNDEBUG -fvisibility=hidden
-fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O3 -ffast-math
-fstrict-aliasing -fomit-frame-pointer -MT tmpfile.lo -MD -MP -MF
.deps/tmpfile.Tpo -c tmpfile.cc -DDLL_EXPORT -DPIC -o .libs/tmpfile.o
tmpfile.cc: In function ‘const char* spot::{anonymous}::get_tmpdir()’:
tmpfile.cc:36:25: error: ‘secure_getenv’ was not declared in this scope
const char* res = secure_getenv("SPOT_TMPDIR");
^~~~~~~~~~~~~
tmpfile.cc: In destructor ‘virtual spot::temporary_file::~temporary_file()’:
tmpfile.cc:89:32: error: ‘secure_getenv’ was not declared in this scope
static bool must_unlink = !secure_getenv("SPOT_TMPKEEP");
[...]
make: *** [Makefile:1194: all] Error 2
===============================
Dear Spot maintainers,
I am a PhD student at the Stanford Intelligent Systems Lab (SISL), we are interested in implementing a Julia wrapper for Spot. So far I have prototyped a very simple version that calls the binary to write to a .hoa file, then parse the .hoa file and build an automata structure, I tried it on very simple formulas.
In the coming day I am going to call the c++ api of spot from Julia and extract the datastructure from it instead of writing my own parser. The idea would be that I can then manipulate the automata using native Julia objects.
I am looking at this example from the documentation:
https://spot.lrde.epita.fr/tut50.html
The explicit interface seems like what I am looking for, please let me know if I am missing other relevant examples.
If you are aware of some people working on this please let us know, we would be happy to contribute and join forces. Would you agree if we name the Julia package Spot.jl ?
Best,
Maxime
Dear SPoT developers,
I am writing to you to ask you a question about the semantics of PSL and SPoT. I will start by explaining my problem.
I am interested in computing the automata associated to a Linear Dynamic Theory under Linear Dynamic Logic semantics. The semantics can be found in the following paper:
https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf
Although the semantics are interpreted on finite traces I would be interested in using infinite traces. I found out that SPoT allows expressing PDL regular expressions on linear (infinite) traces, which is what I was looking for.
However, after checking the specification language, I found that the dynamic operators are not "exactly" the same as those of Linear Dynamic Logic. I mean, I was expecting to write [(true;true)*] p instead of {(1;1)[*]}[]->p to represent the even-state problem. My questions are the followings:
1) Do they allow to express the same properties ? and
2) How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ?
Kind regards,
Martin.
