Commit graph

4 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
5d7f4464ea acc: Adjust generalition of parity acceptance
According to https://github.com/adl/hoaf/issues/46

* src/twa/acc.cc (parity): Adjust generation.
* src/tests/hoaparse.test, wrap/python/tests/accparse.ipynb:
Adjust existing test cases.
* wrap/python/tests/accparse2.py: New test cases.
2015-05-24 00:00:36 +02:00
Alexandre Duret-Lutz
7b5c37d5a5 python: fix check of is_parity()
* wrap/python/tests/accparse2.py: Do not check max and odd if
is_parity is False, as this "argout" parameters are not initialized by
SWIG.
2015-05-22 07:54:45 +02:00
Alexandre Duret-Lutz
e04b4eb9fb acc: better Rabin/Streett detection
* src/twa/acc.cc: Allow duplicate and reordered pairs.  Also recognize
the single-pair cases.
* src/twaalgos/hoa.cc: When Rabin or Streett is detected, canonicalize
the Acceptance: line.
* src/tests/hoaparse.test, wrap/python/tests/accparse2.py: More tests.
* src/tests/sbacc.test: Adjust.
2015-05-21 08:57:49 +02:00
Alexandre Duret-Lutz
04171207e6 acc: recognize parity acceptance
It has two modes: strict or not.  In strict mode (tested in
hoaparse.test), the acceptance formula has to match exactly the one
given in the HOA spec.  In non-strict mode (tested in accparse2.py)
any equivalent formula is accepted.

* src/twa/acc.cc, src/twa/acc.hh (acc_cond::is_parity): New method.
* src/twaalgos/hoa.cc: Use it.
* src/tests/hoaparse.test: Test it.
* wrap/python/spot_impl.i: Bind it.
* wrap/python/tests/accparse2.py: New file.
* wrap/python/tests/Makefile.am: Add it.
2015-05-20 20:00:25 +02:00