1. 05 Jan, 2011 18 commits
    • Alexandre Duret-Lutz's avatar
      Make minimization of obligation properties and deterministic · 241ba112
      Alexandre Duret-Lutz authored
      monitor available in the CGI script.
      
      * wrap/python/spot.i: Declare the minimize() interface.
      * wrap/python/cgi-bin/ltl2tgba.in: Add reduce_dmonitor and
      reduce_wdba options.
      241ba112
    • Alexandre Duret-Lutz's avatar
      Add a WDBA benchmark. · edc71b80
      Alexandre Duret-Lutz authored
      * bench/wdba/: New directory.
      * bench/Makefile.am (SUBDIRS): Add wdba.
      * NEWS: Mention it.
      * configure.ac: Output bench/wdba/defs and bench/wdba/Makefile.
      edc71b80
    • Alexandre Duret-Lutz's avatar
      aadef1fd
    • Alexandre Duret-Lutz's avatar
      Speed up wdba.test, it was too slow for our buildfarm. · d72a2f0a
      Alexandre Duret-Lutz authored
      * src/tgbatest/wdba.test: Speed up execution by running only a
      couple of formula with valgrind.  Half of those with`-l -R3b' and
      the other half with `-f -R3'.
      d72a2f0a
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/ltl2tgba.cc (syntax): Regroup -M, -s, and -S option · 0392058e
      Alexandre Duret-Lutz authored
      under the same heading "automaton conversion".
      0392058e
    • Alexandre Duret-Lutz's avatar
      Preliminary support for monitors. · cc8dd49d
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (-M): New option for building
      deterministic monitors.
      * src/tgbaalgos/minimize.cc (minimize): Take a monitor
      argument and adjust the code.
      * src/tgbaalgos/minimize.hh (minimize): Document it.
      cc8dd49d
    • Alexandre Duret-Lutz's avatar
      "ltl2tgba -Rm -X foo.tgba" would fail. · a962bb6d
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without
      knowing the formula whose automaton is minimized.
      a962bb6d
    • Alexandre Duret-Lutz's avatar
      Fix bugs in minimize(). · 7d8a5310
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory
      leaks and a usage of the wrong automaton.
      * src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with
      valgrind.  This caught all the bugs fixed above.
      7d8a5310
    • Alexandre Duret-Lutz's avatar
      Fix bugs in minimize(), caught by spotlbtt.test. · 72139fd7
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize): Don't add acceptance
      conditions if the final set is empty.
      * src/tgbaalgos/powerset.cc (tgba_powerset): Add the initial state
      to acc_list if it is accepting.  Also do not compute an SCC build
      map if we don't have to build acc_list.
      72139fd7
    • Alexandre Duret-Lutz's avatar
      "ltl2tgba -Rm" will apply WDBA-minimization only if correct. · 54e10c25
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
      it is correct. Either we can quickly determine that a formula or
      its negation is a safety formula, or we can slowly check the
      equivalence of the WDBA-minimized automaton and the original
      automaton.
      * src/tgbatest/wdba.test: New test.
      * src/tgbatest/safety.test: Adjust comment.
      * src/tgbatest/spotlbtt.test: Use -Rm.
      * src/tgbatest/Makefile.am (TESTS): Add wdba.test.
      54e10c25
    • Alexandre Duret-Lutz's avatar
      Better resource handling in minimization. · f9e84ac2
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Delete the minimized automaton.
      * src/tgbaalgos/minimize.cc (minimize): Remove the call to
      unregister_variable() at the end.  It was both
      wrong (unregistering only the first variable) and useless ("delete
      del_a" will unregister all these variables).  Use a map and a set
      to keep track of free BDD variable and reuse them, otherwise the
      algorithm would sometimes use more variables than allocated.
      f9e84ac2
    • Alexandre Duret-Lutz's avatar
      Implement is_safety_automaton(). · 0af8d032
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New
      files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatests/ltl2tgba.cc: Add option "-O".
      * src/tgbaalgos/scc.hh: Update documentation.
      * src/tgbatest/Makefile.am (TESTS): Add safety.test.
      * src/tgbatest/safety.test: New file.
      0af8d032
    • Felix Abecassis's avatar
      99c1b607
    • Felix Abecassis's avatar
      Small fixes. · 52090e48
      Felix Abecassis authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbatest/minimize.cc: Delete useless includes.
      * src/tgbaalgos/minimize.cc: Delete useless includes,
      fixed acceptance conditions.
      * src/tgbatest/ltl2tgba.cc: Add -Rm option for minimization.
      * src/tgba/tgbaexplicit.cc: Fixed typo.
      52090e48
    • Felix Abecassis's avatar
      Test program for the minimization algorithm. · fac30eb0
      Felix Abecassis authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbatest/minimize.cc: New file.  Minimize an automaton
      from a LTL formula and compare the size of the initial automaton
      to the size of the minimized automaton.
      fac30eb0
    • Felix Abecassis's avatar
      * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: · 03e6dc47
      Felix Abecassis authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      New files.  Algorithm to minimize an automaton using first the powerset
      construction to determinize the input automaton, the automaton is then
      minimized using the standard algorithm, using BDDs to check if states
      are equivalent.
      03e6dc47
    • Felix Abecassis's avatar
      Modify the powerset algorithm to keep track of accepting states · e2e138f6
      Felix Abecassis authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      from the initial automaton.
      
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
      Added class tgba_explicit_number, a tgba_explicit where states are
      labelled by integers.
      * src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc:
      When building the deterministic automaton, keep track of which states
      were created from an accepting state in the initial automaton.
      The states are added to the new optional parameter (if not 0),
      acc_list.
      Use tgba_explicit_number instead of tgba_explicit_string to build
      the result.
      * src/tgbaalgos/scc.cc (spot): Small fix.
      Print everything on std::cout.
      e2e138f6
    • Alexandre Duret-Lutz's avatar
      Fix computation of support_conditions for bdd-based TGBA. · bd742ef6
      Alexandre Duret-Lutz authored
      This fixes a bug in the powerset of such TGBA on the minimize branch.
      
      * src/tgba/tgbabddconcrete.cc (compute_support_conditions): Also
      account for the conditions from the acceptance relations.
      * rc/tgba/tgbabddconcretefactory.hh, rc/tgba/tgbabddconcretefactory.cc
      (acceptance_conditions_support): New variable to hold the value
      of bdd_support(acceptance_conditions_support).
      * src/tgba/tgbabddconcretefactory.cc (finish): Update
      data_.acceptance_conditions_support.
      bd742ef6
  2. 26 Dec, 2010 1 commit
  3. 24 Dec, 2010 3 commits
    • Alexandre Duret-Lutz's avatar
      Define SWIG_TYPE_TABLE as suggested by the SWIG documentation. · f1d3e999
      Alexandre Duret-Lutz authored
      * wrap/python/Makefile.am: Add -DSWIG_TYPE_TABLE=spot.
      f1d3e999
    • Alexandre Duret-Lutz's avatar
      Use swig2.0 if available. · 8419cb6f
      Alexandre Duret-Lutz authored
      * configure.ac: Search for swig2.0 and swig.
      * wrap/python/Makefile.am: Use $(SWIG).
      8419cb6f
    • Alexandre Duret-Lutz's avatar
      Get rid of ltihooks.py. · 3d61b3a3
      Alexandre Duret-Lutz authored
      ltihooks.py apparently breaks the import mechanisms of Python 2.6,
      causes SWIG's runtime to fail to share a global type table, and
      yields various failures in our tests.
      
      * wrap/python/ltihooks.py: Delete.
      * wrap/python/Makefile.am (EXTRA_DIST): remove ltihooks.py.
      * wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
      wrap/python/tests/ltlsimple.py, wrap/python/tests/minato.py,
      wrap/python/tests/modgray.py, wrap/python/tests/optionmap.py,
      wrap/python/tests/setxor.py: Do not use ltihooks.
      * wrap/python/tests/run.in (pypath): Include the .libs/ directory
      in the search path so that Python can find the *.so libraries.
      3d61b3a3
  4. 12 Dec, 2010 2 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes. · 2ac37ad5
      Alexandre Duret-Lutz authored
      2ac37ad5
    • Alexandre Duret-Lutz's avatar
      Merge transitions in tgba_tba_proxy. · 01843379
      Alexandre Duret-Lutz authored
      With this change the output of
      ltl2tgba -f -x -k -DS "GF(p_1) & ... & GF(p_n)
      uses less than (n+1)^2 transitions when it used
      exactly (n+1)*(2^n) transitions before.
      
      * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Merge
      transitions going to the same states if they are both accepting or
      if neither are.
      (state_ptr_bool_t, state_ptr_bool_less_than): Helper type to
      store a transition in tgba_tba_proxy_succ_iterator.
      * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh
      (tgba_tba_proxy::transition_annotation): Remove.  We cannot
      implement this method if transitions are merged.
      01843379
  5. 10 Dec, 2010 2 commits
  6. 09 Dec, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Use a cache to speed up tgba_tba_proxy. · 3e7debe5
      Alexandre Duret-Lutz authored
      tgba_tba_proxy used to spend a lot of time (re)computing the
      acceptance condition common to all outgoing transition of a state.
      
      * src/tgba/tgbatba.hh (accmap_): New cache.
      (common_acceptance_conditions_of_original_state): New method.
      * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::~sync)
      Call common_acceptance_conditions_of_original_state() instead of
      computing the result.
      (~tgba_tba_proxy): Cleanup the cache.
      (common_acceptance_conditions_of_original_state): Implement it.
      3e7debe5
  7. 07 Dec, 2010 3 commits
  8. 04 Dec, 2010 4 commits
  9. 01 Dec, 2010 5 commits
  10. 30 Nov, 2010 1 commit