Skip to content
  • Ala-Eddine Ben-Salem's avatar
    Add Testing Automata Product & Emptiness Check · 81e80e60
    Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
    * src/taalgos/stats.hh, src/taalgos/stats.cc: Compute statistics for a
    automaton.
    * src/ta/ta.hh, src/ta/ta.cc: Abstract representation of a Testing
    Automata(TA)
    * src/ta/taexplicit.hh, src/ta/taexplicit.cc: Explicit representation of
    a Testing Automata (TA)
    * src/taalgos/dotty.cc: Print a TA in dot format.
    * src/taalgos/reachiter.hh, src/taalgos/reachiter.cc: Iterate over all
    reachable states of a TA
    * src/taalgos/sba2ta.cc: implements the construction of a TA from a BA
    (Buchi Automata)
    * src/tgbatest/ltl2tgba.cc: add commands to test the TA implementation
    * src/taalgos/emptinessta.hh, src/taalgos/emptinessta.cc: implementation
     of the TA emptiness-check algorithm
    * src/ta/taproduct.hh, src/ta/taproduct.cc: representation of the
    product (automaton) between a TA and a Kripke structure.
    * src/ta/Makefile.am, src/taalgos/Makefile.am: add them
    81e80e60