1. 21 Nov, 2003 1 commit
  2. 14 Nov, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/Makefile.am (AM_CXXFLAGS): New variable. · 982c5efc
      Alexandre Duret-Lutz authored
      * tgba/bdddict.hh (bdd_dict::register_propositions,
      bdd_dict::register_accepting_variables): New methods.
      * src/bdddict.cc: Likewise.
      * tgba/tgbaexplicit.cc (tgba_explicit::add_conditions,
      tgba_explicit::add_accepting_conditions): New methods.
      (tgba_explicit::get_init_state): Add an "empty" initial
      state to empty automata.
      * tgba/tgbaexplicit.hh: (tgba_explicit::add_conditions,
      tgba_explicit::add_accepting_conditions): New methods.
      * tgbaalgos/Makefiles.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES):
      Add dupexp.hh and dupexp.cc.
      * tgbaalgos/dupexp.hh, tgbaalgos/dupexp.cc: New files.
      * tgbatest/Makefile.am (AM_CXXFLAGS): New variable.
      (check_SCRIPTS): Add dupexp.test.
      (CLEANFILES): Add output1 and output2.
      * tgbatest/dupexp.test: New file.
      * tgbatest/ltl2tgba.cc: Handle -s and -S.
      * tgbatest/tgbaread.cc: Remove unused variable exit_code.
      982c5efc
  3. 13 Nov, 2003 1 commit
  4. 28 Oct, 2003 2 commits
  5. 27 Oct, 2003 3 commits
  6. 24 Oct, 2003 5 commits
  7. 23 Oct, 2003 10 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
      * 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. 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
  10. 30 Sep, 2003 1 commit
  11. 25 Sep, 2003 1 commit
    • rebiha's avatar
      * src/tgbatest/emptinesscheckexplicit.test (acc): New file. · 7f3c1131
      rebiha authored
      * src/tgbatest/emptinesscheckexplicit.cc (main): New file.
      
      * src/tgbatest/emptinesscheck.test: New file.
      
      * src/tgbatest/emptinesscheck.cc (main): New file.
      
      * src/tgbaalgos/emptinesscheck.cc (spot): New method.
      
      * src/tgbaalgos/emptinesscheck.hh: New interface.
      7f3c1131
  12. 22 Sep, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ... · 83565fb6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh:
      ... this, and rename ltl_to_tgba() as ltl_to_tgba_lacim as well.
      * iface/gspn/ltlgspn.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlmagic.cc,
      src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
      src/tgbatest/tripprod.cc, wrap/python/spot.i,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py: Adjust.
      83565fb6
  13. 29 Aug, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/state.hh (state::hash): New method. · f0de3868
      Alexandre Duret-Lutz authored
      (state_ptr_equal, state_ptr_hash): New functors.
      * src/tgba/statebdd.hh, src/tgba/statebdd.cc (state_bdd::hash):
      New method.
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
      (state_explicit::hash): New method.
      (ns_map, sn_map): Use Sgi::hash_map instead of std::map.
      * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
      (state_product::hash): New method.
      * src/tgba/tgbatba.cc (state_tba_proxy::hash): New method.
      * src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine
      using Sgi::hash_map or Sgi::hash_set.
      (lbtt_reachable): Don't erase a key that is pointed to by an
      iterator.
      * src/tgbaalgos/reachiter.cc
      (tgba_reachable_iterator::~tgba_reachable_iterator): Likewise.
      * src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise.
      * src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map.
      * src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map.
      * iface/gspn/gspn.cc (state_gspn::hash): New method.
      * src/misc/hash.hh (string_hash): New functor.
      f0de3868
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions) · 6da1f356
      Alexandre Duret-Lutz authored
      Compute all_accepting_conditions_ from neg_accepting_conditions_,
      not by browsing the dictionary.  The dictionary also contains
      accepting conditions from other automata...  This bug was a
      consequence of the change from 2003-07-14.
      * src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not
      browse the dictionary to print accepting conditions.  Call
      ->all_accepting_conditions() instead.
      * src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo
      from 2003-08-22 in the computation of all_accepting_conditions_.
      * src/tgbatest/explpro3.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add explpro3.test.
      * src/tgbatest/explprod.test, src/tgbatest/explpro2.test,
       src/tgbatest/tripprod.test: Sort the output using Perl.
      6da1f356
  14. 28 Aug, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Rewrite all std::map<const formula*, ...> as · 19551509
      Alexandre Duret-Lutz authored
      Sgi::hash_map<const formula*, ...>.
      
      * src/misc/hash.hh: New file.
      * src/misc/Makefile.am (misc_HEADERS): Add it.
      * src/ltlvisit/dotty.cc (dotty_visitor::map): Use a hash_map instead
      of a map.
      * src/tgba/bdddict.hh (bdd_dict::fv_map, bdd_dict::vf_map,
      bdd_dict::ref_set, bdd_dict::var_map): Define as hash_map or
      hash_set.
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::fv_map,
      translate_dict::vf_map): Likewise.
      * src/tgba/tgbabddconcretefactory.hh
      (tgba_bdd_concrete_factory::acc_map_): Likewise.
      * src/tgba/tgbatba.hh, src/tgbaalgos/reachiter.hh: Include <map>.
      19551509
  15. 23 Aug, 2003 1 commit
  16. 15 Aug, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      This implements Couvreur's FM'99 ltl2tgba translation. · 2b9f1720
      Alexandre Duret-Lutz authored
      * src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ...
      (bdd_dict::is_registered_proposition, bdd_dict::is_registered_state,
      bdd_dict::is_registered_accepting_variable): ... these.
      * src/tgba/bdddict.hh: Likewise.
      * src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method.
      (tgba_explicit::declare_accepting_condition): Arrange so that this
      function can be called during the construction of the automaton.
      (tgba_explicit::complement_all_accepting_conditions): New method.
      (tgba_explicit::has_accepting_condition): Adjust to call
      bdd_dict::is_registered_accepting_variable.
      * src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state,
      tgba_explicit::complement_all_accepting_conditions): New methods.
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
      New files.
      * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
      libtgbaalgos_la_SOURCES): Add them.
      * src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt
      and tbalbtt.
      (tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove.
      * src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t".
      * src/tgbatest/ltl2tgba.cc: Implement the -f and -F options.
      * src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of
      "spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add
      also check the ltl2tgba_fm translator.
      * wrap/python/spot.i: Wrap ltl2tgba_fm.
      * wrap/python/cgi/ltl2tgba.in: Add radio buttons to select
      between ltl2tgba and ltl2tgba_fm.
      * wrap/python/tests/ltl2tgba.py: Add support for the -f option.
      * wrap/python/tests/ltl2tgba.test: Try the -f option.
      2b9f1720
  17. 10 Aug, 2003 1 commit
  18. 07 Aug, 2003 1 commit
  19. 31 Jul, 2003 1 commit
  20. 30 Jul, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. · 372d4907
      Alexandre Duret-Lutz authored
      (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES)
      (ltlgspn_srg_SOURCES): New variables.
      (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg.
      
      * iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install
      gspn.hh.
      372d4907
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh, src/tgba/tgba.cc · 24099078
      Alexandre Duret-Lutz authored
      (tgba::project_state): New method.
      * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
      (tgba_product::project_state): New method.
      * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc
      (tgba_bta_proxy::project_state): New method.
      * src/tgbaalgos/magic.cc (magic_search::print_result): Take
      a restrict argument.
      24099078