Commit graph

2407 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
7cfda699e6 Upgrade to gnulib 6b8f1dd1a21ce49319795391e21adf645b64db3c.
* m4/absolute-header.m4: New file.
* lib/Makefile.am, lib/argp-fmtstream.h, lib/argp.h, lib/error.c,
lib/gethrxtime.h, lib/intprops.h, lib/localcharset.c,
lib/quotearg.c, lib/stdio.in.h, lib/strerror-override.h,
lib/sys_time.in.h, lib/timespec.h, lib/unistd.in.h, lib/verify.h,
lib/wctype.in.h, lib/xalloc.h, lib/xsize.h, lib/xtime.h,
m4/configmake.m4, m4/extern-inline.m4, m4/gnulib-comp.m4,
m4/include_next.m4, m4/unistd_h.m4: Update to today's gnulib.
2013-12-17 17:04:11 +01:00
Alexandre Duret-Lutz
0afb9fe103 * src/tgba/tgbaunion.hh: Remove unused private member. 2013-12-16 10:27:39 +01:00
Alexandre Duret-Lutz
2febbd5929 * NEWS, configure.ac: Bump version to 1.2.1a 2013-12-11 11:38:27 +01:00
Alexandre Duret-Lutz
4d7638a269 Release Spot 1.2.1.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.1.
2013-12-11 10:40:33 +01:00
Alexandre Duret-Lutz
f0bcab4add bin: support multi-line CSV fields.
* src/bin/common_finput.cc (job_processor::process_stream): Read
multi-line CSV fields.
* src/ltltest/lbt.test, src/tgbatest/nondet.test: Add tests.
2013-12-06 13:45:55 +01:00
Alexandre Duret-Lutz
6c21089599 ltlcross: end CSV lines with \n, not \r\n
* src/bin/ltlcross.cc (print_stats_csv): Revert the recent
addition of \r, it is caussing too many issues.
* NEWS: Mention it.
2013-12-06 11:29:31 +01:00
Alexandre Duret-Lutz
846e33b9e5 ltl2tgba: Add a --csv-escape option and document CSV I/O.
* src/bin/common_output.cc, src/bin/common_output.hh:
(output_formula_checked, aut_stat_printer): New.
* src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call
output_formula_checked() instead of output_formula().
* src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape.
* doc/org/csv.org: New file to document CSV I/O.
* doc/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org,
doc/org/tools.org: Link to csv.org
2013-12-06 11:09:36 +01:00
Alexandre Duret-Lutz
0faea814da bin: add support for reading formulas from CSV files.
* NEWS: Mention it.
* src/bin/common_finput.cc, src/bin/common_finput.hh: Implement it.
* src/bin/common_output.cc, src/bin/common_output.hh: Add the %< and
%> escapes.
* src/bin/ltlfilt.cc: Connect %< and %> to the
prefix andsuffix of the input, and document them.
* src/tgbatest/det.test, src/tgbatest/nondet.test: Simplify these
tests that read CSV files.
2013-12-06 11:09:36 +01:00
Alexandre Duret-Lutz
8c5875314c * doc/org/satmin.org: Typo 2013-12-06 11:09:11 +01:00
Alexandre Duret-Lutz
0fc189d186 * HACKING: Typos. 2013-11-28 18:44:28 +01:00
Alexandre Duret-Lutz
d719c706f4 ltlcross: report statistics about Rabin and Streett automata
* src/bin/ltlcross.cc: Implement it.
* src/bin/man/ltlcross.x, doc/org/ltlcross.org, NEWS: Document it.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltlcross3.test: Test it.
2013-11-22 08:59:13 +01:00
Alexandre Duret-Lutz
2b10745dfb ltlcross: support --products=+N
* src/bin/ltlcross.cc: Implement it.
* NEWS, doc/org/ltlcross.org: Document it.
* src/tgbatest/ltlcross3.test: Test it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
9577e5d528 * bench/dtgbasat/README: Do not mention VMCAI'14. 2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
3e3d320de5 doc: add suggestions for bibliographic references
* doc/org/tools.org, src/bin/man/genltl.x, src/bin/man/ltl2tgba.x,
src/bin/man/ltl2tgta.x, src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x,
src/bin/man/randltl.x: Add bibliographic references, mostly to
the ATVA'13 paper.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
f65c621a55 ltlcross: report exit_status and exit_code columns in CSV and JSON
* src/bin/ltlcross.cc: Report exit_status and exit_code columns in CSV
and JSON files.  Also output lines for failed translations, and add
a --omit-missing option to disable that.  Move the time column right
after exit_status and exit_code.
* src/bin/man/ltlcross.x: Document each column of the output.
* bench/ltl2tgba/tools: Use the "{name}cmd" notation.
* bench/ltl2tgba/sum.py: Adjust to the new columns.
* bench/ltl2tgba/README: Update to point to the man page for a
description of the columns.
* bench/ltl2tgba/Makefile.am: Build results.pdf as said announced in
README.
* bench/spin13/html.bottom: Update code to ignore these two new
columns and lines with null values.
* src/tgbatest/ltlcross3.test: Add tests.
* doc/org/ltlcross.org: Adjust examples.
* NEWS: Mention this.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
686a45484d ltlcross: report missing input/output sequence
* src/bin/ltlcross.cc: Fix it.
* src/tgbatest/ltlcross3.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
cf91a23711 tests: add some missing "set -e"
* src/ltltest/lbt.test, src/ltltest/utf8.test,
src/tgbatest/dbacomp.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlcross2.test, src/tgbatest/ltlcrossce.test: Add set -e.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
7de25a32ef ltlcross: support short names
* NEWS: Mention it.
* doc/org/ltlcross.org: Document it.
* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
src/tgbatest/ltlcross4.test: Test it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
1c5536ea9c ltlcross: follow RFC 4180 for CSV output.
* src/misc/escape.cc, src/misc/escape.hh (escape_rfc4180): New
function.
* src/bin/ltlcross.cc: Do not output space after ',', use
"\r\n" for end of line, and use escape_rfc4180().
* NEWS: Mention it.
2013-11-22 02:13:50 +01:00
Alexandre Duret-Lutz
925a807f4f * doc/org/ltlcross.org: Show how to call ltl3dra and fix typos. 2013-11-22 02:07:13 +01:00
Alexandre Duret-Lutz
2cda03f8ce * doc/org/ltlcross.org: Typos, reported by František Blahoudek. 2013-11-11 18:51:12 +01:00
Alexandre Duret-Lutz
d415a23804 * src/bin/ltl2tgta.cc: Simplify using spot::translator(). 2013-10-22 17:55:29 +02:00
Alexandre Duret-Lutz
9dd59f1974 * README: Document utf8/. 2013-10-22 17:54:52 +02:00
Alexandre Duret-Lutz
fd80e944b5 * doc/tl/tl.tex: Typo. 2013-10-17 05:08:49 +02:00
Alexandre Duret-Lutz
54c01cfcdf * doc/org/ltlfilt.org: Typo. 2013-10-11 17:52:37 +02:00
Alexandre Duret-Lutz
f38570138d * src/ltlvisit/relabel.cc: Add more comments. 2013-10-01 18:32:57 +02:00
Alexandre Duret-Lutz
65dc65b061 * NEWS, configure.ac: Bump version to 1.2a 2013-10-01 13:48:40 +02:00
Alexandre Duret-Lutz
c0a845b274 Release Spot 1.2.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.
2013-10-01 13:23:47 +02:00
Alexandre Duret-Lutz
f48b5e507c * HACKING: Update version requirements for Bison and SWIG. 2013-10-01 11:02:33 +02:00
Alexandre Duret-Lutz
f3b87c85a2 Fix uninitialized variables in spot::postprocessor.
* src/tgbaalgos/postproc.cc: Initialize option
variables when opt is not given.
2013-09-30 20:32:54 +02:00
Alexandre Duret-Lutz
c0851a9559 * iface/dve2/finite.test: Work around Darwin's wc. 2013-09-30 20:32:54 +02:00
Alexandre Duret-Lutz
3c943d836a Add support for Bison 3.0.
We still want to remain compatible with Bison 2.7 so instead of fixing
all the new errors reported by 3.0 we silence some warning.  We should
fix these for good once Bison 3.0 is more widespread.

* m4/bison.m4: New file. Test if bison support -Wno-empty-rule and
-Wno-deprecated.  Define BISON and BISON_EXTRA_FLAGS.
* configure.ac: Do not test for yacc, use the above test instead.
* src/dstarparse/Makefile.am, src/eltlparse/Makefile.am,
src/kripkeparse/Makefile.am, src/ltlparse/Makefile.am,
src/neverparse/Makefile.am, src/tgbaparse/Makefile.am: Use BISON
and BISON_EXTRA_FLAGS.
* src/ltlparse/ltlparse.yy: Fix or and remove useless %right/%nonassoc
settings.
* src/eltlparse/eltlparse.yy: Likewise, and remove "%pure-parser".
2013-09-30 20:32:15 +02:00
Alexandre Duret-Lutz
5663872083 Work around some configurations of latexmk.
* src/ltltest/latex.test: Use latexmk -pvc- like in doc/tl/Makefile.am.
Reported by Étienne Renault.
2013-09-30 11:52:24 +02:00
Alexandre Duret-Lutz
df109869eb Generalize implication-based simplifications for multops.
And also speedup implication checks for Boolean expressions.

* src/ltlvisit/simplify.cc: Improve implication-based rules
rules for multops by checking one operand against all the
other at once (instead of one by one).  Do not break
Boolean expressions while performing implication checks.
* src/ltlvisit/simplify.hh: Typo.
* src/ltltest/reduccmp.test: More tests.
2013-09-29 21:06:09 +02:00
Alexandre Duret-Lutz
c01909e3ff Sort comutative binops like we sort multops.
* src/ltlast/formula.hh (is_literal): Rename as...
(get_literal): ... this.
(is_literal): New method.
(formula_ptr_less_than_multop): Rename as...
(formula_ptr_less_than_bool_first): ... this.
* src/ltlast/binop.cc: Use formula_ptr_less_than_bool_first.
* src/ltlast/multop.cc, src/ltlast/formula.cc: Adjust
to renamings.
2013-09-29 20:58:19 +02:00
Alexandre Duret-Lutz
228121c963 Include lib/ and config.h in ltlast/.
* src/ltlast/Makefile.am: Include lib/ in search path.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc,
src/ltlast/constant.cc, src/ltlast/formula_tree.cc,
src/ltlast/multop.cc, src/ltlast/nfa.cc,
src/ltlast/refformula.cc, src/ltlast/unop.cc: Include
config.h.
2013-09-28 16:02:18 +02:00
Alexandre Duret-Lutz
87b65b9bce relabel: implement relabeling of Boolean subexpressions.
* src/ltlast/multop.cc, src/ltlast/multop.hh (multop::boolean_operands,
multop::boolean_count): New methods.
* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh
(relabel): Take an optional relabeling_map as parameter.
(relabel_bse): New.
* src/ltltest/ltlrel.test, src/ltltest/ltlrel.cc: New files.
* src/ltltest/Makefile.am: Add them.
* src/bin/ltlfilt.cc: Add option --relabel-bool.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.
* doc/org/ltlfilt.org: Illustrate it.
2013-09-28 09:02:30 +02:00
Alexandre Duret-Lutz
2efe52fab0 * src/ltlvisit/clone.cc: Use reserve() for multop. 2013-09-27 16:22:58 +02:00
Alexandre Duret-Lutz
1f1feb935d * src/tgbaalgos/randomgraph.hh: Two typos, reported by Akim. 2013-09-27 14:38:03 +02:00
Alexandre Duret-Lutz
536e45b342 Arrange multops so that Boolean arguments come first.
This helps recursive implication checks.  Also order
atomic propositions with strverscmp().

* src/ltlast/formula.hh (formula_ptr_less_than_multop,
is_literal, atomic_prop_cmp): New.
* src/ltlast/formula.cc (is_literal, atomic_prop_cmp): Implement them.
* src/ltlast/multop.cc: Use formula_ptr_less_than_multop.
* src/ltltest/isop.test, src/ltltest/ltlfilt.test,
src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
src/tgbatest/nondet.test, src/tgbatest/tripprod.test: Adjust tests.
* NEWS: Mention the new order.
2013-09-26 17:14:58 +02:00
Alexandre Duret-Lutz
1f384c2c63 gnulib: Add module strverscmp.
* lib/strverscmp.c, m4/strverscmp.m4: New files.
* lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.
2013-09-26 17:14:58 +02:00
Alexandre Duret-Lutz
b486d4f1dc Fix compilation with g++-4.4.7.
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/reducerun.cc: Remove
superfluous definition of state_set.  Reported by František Blahoudek.
2013-09-26 16:29:36 +02:00
Alexandre Duret-Lutz
9b582691b7 * src/ltlvisit/simplify.cc: Cosmetics. 2013-09-23 10:58:04 +02:00
Alexandre Duret-Lutz
ce5ea829bd tools: Add a --format option
* src/bin/common_output.cc: Add option --format and implement
it.
* src/bin/ltlfilt.cc, src/bin/randltl.cc: Document the
supported %-sequences.
* src/bin/genltl.cc: Document the %-sequences, and supply
the name of the pattern to output_formula().
* doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltlfilt.org,
NEWS: Document it.
* src/ltltest/latex.test: Use it.
2013-09-22 23:56:56 +02:00
Alexandre Duret-Lutz
983feb5290 Add benchmark for our DTGBA SAT-minimization.
* bench/dtgbasat/: New directory.
* bench/Makefile.am: New file.
* configure.ac, README: Adjust.
2013-09-18 18:08:41 +02:00
Alexandre Duret-Lutz
3076c3da4e org: document SAT-based minimization
* doc/org/satmin.org, doc/org/satmin.tex: New files.
* doc/Makefile.am: Add them.
* doc/org/tools.org: Point to satmin.org.
* NEWS: Mention satmin.html.
2013-09-16 08:39:06 +02:00
Alexandre Duret-Lutz
cda847e207 satdtba: optimize number of clauses of variables
* src/tgbaalgos/dtbasat.cc: Skip variables of the form <q,q',q,q'>C or
<q,q',q,q'>R and replace them by <q,q'>G.
2013-09-16 08:31:43 +02:00
Alexandre Duret-Lutz
77cef16ca0 dtgbasat: Improve handling of weaks SCC in the ref automaton
* src/tgbaalgos/dtgbasat.cc: Here.
2013-09-16 08:31:43 +02:00
Alexandre Duret-Lutz
795c6e48d9 dtgbasat: get rid of the <q1,q1'>G variables
Reuse the existing <q1,q1',q1,q1',0,0> instead.

* src/tgbaalgos/dtgbasat.cc: Simplify.
2013-09-16 08:31:43 +02:00
Alexandre Duret-Lutz
b318b151c8 satmin: ignore (s,l,d2) if (s,l,d1) is already in result
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
2013-09-16 08:31:43 +02:00