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

182 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
cc1191cd66 ltlcross: fix --verbose --no-check crash 
Report from František Blahoudek.

* bin/ltlcross.cc: Do not display stats for automata
that do not exist.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the fix.
 2016-10-13 13:53:42 +02:00
Alexandre Duret-Lutz
a5d6aa2533 introduce SPOT_FALLTHROUGH to cope with -Wimplicit-fallthrough 
* NEWS: Mention the fix.
* HACKING: Mention the new macro.
* spot/misc/common.hh (SPOT_FALLTHROUGH): Add the macro.
* bin/randltl.cc, spot/misc/escape.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.hh, spot/tl/snf.cc, spot/twa/acc.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/sepsets.cc, spot/twaalgos/translate.cc: Use it.
 2016-10-07 21:29:34 +02:00
Alexandre Duret-Lutz
9ccdd8c618 genltl: add some formulas from Tabakov & Vardi (RV'10) 
* bin/genltl.cc: Implement the families.
* NEWS, bin/man/genltl.x: Document them.
* tests/core/genltl.test: Add a test.
 2016-10-03 17:41:14 +02:00
Alexandre Duret-Lutz
e2b4d38ade more file to ignore 
* bin/.gitignore, doc/org/.gitignore: Here.
 2016-10-03 16:15:35 +02:00
Alexandre Duret-Lutz
0c9c4be4ae bin: workaround flushing issues 
* bin/common_cout.cc (check_cout): Force a flush of cout if more than
20ms has elapsed since the last explicit flush.
* bin/common_setup.cc (setup): Untie cin and cout if the input
is not a TTY, so that cout is flush less often.
* NEWS: Mention the change.
 2016-10-03 15:27:06 +02:00
Alexandre Duret-Lutz
90214d7c39 genltl: fix typo in --help 
Reported by František Blahoudek.

* bin/genltl.cc: Here.
* NEWS: Mention it, and the typos previously fixed in spot-x.7.
 2016-09-15 15:36:53 +02:00
Alexandre Duret-Lutz
120118f66b man: two fixups for spot-x 
* bin/man/spot-x.x: Fix the example of SPOT_DEFAULT_FORMAT,
and clarify the text for SPOT_DOTDEFAULT.
 2016-09-06 12:24:43 +02:00
Alexandre Duret-Lutz
ed254ea19f man: fix an apostrophe 
* bin/man/ltl2tgba.x: Fix apostrophe.  It was appearing incorrectly in
the generated html pages.
 2016-09-05 14:01:44 +02:00
Alexandre Duret-Lutz
ca6435d847 help2man: update to 1.47.4 
Also disable i18n because that seems to be causing many problem to Mac
users building Spot for git and not knowing how to install
Locale::gettext.

* tools/help2man: Update from upstream, plus the two changes from
2b4cf8e7cb and
f7b65001e9.
* bin/man/Makefile.am: Remove the -L flag.
 2016-09-03 19:54:08 +02:00
Alexandre Duret-Lutz
571f0112ab bin: add options for --stats=%c 
* spot/twaalgos/stats.cc: Implement options.
* bin/common_aoutput.cc, NEWS: Document them.
* tests/core/format.test: Add some quick tests.
 2016-08-17 16:35:00 +02:00
Alexandre Duret-Lutz
4f0a630dbc stats: preparatory change of the implementation of %c 
This now holds the scc_info while processing the %c sequence, so that
using options we will soon be able to specify which SCC to count.

* spot/twaalgos/stats.hh, spot/twaalgos/stats.cc (printable_scc_info):
New class.
(state_printer): Use it for %c.
* spot/misc/formater.hh: Add move assignment.
* bin/common_aoutput.hh, bin/common_aoutput.cc: Use printable_scc_info
for %C.
* tests/core/format.test: Add a quick test case to make sure nothing
changed.
 2016-08-17 14:49:28 +02:00
Alexandre Duret-Lutz
70de1328d8 bin: hide the hoa_state_printer code 
* bin/common_aoutput.hh (hoa_state_printer::hoa_state_printer,
hoa_state_printer::print): Move the definition...
* bin/common_aoutput.cc: ... here.
 2016-08-17 13:42:13 +02:00
Alexandre Duret-Lutz
825332029c autfilt: implement %D, %N, %P, %W 
* bin/common_aoutput.cc, bin/common_aoutput.hh: Implement.
* tests/core/format.test: Test.
* NEWS: Mention.
 2016-08-16 19:20:12 +02:00
Alexandre Duret-Lutz
926ffbf965 bin: %a,%b,%s format specs for LTL output 
* NEWS: Mention those.
* bin/common_output.cc, bin/common_output.hh: Implement them.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Update
--help.
* tests/core/format.test: New file.
* tests/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org: Update documentation.
 2016-08-15 16:09:53 +02:00
Alexandre Duret-Lutz
e97ea5fa74 bin: diagnose more write errors 
* tests/core/full.test: New file.
* tests/Makefile.am: Add it.
* bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh,
bin/common_file.cc, bin/common_file.hh, bin/genltl.cc, bin/ltlcross.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Add diagnostics.
* NEWS: Mention the fix.
 2016-08-14 18:18:20 +02:00
Alexandre Duret-Lutz
ca0d81b5d7 autfilt, dstar2tgba: add CSV input 
Fixes #91.

* bin/autfilt.cc, bin/dstar2tgba.cc: Implement reading CSV files.
* bin/common_finput.cc: Fix comments.
* bin/common_aoutput.cc: Show %<, %> in help text.
* NEWS, doc/org/csv.org: Document it.
* tests/core/readsave.test: Add a short test case.
 2016-08-08 13:18:50 +02:00
Alexandre Duret-Lutz
f423c424eb bin: --stats=%H --stats=%h 
Part of #91.

* bin/common_aoutput.cc, bin/common_aoutput.hh: implement %H and %h.
* tests/core/readsave.test: Test them.
* NEWS: Mention it.
 2016-08-08 12:41:36 +02:00
Alexandre Duret-Lutz
0d753048ce formater: add support for double-quoted fields 
Part of #91.

* spot/misc/formater.cc, spot/misc/formater.hh: Here.
* bin/common_output.cc: Adjust automatic output format.
* doc/org/csv.org: Adjust.
* tests/core/lbt.test, tests/core/ltlfilt.test: More tests.
* NEWS: Mention the changes.
 2016-08-08 10:53:33 +02:00
Alexandre Duret-Lutz
14bee1ae7f implement conversion to GRA and GSA 
Fixes #174.

* spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc
(to_generalized_streett, to_generalized_rabin): New functions.
* spot/twa/acc.hh: Declare more methods as static.
* bin/autfilt.cc: Implement --generalized-rabin and
--generalized-streett options.
* NEWS: Mention these.
* tests/core/gragsa.test: New file.
* tests/Makefile.am: Add it.
 2016-08-04 22:24:30 +02:00
Alexandre Duret-Lutz
51afd4adfe ltlcross: prefer execl("/bin/sh", ...) to execlp("sh", ...) 
Fixes #98.

* bin/common_trans.cc: Here.
 2016-08-02 14:24:08 +02:00
Alexandre Duret-Lutz
7524e05128 ltlcross: bypass the shell for simple command 
For #98.

* bin/common_trans.cc: Here.
* NEWS: Mention it.
 2016-08-02 14:24:05 +02:00
Alexandre Duret-Lutz
59efe470ca ltlcross: show cross-comparison checks counterexamples 
Part of #38.

* bin/ltlcross.cc: Implement it.
* NEWS: Mention it.
* doc/org/ltlcross.org: Adjust example.
* tests/core/ltlcrossce2.test: New test case.
 2016-07-29 11:58:12 +02:00
Alexandre Duret-Lutz
64c7036660 active -Wsuggest-override where supported 
* m4/gccwarn.m4: Add the option.
* bin/autfilt.cc, bin/common_output.hh, bin/dstar2tgba.cc,
bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, spot/kripke/kripke.hh,
spot/ltsmin/ltsmin.cc, spot/ta/ta.hh, spot/ta/tgtaproduct.hh,
spot/taalgos/dot.cc, spot/taalgos/reachiter.hh,
spot/taalgos/statessetbuilder.cc, spot/taalgos/stats.cc,
spot/twa/twaproduct.cc, spot/twaalgos/emptiness.cc,
spot/twaalgos/gtec/ce.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ndfs_result.hxx, spot/twaalgos/stats.hh,
spot/twaalgos/tau03opt.cc, tests/core/ngraph.cc: Add suggested override
qualifiers.
 2016-07-27 10:30:10 +02:00
Alexandre Duret-Lutz
7534f62dba org: add autfilt decoration examples 
* doc/org/autfilt.org: Here.
* doc/org/hoa.org: Add a link to it.
* bin/autfilt.cc: Typo.
 2016-07-20 11:22:20 +02:00
Alexandre Duret-Lutz
dd6875d5fe bin: overhaul default input selection 
If no input have been specified, and the standard input is not a tty all
tools now default to reading it.  If standard input is a tty, all tools
display an error message.  Additionally, - is now a shorthand for -F- in
all tools.

* NEWS: Summarize this.
* bin/common_finput.cc, bin/common_finput.hh (check_no_formulas,
check_no_automaton): New functions that implement the above istty()
logic.
* bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc,
bin/ltlcross.cc, bin/ltldo.cc, bin/ltlgrind.cc: Use these function,
and recognize '-' if it was not the case.
* tests/core/acc_word.test, tests/core/ltldo.test,
tests/core/minusx.test, tests/core/readsave.test,
tests/core/unambig.test: Adjust some tests to exercise this.
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
doc/org/oaut.org: Adjust the documentation and simplify some
examples.
 2016-07-19 21:55:12 +02:00
Alexandre Duret-Lutz
4c0500a8a9 autfilt: add --stutter-invariant 
* bin/autfilt.cc: Implement the option.
* NEWS: Mention it.
* tests/core/readsave.test, tests/core/stutter-tgba.test: Add some
tests.
 2016-07-19 13:20:08 +02:00
Alexandre Duret-Lutz
014a9dbd6b twa: add accepting_run() and accepting_word() methods 
Fixes #153.

* spot/twa/twa.cc, spot/twa/twa.hh: Add the methods.
* bin/autfilt.cc, bin/common_aoutput.hh, bin/ltlcross.cc,
tests/python/highlighting.ipynb, tests/python/word.ipynb: Use
them to simplify the code.
* NEWS: Mention them.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
b13caea3d8 autfilt: --highlight-word 
* bin/autfilt.cc: Add the option.
* NEWS: Mention it.
* tests/core/acc_word.test: Test it.
* spot/twaalgos/emptiness.cc,
spot/twaalgos/emptiness.hh (twa_run::project): New method.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
57f47c16e7 genltl: support --positive and --negative 
* bin/genltl.cc: Implement these options.
* NEWS: Mention them.
* tests/core/genltl.test: New file with test cases.
* tests/Makefile.am: Add it.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
31a1dfbc6a autfilt: add --nondet-states=RANGE 
* bin/autfilt.cc: Here.
* tests/core/det.test: Test it.
* NEWS: Mention it.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
9af7001329 autfilt: swap transformation and filtering --help 
It makes more sense to keep the transformationn options near the
simplification options.

* bin/autfilt.cc: Reorder --help.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
b6cd54ab16 autfilt: add highlighting options for nondeterminism 
Fixes #123.

* bin/autfilt.cc: Add options --highlight-nondet-states=NUM,
 --highlight-nondet-edges=NUM, and  --highlight-nondet=NUM.
* spot/twaalgos/isdet.cc,
spot/twaalgos/isdet.hh (highlight_nondet_states,
highlight_nondet_edges): New functions.
* tests/core/det.test: Add test cases.
* NEWS: Mention them.
 2016-07-18 23:23:01 +02:00
Alexandre Duret-Lutz
486d9edad7 ltlcross: list collected automata on --verbose 
* bin/ltlcross.cc: Here.
 2016-07-13 17:33:39 +02:00
Alexandre Duret-Lutz
fafb135c87 isdet: update prop_deterministic in count_nondet_states() 
* spot/twaalgos/isdet.cc: Here.
* bin/ltlcross.cc: Simplify.
* NEWS: Update.
 2016-07-13 17:33:39 +02:00
Alexandre Duret-Lutz
a2f0b22810 ltlcross: fix swapped automata in error diagnostic 
Failures could be reported against "Comp(Ni)*Comp(Pj)" when
it was really "Comp(Nj)*Comp(Pi)" that failed.

* bin/ltlcross.cc: Here.
* NEWS: Mention the bug.
 2016-07-13 14:40:04 +02:00
Alexandre Duret-Lutz
91e8493c7f ltl2tgta: remove options --ba, --tgba, and friends 
* bin/common_post.cc, bin/common_post.hh: Add a "nooutput" variant of
the options.
* bin/ltl2tgta.cc: Use it.
* NEWS: Mention the fix.
 2016-07-06 15:03:22 +02:00
Alexandre Duret-Lutz
e419150c30 option_map: Diagnose unused option on request 
* spot/misc/optionmap.hh, spot/misc/optionmap.cc (report_unused_options,
set_, set_set_): New methods.
* bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc,
bin/ltl2tgta.cc: Call report_unused_options().
* tests/core/ltlcross2.test, tests/core/readsave.test: Fix typos in
options.
* tests/core/minusx.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention this.
 2016-06-22 20:57:53 +02:00
Alexandre Duret-Lutz
f7f353db68 bin: improve range diagnostic 
Fixes #181.

* bin/common_range.cc: Here.
* tests/core/ltlfilt.test: Add test case.
 2016-06-21 18:15:08 +02:00
Alexandre Duret-Lutz
b708ab778f genltl: add formulas from three papers 
Fixes #166.

* bin/genltl.cc: Add option --dac-patterns, --eh-patterns,
--sb-patterns.
* NEWS, bin/man/genltl.x, doc/org/genltl.org: Document them.
* bench/ltl2tgba/formulae.ltl: Delete.
* bench/ltl2tgba/known: Use genltl instead.
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README: Update.
* tests/core/ltl2tgba2.test: New test case, using genltl.
* tests/Makefile.am: Add it.
 2016-05-05 18:39:13 +02:00
Alexandre Duret-Lutz
79ef4e5a1e * bin/man/genltl.x: Typo. 2016-05-05 14:06:01 +02:00
Alexandre Duret-Lutz
d02ee34e10 doc: add a spot(7) man page 
Suggested by Akim Demaille.  Fixes #171.

* bin/man/spot.x, bin/spot.cc: New files.
* bin/man/Makefile.am, bin/Makefile.am: Add them.
* doc/org/tools.org, NEWS: Mention the new page.
 2016-05-02 10:41:41 +02:00
Alexandre Duret-Lutz
d9174593c8 common_trans: allow rewriting operators 
Part of #168.

* spot/misc/formater.cc: Adjust to support bracketed options.
* bin/common_trans.hh, bin/common_trans.cc: Use that to
support rewriting operators.
* doc/org/ltlcross.org, tests/core/ltldo.test: Add some examples.
* NEWS: Mention it.
 2016-05-01 21:05:49 +02:00
Alexandre Duret-Lutz
f5bfc07cfc autfilt: add --unused-ap and --used-ap 
Last part of #170.

* bin/autfilt.cc: Implement the new options.
* tests/core/remprop.test: Add a quick test.
* NEWS: Mention these options.
 2016-05-01 13:29:03 +02:00
Alexandre Duret-Lutz
95d16ba009 autfilt: add --remove-unused-ap 
Part of #170.

* bin/autfilt.cc: Here.
* tests/core/remprop.test: Test it.
* NEWS: Mention it.
 2016-05-01 13:03:18 +02:00
Alexandre Duret-Lutz
1ceb0ed272 autfilt: fix simpification of exclusive AP 
* bin/autfilt.cc: Here.
* tests/core/exclusive-tgba.test: Test it.
* NEWS: Mention the fix.
 2016-04-29 12:08:32 +02:00
Alexandre Duret-Lutz
9d5d1dc8dd doc: ltlcross is not only about Büchi anymore 
* bin/man/ltlcross.x, doc/org/ltlcross.org, doc/org/tools.org: Fix
one-line summaries.
 2016-04-21 17:13:13 +02:00
Alexandre Duret-Lutz
e50ff35d0f autfilt: add options to filter by SCC count and types 
* bin/autfilt.cc: Implement those options.
* NEWS: Mention them.
* doc/org/randaut.org: Add a quick example.
* tests/core/strength.test: Add some basic tests.
* tests/core/acc_word.test: Adjust options abbreviations.
 2016-04-21 16:56:45 +02:00
Alexandre Duret-Lutz
b79e307258 * bin/autfilt.cc: Typos in --help. 2016-04-21 14:43:32 +02:00
Alexandre Duret-Lutz
7d930359c1 ltldo: add option --errors 
* bin/ltldo.cc: Implement --errors.
* tests/core/ltldo.test: Test it.
* NEWS: Mention it.
 2016-04-21 14:39:56 +02:00
Alexandre Duret-Lutz
7144efabb9 hoa: add option to output version 1.1 
* spot/twaalgos/hoa.cc: Implement the option.
* bin/common_aoutput.cc, doc/org/hoa.org,
doc/org/oaut.org, spot/twaalgos/hoa.hh, NEWS: Document it.
* tests/core/strength.test: Test that.
 2016-04-20 15:23:55 +02:00