alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
2043 commits 6 branches 0 tags 36 MiB
Commit graph

2043 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
f4381d59ce Add option --lbt-input to ltl2tgba. Factor it with ltlfilt. 
* src/bin/ltlfilt.cc: Extra input options into...
* src/bin/common_finput.cc, src/bin/common_finput.hh: ... these new
files...
* src/bin/ltl2tgba.cc: ... and use them here.
* src/bin/Makefile.am: Adjust.
 2012-09-18 21:44:58 +02:00
Alexandre Duret-Lutz
f02156ebff Various utf-8 fixes. 
* src/bin/ltl2tgba.cc: Add option -8.
* src/tgbatest/ltl2tgba.cc, wrap/python/spot.i: Enable utf8 on
sba_explicit_formula automata too.
 2012-09-18 21:12:09 +02:00
Alexandre Duret-Lutz
4ed153a247 * src/bin/ltl2tgba.cc: Fix display of BA. 2012-09-18 16:04:48 +02:00
Alexandre Duret-Lutz
10189b2d61 * src/tgbaalgos/postproc.cc: Misplaced call to scc_filter(). 2012-09-17 18:47:04 +02:00
Alexandre Duret-Lutz
675fc0bc67 * src/bin/genltl.cc (parse_opt): Add OPT_U_LEFT and OPT_U_RIGHT cases. 2012-09-17 18:03:04 +02:00
Alexandre Duret-Lutz
0c005c8159 More fixes for the OS X builds. 
* src/bin/common_r.hh: Include common_sys.hh first.
* src/sanity/80columns.test: Set LANG.
 2012-09-17 11:51:44 +02:00
Alexandre Duret-Lutz
42665b87b0 * src/bin/ltlfilt.cc: Add a --remove-wm option. 2012-09-17 11:08:10 +02:00
Alexandre Duret-Lutz
28e7d9aa4d Fix sanity failure on Mac OS X. 
* src/sanity/Makefile.am: Pass TOPBUILD to includes.test, and split the
tests in different targets.
* src/sanity/includes.test: Add include directories to bin/'s headers.
 2012-09-17 10:31:55 +02:00
Alexandre Duret-Lutz
d9dc1f489d Add a visitor to relabel the atomic proposition in formulas. 
* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/ltlvisit/clone.cc (recurse): Don't call clone(), nobody
needs that.  Instead, really recurse.
* src/bin/ltlfilt.cc: Add a --relabel option.
* src/bin/genltl.cc: Relabel formulas if --lbt is used.
* src/sanity/style.test: Tweak detection of i++.
 2012-09-16 21:30:54 +02:00
Alexandre Duret-Lutz
1a84c17ece Add an LTL printer in LBT's syntax. 
* src/ltlvisit/lbt.cc, src/ltlvisit/lbt.hh: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/bin/common_output.cc, src/bin/common_output.hh: Add
support for LBT output, and reporting formulae that cannot
be output in this syntax.
* src/bin/ltlfilt.cc: Pass filename and linenum to
output_formula() for better error reporting.
 2012-09-14 18:55:04 +02:00
Alexandre Duret-Lutz
106a14f8db Implement a parser for LBT's prefix syntax for LTL. 
* src/ltlparse/public.hh (parse_lbt): New function.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Implement it.
* src/bin/ltlfilt.cc: Use it.
 2012-09-14 18:34:54 +02:00
Alexandre Duret-Lutz
a010ebc805 Use more sba_explicit more often. 
* src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh
(minimize_dfa, minimize_wdba): Return a sba_explicit_number automaton
instead of tgba_explicit_number.
* src/tgba/tgbaexplicit.hh (declare_acceptance_condition): Fix code
so it works on sba as well.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Specialize
for sba instead of tgba_sba_proxy.
* src/tgbaalgos/neverclaim.hh: Point to degeneralize().
 2012-09-14 15:10:12 +02:00
Alexandre Duret-Lutz
807834ec41 Detect fail conditions on std::cout in user's tools. 
* src/bin/common_cout.cc, src/bin/common_cout.hh: New files.
* src/bin/Makefile.am: Add them.
* src/bin/ltl2tgba.cc, src/bin/ltlfilt.cc, src/bin/common_output.cc:
Report error when writing to std::cout failed.  This is mainly
motivated by ltlfilt not being killed by SIGPIPE on lip6's OSX
buildfarm (SIGPIPE is probably ignored when the build is started), but
it could detect other errors such as a disk full.
 2012-09-14 11:56:42 +02:00
Alexandre Duret-Lutz
70f51b2786 * src/tgbatest/wdba2.test: Adjust to yesterday's change to -kt. 2012-09-12 18:53:16 +02:00
Alexandre Duret-Lutz
6a3cf7538c bin/ltl2tgba: New user binary. 
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: New class to
capture the postprocessing logic.
* src/tgbaalgos/Makefile.am: Add them.
* src/bin/ltl2tgba.cc, src/bin/man/ltl2tgba.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* src/tgbatest/spotlbtt.test: Prune the list of configurations slightly.
* src/tgbatest/spotlbtt2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Adjust to
use the new binary.
* NEWS: Update.
 2012-09-12 18:53:16 +02:00
Alexandre Duret-Lutz
26deb56a9c Fix multiple inclusions of config.h. 
* src/bin/common_sys.hh: New file.
* src/bin/Makefile.am: Add it.
* src/bin/common_output.hh, src/bin/common_r.cc,
src/bin/common_range.cc, src/bin/genltl.cc, src/bin/ltlfilt.cc,
src/bin/randltl.cc: Include common_sys.hh instead of config.h.
 2012-09-12 13:19:17 +02:00
Alexandre Duret-Lutz
04b5e37055 Add count_nondet_states(aut) and is_deterministic(aut). 
* src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* wrap/python/spot.i: Wrap them.
* wrap/python/ajax/spot.in: Display count of nondeterministic
states.
* src/tgbatest/ltl2tgba.cc (-kt): Likewise.
* NEWS: Upadte.
 2012-09-12 08:27:38 +02:00
Alexandre Duret-Lutz
45e93ea16c * NEWS: Summarize recent changes. 2012-09-07 18:00:36 +02:00
Alexandre Duret-Lutz
2d1460a2bd Kill the gspn-ssp benchmark (it was not working anymore). 
* bench/gspn-ssp/: Delete recursively.
* bench/Makefile.am, README, configure.ac: Adjust.
 2012-09-07 18:00:36 +02:00
Alexandre Duret-Lutz
649e8e2def Kill src/ltltest/randltl and replace it by src/bin/randltl. 
* src/ltltest/randltl.cc: Delete.
* src/ltltest/Makefile.am (noinst_PROGRAMS, randltl_SOURCES): Remove.
* src/ltltest/reduc.test, src/ltltest/reducpsl.test,
src/ltltest/utf8.test, src/tgbatest/randpsl.test,
bench/emptchk/README: Adjust to use bin/randltl.
 2012-09-07 18:00:36 +02:00
Alexandre Duret-Lutz
1257893fb2 Kill src/ltltest/genltl now that src/bin/genltl does everything it did. 
* src/ltltest/genltl.cc: Delete.
* src/ltltest/Makefile.am (noinst_PROGRAMS): Remove genltl.
* src/tgbatest/ltlcounter.test, bench/ltlclasses/run,
bench/ltlcounter/run: Adjust to call bin/genltl.
 2012-09-07 18:00:36 +02:00
Alexandre Duret-Lutz
0990de50df Fix missing spaces after comma. 
* src/sanity/style.test: Fix the space-after-comma test.
* src/bin/randltl.cc, src/tgba/tgbaexplicit.hh: Add missing spaces.
 2012-09-07 18:00:24 +02:00
Alexandre Duret-Lutz
f19526a93f randltl: Output unique formulae by default. 
* src/bin/randltl.cc: Replace the --unique by an --allow-dups option.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
bc6fa22b13 * src/bin/randltl.cc: Add a --weak-fairness option. 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
134fbd203d * src/bin/Makefile.am: Use a static library for all common functions. 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
e43bc893fd randltl: add option to simplify formulas 
* src/bin/common_r.cc, src/bin/common_r.hh: New files, extracted from...
* src/bin/ltlfilt.cc: Here.
* src/bin/randltl.cc: Use them.
* src/bin/Makefile.am: Adjust.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
7274ca2bb7 Fix prototype of ltl_simplifier::ltl_simplifier. 
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Here.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
a80356e440 * src/ltlvisit/apcollect.hh: Improve doc. 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
760d75cc44 randltl: first stage of the reimplementation 
* src/bin/common_range.cc, src/bin/common_range.hh: New files,
extracted from...
* src/bin/genltl.cc: ... here.
* src/bin/randltl.cc, src/bin/man/randltl.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust.
* src/bin/man/genltl.x: Point to randltl(1).
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
a3e54af924 * src/bin/common_output.hh, src/bin/common_output.cc: Fix includes. 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
c96513b6b8 help2man: generate man pages for genltl and ltlfilt 
* tools/help2man, tools/x-to-1.in: New files, copied from gnulib
1af55d85d9762a679b4302d5995f05ccd883e956.
* configure.ac: Create x-to-1 and export CROSS_COMPILING.
* Makefile.am: Distribute help2man.
* src/bin/Makefile.am (SUBDIRS): New.
* src/bin/man/Makefile.am: New file.
* src/bin/man/genltl.x, src/bin/man/ltlfilt.x: New files.
* src/bin/genltl.cc: Document the RANGE in the options,
and move the bibliography to genltl.x.
* README: Document src/bin/man
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
e0873cc7d6 ltlfilt, genltl: factor the common output options. 
* src/bin/common_output.cc, src/bin/common_output.hh: New file
with the common output code.
* src/bin/Makefile.am: Add them.
* src/bin/genltl.cc, src/bin/ltlfilt.cc: Simplify, using
argp's children parser, and calling output_formula().
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
267183bda7 ltlfilt: update the exit status in the same way as grep 
* src/bin/ltlfilt.cc: Do it.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
24a8c03192 ltlfilt: add option to filter by implication or equivalence 
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Add a
implication() option.
* src/bin/ltlfilt.cc: Add options --implied-by, --imply, and
--equivalent-to.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
d1b8537f98 genltl: reimplement using argp, and allowing ranges. 
* src/bin/genltl.cc: New file.
* src/bin/Makefile.am: Add it.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
90279bd40c ltlfilt: use error() to report errors. 
* lib/error.c, lib/error.h, lib/msvc-inval.c, lib/msvc-inval.h,
lib/msvc-nothrow.c, lib/msvc-nothrow.h, m4/error.m4, m4/msvc-inval.m4,
m4/msvc-nothrow.m4: New files from gnulib
1af55d85d9762a679b4302d5995f05ccd883e956.
* lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Adjust.
* src/bin/ltlfilt.cc: Use error() and error_at_line().
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
8132f91867 ltlfilt: Call set_program_name(). 
* src/bin/ltlfilt.cc (main): Call set_program_name().
* lib/progname.c, lib/progname.h: New files, from gnulib
1af55d85d9762a679b4302d5995f05ccd883e956.
* lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Adjust.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
93f6e21759 Install gnulib to make sure we can use argp in ltlfilt. 
* lib/Makefile.am, lib/alloca.c, lib/alloca.in.h, lib/argp-ba.c,
lib/argp-eexst.c, lib/argp-fmtstream.c, lib/argp-fmtstream.h,
lib/argp-fs-xinl.c, lib/argp-help.c, lib/argp-namefrob.h,
lib/argp-parse.c, lib/argp-pin.c, lib/argp-pv.c, lib/argp-pvh.c,
lib/argp-xinl.c, lib/argp.h, lib/asnprintf.c, lib/basename-lgpl.c,
lib/dirname-lgpl.c, lib/dirname.h, lib/dosname.h, lib/errno.in.h,
lib/float+.h, lib/float.c, lib/float.in.h, lib/getopt.c,
lib/getopt.in.h, lib/getopt1.c, lib/getopt_int.h, lib/gettext.h,
lib/intprops.h, lib/itold.c, lib/malloc.c, lib/memchr.c,
lib/memchr.valgrind, lib/mempcpy.c, lib/printf-args.c,
lib/printf-args.h, lib/printf-parse.c, lib/printf-parse.h,
lib/rawmemchr.c, lib/rawmemchr.valgrind, lib/size_max.h,
lib/sleep.c, lib/stdalign.in.h, lib/stdbool.in.h, lib/stddef.in.h,
lib/stdint.in.h, lib/stdio.in.h, lib/stdlib.in.h, lib/strcasecmp.c,
lib/strchrnul.c, lib/strchrnul.valgrind, lib/strerror-override.c,
lib/strerror-override.h, lib/strerror.c, lib/string.in.h,
lib/strings.in.h, lib/stripslash.c, lib/strncasecmp.c,
lib/strndup.c, lib/strnlen.c, lib/sys_types.in.h, lib/sysexits.in.h,
lib/unistd.in.h, lib/vasnprintf.c, lib/vasnprintf.h, lib/verify.h,
lib/vsnprintf.c, lib/wchar.in.h, lib/xsize.h, m4/00gnulib.m4,
m4/alloca.m4, m4/argp.m4, m4/dirname.m4, m4/double-slash-root.m4,
m4/errno_h.m4, m4/exponentd.m4, m4/extensions.m4, m4/float_h.m4,
m4/getopt.m4, m4/gnulib-cache.m4, m4/gnulib-common.m4,
m4/gnulib-comp.m4, m4/gnulib-tool.m4, m4/include_next.m4,
m4/intmax_t.m4, m4/inttypes_h.m4, m4/longlong.m4, m4/malloc.m4,
m4/math_h.m4, m4/memchr.m4, m4/mempcpy.m4, m4/mmap-anon.m4,
m4/multiarch.m4, m4/nocrash.m4, m4/off_t.m4, m4/printf.m4,
m4/rawmemchr.m4, m4/size_max.m4, m4/sleep.m4, m4/ssize_t.m4,
m4/stdalign.m4, m4/stdbool.m4, m4/stddef_h.m4, m4/stdint.m4,
m4/stdint_h.m4, m4/stdio_h.m4, m4/stdlib_h.m4, m4/strcase.m4,
m4/strchrnul.m4, m4/strerror.m4, m4/string_h.m4, m4/strings_h.m4,
m4/strndup.m4, m4/strnlen.m4, m4/sys_socket_h.m4, m4/sys_types_h.m4,
m4/sysexits.m4, m4/unistd_h.m4, m4/vasnprintf.m4, m4/vsnprintf.m4,
m4/warn-on-use.m4, m4/wchar_h.m4, m4/wchar_t.m4, m4/wint_t.m4,
m4/xsize.m4, tools/snippet/_Noreturn.h, tools/snippet/arg-nonnull.h,
tools/snippet/c++defs.h, tools/snippet/warn-on-use.h: New files from
gnulib 1af55d85d9762a679b4302d5995f05ccd883e956.
* configure.ac, Makefile.am: Adjust to compile gnulib.
* src/bin/Makefile.am: Adjust to use gnulib.
* README: Mention lib/.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
f38f9df020 * src/ltlvisit/tostring.hh: Cosmetics. 2012-09-04 14:47:48 +02:00
Alexandre Duret-Lutz
a0e1a144ad ltlfilt: initial implementation. 
* src/bin/ltlfilt.cc, src/bin/Makefile.am: New files.
* src/Makefile.am (SUBDIRS): Add bin.
* configure.ac: Add src/bin/Makefile.am.
* README: Document src/bin/.
 2012-09-04 14:47:48 +02:00
Alexandre Duret-Lutz
eb5de929ca ta: compatibility with Swig 1.3. 
* src/ta/taexplicit.hh (state_ta_explicit): Hide contents from Swig.
* src/ta/ta.hh (scc_stack_ta): Hide class from Swig.
 2012-09-04 14:32:42 +02:00
Alexandre Duret-Lutz
5939d6f493 Add back the '*' syntax for And. 
This somehow revert changes from 2010-01-30 which killed this use of
star to make room for the Kleen star.  Here we only allow '*' in the
temporal formula, so that it can still be the Kleen star in SERE.  The
motivation for '*' available as And is better compatibility with Wring
and VIS.

* src/ltlparse/ltlscan.ll: Distinguish * from [*].
* src/ltlparse/ltlparse.yy: Allows * to be used as AND between
temporal formulae.
* src/ltltest/equals.test, src/ltltest/parse.test: Add a few
tests.
* doc/tl/tl.tex: Document it.
 2012-08-29 18:05:31 +02:00
Alexandre Duret-Lutz
60ec3acea0 Add an option to use WDBA only if it reduces the size of the automaton. 
* src/tgba/tgbaexplicit.hh (num_states): New method.
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
(minimize_obligation): Add a reject_bigger option.
* src/tgbatest/ltl2tgba.cc (-RM): New option.
* src/tgbatest/spotlbtt.test: Test -RM.
* bench/ltl2tgba/algorithms: Include -RM in addition to -Rm, and
replace -RDS by -RIS.
* NEWS: Mention this.
 2012-08-28 14:39:17 +02:00
Alexandre Duret-Lutz
f7af4e65f6 CGI: Do not call any simulation on WDBA's success. 
* wrap/python/ajax/spot.in: Here.
 2012-08-24 13:38:04 +02:00
Alexandre Duret-Lutz
70306d184e CGI: Better call of scc_filter. 
* wrap/python/ajax/spot.in: Account for reverse and iterated simulations
when calling scc_filter the first time.
 2012-08-24 13:14:18 +02:00
Alexandre Duret-Lutz
dce79ffed5 * NEWS: Summarize recent changes. 2012-08-22 15:16:46 +02:00
Alexandre Duret-Lutz
8cb68d76b5 * NEWS, buddy/src/bddop.c, m4/valgrind.m4: s/wether/whether/. 2012-08-22 13:53:59 +02:00
Alexandre Duret-Lutz
2ea652d32c Cleanup ltl2tgba.cc. 
* src/tgbatest/ltl2tgba.cc: Fix some typos, and factor the second
call to scc_filter when simulations are used.
 2012-08-21 16:38:49 +02:00
Alexandre Duret-Lutz
74bd671350 Add cosimulation and iterated_simulations to the web interface. 
* wrap/python/spot.i (cosimulation, iterated_simulations): Declare.
* wrap/python/ajax/spot.in, wrap/python/ajax/protocol.txt,
wrap/python/ajax/ltl2tgba.html: Add options to trigger these two
optimizations.
 2012-08-21 16:26:28 +02:00
Alexandre Duret-Lutz
84b6240aa9 * src/tgbaalgos/simulation.hh: Improve documentation. 2012-08-21 15:34:18 +02:00