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

3 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
f0b77e21c8 autcross: simplify code using complement() and intersecting_word() 
* bin/autcross.cc: Let complement() decide how to complement automata.
Do not apply remove_fin(), because we have a generic emptiness check
now.  Use intersecting_word() instead of product()+accepting_word() so
that the former can maybe be optimized in the future.
* tests/core/autcross2.test: Adjust test case to use TGBA instead
of monitors, as calling complement() had a side-effect of setting
the "weak" property on the input.
 2019-06-07 14:56:56 +02:00
Alexandre Duret-Lutz
6e8af75ee9 autcross: exercise %S, %L, and {name{nest}} 
* tests/core/autcross.test, tests/core/autcross2.test: More tests.
 2018-05-21 17:39:38 +02:00
Alexandre Duret-Lutz
0cf250d839 bin: introduce autcross 
Fixes #252.

* NEWS: Mention it.
* bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
files.
* bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
doc/Makefile.am: Add them.
* bin/autfilt.cc: Use is_universal() instead of is_deterministic().
* bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
ltlcross, ltldo and autcross.
* tests/core/autcross.test, tests/core/autcross2.test: New files.
* tests/Makefile.am: Add them.
* tests/core/dra2dba.test, tests/core/sbacc.test,
tests/core/streett.test: Use autcross.
 2017-07-28 10:33:14 +02:00