Skip to content
  • Thomas Medioni's avatar
    Implement sum(..) and sum_and(..). · 62fd38e6
    Thomas Medioni authored
    See #231.
    
    * bin/autfilt.cc: Add --sum, --sum-or and --sum-and options.
    * python/spot/impl.i: Add bindings for sum, sum_and.
    * spot/twaalgos/Makefile.am: Add sum.cc, sum.hh.
    * spot/twaalgos/sum.cc: Implement sum, sum_and.
    * spot/twaalgos/sum.hh: Declaration of sum, sum_and.
    * tests/Makefile.am: Add sum tests.
    * tests/core/.gitignore: Ignore ltlsum binary.
    * tests/core/explsu2.test: Test false or false.
    * tests/core/explsu3.test: Test whether unsatisfied marks propagate
      onto other automaton sum of the term.
    * tests/core/explsu4.test: Test whether universal transitions are
      handled.
    * tests/core/explsu5.test: Generate two sets of persistence LTL
      formulas, apply both sum and sum_and on both sets, test equivalence
      of the result with the disjunction resp. conjunction of the formulas.
    * tests/core/explsum.test: Test the sum of two automatons
    * tests/core/ltlsum.cc: Standalone sum program that takes two formulas
      as input
    * tests/core/ltlsum.test: Test some random formulas, in order to
      trigger basic assertions
    * tests/python/sumexpt.py: Check that two automatons that does not
      share their bdd dict are not accepted
    62fd38e6