1. 03 Nov, 2003 5 commits
  2. 31 Oct, 2003 2 commits
  3. 30 Oct, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * m4/gspnlib.m4: Define LIBGSPNESRG_LDFLAGS. · 65bfea0c
      Alexandre Duret-Lutz authored
      * iface/gspn/Makefile.am (gspn_HEADERS): Add common.hh.
      (libspotgspn_la_SOURCES): Add common.cc.
      (libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS)
      (libspotgspneesrg_la_SOURCES, ltlgspn_eesrg_SOURCES)
      (dotty_eesrg_LDADD, dotty_eesrg_CPPFLAGS): New variables.
      (lib_LTLIBRARIES): Add libspotgspneesrg.la.
      (check_PROGRAMS): Add dottygspn-eesrg.
      * iface/gspn/gspn.hh, iface/gspn/gspn.cc
      (gspn_exeption, operator<<(gspn_exeption), gspn_environment): Move ...
      * iface/gspn/common.hh, iface/gspn/common.cc: ... in these new files.
      * iface/gspn/eesrg.hh, iface/gspn/eesrg.cc, iface/gspn/dottyeesrg.cc:
      New files.
      65bfea0c
  4. 28 Oct, 2003 2 commits
  5. 27 Oct, 2003 4 commits
  6. 24 Oct, 2003 5 commits
  7. 23 Oct, 2003 13 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check, · 071cb5d6
      Alexandre Duret-Lutz authored
      emptiness_check::counter_example): Simplify access to hashes
      after calls to find() for the same element..
      071cb5d6
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh (connected_component::set_of_state): · fb4873d9
      Alexandre Duret-Lutz authored
      Rename as ...
      (connected_component::set_type): ... this, and define as a hash_set.
      (connected_component::has_state): New method.
      * src/tgbaalgos/emptinesscheck.cc (connected_component::has_state):
      New method.
      (emptiness_check::counter_example, emptiness_check::complete_cycle,
      emptiness_check::accepting_path): Simplify using has_state().
      fb4873d9
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh (emptiness_check::seen_state_num): · f0dd415f
      Alexandre Duret-Lutz authored
      Rename as ...
      (emptiness_check::h): ... this, and define as a hash_map.
      (emptiness_check::remove_component): Remove superfluous state_map
      argument.
      * src/tgbaalgos/emptinesscheck.cc: Adjust.
      f0dd415f
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: · dfdefdf6
      Alexandre Duret-Lutz authored
      Remove superfluous includes.
      dfdefdf6
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh (emptiness_check::emptiness_check): · 90099e47
      Alexandre Duret-Lutz authored
      New, take the automaton to work on, and store it ...
      (emptiness_check::aut_): ... in this new attribute.
      (emptiness_check::tgba_emptiness_check): Rename as ...
      (emptiness_check::check): ... this, and remove the automata
      argument.
      (emptiness_check::counter_example, emptiness_check::print_result,
      emptiness_check::remove_component, emptiness_check::accepting_path,
      emptiness_check::complete_cycle): Remove the automata argument.
      * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
      iface/gspn/ltlgspn.cc: Adjust.
      90099e47
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh (connected_component::not_null, · b60722bc
      Alexandre Duret-Lutz authored
      connected_component::transition_acc,
      connected_component::nb_transition,
      connected_component::nb_state): Remove these unused attributes.
      (connected_component::connected_component): Merge the two
      definitions into one.
      (connected_component::~connected_component): Remove.
      (connected_component::isAccepted): Delete, unused.
      * src/tgbaalgos/emptinesscheck.cc
      (connected_component::connected_component,
      connected_component::~connected_component): Adjust.
      (connected_component::isAccepted): Delete.
      (spot):
      
      * src/tgbatest/emptchk.test: Typo.
      b60722bc
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh · 636f5238
      Alexandre Duret-Lutz authored
      (emptiness_check::remove_component, emptiness_check::root_component,
      emptiness_check::seen_state_num, emptiness_check::suffix): Move in
      private part.
      (emptiness_check::arc_accepting, emptiness_check::todo): Move ...
      * src/tgbaalgos/emptinesscheck.cc
      (emptiness_check::tgba_emptiness_check): ... as local variables
      of this function.
      * src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component):
      Move ...
      (emptiness_check::counter_example): ... as local variable of this
      function.
      * src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet):
      Move ...
      * src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet):
      ... here.
      636f5238
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh · fda83b9c
      Alexandre Duret-Lutz authored
      (emptiness_check::remove_component, emptiness_check::root_component,
      emptiness_check::seen_state_num, emptiness_check::suffix): Move in
      private part.
      (emptiness_check::arc_accepting, emptiness_check::todo): Move ...
      * src/tgbaalgos/emptinesscheck.cc
      (emptiness_check::tgba_emptiness_check): ... as local variables
      of this function.
      * src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component):
      Move ...
      (emptiness_check::counter_example): ... as local variable of this
      function.
      * src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet):
      Move ...
      * src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet):
      ... here.
      fda83b9c
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result): · 008056f2
      Alexandre Duret-Lutz authored
      Indent output as in the magic search.
      008056f2
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Merge emptinesscheckexplicit into ltl2tgba. · d46c63a2
      Alexandre Duret-Lutz authored
      * src/tgbatest/Makefile.am (check_PROGRAMS): Remove
      emptinesscheckexplicit.
      (emptinesscheckexplicit_SOURCES): Remove.
      (TESTS): Replace emptinesscheckexplicit.test by emptchke.test.
      * src/tgbatest/emptinesscheckexplicit.cc,
      src/tgbatest/emptinesscheckexplicit.test: Delete.
      * src/tgbatest/empchke.test: New file.
      * src/tgbatest/ltl2tgba.cc: Add support for -X.
      d46c63a2
    • Alexandre Duret-Lutz's avatar
      Merge emptiness-checks tests into ltl2tgba. · 65f84e2c
      Alexandre Duret-Lutz authored
      * src/tgbatest/Makefile (check_PRORGRAMS): Remove
      emptinesscheck and ltlmagic.
      (emptinesscheck_SOURCES, ltlmagic_SOURCES): Remove.
      (TESTS): Replace emptinesscheck.test and ltlmagic.test by
      emptchk.test.
      * src/tgbatest/emptinesscheck.test, src/tgbatest/ltlmagic.test:
      Delete.
      * src/tgbatest/emptchk.test: New file.
      * src/tgbatest/emptinesscheck.cc, src/tgbatest/ltlmagic.cc:
      Delete.
      * src/tgbatest/ltl2tgba.cc: Add support for -e, -E, -m, -M, and -n.
      65f84e2c
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.cc · a11a29a1
      Alexandre Duret-Lutz authored
      (emptiness_check::tgba_emptiness_check): Do not print anything.
      (emptiness_check::counter_example): Assume that tgba_emptiness_check
      has already been called.
      a11a29a1
  8. 22 Oct, 2003 3 commits
  9. 15 Oct, 2003 1 commit
  10. 14 Oct, 2003 1 commit
  11. 08 Oct, 2003 2 commits
  12. 07 Oct, 2003 1 commit
    • rebiha's avatar
      * iface/gspn/ltlgspn.cc: We call tgba_emptiness_check before · 6920a1c3
      rebiha authored
      counter_example. And we print the prefix and the periode of
      counter_example's result.
      
      * src/tgbatest/emptinesscheckexplicit.cc (main):
      We call tgba_emptiness_check before counter_example.
      * src/tgbatest/emptinesscheck.cc (main):
      We call tgba_emptiness_check before counter_example.
      
      * src/tgbaalgos/emptinesscheck.hh (spot):
      (spot::print_result): New methode to print the prefix and the
      periode of counter_example's result.
      
      * src/tgbaalgos/emptinesscheck.cc (spot): counter_example doesn't
      call tgba_emptiness_check. counter_example must be executed after
      calling tgba_emptiness_check.  Remove tgba_emptiness_check calls.
      (print_result): New methode to print the prefix and the
      periode of counter_example's result.  Remove most of all std::cout
      during execution of emptiness_check's methodes.
      6920a1c3