1. 09 Dec, 2009 2 commits
  2. 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
  3. 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
  4. 26 Nov, 2009 3 commits
  5. 25 Nov, 2009 2 commits
  6. 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
  7. 23 Nov, 2009 4 commits
  8. 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
  9. 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
  10. 17 Nov, 2009 1 commit
  11. 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
  12. 12 Nov, 2009 3 commits
  13. 11 Nov, 2009 2 commits
  14. 10 Nov, 2009 5 commits
    • Alexandre Duret-Lutz's avatar
      Do not comment states in the never claim by default. It takes too · 8c6a2b33
      Alexandre Duret-Lutz authored
      much time when the formula is large, and it is useless when the
      purpose is model-checking with Spin.
      
      * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the
      comments option.
      * src/tgbaalgos/neverclaim.cc (never_claim_bfs,
      never_claim_reachable): Honor the comment option.
      * src/tgba/tests/ltl2tgba.cc (-N): Do not comment states.
      (-NN) New option to output a commented never claim.
      8c6a2b33
    • Damien Lefortier's avatar
      * src/tgba/taa.cc, src/tgba/taa.hh: Fix it. · 1d8b115b
      Damien Lefortier authored
      * src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both
      the translation and the language containment checker.
      * src/tgbatest/spotlbtt.test: Update TAA related tests.
      1d8b115b
    • Alexandre Duret-Lutz's avatar
      Use tgba_explicit_formula instead of tgba_explicit_string in FM. · 007e2bd0
      Alexandre Duret-Lutz authored
      This gives a nice speedup (>1.4) in the ltlcounter benchmark,
      because we no longer have to generate a copy the string
      representations of the LTL formulae.
      
      * src/tgbaalgos/ltl2tgba_fm.cc: Adjust.  Also get rid of the
      formulae_seen map, since we can now ask the tgba_explicit_formula
      if it knows the state.
      007e2bd0
    • Alexandre Duret-Lutz's avatar
      Ease debugging of LTL formulae leaks. · 32a4647d
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc: Dump all LTLinstances with their
      reference count.
      32a4647d
    • Alexandre Duret-Lutz's avatar
      Introduce tgba_explicit_labelled<label> so that we can build · 4e22bb8b
      Alexandre Duret-Lutz authored
      tgba_explicit instances labelled by other objects than strings.
      
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
      Split tgba_explicit in two levels: tgba_explicit with unlabelled
      states, and tgba_explicit_labelled templated by the type of
      the label.  Define tgba_explicit_string (with the interface
      of the former tgba_explicit class) and tgba_explicit_formula
      for future use in ltl2tgba.cc.
      * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
      src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
      use tgba_explicit_string when appropriate.
      4e22bb8b
  15. 09 Nov, 2009 6 commits
    • Alexandre Duret-Lutz's avatar
      Do not use the Boost macro from the Autoconf macro archive. · d3dcecc6
      Alexandre Duret-Lutz authored
      * m4/boost.m4: Rewrite like I already did in Vaucanson.
      d3dcecc6
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/ltlcounter.test (run): Do not run with n=12, as · 39912aa5
      Alexandre Duret-Lutz authored
      the test case might become too slow for the autobuilder.
      39912aa5
    • Alexandre Duret-Lutz's avatar
      Add a benchmark using Kristin Y. Rozier's LTLcounter scripts. · 3ce16272
      Alexandre Duret-Lutz authored
      * bench/ltlcounter/README, bench/ltlcounter/run,
      bench/ltlcounter/plot.gnu, bench/ltlcounter/defs.in,
      bench/ltlcounter/Makefile.am: New files.
      * bench/Makefile.am (SUBDIRS): Add ltlcounter.
      * configure.ac (AC_CONFIG_FILES): Adjust.
      * THANKS: Add her.
      3ce16272
    • Alexandre Duret-Lutz's avatar
      Use a timer to clock the different phases of the translation. · e539226e
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc: Add option -T.
      e539226e
    • Alexandre Duret-Lutz's avatar
      Deprecate ltl::destroy(f) in favor of f->destroy() · 77df39b4
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone):
      Transform this static function into a member function.
      * src/ltlvisit/destroy.hh (destroy): Document and declare as
      deprecated.
      * bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc,
      src/eltlparse/eltlparse.yy, src/eltltest/acc.cc,
      src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc,
      src/ltlast/automatop.cc, src/ltlast/binop.cc,
      src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
      src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy,
      src/ltltest/equals.cc, src/ltltest/randltl.cc,
      src/ltltest/readltl.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltltest/tostring.cc,
      src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc,
      src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
      src/tgba/bddprint.cc, src/tgba/taa.cc,
      src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc,
      src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
      wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove
      the #include "destroy.hh" when appropriate.
      77df39b4
    • Alexandre Duret-Lutz's avatar
      Deprecate ltl::clone(f) in favor of f->clone(). · 48fb19ea
      Alexandre Duret-Lutz authored
      * src/ltlvisit/clone.hh (clone): Document and declare as deprecated.
      * src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc,
      src/ltlvisit/clone.cc, src/ltlvisit/contain.cc,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
      src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py:
      Adjust clone() usage, and remove the #include "clone.hh" when
      appropriate.
      48fb19ea