Commit graph

10 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
b4da0cf660 hierarchy: add a new way to check DBA-realizability via DPA
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here.
* tests/core/hierarchy.test: Test it.
* bin/man/spot-x.x: Document SPOT_PR_CHECK.
* doc/org/hierarchy.org, NEWS: Update.
2019-06-12 23:38:17 +02:00
Alexandre Duret-Lutz
d94efe9fe1 implement is_liveness() and is_liveness_automaton()
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh,
spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here.
* bin/ltlfilt.cc (--liveness): New filter.
* NEWS: Mention those.
* tests/core/ltlfilt.test, tests/python/ltlsimple.py: Add test cases.
2018-10-15 21:37:31 +02:00
Alexandre Duret-Lutz
62d1e0219d Add support for computing operator nesting depth
* spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
function.
* python/spot/__init__.py: Also make it a method of formula in Python
* bin/common_output.cc, bin/common_output.hh: Implement
--stats=%[OP]n.
* NEWS: Mention it.
* tests/core/format.test, tests/python/formulas.ipynb: Test it.
2017-12-10 20:31:56 +01:00
Alexandre Duret-Lutz
49b76bcf66 doxygen doc: minor improvements
* doc/footer.html: Make the footer XML compatible.
* doc/mainpage.dox: Fix references to modules.
* spot/tl/formula.hh: Introduce a hierarchy module.
* spot/tl/hierarchy.hh: Use it.
2017-12-08 22:07:11 +01:00
Alexandre GBAGUIDI AISSE
7e0fc448c5 hierarchy: Rewrite is_recurrence(), is_persistence() and add tests
* spot/tl/hierarchy.cc: Rewrite is_recurrence(), is_persistence()
* spot/tl/hierarchy.hh: Fix typo.
* tests/core/hierarchy.test: Add tests.
2017-11-21 01:20:05 +01:00
Alexandre Duret-Lutz
50fe34a55a introduce is_obligation(f)
This is not optimal yet because it still construct a minimal WDBA
internally, but it's better than the previous way to call
minimize_obligation() since it can avoid constructing the minimized
automaton in a few more cases.

* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
is_obligation().
* bin/ltlfilt.cc: Wire it to --obligation.
* spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
needed by the above.
* tests/core/obligation.test: Test it.
* bin/man/spot-x.x, NEWS: Document it.
2017-11-16 07:26:34 +01: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 Duret-Lutz
ebdb198b64 hierarchy: expose mp_class to python
* bin/common_output.cc: Move some of the printing code...
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: ... here, as new
  variants of mp_class...
* python/spot/impl.i: ... that we can now call from Python.
* python/ajax/spotcgi.in: Use those to simplify and extend
the code printing class membership.
2017-01-14 23:43:01 +01:00
Alexandre Duret-Lutz
7d9ce0d6fc tl: mp_class() and --format=%[vw]h
Tools for deciding the class of a formula.

* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/common_output.cc, bin/common_output.hh: Implement --format=%h.
* tests/core/hierarchy.test: More tests.
* NEWS: Update.
2017-01-10 22:41:11 +01:00