- 19 Sep, 2012 3 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/bin/ltl2tgba.cc (--stats): New option. * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh (stat_printer): New class.
-
- 18 Sep, 2012 3 commits
-
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* src/bin/ltl2tgba.cc: Add option -8. * src/tgbatest/ltl2tgba.cc, wrap/python/spot.i: Enable utf8 on sba_explicit_formula automata too.
-
Alexandre Duret-Lutz authored
-
- 17 Sep, 2012 5 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/bin/common_r.hh: Include common_sys.hh first. * src/sanity/80columns.test: Set LANG.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* 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.
-
- 16 Sep, 2012 1 commit
-
-
Alexandre Duret-Lutz authored
* 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++.
-
- 14 Sep, 2012 4 commits
-
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* src/ltlparse/public.hh (parse_lbt): New function. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Implement it. * src/bin/ltlfilt.cc: Use it.
-
Alexandre Duret-Lutz authored
* 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().
-
Alexandre Duret-Lutz authored
* 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.
-
- 12 Sep, 2012 4 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* 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.
-
- 07 Sep, 2012 20 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* bench/gspn-ssp/: Delete recursively. * bench/Makefile.am, README, configure.ac: Adjust.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* src/sanity/style.test: Fix the space-after-comma test. * src/bin/randltl.cc, src/tgba/tgbaexplicit.hh: Add missing spaces.
-
Alexandre Duret-Lutz authored
* src/bin/randltl.cc: Replace the --unique by an --allow-dups option.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Here.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* 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).
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* 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
-
Alexandre Duret-Lutz authored
* 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().
-
Alexandre Duret-Lutz authored
* src/bin/ltlfilt.cc: Do it.
-
Alexandre Duret-Lutz authored
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Add a implication() option. * src/bin/ltlfilt.cc: Add options --implied-by, --imply, and --equivalent-to.
-
Alexandre Duret-Lutz authored
* src/bin/genltl.cc: New file. * src/bin/Makefile.am: Add it.
-
Alexandre Duret-Lutz authored
* 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().
-
Alexandre Duret-Lutz authored
* 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.
-