• Ala-Eddine Ben-Salem's avatar
    Add a new form of TA with a Single-pass emptiness check (STA) · 782ba001
    Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
    * src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc,
    src/ta/taexplicit.hh, src/ta/taproduct.cc,src/ta/taproduct.hh,
    src/taalgos/dotty.cc, src/taalgos/emptinessta.cc,
    src/taalgos/emptinessta.hh, src/taalgos/minimize.cc,
    src/taalgos/reachiter.cc, src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh,
    src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc: Impacts of the
    implementation of a new variant of TA, called STA, which involve a
    Single-pass emptiness check. The new options (-in and -lv) added to
    build the new variants of TA allow to add two artificial states:
    1- an initial artificial state to have an unique initial state (-in)
    2- a livelock artificial state which has no successors in order to
    obtain the new form of TA which requires only a Single-pass emptiness-
    check: STA (-lv).