1. 18 Nov, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix acceptance check in scc_map: trivial SCCs are not accepting. · 99981153
      Alexandre Duret-Lutz authored
      Also compute useless SCCs.
      
      * src/tgbaalgos/scc.cc (scc_map::scc::trivial): New field.
      (scc_stats::useless_scc_map): New field.
      * src/tgbaalgos/scc.cc (scc_map::build_map): Mark SCCs that are
      not trivial.
      (scc_map::accepting): Always return false for trivial SCC.
      (build_scc_stats): Fill in useless_scc_map.
      99981153
  2. 18 Sep, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Optimize previous patch. · fd0de04d
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::scc::supp_rec): Initialize to
      bddfalse, since this cannot occur in reallife.
      * src/tgbaalgos/scc.cc (scc_map::update_supp_rec): Adjust.
      fd0de04d
  3. 17 Sep, 2009 2 commits
  4. 08 Jul, 2009 1 commit
    • Flix Abecassis's avatar
      Add 2 benchmarks directories. · 414956c5
      Flix Abecassis authored
      Add an algorithm to split an automaton in several automata.
      
      * bench/scc-stats: New directory.  Contains input files and test
      program for computing statistics.
      * bench/split-product: New directory.  Contains test program for
      synchronised product on splitted automata.
      * bench/split-product/models: New directory.  Contains Promela
      files and LTL formulae that should be verified by the models.
      * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh:
      New files.  Small class to avoid long initializations with numerous
      constants when translating to TGBA many LTL formulae from a
      given file.
      * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh:
      New file.  From a single automaton, create, at most,
      X sub automata.
      * src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh:
      Adjust to compute self-loops count.
      414956c5
  5. 02 Jun, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/scc.test: New file. · a2b6bef0
      Alexandre Duret-Lutz authored
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbaalgos/scc.hh: More documentation.
      * src/tgbaalgos/scc.cc (scc_recurse): Fix computation of
      acc_paths and dead_paths.  Prevent recursions in states that
      have already been visited.
      a2b6bef0
  6. 28 May, 2009 4 commits
    • Alexandre Duret-Lutz's avatar
      Test "ltl2tgba -FC" and plug the memory leaks of scc_map. · 35298429
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::~scc_map): Declare it.
      * src/tgbaalgos/scc.cc (scc_map::~scc_map): Implement it.
      (scc_map::build_map): Delete duplicate states.
      * src/tbbatest/ltl2tgba.test: Run ltl2tgba -FV to catch
      memory leaks with valgrind.
      35298429
    • Alexandre Duret-Lutz's avatar
      Number states using negative values and SCCs using nonnegative · 15b3b9e0
      Alexandre Duret-Lutz authored
      values.
      
      Before this change states were numbered using positive values and
      SCCs using negative values.  That meant the user had to work with
      negative values.  With this changes, the nonnegative values used
      to label SCCs can also directly be used as index in the scc_map_.
      
      * src/tgbaalgos/scc.hh (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of,
      scc_map::initial, scc_map::scc_type, scc_map::succ,
      scc_map::accepting): Adjust prototypes to take or return unsigned
      arguments.
      * src/tgbaalgos/scc.cc: Adjust prototypes of the above functions.
      (scc_map::build_map, scc_map::relabel_component): Number states
      using negative values, and SCCs using nonnegative values.
      (dump_scc_dot): Adjust to use nonnegative values.
      15b3b9e0
    • Alexandre Duret-Lutz's avatar
      Store the scc_map_ as a vector instead of a std::map. There is no · 96a7a49c
      Alexandre Duret-Lutz authored
      point in using a map since the SCC are numbered in sequence.
      
      * src/tgbaalgos/scc.hh (scc_map::relabel_component): Return the
      number of the SCC instead of taking it as argument.
      (scc_map::scc_num_): Delete this variable.  scc_map_.size() gives
      the same information.
      (scc_map::scc_map_type): Define using std::vector instead of
      std::map.
      * src/tgbaalgos/scc.cc: Adjust all uses.
      96a7a49c
    • Alexandre Duret-Lutz's avatar
      Keep track of conditions in SCC, and add a more verbose dump. · 07ead613
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
      New functions.
      (scc_map::scc::conds): New attribute.
      (dump_scc_dot): Take an optional VERBOSE argument.
      * src/tgbaalgos/scc.cc (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
      Implement these new functions.
      (dump_scc_dot): Display number of states, conditions and
      acceptance conditions, with VERBOSE is set.
      (build_map): Fill the new scc_map::scc::cond field.
      07ead613
  7. 25 Mar, 2009 1 commit
  8. 11 Dec, 2008 2 commits
  9. 10 Dec, 2008 1 commit