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

2305 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
13025d6cc8 * src/tgbaalgos/cycles.hh: Add virtual destructor. 2012-09-22 01:14:07 +02:00
Alexandre Duret-Lutz
3c17c418a2 Speedup is_weak_scc() if all transitions in the SCC are accepting. 
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Speedup when
all transitions are accepting.
 2012-09-21 15:12:23 +02:00
Alexandre Duret-Lutz
d228784c39 Don't pass the automaton to enumerate_cycle and is_weak_scc. 
The scc_map knows the automaton already.

* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Simplify the
interface.
* src/tgbatest/ltl2tgba.cc: Adjust calls.
 2012-09-21 15:12:16 +02:00
Alexandre Duret-Lutz
40de47f159 dve2: use postprocessor to simplify the code. 
* iface/dve2/dve2check.cc: Use postprocessor to simplify the code.
* iface/dve2/dve2check.test: Adjust to some different output values
when a counterexample is found, caused by nondeterminism introduced by
the orders of transitions.
 2012-09-21 15:10:13 +02:00
Alexandre Duret-Lutz
09b540315a * NEWS: Reorganize and update recent changes. 2012-09-21 15:10:13 +02:00
Alexandre Duret-Lutz
92e37998b2 Better documentation for the cycle enumeration algorithms. 
* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/isweakscc.hh: Improve .doc
* src/tgbaalgos/isweakscc.cc (weak_checker::cycle_found):
Scan the DFS backward so we only look at the cycle part.
 2012-09-21 11:15:12 +02:00
Alexandre Duret-Lutz
420fcd62e4 Add a is_weak_scc() function based on cycle enumeration. 
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Add a -KW option.
* src/tgbatest/cycles.test: Test it on a small example.
 2012-09-20 19:46:48 +02:00
Alexandre Duret-Lutz
374a489e3f Implement Loizou & Thanisch's algorithm for enumerating cycles. 
* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbatest/cycles.test: New files.
* src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Add a -KC option for testing.
 2012-09-20 18:05:14 +02:00
Alexandre Duret-Lutz
379e0d5eb4 * src/tgba/tgbascc.cc: Cosmetics. 2012-09-19 22:13:58 +02:00
Alexandre Duret-Lutz
64f0f653e3 * src/bin/ltl2tgba.cc: Fix cases where --stats is not used... 2012-09-19 22:13:41 +02:00
Alexandre Duret-Lutz
f3a2675588 * src/bin/ltl2tgba.cc: Improve documentation. 2012-09-19 10:29:10 +02:00
Alexandre Duret-Lutz
26ad32d561 ltl2tgba: Add a --stats option. 
* src/bin/ltl2tgba.cc (--stats): New option.
* src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh (stat_printer): New
class.
 2012-09-19 00:33:39 +02:00
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