- Spot - LRE

Spot build fails
by Maxime Bouton 11 Nov '18

11 Nov '18

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

2 3

Compilation under Cygwin
by Jerry Swan 29 Oct '18

29 Oct '18

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 ===============================

2 2

Julia bindings for Spot
by Maxime Bouton 05 Oct '18

05 Oct '18

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

2 1

SPoT + PSL + Dynamic Logic.
by Martin Dieguez 05 Oct '18

05 Oct '18

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.

2 1

SPoT + PSL + Dynamic Logic.
by Martin Dieguez 03 Oct '18

03 Oct '18

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.

1 0

Potential Bug in Spot?
by Andreas Tollkötter 25 Sep '18

25 Sep '18

Hello, with the currently newest version of Spot 2.6.1, the following behavior occurred for me, which I would call a bug. I attached a DOT file of a deterministic parity automaton which was written by "autfilt --dot --highlight-languages". What is notable that (among other pairs), states 10 and 66 are marked as language-equivalent states. Their "a1"-successors, 30 and 62 are not equivalent however, so something must be wrong here. I assume a potential cause is that there are a total of 18 non-trivial equivalence classes but only 16 different colors defined to be used by Spot, so some are used for multiple classes? If that is the case, I feel like there should be at least a warning output by "autfilt" when this happens. Best regards, Andreas Tollkötter

2 1

ltlfilt does not exhaustively simplify when --remove-wm is enabled
by Simon Jantsch 23 Sep '18

23 Sep '18

Hello, I am confused by the fact that the following two commands do not produce the same result: ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --simplify=3 The first command gives the same formula as: ltlfilt --simplify=3 --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --remove-wm which makes me believe that simplification is done before removing the operators M and W. I would expect ltlfilt to first remove the operators and then simplify exhaustively. Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators? Best regards, Simon

2 1

spot-2.6.1 conflicts with libiconv-1.14: it installs the file lib/charset.alias
by Yuri 10 Aug '18

10 Aug '18

Installing spot-2.6.1... pkg-static: spot-2.6.1 conflicts with libiconv-1.14_11 (installs files into the same place). Problematic file: /usr/local/lib/charset.alias *** Error code 70 Please remove this file. Thanks! Yuri

3 4

--disable-doxygen doesn't disable doxygen
by Yuri 10 Aug '18

10 Aug '18

gmake[5]: Leaving directory '/wrkdirs/usr/ports/math/spot/work/spot-2.6.1/doc' rm -rf spot.html spot.latex doxygen gmake[4]: doxygen: Command not found Version 2.6.1 on FreeBSD. Thanks, Yuri

2 2

Multiple accepting runs for Buchi Automaton
by Thakur Neupane 10 Aug '18

10 Aug '18

Hello, I am using SPOT to work with Buchi Automaton. Does SPOT supports finding all the accepting runs instead of only one? Sincerely, Thakur Neupane

2 1