Skip to content
  • Alexandre Duret-Lutz's avatar
    Add an ltl2tgba option to read Kripke structure. · ba3108f9
    Alexandre Duret-Lutz authored
    Also offers two ways to output Kripke structures.
    
    * src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc
    : Simplify includes.
    * src/kripke/kripkeprint.hh (kripke_save_reachable,
    kripke_save_reachable_renumbered): New declarations.
    (KripkePrinter): Move and rename...
    * src/kripke/kripkeprint.cc (kripke_printer): ... here.
    (kripke_printer_renumbered): New class.
    (kripke_save_reachable, kripke_save_reachable_renumbered): New
    function.
    * src/tgbatest/ltl2tgba.cc: Add an option to read Kripke
    structures.
    * iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered.
    * iface/dve2/defs.in (run2): Remove.
    * iface/dve2/kripke.test: Adjust tests.
    ba3108f9