1. 05 Jan, 2011 4 commits
    • 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
      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
  2. 10 Dec, 2010 1 commit
  3. 01 Dec, 2010 1 commit
  4. 30 Nov, 2010 1 commit
  5. 27 Nov, 2010 1 commit
  6. 25 Nov, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Never claim output used to print the degeneralized automaton · 67f46b85
      Alexandre Duret-Lutz authored
      before some optional operations (like more optimizations, or a
      product).
      
      * src/tgbatest/ltl2tgba.cc (-N, -NN): Make sure we print the last
      automaton computed, not just the automaton when we degeneralized
      it.  We may have applied other algorithms since the original
      degeneralization.
      67f46b85
  7. 06 Nov, 2010 4 commits
    • Alexandre Duret-Lutz's avatar
      Cosmetics to please sanity checks. · 1e0f99e8
      Alexandre Duret-Lutz authored
      * src/neverparse/public.hh, src/neverparse/parsedecl.hh: Fix
      inclusion guards.
      * src/tgba/tgbaexplicit.hh, src/tgbatest/emptchk.test,
      src/tgbatest/ltl2tgba.cc: Fix trailing whitespaces.
      1e0f99e8
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Do not output a counterexample by default in ltl2tgba, introduce · a6677c29
      Alexandre Duret-Lutz authored
      options -C and -CR for that.
      
      * src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control
      whether we want the accepting run to be printed or replayed.
      * src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR.
      a6677c29
    • Alexandre Duret-Lutz's avatar
      Cleanup neverclaim support. · ac08c5ab
      Alexandre Duret-Lutz authored
      * src/neverclaimparse/: Shorthen as ...
      * src/neverparse/:... this.
      * src/Makefile.am: Adjust, and add back the directories mistakenly
      removed by previous patch.
      * README: Adjust, and keep the file's width under 80 columns.
      * configure.ac: Adjust.
      * src/neverparse/Makefile.am, src/neverparse/fmterror.cc,
      src/neverparse/neverclaimparse.yy,
      src/neverparse/neverclaimscan.ll, src/neverparse/public.hh:
      Fix copyright.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread.
      * src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim.
      * src/tgbatest/readneverclaim.cc: Delete.
      * src/tgbatest/neverclaimread.test: Use ltl2tgba instead of
      neverclaimread.
      ac08c5ab
  8. 15 Apr, 2010 1 commit
  9. 12 Apr, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Add support for W (weak until) and M (strong release) operators. · 0fc0ea31
      Alexandre Duret-Lutz authored
      * src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for
      these new operators.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them.
      * src/ltltest/reduccmp.test: Add new tests for W and M.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
      src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc,
      src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
      Add support for W and M.
      * src/tgbatest/ltl2neverclaim.test: Test never claim output
      using LBTT, this is more thorough.  Also we cannot use -N
      any more in the spotlbtt.test.
      * src/tgbatests/ltl2tgba.cc: Define M and W for ELTL.
      * src/tgbatest/ltl2neverclaim.test: Test W and M, and use
      -DS instead of -N, because lbtt-translate does not want
      to translate these operators for tools that masquerade as Spin.
      0fc0ea31
  10. 06 Mar, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Keep acceptance conditions on transitions going to accepting SCCs · 27b419ce
      Alexandre Duret-Lutz authored
      by default in scc_filter().
      
      Doing so helps the degeneralization algorithm, because it will
      have more opportunity to be in an accepting level when it reaches
      the accepting SCCs.
      
      * src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
      remove_all_useless argument.
      (filter_iter::process_link): Use the flag to decide whether to
      filter acceptance conditions going to accepting SCCs.
      (scc_filter): Take a remove_all_useless argument and pass it to
      filter_iter.
      * src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
      and document the function.
      * src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
      for remove_all_useless=false and add -R3f for
      remove_all_useless=true.
      * src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
      the degeneralization worse than -R3.
      27b419ce
  11. 03 Mar, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: apply -R3 before -D or -DS. · efb15a91
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
      degeneralization, because it might remove useless acceptance
      conditions.  I realized this while looking at experiments from
      Rüdiger Ehlers.
      efb15a91
  12. 30 Jan, 2010 4 commits
    • Alexandre Duret-Lutz's avatar
      Remove the theoretically bogus "containment" option of ltl2tgba_fm. · dd71e37d
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
      Remove the containment option.
      * src/tgbafromfile.cc, src/tgbafromfile.hh: Remove the
      containment_ member.
      * src/tgbatest/ltl2tgba.cc (syntax): Remove -c option for
      FM algorithm, use it exclusively for TAA.
      dd71e37d
    • Alexandre Duret-Lutz's avatar
      Make Couvreur/FM the default translation. · 55b693e1
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (syntax, main): Do it.
      * NEWS: Mention it.
      55b693e1
    • Alexandre Duret-Lutz's avatar
      Overhaul LaCIM's ELTL options. · 369e4c41
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select
      this algorithm and -lo to add the default LTL operators.  This
      replace the undocumented hack to add LTL operators when the
      formula with read for command-line, or the automaton was output
      for LBTT.
      * src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update
      call syntax.
      * NEWS: Mention -le, -lo, and -taa.
      369e4c41
    • Alexandre Duret-Lutz's avatar
      Touch up -R3b handling. · 9a43a06b
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other
      LaCIM options.
      (main): Speak of "symbolic SCC pruning" instead of "deleting
      unaccepting SCC", and do that right after the translation, before
      degeneralization.  Also error out when -R3b is used on non
      symbolic automata.
      9a43a06b
  13. 24 Jan, 2010 1 commit
    • Guillaume Sadegh's avatar
      Fix copyrights. · 3a974d61
      Guillaume Sadegh authored
      * bench/Makefile.am, bench/gspn-ssp/Makefile.am,
      bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am,
      bench/split-product/Makefile.am, configure.ac,
      iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh,
      iface/nips/Makefile.am, iface/nips/common.cc,
      iface/nips/common.hh, iface/nips/dottynips.cc,
      iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am,
      src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
      src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc,
      src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am,
      src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh,
      src/evtgba/product.cc, src/evtgba/product.hh,
      src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am,
      src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
      src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
      src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
      src/evtgbatest/readsave.test, src/ltlast/atomic_prop.cc,
      src/ltlast/atomic_prop.hh, src/ltlast/binop.cc,
      src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
      src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
      src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
      src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlenv/declenv.cc,
      src/ltlenv/declenv.hh, src/ltlenv/environment.hh,
      src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
      src/ltltest/Makefile.am, src/ltltest/defs.in,
      src/ltltest/equals.cc, src/ltltest/equals.test,
      src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
      src/ltltest/parse.test, src/ltltest/parseerr.test,
      src/ltltest/randltl.cc, src/ltltest/readltl.cc,
      src/ltltest/reduccmp.test, src/ltltest/syntimpl.cc,
      src/ltltest/syntimpl.test, src/ltltest/tostring.cc,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/ltlvisit/basicreduce.cc,
      src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
      src/ltlvisit/contain.cc, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc,
      src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/misc/bddalloc.cc,
      src/misc/bddop.cc, src/misc/bddop.hh, src/misc/freelist.hh,
      src/misc/hash.hh, src/misc/minato.cc, src/misc/minato.hh,
      src/misc/optionmap.cc, src/misc/timer.cc, src/misc/timer.hh,
      src/saba/Makefile.am, src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
      src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
      src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
      src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
      src/sabatest/Makefile.am, src/sabatest/defs.in,
      src/sanity/Makefile.am, src/tgba/Makefile.am,
      src/tgba/bdddict.cc, src/tgba/bddprint.cc,
      src/tgba/formula2bdd.cc, src/tgba/state.hh,
      src/tgba/succiterconcrete.cc, src/tgba/taatgba.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbacomplement.cc,
      src/tgba/tgbacomplement.hh, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
      src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc,
      src/tgba/tgbaunion.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/ltl2taa.cc,
      src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim.hh,
      src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/stats.cc,
      src/tgbaalgos/stats.hh, src/tgbaparse/Makefile.am,
      src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am,
      src/tgbatest/bddprod.test, src/tgbatest/complementation.cc,
      src/tgbatest/complementation.test, src/tgbatest/defs.in,
      src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
      src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
      src/tgbatest/explpro3.test, src/tgbatest/explpro4.test,
      src/tgbatest/explprod.cc, src/tgbatest/explprod.test,
      src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.cc,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.cc,
      src/tgbatest/mixprod.test, src/tgbatest/powerset.cc,
      src/tgbatest/readsave.cc, src/tgbatest/readsave.test,
      src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
      src/tgbatest/reductgba.test, src/tgbatest/taatgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test,
      src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py:
      Fix copyrights.
      3a974d61
  14. 18 Jan, 2010 1 commit
  15. 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
  16. 26 Nov, 2009 1 commit
  17. 25 Nov, 2009 1 commit
  18. 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
  19. 18 Nov, 2009 1 commit
    • 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
  20. 12 Nov, 2009 2 commits
  21. 10 Nov, 2009 3 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
    • 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
  22. 09 Nov, 2009 3 commits
    • 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
      Add missing instance_count() in automatop and eltl2tgba. · f2e941cd
      Alexandre Duret-Lutz authored
      * src/ltlast/automatop.hh, src/ltlast/automatop.cc: Add missing
      instance_count() functions.
      * src/tgbatests/eltl2tgba.cc: Add missing instance_count()
      assertions at the end.
      * src/tgbatests/ltl2tgba.cc: Also call automatop::instance_count(),
      even if automatop are not used in ltl2tgba yet.  This way we won't
      forget once eltl2tgba and ltl2tgba are merged.
      f2e941cd
  23. 03 Nov, 2009 1 commit
  24. 22 Oct, 2009 1 commit
    • Damien Lefortier's avatar
      Improve ltl_to_taa. · 7ce27ef9
      Damien Lefortier authored
      * src/tgba/taa.cc, src/tgba/taa.hh: taa_succ_iterator is not
      on-the-fly anymore allowing some redundant transitions to be
      removed. Also a new function to output a TAA.
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: Add the
      refined rules from Tauriainen.
      * src/tgbatest/ltl2tgba.cc: Use -c to activate refined rules in
      ltl_to_taa.
      * src/tgbatest/spotlbtt.test: More tests.
      7ce27ef9
  25. 16 Oct, 2009 1 commit
    • Damien Lefortier's avatar
      Add a new algorithm (from Tauriainen) to translate LTL formulae to · 627b6677
      Damien Lefortier authored
      TGBA which uses TAA as an intermediate representation.  This is a
      basic version, optimizations and enhancements will come later.
      
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: The algortihm.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba: New option: -taa, which uses this new
      translation algorithm.
      * src/tgbatest/spotlbtt.test: Add ltl2tgba -taa.
      627b6677
  26. 01 Oct, 2009 1 commit