1. 04 Feb, 2011 2 commits
  2. 03 Feb, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      Read guard of the form !(x) in neverclaims. · 91e51c4c
      Alexandre Duret-Lutz authored
      So far all neverclaims encountered would use (!(x)), but the
      files from the Büchi store do not.
      
      * src/neverparse/neverclaimscan.ll: Accept ! in front of guard,
      so that we can read Promela files from Goal's Büchi store.
      * src/tgbatest/neverclaimread.test: Test it.
      91e51c4c
    • Alexandre Duret-Lutz's avatar
      Recognize Goal's syntax for Boolean operators. · 3278844c
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll: Recognize ~, -->, and <--> operators
      from Goal, to ease the use of formulas provided by the Goal team.
      * src/ltltest/equals.test: Use these once, just to be on the
      safe side.
      3278844c
    • Alexandre Duret-Lutz's avatar
      Minor fixes to ltl2tgba.html. · 2fe5b3fb
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/css/ltl2tgba.css,
      wrap/python/ajax/ltl2tgba.html: Tweak a few things for Firefox
      3.0, and fix a </li> tag.
      2fe5b3fb
  3. 01 Feb, 2011 3 commits
  4. 28 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fixup minimize_monitor(). · ad93f875
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding
      incorrect monitor if the input tgba is not deterministic.
      * src/tgbatest/ltl2tgba.test: Add test case.
      ad93f875
  5. 27 Jan, 2011 7 commits
    • Alexandre Duret-Lutz's avatar
      more files to ignore · dd0f01fe
      Alexandre Duret-Lutz authored
      dd0f01fe
    • Alexandre Duret-Lutz's avatar
      Report formulas that are both safety and guarantee. · c8140de9
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both
      safety and guarantee.
      * src/tgbatest/obligation.test: Add cases.
      c8140de9
    • Alexandre Duret-Lutz's avatar
      Rename is_safety_automaton() as is_guarantee_automaton() and · db124d02
      Alexandre Duret-Lutz authored
      implement is_safety_mwdba().
      
      Note: I swapped the name of safety and guarantee when I
      implemented is_safety_automaton() on 2010-03-20.  Fortunately,
      is_safety_automaton() was only used where is_guarantee_automaton()
      would have been correct.
      
      * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ...
      (is_guarantee_automaton): ... this.
      (is_safety_mwdba): New function.
      * src/tgbaalgos/safety.hh: Adjust and add documentation.
      * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead
      of is_safety_automaton().
      * src/tgbatests/safety.test: Rename as ...
      * src/tgbatests/obligation.test: ... this, and augment the
      test.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula
      represent a safety, guarantee, or obligation property.
      * NEWS: Adjust.
      db124d02
    • Alexandre Duret-Lutz's avatar
      * NEWS: Minor rewritings. · 14b701b5
      Alexandre Duret-Lutz authored
      14b701b5
    • Alexandre Duret-Lutz's avatar
      Replace delete by destroy in comments dealing with states. · 0c9c9fc6
      Alexandre Duret-Lutz authored
      * src/tgba/succiter.hh, src/tgba/tgba.hh,
      src/tgba/tgbabddconcrete.hh, src/tgba/tgbaproduct.hh,
      src/tgba/tgbaunion.hh, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.hh,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Update comments
      to say that we "destroy" a state instead of "deleting" it.
      0c9c9fc6
    • Alexandre Duret-Lutz's avatar
      Update gspn interface for recent tools. · 95cc50da
      Alexandre Duret-Lutz authored
      * iface/gspn/ssp.cc: Use the new destroy() interface, and
      fix a couple of recent g++ reports.
      * iface/gspn/gspn.cc: Adjust to newer g++.
      95cc50da
    • Alexandre Duret-Lutz's avatar
      Introduce a destroy() method on states, and use it instead of delete. · 574a2285
      Alexandre Duret-Lutz authored
      Right now, destroy() just executes "delete this".  But in a later
      version, we will rewrite tgba_explicit so that it does not
      allocate new states (and the destroy() method for explicit state
      will do nothing).
      
      * src/tgba/state.hh (state::destroy): New method, to replace
      state::~state() in the future.
      (shared_state_deleter): New function.
      * src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc,
      src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc,
      src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
      src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc,
      src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc,
      src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc,
      src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call
      "s->destroy()" instead of "delete s".
      * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc:
      Pass shared_state_deleter to the shared_ptr constructor, so that
      it calls destroy() instead of delete.
      574a2285
  6. 26 Jan, 2011 4 commits
  7. 19 Jan, 2011 1 commit
  8. 18 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Preliminary implementation of an ajax-based ltl2tgba translator. · 34f49a86
      Alexandre Duret-Lutz authored
      * configure.ac: Output wrap/python/ajax/Makefile.
      * wrap/python/Makefile.am (SUBDIRS): Add ajax.
      * wrap/python/ajax/Makefile.am, wrap/python/ajax/README,
      wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files.
      * wrap/python/ajax/css/, wrap/python/ajax/js,
      wrap/python/ajax/logos: New directories.
      * README: Document wrap/python/ajax/.
      34f49a86
  9. 17 Jan, 2011 1 commit
  10. 12 Jan, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      Fix "unused function" warnings reported by clang++. · fe535a15
      Alexandre Duret-Lutz authored
      * src/evtgbaparse/Makefile.am, src/ltlparse/Makefile.am,
      src/neverparse/Makefile.am, src/tgbaparse/Makefile.am
      (AM_CPPFLAGS): Define -DYY_NO_INPUT so that the unused yyinput()
      function does not get compiled.
      * src/eltlparse/Makefile.am (AM_CPPFLAGS): Likewise.
      (AM_CXXFLAGS): Also enable warnings.
      * src/eltlparse/eltlparse.yy: Move helper functions from
      the "%code requires" block to the "%code" block, so that they
      do not appear in the eltlparse.hh file (which is included in
      two places...).
      * iface/nips/nips.cc (search_error_callback_assert): Comment
      this unused function.
      fe535a15
    • Alexandre Duret-Lutz's avatar
      Fix segfault with g++-3.3. · 45d7c880
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_dfa): Fix deletion of the
      state_set_map.  It led to a crash when compiled with g++-3.3.
      45d7c880
    • Alexandre Duret-Lutz's avatar
      Fix a compilation failure with g++-3.3. · b39e68c5
      Alexandre Duret-Lutz authored
      * src/misc/hash.hh (identity_hash): New function.
      * src/tgba/tgbaexplicit.hh (tgba_explicit_number): Use
      identity_hash<int> instead of std::tr1::hash<int> that does not
      exist with g++-3.3.
      b39e68c5
  11. 07 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix usage of minimize_obligation in the CGI script. · 74f14567
      Alexandre Duret-Lutz authored
      * wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use
      minimize_obligation_new a pass the formula.
      * wrap/python/spot.i (minimize_obligation_new): New function, to
      cope with the strange specification of spot::minimize_obligation()
      not always creating a new automaton.
      74f14567
  12. 06 Jan, 2011 6 commits
  13. 05 Jan, 2011 7 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/Makefile.am: Remove the unused minimize program. · b9dd72b2
      Alexandre Duret-Lutz authored
      * src/tgbatest/minimize.cc: Delete.
      b9dd72b2
    • Alexandre Duret-Lutz's avatar
      Cleanup the minimize.hh interface. · 8c972ad3
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
      (minimize): Split into ...
      (minimize_wdba, minimize_monitor): ... these two functions.
      * src/tgbatest/ltl2tgba.cc (main): Adjust the call to
      minimize_monitor.
      * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to
      minimize_monitor and minimize_obligation.
      * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba,
      minimize_obligations.
      * src/tgba/tgbaexplicit.hh (tgba_explicit_string)
      (tgba_explicit_formula, tgba_explicit_number): Add fake
      declarations so that SWIG can see they inherits from tgba.
      8c972ad3
    • Alexandre Duret-Lutz's avatar
      Cleanup the DFA minimization algorithm. · 92126a6c
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize):  Move the minimization
      code into...
      (minimize_dfa): ... this new function, and fix the condition
      under which a partition is considered to be minimal.  Also
      use a map instead of a list to lookup known formulae.
      92126a6c
    • Alexandre Duret-Lutz's avatar
      Speed up the obligation test. · ef317685
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_obligation): Do not
      minimize aut_neg_f, complement min_aut_f instead.
      * src/tgbaalgos/minimize.hh: Adjust description.
      ef317685
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm · f06fc8ac
      Alexandre Duret-Lutz authored
      to label transient states.
      f06fc8ac
    • Alexandre Duret-Lutz's avatar
      Rewrite the check of WDBA state acceptance in minimize(). · 358d4bfd
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/powerset.hh (power_map): New structure, allowing
      the caller to retrieve the set of original states corresponding to
      the set in the deterministic automaton.
      (power_set): Adjust prototype to take a power_map instead of the
      acc_list.
      * src/tgbaalgos/powerset.cc (power_set): Strip all code using
      acc_list, and update power_set.
      * src/tgbaalgos/minimize.cc (minimize): Rewrite, using an
      algorithm similar to the one in the Dax paper to check whether
      state of the minimized automaton should be accepting.
      358d4bfd
    • Alexandre Duret-Lutz's avatar
      Add trivial() and one_state_of() functions to scc_map. · 37a8d1dc
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial,
      scc_map::one_state_of): Two new helper functions.
      37a8d1dc