1. 20 Jan, 2010 3 commits
    • Damien Lefortier's avatar
      When iterating a hash_map, be careful not to delete i->first · 04827ef4
      Damien Lefortier authored
      before doing ++i to avoid memory issues.
      
      * src/tgba/taatgba.cc, src/tgba/taatgba.hh,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Fix them.
      04827ef4
    • Damien Lefortier's avatar
      Minor fixes to compile with GCC 3.3 · 0d6fd322
      Damien Lefortier authored
      * src/ltlast/automatop.cc, src/ltlast/automatop.hh: Rename nfa as
      get_nfa to avoid a name clash with the `nfa' class.
      * src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/tostring.cc, src/tgbaalgos/eltl2tgba_lacim.cc: Use
      get_nfa instead of nfa.
      * src/tgba/tgbasafracomplement.cc: Don't use a
      const_reverse_iterator.
      0d6fd322
    • Alexandre Duret-Lutz's avatar
      Remove some non-determinism in random_graph() · dcf7eed1
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/randomgraph.cc (random_graph): Revert the part of
      the patch from 2007-02-06 which silently replaced the use of state
      index by state pointers.  Storing states pointer in this map cause
      some non-determinism because of the memory layout.  It was almost
      impossible to reproduce bugs found by tests based on randtgba.
      dcf7eed1
  2. 19 Jan, 2010 1 commit
  3. 18 Jan, 2010 1 commit
  4. 17 Jan, 2010 3 commits
  5. 16 Jan, 2010 1 commit
    • Damien Lefortier's avatar
      Introduce taa_tgba_labelled<label> so that we can build · 7c20d8ae
      Damien Lefortier authored
      taa_tgba instances labelled by other objects than strings
      in the same way Alexandre did for tgba_explicit.
      
      * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Split taa_tgba in two
      levels: taa_tgba with no label and taa_tgba_labelled templated by
      the type of the label.  Define taa_tgba_string (with the interface
      of the former taa_tgba class) and taa_tgba_formula for future use
      in ltl2taa.cc.
      * src/tgbaalgos/ltl2taa.cc, src/tgbatest/taatgba.cc: Adjust to use
      taa_tgba_string.
      7c20d8ae
  6. 06 Jan, 2010 1 commit
  7. 05 Jan, 2010 1 commit
    • Damien Lefortier's avatar
      Merge eltl2tgba.cc into ltl2tgba.cc. · 830e4828
      Damien Lefortier authored
      * src/tgbatest/eltl2tgba.cc: Remove.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc: New option: -xltl to translate an
      extended LTL instead of an LTL, a feature previously offered by
      eltl2tgba.cc. Also: -R3b to use delete_unaccepting_scc.
      * src/tgbatest/spotlbtt.test: Adjust.
      830e4828
  8. 18 Dec, 2009 1 commit
  9. 11 Dec, 2009 1 commit
  10. 09 Dec, 2009 2 commits
  11. 30 Nov, 2009 2 commits
    • Guillaume Sadegh's avatar
      An algorithm to complement TGBA into SABA. · d659001f
      Guillaume Sadegh authored
      * src/saba/sabacomplementtgba.hh,
      src/saba/sabacomplementtgba.cc: New.  The algorithm.
      * src/saba/Makefile.am: Adjust.
      * src/sabatest/sabacomplementtgba.cc, src/sabatest/Makefile.am,
      src/sabatest/defs.in: New.  Test the algorithm.
      * configure.ac, src/Makefile.am: Adjust to the new directory
      `sabatest'.
      d659001f
    • Guillaume Sadegh's avatar
      Add a new type of automata: State-labeled Alternating Büchi · 7cb6ff33
      Guillaume Sadegh authored
      Automata (SABA).
      
      * src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh: New.  Interface for
      SABA (State-labeled Alternating Büchi Automata).
      * src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh: New.  Default
      implementation for a conjunction of states.
      * src/saba/Makefile.am: New.
      * src/Makefile.am, configure.ac: Adjust.
      * src/sabaalgos/sabareachiter.cc,
      src/sabaalgos/sabareachiter.hh: New.  Iterate over all reachable
      states of a spot::saba.
      * src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh: New.
      Print reachable states in dot format.
      * src/sabaalgos/Makefile.am: New.
      7cb6ff33
  12. 27 Nov, 2009 1 commit
    • Guillaume Sadegh's avatar
      Rename the class taa as taa_tgba. · f00aa49d
      Guillaume Sadegh authored
      * src/tgba/taa.cc, src/tgba/taa.hh: Rename as ...
      * src/tgba/taatgba.cc, src/tgba/taatgba.hh: ... these, and
      rename the class taa as taa_tgba.
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/taa.test: Rename as ...
      * src/tgbatest/taatgba.test ... this.
      * src/tgbatest/taa.cc: Rename as ...
      * src/tgbatest/taatgba.cc ... this, and adjust.
      f00aa49d
  13. 26 Nov, 2009 3 commits
  14. 25 Nov, 2009 2 commits
  15. 24 Nov, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Detect running timers, and stop a timer in ltl2tgba. · b796bb3d
      Alexandre Duret-Lutz authored
      * src/misc/timer.hh (time_info::running): New attribute.
      (time_info::start, time_info::stop): Update and check
      time_info::running.
      * src/misc/timer.cc (timer_map::print): Mark running timers with
      a "+" in the output.
      * src/tgbatest/ltl2tgba.cc (main): Rename the name of the timers
      for SCC and simulation reduction, and actually stop the SCC timer.
      b796bb3d
  16. 23 Nov, 2009 4 commits
  17. 20 Nov, 2009 2 commits
    • Alexandre Duret-Lutz's avatar
      Strip useless acceptance conditions in scc_filter(). · dfb9c662
      Alexandre Duret-Lutz authored
      A useless acceptance conditions is one that is always implied by
      another.
      
      * src/misc/bddop.hh, src/misc/bddop.cc
      (compute_neg_acceptance_conditions): New function.
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
      (set_acceptance_conditions): New function.
      * src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot):
      Keep track of useful acceptance conditions.
      (useful_acc_of): New function.
      * src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New
      attributes.
      * src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter
      useless acceptance conditions.
      (scc_filter): Compute useful acceptance conditions and pass them
      to filter_iter.
      dfb9c662
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/sccfilter.cc (scc_filter): Merge transitions · 5d427f6d
      Alexandre Duret-Lutz authored
      after removing acceptance conditions.
      5d427f6d
  18. 18 Nov, 2009 5 commits
    • Alexandre Duret-Lutz's avatar
      Remove prune_scc(), prune_acc(), and related fonctions. · 7ac3c5e7
      Alexandre Duret-Lutz authored
      * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh (prune_scc,
      prune_acc, remove_component, compute_scc, remove_acc,
      is_not_accepting, delete_scc, is_terminal, remove_scc,
      display_scc): Remove anything related to the simplification of
      SCCs.
      7ac3c5e7
    • Alexandre Duret-Lutz's avatar
      Replace prune_scc() by scc_filter(). · 7ea51cc6
      Alexandre Duret-Lutz authored
      prune_scc() leaked memory and failed to remove chains of useless SCCs.
      
      * src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Call
      scc_filter() instead of prune_scc(), and do it before running
      any simulation-based reduction.
      * src/tgbaalgos/reductgba_sim.hh (reduc_tgba_sim): Return a const
      tgba*.
      * src/tgbatest/ltl2tgba.cc: Call scc_filter() instead of
      prune_scc().
      * src/tgbatest/scc.test: Add two more tests that failed with
      prune_scc().
      7ea51cc6
    • Alexandre Duret-Lutz's avatar
      Quick implementation of a "useless SCC" filter using scc_map. · 74f620d1
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: New
      files.
      * src/tgbaalgos/Makefile.am: Add them.
      74f620d1
    • 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
    • Alexandre Duret-Lutz's avatar
      Make it easy to filter states while iterating over an automaton. · ac5dda10
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/reachiter.hh (tgba_reachable_iterator::want_state):
      New method.
      * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::want_state):
      Implement it.
      (tgba_reachable_iterator::run): Call want_state before processing
      a state.
      ac5dda10
  19. 17 Nov, 2009 1 commit
  20. 13 Nov, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Replace the hash key construction of LTL formulae by a simple · f2be64dd
      Alexandre Duret-Lutz authored
      counter updated each time we create a new (unique) formula.
      
      Doing so saves a lot of memory during the translation of the
      ltlcounter formulae, because the formulae are quite big and
      storing a string representation of each formula on its node was a
      bad idea.  For instance with n=12, the translation now uses 40MB
      where it used 290MB.  (Note: in both cases, 20MB is being used by
      the BDD cache.)
      
      * src/ltlast/formula.hh (hash_key_): Rename as ...
      (count_): ... this.
      (hash): Adjust.
      (max_count): New static variable to count the number of
      formulae created.
      (formula): Update max_count and set count_.
      (dump): Make it a virtual pure method.
      (set_key_): Remove.
      (formula_ptr_less_than): Speed up and return false when
      the two formula pointer are equal.
      * src/ltlast/formula.cc (set_key_, dump): Remove.
      * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/automatop.cc, src/ltlast/automatop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/multop.cc,
      src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
      Empty the constructor (do not precompute the dump_ anymore),
      and add a dump() implementation.
      f2be64dd
  21. 12 Nov, 2009 3 commits