1. 18 Jan, 2015 2 commits
  2. 14 Jan, 2015 2 commits
  3. 13 Jan, 2015 4 commits
  4. 12 Jan, 2015 1 commit
  5. 11 Jan, 2015 2 commits
  6. 09 Jan, 2015 16 commits
    • Alexandre Duret-Lutz's avatar
      ltltest: get rid of equals.cc · c85ba787
      Alexandre Duret-Lutz authored
      * src/ltltest/equals.cc: Delete.
      * src/ltltest/Makefile.am: Adjust.
      * src/ltltest/unabbrevwm.test: Rewrite using ltlfilt.
    • Alexandre Duret-Lutz's avatar
      never: add an option to output in Spin's 6.2.4 style · 6a2aad62
      Alexandre Duret-Lutz authored
      Fixes #46.
      * src/tgbaalgos/neverclaim.cc: Add option '6'.
      * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Make it
      possible to use the option.
      * NEWS, doc/org/oaut.org: Document it.
      * src/tgbatest/ltlcross2.test: Test it.
    • Alexandre Duret-Lutz's avatar
      postproc: use scc_filter_states on SBA · 604971d6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc: Here.  Otherwise, reading
      a neverclaim with autfilt would loose the SBA property
      and degeneralize again.
    • Alexandre Duret-Lutz's avatar
      degen: remove two useless casts · b2c2411b
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/degen.cc: Here.
    • Alexandre Duret-Lutz's avatar
      neverclaim: rewrite the output using the tgba_digraph interface · 4f6f71fe
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh: Here.
      Also take a string to supply options.
      * src/tgbatest/ltl2tgba.cc: Adjust call.
    • Alexandre Duret-Lutz's avatar
      powerset: rewrite using the tgba_digraph interface · eadcf953
      Alexandre Duret-Lutz authored
      Fixes #48.
      * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh: Here.
      * src/tgbaalgos/minimize.cc: Adjust usage.
    • Alexandre Duret-Lutz's avatar
      org: add another example · d6ba00ff
      Alexandre Duret-Lutz authored
      * doc/org/oaut.org: Show another way to perform the last computation.
    • Alexandre Duret-Lutz's avatar
      style: make sure we do not have SPOT_API in *.cc files · a539dc90
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Check for it.
      * src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
      src/tgbaalgos/randomize.cc, src/tgbaalgos/stutter.cc: Fix all those.
    • Alexandre Duret-Lutz's avatar
      dstarparse, hoaparse: rename inline namespace to please clang · 5536bac4
      Alexandre Duret-Lutz authored
      The namespace dstaryy was declared inline and then reopened as
      non-inline.  Likewise for hoayy.  Let's use different names.
      * src/dstarparse/dstarparse.yy, src/hoaparse/hoaparse.yy: Here.
    • Alexandre Duret-Lutz's avatar
      randltl: fix determinism · 2460f5d0
      Alexandre Duret-Lutz authored
      * src/ltlvisit/randomltl.cc: Make sure generation of binary operator is
      done in a deterministic order.
    • Alexandre Duret-Lutz's avatar
      more files to ignore · 838a2836
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      ltlgrind: fix indeterminism · ec408c36
      Alexandre Duret-Lutz authored
      * src/ltlvisit/mutation.cc: Force order of evaluation of arguments of
    • Alexandre Duret-Lutz's avatar
      sccinfo: make it easier to iterate over all SCCs · e01ab2b2
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: add
      scc_info::begin() and scc_info::end() methods to iterate over the
      node_ vector.   Tidy the scc_node structure that that its member
      are accessed via methods.
      * src/tgbaalgos/safety.cc, src/bin/ltlcross.cc: Simplify using
      this interface.
    • Alexandre Duret-Lutz's avatar
      add missing utf-8 header to many source files · 579e8fc0
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Test for the missing header.
      * iface/ltsmin/check.test, src/kripketest/kripke.test,
      src/kripketest/parse_print_test.cc, src/ltlparse/fmterror.cc,
      src/ltltest/consterm.test, src/ltltest/kind.test,
      src/ltltest/length.test, src/ltltest/ltlfilt.test,
      src/ltltest/reduc.cc, src/ltltest/reduc.test,
      src/ltltest/reduc0.test, src/ltltest/reducpsl.test,
      src/ltltest/remove_x.test, src/ltltest/unabbrevwm.test,
      src/ltltest/utf8.test, src/ltltest/uwrm.test, src/ltlvisit/dump.cc,
      src/ltlvisit/remove_x.cc, src/misc/casts.hh, src/misc/fixpool.hh,
      src/misc/hashfunc.hh, src/misc/ltstr.hh, src/sanity/readme.test,
      src/taalgos/tgba2ta.cc, src/tgbaalgos/bfssteps.cc,
      src/tgbaalgos/stats.cc, src/tgbatest/acc.test,
      src/tgbatest/bitvect.test, src/tgbatest/complementation.test,
      src/tgbatest/cycles.test, src/tgbatest/degendet.test,
      src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
      src/tgbatest/emptchkr.test, src/tgbatest/intvcomp.test,
      src/tgbatest/ltl2ta.test, src/tgbatest/ltl2ta2.test,
      src/tgbatest/ltlprod.test, src/tgbatest/maskacc.test,
      src/tgbatest/obligation.test, src/tgbatest/randpsl.test,
      src/tgbatest/readsat.cc, src/tgbatest/readsat.test,
      src/tgbatest/scc.test, src/tgbatest/sccsimpl.test,
      src/tgbatest/taatgba.test, src/tgbatest/tgbaread.test,
      src/tgbatest/tripprod.test, src/tgbatest/uniq.test,
      src/tgbatest/wdba.test: Add it.
    • Alexandre Duret-Lutz's avatar
      projrun: modernize · 3a70b570
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/emptiness.hh (step): Add constructors...
      * src/tgbaalgos/projrun.cc: ... to simplify this.
    • Alexandre Duret-Lutz's avatar
      product: rename the one-the-fly version as otf_product · 94577d65
      Alexandre Duret-Lutz authored
      This avoid compiler errors about ambiguous calls and make sure we are
      calling the intended algorithms everywhere (this wasn't the case).
      * src/tgba/tgbaproduct.hh (product, product_at): Rename as...
      (otf_product, otf_product_at): ... this.
      * iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc, src/bin/ltlfilt.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/checkpsl.cc,
      src/tgbatest/complementation.cc, src/tgbatest/ltlprod.cc: Adjust
  7. 08 Jan, 2015 9 commits
  8. 07 Jan, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      org: factor headers into setup.org · 56ed13a9
      Alexandre Duret-Lutz authored
      * doc/org/setup.org: New file.
      * doc/Makefile.am: Distribute it.
      * doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
      doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
      doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
      doc/org/ltlgrind.org, doc/org/oaut.org, doc/org/randaut.org,
      doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org: Use
    • Alexandre Duret-Lutz's avatar
      org: update randltl.org · 15852b4e
      Alexandre Duret-Lutz authored
      * doc/org/randltl.org: The first example used to output '1' as
      only random formula.  This is not very sexy.
    • Alexandre Duret-Lutz's avatar
      org: use a white background and ship the CSS · fbcc9fb8
      Alexandre Duret-Lutz authored
      * doc/org/spot.css: New file.
      * doc/Makefile.am: Distribute it.
      * doc/org/init.el.in, doc/org/.dir-locals.el: Adjust links.
  9. 06 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      org: Update results to new output · f9029858
      Alexandre Duret-Lutz authored
      The dotty output changed to be horizontal, and also
      the acceptance sets are now numbers.
      * doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org,
      doc/org/satmin.org: Adjust these four.