1. 07 Nov, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] · 4034b7f8
      Alexandre Duret-Lutz authored
      * src/bddop.c (bdd_setxor): New function.
      * src/bdd.h (bdd_setxor): New function.
      4034b7f8
  2. 06 Nov, 2010 10 commits
    • Alexandre Duret-Lutz's avatar
      * src/Makefile.am (libspot_la_LIBADD): Rename libneverclaimparse.la · 38913302
      Alexandre Duret-Lutz authored
      as libneverparse.la.
      * src/neverparse/Makefile.am: Install files in
      $(pkgincludedir)/neverparse, not $(pkgincludedir)/neverclaimparse.
      38913302
    • 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
      * src/tgbatest/neverclaimread.test: Check that Spot can read the · b1dbfed1
      Alexandre Duret-Lutz authored
      neverclaims it outputs.
      b1dbfed1
    • 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
      Make sure the neverclaim parser works on the output of spin and · fe1f59cd
      Alexandre Duret-Lutz authored
      ltl2ba.
      
      * src/neverparse/neverclaimparse.yy: Accept multiple labels
      for the same state.  Honor accepting states.  Forward parse
      error from the parser used for guards.  Accept "false" as a
      single instruction for a state.
      * src/neverparse/neverclaimscan.ll: Recognize "false" specifically,
      and remove the ";" hack.
      * src/tgba/tgbaexplicit.cc
      (tgba_explicit_string::~tgba_explicit_string): Adjust not to
      destroy a state twice.
      * src/tgba/tgbaexplicit.hh
      (tgba_explicit_string::add_state_alias): New function.
      * src/tgbatest/defs.in (SPIN, LTL2BA): New variables.
      * src/tgbatest/neverclaimread.test: Check error messages for
      syntax errors in guards.  Make sure we can read the output
      of `spin -f' and `ltl2ba -f' on a few test formulae.
      fe1f59cd
    • 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
    • Felix Abecassis's avatar
      Add never claim parser. · ab6ec5cb
      Felix Abecassis authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/neverclaimparse/: New directory.
      * src/neverclaimparse/fmterror.cc: New file.  Print a formatted parse
      error on a output stream.
      * src/neverclaimparse/neverclaimparse.yy: New file.  Parser declaration
      for Bison.
      * src/neverclaimparse/neverclaimscan.ll: New file.  Scanner declaration
      for Flex.
      * src/neverclaimparse/public.hh: New file.  Public header for external
      use.
      * src/neverclaimparse/parsedecl.hh: New file.  Header file for
      Flex-Bison interaction.
      * src/neverclaimparse/Makefile.am: New Makefile.
      * src/tgbatest/neverclaimread.cc: New file.  Test program for the
      never claim parser.
      * src/tgbatest/neverclaimread.test: New file.  Test script for the
      never claim parser.
      * src/tgbatest/Makefile.am: Adjust.
      * configure.ac : Adjust.
      * README: Adjust.
      ab6ec5cb
    • Alexandre Duret-Lutz's avatar
      Remove `readsave' and fix line numbers in tgbaparse error messages. · 7da11234
      Alexandre Duret-Lutz authored
      * src/tgbaparse/tgbaparse.yy (line): Fix computation of line number
      for error messages when parsing conditions.
      * src/tgbatest/readsave.test: Check the syntax position of syntax errors
      in the diagnostics.  Use ltl2tgba instead of readsave.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Remove readsave.
      7da11234
    • Alexandre Duret-Lutz's avatar
  3. 07 Oct, 2010 2 commits
  4. 21 Jun, 2010 1 commit
  5. 25 May, 2010 1 commit
    • Felix Abecassis's avatar
      Add never claim parser. · 9aaa638b
      Felix Abecassis authored
      * src/neverclaimparse/: New directory.
      * src/neverclaimparse/fmterror.cc: New file.  Print a formatted parse
      error on a output stream.
      * src/neverclaimparse/neverclaimparse.yy: New file.  Parser declaration
      for Bison.
      * src/neverclaimparse/neverclaimscan.ll: New file.  Scanner declaration
      for Flex.
      * src/neverclaimparse/public.hh: New file.  Public header for external
      use.
      * src/neverclaimparse/parsedecl.hh: New file.  Header file for
      Flex-Bison interaction.
      * src/neverclaimparse/Makefile.am: New Makefile.
      * src/tgbatest/neverclaimread.cc: New file.  Test program for the
      never claim parser.
      * src/tgbatest/neverclaimread.test: New file.  Test script for the
      never claim parser.
      * src/tgbatest/Makefile.am: Adjust.
      * configure.ac : Adjust.
      * README: Adjust.
      9aaa638b
  6. 20 May, 2010 1 commit
  7. 16 Apr, 2010 3 commits
  8. 15 Apr, 2010 7 commits
  9. 14 Apr, 2010 2 commits
  10. 12 Apr, 2010 7 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      More LTL reductions for W and M. · e6809b8c
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Perform the following reductions:
      (a U b) & (c W b) = (a & c) U b
      (a W b) & (c W b) = (a & c) W b
      (a R b) | (c M b) = (a | c) R b
      (a M b) | (c M b) = (a | c) M b
      * src/ltltest/reduccmp.test: Test them.
      e6809b8c
    • Alexandre Duret-Lutz's avatar
      Add LTL reductions for strong release. · f003c3d1
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Perform the following reductions.
      a R (b & F(a)) = a M b
      a M (b & F(a)) = a M b
      a R Fa = Fa
      a M Fa = Fa
      a R b & Fa = a M b
      a R b & a M c = a M (b & c)
      a M b & a M c = a M (b & c)
      * src/ltltest/reduccmp.test: More tests.
      f003c3d1
    • Alexandre Duret-Lutz's avatar
      Add LTL reductions for weak until. · 80ceca59
      Alexandre Duret-Lutz authored
      * src/ltlvisit/basicreduce.cc: Perform the following reductions.
      a U (b | Ga) = a W b
      a W (b | Ga) = a W b
      a U b | Ga = a W b
      a U b | a W c = a W (b | c)
      a W b | a W c = a W (b | c)
      a U Ga = Ga
      a W Ga = Ga
      * src/ltltest/reduccmp.test: More tests.
      80ceca59
    • 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
    • Alexandre Duret-Lutz's avatar
      [lbtt] Accept W and M in lbtt-translate --spot. · 35a57c6d
      Alexandre Duret-Lutz authored
      * src/SpotWrapper.cc: Translate W and M operators.
      35a57c6d
    • Alexandre Duret-Lutz's avatar
      Adjust ltl2tgba.py to call scc_filter() with the "full" option as · 60dbeb11
      Alexandre Duret-Lutz authored
      appropriate.
      
      * wrap/python/spot.i (spot::scc_filter): Make it available.
      * wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
      Use the "full" option unless the show_degen_png or
      show_never_claim are set.  Also reduce_scc the default.
      60dbeb11
  11. 08 Apr, 2010 3 commits
  12. 10 Mar, 2010 1 commit
  13. 07 Mar, 2010 1 commit