Commit graph

630 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
2bca21f7f8 postproc: fix a comment
* spot/twaalgos/postproc.cc: Here.
2017-09-24 16:09:29 +02:00
Maximilien Colange
1689c08e09 genltl: add a new family from SYNTCOMP'2017
* bin/genltl.cc, spot/gen/formulas.cc, spot/gen/formulas.hh: Implement
  it.
* tests/core/genltl.test: Test it.
* NEWS: Document it.
2017-09-22 10:35:24 +02:00
Alexandre GBAGUIDI AISSE
c827f75c37 hierarchy: Add is_persistence() and make is_recurrence() use it
* NEWS: Update.
* bin/man/spot-x.x: Add environment variable.
* spot/tl/hierarchy.cc: Implement them.
* spot/tl/hierarchy.hh: Declare them.
2017-09-20 15:25:31 +01:00
Alexandre GBAGUIDI AISSE
e59274b609 hierarchy: Make is_recurrence() public
* NEWS: Declare it.
* spot/tl/hierarchy.cc: Remove static keyword and anonymous namespace.
* spot/tl/hierarchy.hh: Declare function.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
ad9bc644ba misc/timer: Gather handling of %r and %R options
* bin/autcross.cc: Update.
* bin/autfilt.cc: Update.
* bin/common_aoutput.cc: Gather them. Move process_timer struct.
* bin/common_aoutput.hh: Gather them.
* bin/common_output.hh: Update.
* bin/dstar2tgba.cc: Update.
* bin/ltl2tgba.cc: Update.
* bin/ltlcross.cc: Update.
* bin/ltldo.cc: Update.
* bin/ltlfilt.cc: Update.
* bin/randaut.cc: Update.
* spot/misc/formater.hh: Remove an useless function.
* spot/misc/timer.hh: Add process_timer struct definition.
* spot/misc/timer.cc: Remove old dead code.
* spot/twaalgos/stats.cc: Update.
* spot/twaalgos/stats.hh: Update.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
302095ff9e typos
* spot/twaalgos/alternation.hh: Typos.
* spot/twa/twa.hh: Typos.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
8ae10f744f twaalgos/cobuchi: Add dnf_to_dca()
* NEWS: Update news with all co-Büching functions.
* spot/twaalgos/cobuchi.hh: Declare it.
* spot/twaalgos/cobuchi.cc: Implement it.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
5f6a71d27a twaalgos/cobuchi: Add breakpoint construction and nsa_to_dca()
* spot/twaalgos/cobuchi.hh: Declare nsa_to_dca().
* spot/twaalgos/cobuchi.cc: Implement nsa_to_dca().
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
f2616069be twaalgos/cobuchi: Add dnf_to_nca() method
* NEWS: Update.
* spot/twaalgos/cobuchi.hh: Declare dnf_to_nca().
* spot/twaalgos/cobuchi.cc: Implement it.
* tests/core/dca.test: Add tests.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
50e99cdca7 twaalgos/totgba: Add dnf_to_streett() method
* NEWS: Update.
* spot/twaalgos/totgba.hh: Declare dnf_to_streett().
* spot/twaalgos/totgba.cc: Implement dnf_to_streett().
* bin/autfilt.cc: Add --dnf-to-streett cmd line option.
* tests/core/dnfstreett.test: Add test.
* tests/Makefile.am: Add test file.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
cf18c06940 twaalgos/cobuchi: Add nsa_to_nca()
* NEWS: Update.
* spot/twaalgos/cobuchi.hh: Declare to_dca() and nsa_to_nca().
* spot/twaalgos/cobuchi.cc: Implement them.
* python/spot/impl.i: Include new file for python bindings.
* spot/twaalgos/Makefile.am: Add new file.
* bin/autfilt.cc: Add --dca command line option. This option does not
return a deterministic automaton yet, but it will.
* tests/core/dca.test: Add tests for Büchi automata.
* tests/python/dca.py: Add a python script that builds a nondet. Streett
automaton.
* tests/python/dca.test: Add tests for Streett automata.
* tests/Makefile.am: Add all tests.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
37c1a19b39 twaalgos/scc_info: Add states_on_acc_cycle_of() method
* NEWS: Update.
* spot/twaalgos/sccinfo.hh: Declare states_on_acc_cycle_of().
* spot/twaalgos/sccinfo.cc: Implement it.
2017-09-19 17:37:00 +01:00
Alexandre GBAGUIDI AISSE
0957317ad7 spot/twa: Add methods to set co-Büchi acceptance
* spot/twa/acc.hh: Add set_generalized_co_buchi() method.
* spot/twa/twa.hh: Add set_generalized_co_buchi() and set_co_buchi()
wrappers.
2017-09-19 17:37:00 +01:00
Maximilien Colange
bd5c6920b1 Use clearer names for three methods of spot::scc_info
scc_info::used_acc() and spot::info::used_acc_of() have been renamed to
scc_info::marks() and scc_info::marks_of().
scc_info::acc() has been renamed to (the already existing and redundant)
scc_info::acc_sets_of().
Old names have been deprecated.

* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: implement it.
* spot/twaalgos/dtwasat.cc, spot/twaalgos/isweakscc.cc,
  spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc: update names.
* NEWS: documentate it.
2017-09-19 10:24:12 +02:00
Alexandre Duret-Lutz
7eb50bc1f8 genltl: add 4 new families from Müller & Sickert (GandALF'17)
* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc:
Implement them.
* NEWS, bin/man/genltl.x: Document them.
* tests/core/genltl.test: Add some tests.
2017-09-15 22:32:04 +02:00
Clément Gillard
ad3588420c fix typos and indentation
* bin/autfilt.cc, python/spot/__init__.py, spot/twa/twa.hh,
spot/twa/twaproduct.cc, spot/twaalgos/couvreurnew.cc,
tests/python/bugdet.py: Here.
2017-09-05 13:23:01 +02:00
Alexandre Duret-Lutz
bc626788af dot: make 'x' compatible with 'b'/'r'/'R'
* spot/twaalgos/dot.cc: Implement.
* doc/org/oaut.org: Illustrate.
* tests/core/dot2tex.test: Add some limited tests.
2017-09-05 07:45:11 +02:00
Alexandre Duret-Lutz
e7df182a30 gen: rename KS_COBUCHI to KS_NCA for consistency
* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
the enum, function, and command-line option.
* tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
Adjust test cases.
* doc/org/genaut.org: Adjust doc.
2017-09-03 15:47:27 +02:00
Alexandre Duret-Lutz
6cd6802ace simplify: rewrite GF(a & Fb) as G(Fa & Fb)
This addresses part of #35, and is just a generalization of the rules
from 646c5170 for #263 (hence, no new documentation).

* spot/tl/simplify.cc: Implement this.
* tests/core/reduccmp.test: Add test cases.
* tests/core/stutter-tgba.test: Adjust to expect smaller automata.
2017-09-02 20:02:20 +02:00
Alexandre Duret-Lutz
e8527d5ae9 Improve simplification of expr[*0..1]
Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
2017-09-02 16:35:18 +02:00
Alexandre Duret-Lutz
190d4cfaf1 ltl2tgba_fm: implement a small optimization
Fixes #277.

* spot/twaalgos/ltl2tgba_fm.cc: Improve the translation of f U g
when f is universal.  Suggested by Maximilien Colange.
* tests/core/ltl2tgba.test: Test it.
2017-09-02 14:48:52 +02:00
Alexandre Duret-Lutz
42abcf8559 genltl: add --gxf-and and --fxg-or
As suggested in #263.

* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
these options.
* tests/core/genltl.test: Use them.
* NEWS: Mention them.
2017-09-02 11:51:54 +02:00
Alexandre Duret-Lutz
646c5170ed simplify: some new simplification rules
For #263, reported by Mikuláš Klokočka.

G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)

* spot/tl/simplify.cc: Implement the rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
* tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
smaller automata.
* THANKS: Add Mikuláš.
2017-09-02 11:27:04 +02:00
Alexandre Duret-Lutz
cd6f1c2c3e get rid of some unnecessary code
* spot/priv/enumflags.hh: Delete.
* spot/priv/Makefile.am, debian/copyright: Adjust.
* spot/twaalgos/remfin.cc: Replace the complex enum
definition by a plain enum that is almost not used.
2017-09-01 22:09:52 +02:00
Alexandre Duret-Lutz
15cc7301cc remove_fin: apply Rabin conversion before Streett
* spot/twaalgos/remfin.cc (remove_fin_impl): Apply the Rabin strategy
before the Streett one.
2017-09-01 22:09:52 +02:00
Alexandre Duret-Lutz
f7ba490898 streett_to_generalize_buchi: fix handling of SCCs without Fin
The generalization to Streett-like of 7b5b8f34 was incomplete for this
case.  Thanks to František Blahoudek for reporting the bug.
Fixes #279.

* spot/twaalgos/totgba.cc (streett_to_generalized_buchi): Here.
* tests/core/remfin.test: Add more tests.
2017-09-01 22:09:49 +02:00
Alexandre Duret-Lutz
fbb9e4374e dot: add x option for dot2tex
* spot/twa/acc.cc, spot/twa/acc.hh: Add a LaTeX output for acceptance
conditions.
* spot/twaalgos/dot.cc: Implement the 'x' option and refactor the code
a bit to limit duplication.
* tests/core/dot2tex.test: New test case (requires dot2tex).
* tests/Makefile.am: Add dot2tex.test.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/automata-io.ipynb: Adjust expected output.
* NEWS, doc/org/oaut.org: Mention the new option.
2017-08-31 19:50:08 +02:00
Alexandre Duret-Lutz
b242122ce8 dot: add option 'A' to disable 'a'
This way in 2.5 we can make 'a' the default, and tell people to use
SPOT_DOTDEFAULT=A if they want the old behavior in both 2.4 and 2.5.

* spot/twaalgos/dot.cc: Implement the option.
* NEWS, bin/common_aoutput.cc: Mention it.
* tests/core/readsave.test: Test it.
2017-08-30 16:15:53 +02:00
Alexandre Duret-Lutz
205294c2c2 dot: display Rabin-like and Streett-like acceptances
* spot/twaalgos/dot.cc (print_acceptance_for_human): Add Rabin-like
and Streett-like checks.
* tests/core/sccdot.test, tests/python/decompose.ipynb,
tests/python/randaut.ipynb, tests/core/alternating.test: Adjust.
2017-08-30 16:15:48 +02:00
Maximilien Colange
1b2f2a79c1 Fix a bug in spot.complete()
spot.complete() could complete an empty co-Büchi automaton into an
automaton accepting everything.

* NEWS: Document it
* spot/twaalgos/complete.cc: Fix it
* tests/core/complete.test, tests/core/prodor.test: Test it
2017-08-28 17:55:32 +02:00
Maximilien Colange
eb91ecf66f Typos
* NEWS, doc/org/concepts.org, doc/org/hierarchy.org,
  spot/misc/optionmap.hh, spot/twa/acc.hh, spot/twaalgos/ltl2tgba_fm.hh,
  spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.cc: fix typos
2017-08-28 17:54:21 +02:00
Alexandre Duret-Lutz
f5dce597c6 switch to C++14 compilation
* configure.ac: Compile in C++14 by default and rename
--enable-c++14 as c++17.
* doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
NEWS, README: Adjust all mentions of C++11.
* spot/twaalgos/stats.hh: Use std::make_unique.
2017-08-22 18:21:49 +02:00
Alexandre Duret-Lutz
1cc45b2413 dot: display acceptance names
* spot/twaalgos/dot.cc: Display common acceptance names.
* NEWS: Mention the change.
* doc/org/oaut.org: Adjust text.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
f8ef06acc6 acc: fix operator| and operator&
Bug introduced in abe2c08b, visible in tests/python/product.ipynb,
and tests/python/acc_cond.ipynb.

* spot/twa/acc.hh: fix operator| and operator&.
* tests/python/acc_cond.ipynb: Adjust test case.
2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
2e8a67027f hierarchy: avoid sbacc()
* spot/tl/hierarchy.cc (is_recurrence): Do not request state-based
acceptance, now that the Rabin->DBA conversionn works on
transition-based acceptance as well.
2017-08-17 15:21:59 +02:00
Alexandre Duret-Lutz
e3b30e6d8e remfin: remove some unnecessary copies
* spot/twaalgos/remfin.cc (tra_to_tba, is_scc_tba_type): Here.
2017-08-17 15:21:59 +02:00
Thomas Medioni
4b5606e742 to_weak_alternating(): fixes a bug on generalized co-Büchi automata
Fixes #278. Also adds a test ensuring non-regression.

* spot/twaalgos/toweak.cc: Fixes the bug.
* tests/python/toweak.py: Add a test case.
2017-08-17 13:07:20 +02:00
Alexandre Duret-Lutz
df04c715cf remove_fin: fix incorrect state-based output
* spot/twaalgos/remfin.cc: If no Inf set is used, set sbacc early so
that it is used in the algorithm.
* tests/core/remfin.test: Add more tests.
* NEWS: Mention the bug.
2017-08-09 18:25:36 +02:00
Thomas Medioni
30a68d288b Fix typo automatons -> automata
* NEWS, spot/twaalgos/dualize.cc, spot/twaalgos/dualize.hh,
  spot/twaalgos/langmap.cc, spot/twaalgos/sum.hh,
  tests/python/streett_totgba.py: Fixes typo.
2017-08-09 15:51:23 +02:00
Alexandre Duret-Lutz
f0161618ca * spot/twaalgos/simulation.cc (print_partition): Improve. 2017-08-08 15:00:33 +02:00
Alexandre Duret-Lutz
55113ed1d0 fix error message in exception
* spot/twaalgos/alternation.cc: Here.
2017-08-04 17:01:03 +02:00
Alexandre Duret-Lutz
1cf5778faa stats: allow counting complete SCCs
* bin/common_aoutput.cc, NEWS: Update documentation.
* spot/twaalgos/stats.cc: Honor c and C.
* tests/core/alternating.test: Test it.
2017-08-04 17:01:03 +02:00
Alexandre Duret-Lutz
223b0c6a9e is_weak_scc and friend: make them work for alternating automata
* spot/twaalgos/isweakscc.cc, spot/twaalgos/isweakscc.hh,
spot/twaalgos/mask.cc, spot/twaalgos/mask.hh: Adjust to
work with alternating automata.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh
(determine_unknown_acceptance): Do not complain about
not supporting alternating automata if there is not
indeterminate acceptance.
* spot/twaalgos/stats.cc: Fix a bug were %[iw]c was
read as %[iww]c.
* tests/core/alternating.test: Test is_inherently_weak_scc() and
is_weak_scc().
* python/spot/impl.i: Add missing python bindings
for isweakscc.hh.
2017-08-04 15:12:27 +02:00
Alexandre Duret-Lutz
e041db6101 dot: extend the palette from 9 to 16 colors
Let's close #212 even if this does not cover the 32 sets.

* spot/twaalgos/dot.cc: Change the palette.
* doc/org/autfilt.org, NEWS: Adjust documentation.
* tests/core/alternating.test, tests/core/readsave.test,
tests/core/tgbagraph.test, tests/python/_altscc.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/gen.ipynb,
tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
tests/python/piperead.ipynb, tests/python/product.ipynb,
tests/python/randaut.ipynb, tests/python/word.ipynb: Adjust
test cases.
2017-08-03 14:32:11 +02:00
Alexandre Duret-Lutz
ab42075dce formula: hide throw statements from inline methods
* spot/tl/formula.hh: Move all throw statements behind
some [[noreturn]] report...() methods...
* spot/tl/formula.cc: ... defined here.  This makes the methods
shorter and helps their inlining.  Incidentally, this also removes the
uninitialized read that weirdly occurs when _GLIBCXX_DEBUG is on, as
observed with #184, but I do not know why.
2017-08-02 11:31:47 +02:00
Alexandre Duret-Lutz
6b96aa4f27 is_unabiguous: fix incorrect vector usage
* spot/twaalgos/isunamb.cc: Actually set the size of the vector
instead of just reserving the size.
2017-08-01 18:04:07 +02:00
Alexandre Duret-Lutz
eb8df6d72c parseaut: allow the univ-branch diagnostics to be ignored
* spot/parseaut/parseaut.yy: Check the SPOT_HOA_TOLERANT variable.
* tests/core/ltl3ba.test, tests/core/parseaut.test: Adjust test cases.
* NEWS, bin/man/spot-x.x: Mention SPOT_HOA_TOLERANT.
2017-08-01 18:03:06 +02:00
Alexandre Duret-Lutz
d3607a7ce3 hoa: fix I/O of determinism
Fixes #212.

* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Recognize
exist-branch, and adjust printer to the 1.1 semantics.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/det.test, tests/core/explsum.test,
tests/core/parseaut.test, tests/core/readsave.test,
tests/core/sbacc.test, tests/core/tgbagraph.test,
tests/python/alternating.py, tests/python/dualize.py: Adjust test
cases.
* NEWS: Mention the change.
2017-07-31 22:33:56 +02:00
Alexandre Duret-Lutz
b9fff6a4b1 parseaut: make the scanner reentrant
* spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh,
spot/parseaut/public.hh, spot/parseaut/scanaut.ll: Use a reentrant
scanner, so that we can now parse multiple automaton streams at the
same time.  This is needed for the future autcross, which is going to
read several individual automata produced by different tools, while
reading the stream of automata to process.
2017-07-27 17:33:53 +02:00
Alexandre Duret-Lutz
ff4f4ee482 parseaut: use prop_universal() instead of prop_deterministic()
* spot/parseaut/parseaut.yy: Here.
2017-07-25 17:54:31 +02:00