1. 23 May, 2014 5 commits
  2. 20 May, 2014 4 commits
  3. 16 May, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/equals.cc: Fix style. · 7bcf6553
      Alexandre Duret-Lutz authored
      7bcf6553
    • Alexandre Duret-Lutz's avatar
      snf: Fix the handling of bounded repetition. · 05ed3def
      Alexandre Duret-Lutz authored
      star_normal_form() used to be called under bounded
      repetitions like [*0..4], but some of these rewritings
      are only correct for [*0..].  For instance
           (a*|1)[*]      can be rewritten to    1[*]
      but  (a*|1)[*0..1]  cannot be rewritten to 1[*0..1]
      it would be correct to rewrite the latter as (a[+]|1)[*0..1],
      canceling the empty word in a*.
      
      Also (a*;b*)[*]     can be rewritten to    (a|b)[*]
      but  (a*;b*)[*0..1]  cannot be rewritten to (a|b)[*0..1]
      and it cannot either be rewritten to (a[+]|b[+])[*0..1].
      
      This patch introduces a new function to implement
      rewritings under bounded repetition.
      
      * src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
      New function.
      * src/ltlvisit/simplify.cc: Use it.
      * src/ltltest/reduccmp.test: Add tests.
      * doc/tl/tl.tex: Document the rewritings implemented.
      05ed3def
  4. 15 May, 2014 3 commits
  5. 14 May, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      doc: update bibliographic references · 97617037
      Alexandre Duret-Lutz authored
      * doc/org/satmin.org, src/bin/man/dstar2tgba.x, src/bin/man/ltl2tgba.x:
      Cite the FORTE'14 paper.
      * doc/org/tools.org, src/bin/man/ltl2tgba.x: Replace the VECOS'11
      citation by IJCCBS'14.
      * src/bin/man/ltl2tgba.x: Cite SPIN'13.
      97617037
  6. 13 May, 2014 4 commits
  7. 28 Apr, 2014 1 commit
  8. 24 Apr, 2014 1 commit
  9. 11 Apr, 2014 1 commit
  10. 07 Apr, 2014 5 commits
  11. 03 Apr, 2014 1 commit
  12. 27 Mar, 2014 1 commit
  13. 20 Mar, 2014 1 commit
  14. 26 Feb, 2014 1 commit
  15. 17 Feb, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      tgba: remove the global_state and global_automaton argument of succ_iter · bd870f9a
      Alexandre Duret-Lutz authored
      * iface/dve2/dve2.cc, src/kripke/kripkeexplicit.cc,
      src/kripke/kripkeexplicit.hh, src/ta/tgtaexplicit.cc,
      src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
      src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh,
      src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
      src/tgba/tgbakvcomplement.hh, src/tgba/tgbamask.cc,
      src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
      src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
      src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc:
      Here.
      * NEWS: Mention it.
      bd870f9a
    • Alexandre Duret-Lutz's avatar
      tgba: remove the support_variable() method. · 0fba428c
      Alexandre Duret-Lutz authored
      * src/kripke/fairkripke.cc, src/kripke/fairkripke.hh,
      src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/tgba/taatgba.cc,
      src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
      src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
      src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
      src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc:
      Remove anything related to support_variables() and
      compute_support_variables().
      * NEWS: Mention it.
      * src/tgbaalgos/powerset.cc: Adjust the computation of all possible
      conditions.
      0fba428c
  16. 14 Feb, 2014 1 commit
  17. 12 Feb, 2014 6 commits
    • Alexandre Duret-Lutz's avatar
      gtec: replace nsheap by a simple unordered_map · 393637f1
      Alexandre Duret-Lutz authored
      nsheap was an horror full of virtual functions required to
      customize gtec to implement inclusion-based emptiness-check
      in GreatSPN support.  Since this support has been removed, we
      can remove the nsheap cruft as well.  Note that nsheap was
      also used in emptinessta for no good reason (the code from
      emptinessta was simply copied from gtec without cleanup).
      
      * src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
      Delete.
      * src/tgbaalgos/gtec/Makefile.am: Adjust.
      * src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/tgba2ta.cc, src/tgbaalgos/gtec/ce.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
      Use a simple unordered_map.
      393637f1
    • Alexandre Duret-Lutz's avatar
      gspn: remove the interface with GreatSPN · 46e4408a
      Alexandre Duret-Lutz authored
      It hasn't been tested for several year, may not even compile, has
      to be linked with source code that isn't even publicly available,
      and its presence was the only reason to keep some inefficient
      code in gtec.cc and friends.
      
      * iface/gspn/: Delete this directory.
      * iface/Makefile.am, configure.ac, README: Adjust.
      * m4/gspnlib.m4: Delete.
      * src/sanity/Makefile.am: Do not use LIBGSPN_CPPFLAGS.
      46e4408a
    • Alexandre Duret-Lutz's avatar
      simulation: use tuple and emplace_back for constraints · 83ed4f8c
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/simulation.cc: Here.
      83ed4f8c
    • Alexandre Duret-Lutz's avatar
      Replace << "c" by << 'c', and check for it in style.sh · ba5aff24
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Add a test.
      * iface/dve2/dve2.cc, iface/dve2/dve2check.cc, src/bin/common_output.cc,
      src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltlcross.cc,
      src/dstarparse/dra2ba.cc, src/dstarparse/fmterror.cc,
      src/dstarparse/nsa2tgba.cc, src/kripke/kripkeprint.cc,
      src/kripkeparse/fmterror.cc, src/ltlast/atomic_prop.cc,
      src/ltlast/bunop.cc, src/ltltest/ltlrel.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/lbt.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/relabel.cc,
      src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/misc/bitvect.cc,
      src/misc/optionmap.cc, src/misc/timer.cc, src/neverparse/fmterror.cc,
      src/priv/freelist.cc, src/saba/sabacomplementtgba.cc,
      src/sabaalgos/sabadotty.cc, src/taalgos/dotty.cc,
      src/taalgos/minimize.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc,
      src/tgba/futurecondcol.cc, src/tgba/taatgba.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/cycles.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/weight.cc, src/tgbaalgos/word.cc,
      src/tgbaparse/fmterror.cc, src/tgbatest/bitvect.cc,
      src/tgbatest/complementation.cc, src/tgbatest/intvcmp2.cc,
      src/tgbatest/intvcomp.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc: Replace << "c" by << 'c' when
      appropriate.
      ba5aff24
    • Alexandre Duret-Lutz's avatar
      c++11: replace push(Type(args...)) by emplace(args...) · 49c66c63
      Alexandre Duret-Lutz authored
      This of course concerns push_back and push_front as well.
      
      * src/bin/common_finput.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
      src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltlfilt.cc,
      src/dstarparse/dstarparse.yy, src/kripkeparse/kripkeparse.yy,
      src/ltlast/formula.cc, src/ltlparse/ltlparse.yy, src/misc/minato.cc,
      src/neverparse/neverclaimparse.yy, src/priv/bddalloc.cc, src/ta/ta.cc,
      src/taalgos/emptinessta.cc, src/tgba/taatgba.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/sccstack.cc,
      src/tgbaalgos/magic.cc, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/rundotdec.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03opt.cc, src/tgbaparse/tgbaparse.yy: Use emplace
      to make the code less verbose and avoid creating temporaries.
      49c66c63
    • Alexandre Duret-Lutz's avatar
      c++11: more range-based for · e0bbc265
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc, src/tgbaalgos/replayrun.cc: Here.
      e0bbc265