Commit graph

17 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
99241d0bea typos: coma -> comma
* ChangeLog.1, tests/core/autcross3.test, tests/core/ltl3ba.test,
tests/core/ltl3dra.test, tests/core/ltlcross3.test,
tests/core/ltlsynt.test, tests/sanity/style.test: Here.
2021-06-11 11:47:34 +02:00
Alexandre Duret-Lutz
457e130e24 ltlcross: completely fix #420
Reported by Salomon Sickert.

* bin/ltlcross.cc: Also call determinize_unknown_acceptance() for
positive automata.
* tests/core/ltlcross3.test: Add another test case.
* NEWS: Mention the fix.
2020-07-21 22:18:00 +02:00
Alexandre Duret-Lutz
33b28c8151 ltlcross: fix cross-checks for automata using Fin acceptance
Fixes #420 reported by Salomon Sickert.

* bin/ltlcross.cc: Call determine_unknown_acceptance().
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Document
that one_accepting_scc()==-1 can mean "don't know", and update
determine_unknown_acceptance() to set one_acc_scc_.
* tests/core/ltlcross3.test: Add test case.
* NEWS: Mention the fixes.
2020-07-20 13:38:47 +02:00
Alexandre Duret-Lutz
3805b63e24 ltlcross: add option --save-inclusion-products
* NEWS: Mention it.
* bin/ltlcross.cc: Implement it.
* tests/core/ltlcross3.test: Test it.
2020-03-08 09:15:06 +01:00
Alexandre Duret-Lutz
6f37ff8ed0 ltlcross, autcross: add --quiet/-q option
* bin/autcross.cc, bin/ltlcross.cc: Implement it.
* doc/org/autcross.org, doc/org/ltlcross.org, NEWS: Document it.
* doc/org/spot.css: Add colors for Makefile snippets.
* tests/core/autcross4.test, tests/core/ltlcross3.test,
tests/core/ltlcrossce.test: Add test cases.
2019-07-17 17:34:01 +02:00
Alexandre Duret-Lutz
a85045091b introduce output_aborter, and use it in ltlcross
* spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges.  Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
2019-05-28 14:27:30 +02:00
Maximilien Colange
d7ee23ed2f acc_cond::mark_t now relies on bitset
This allows to represent more than 32 acceptance marks.

* configure.ac: add an option to specify the number of marks
* spot/twa/acc.hh: implement it
* tests/python/acc_cond.ipynb, tests/core/acc.cc,
  tests/core/ltlcross3.test: update tests
* NEWS: document it
* bin/randltl.cc: fix an include
2018-05-22 09:54:19 +02:00
Alexandre Duret-Lutz
c369f899a3 bin: teach conversion options to report about the options
* bin/common_conv.cc, bin/common_conv.hh: Here.
* bin/autfilt.cc, bin/common_trans.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Pass
the name of the argumennt to the conversion function.
* tests/core/ltlcross3.test, tests/core/ltldo.test,
tests/core/randaut.test: Add test cases.
2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
f0b57d7264 tests: use ltlcross --color for better code coverage
* tests/core/ltlcross3.test: Here.
2018-05-16 17:05:21 +02:00
Alexandre Duret-Lutz
020c981188 ltlcross: detect remove_fin failures
Fixes #314, reported by František Blahoudek.

* bin/ltlcross.cc: Here.
* tests/core/ltlcross3.test: Add new test case.
* NEWS: Mention the bug.
2018-01-06 14:08:44 +01:00
Alexandre Duret-Lutz
a9a375ccd8 tests: git rid of all the tool=tool assignents
Our use of
  ltl2tgba=ltl2tgba
  autfilt=autfilt
  ...
all over the test cases comes from the time where those tools were not
in PATH and we actually had something like
  ltl2tgba=../../bin/ltl2tgba
  autfilt=../../bin/autfilt

But today that is useless, and we prefer to write ltl2tgba rather than
$ltl2tgba, so let's remove this old cruft.

* tests/core/basimul.test, tests/core/det.test, tests/core/lbt.test,
tests/core/lenient.test, tests/core/ltl2dstar.test,
tests/core/ltl2dstar2.test, tests/core/ltl2dstar3.test,
tests/core/ltl2dstar4.test, tests/core/ltlcross2.test,
tests/core/ltlcross3.test, tests/core/ltlcross4.test,
tests/core/ltlcrossce2.test, tests/core/ltldo.test,
tests/core/ltlfilt.test, tests/core/optba.test,
tests/core/prodor.test, tests/core/rand.test,
tests/core/randomize.test, tests/core/remfin.test,
tests/core/satmin.test, tests/core/sbacc.test,
tests/core/strength.test, tests/core/stutter-ltl.test,
tests/core/stutter-tgba.test, tests/core/unabbrevwm.test,
tests/core/unambig.test: Get rid of all tool=tool assignments.
2017-11-24 19:35:58 +01:00
Alexandre Duret-Lutz
fcccd5f425 ltlcross: add support for --reference translators
Suggested by Tobias Meggendorfer.  Fixes #295.

* bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
this --reference option.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross3.test: Test it.
2017-10-15 19:35:28 +02:00
Alexandre Duret-Lutz
183ec1fb4e ltlcross, autcross, ltldo: support --fail-on-timeout
Suggested by Tobias Meggendorfer.  Fixes #294.

* bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option.
* tests/core/autcross3.test, tests/core/ltlcross3.test,
tests/core/ltldo.test: Test it.
* tests/Makefile.am: Add autcross3.test.
* NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
Mention the option.
* THANKS: Add Tobias.
2017-10-15 12:22:15 +02:00
Alexandre Duret-Lutz
c7141bd189 ltlcross: disable products columns in CSV if --products=0
* bin/ltlcross.cc: Fix it.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the bug.
2017-01-14 10:43:35 +01:00
Alexandre Duret-Lutz
3b5fa22a3b ltlcross: add option --strength and --ambiguous
Suggested by František Blahoudek.

* bin/ltlcross.cc: Implement the two options.
* doc/org/ltlcross.org, NEWS: Document them.
* tests/core/complementation.test: Adjust test case.
* tests/core/ltlcross3.test, tests/core/unambig.test: More tests.
2016-10-13 15:41:49 +02:00
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
5cb94a1a3f Merge the core and python tests in the tests/ directory
* tests/: Rename as...
* tests/core/: ... this.
* python/tests/: Rename as...
* tests/python/: ... this.
* python/tests/run.in: Move as...
* tests/run.in: This, and adjust.
* tests/Makefile.am: Adjust to run both core and python tests.
* configure.ac, README, debian/python3-spot.examples, debian/rules,
doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
2016-01-04 16:02:30 +01:00
Renamed from tests/ltlcross3.test (Browse further)