1. 30 Nov, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix a GCC 4.6 warning. · ae03bc67
      Alexandre Duret-Lutz authored
      * src/tgbatest/randtgba.cc (main): Remove the set but unused opt_A
      variable (the upcoming GCC 4.6 would warn about it) and set opt_ec
      to 1 if -A is used without -e.
      ae03bc67
  2. 27 Nov, 2010 4 commits
    • Alexandre Duret-Lutz's avatar
      3b371128
    • Alexandre Duret-Lutz's avatar
      [iface/nips/nips_vm] · 0785d729
      Alexandre Duret-Lutz authored
      Fix compilation with Clang.
      
      * state.c: Do not include state_inline.h twice with different
      value of STATE_INLINE.  It was included once via state.h with
      STATE_INLINE = "extern inline", and another time directly with
      STATE_INLINE = "extern". Now...
      * state.h: ... only include it once here with STATE_INLINE =
      "static inline".
      0785d729
    • Alexandre Duret-Lutz's avatar
      Another Clang report. · 8156766f
      Alexandre Duret-Lutz authored
      * iface/nips/nips.cc (format_state): Do not use a variable-sized
      array, this is not allowed in C++.
      8156766f
    • Alexandre Duret-Lutz's avatar
      Fix more errors reported by Clang. · 019c85df
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/reducerun.hh (tgba_run): Predeclare as a struct
      since this is what it is.
      * src/tgbatest/randtgba.cc (main): Avoid using "i" with two
      different type in the same loop.
      019c85df
  3. 26 Nov, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Finalize Kripke interface. · 0d9d0b08
      Alexandre Duret-Lutz authored
      * src/kripke/fairkripke.hh, src/kripke/fairkripke.cc,
      * src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and
      document the Kripke interface.  I have tested it by updating
      checkpn to use it.
      0d9d0b08
  4. 25 Nov, 2010 3 commits
  5. 24 Nov, 2010 2 commits
  6. 20 Nov, 2010 1 commit
  7. 07 Nov, 2010 2 commits
  8. 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
  9. 07 Oct, 2010 2 commits
  10. 21 Jun, 2010 1 commit
  11. 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
  12. 20 May, 2010 1 commit
  13. 16 Apr, 2010 3 commits
  14. 15 Apr, 2010 7 commits
  15. 14 Apr, 2010 1 commit