1. 19 Jan, 2015 7 commits
    • Alexandre Duret-Lutz's avatar
      dupexp: remove the version that fills a vector · 8c83c8a8
      Alexandre Duret-Lutz authored
      Fixes #45.
      * src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Remove unused code.
    • Alexandre Duret-Lutz's avatar
      simulation: take a tgba_digraph as input · 64469f3d
      Alexandre Duret-Lutz authored
      Issue #45.
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Take
      a tgba_digraph is input.
      * src/tgbatest/ltl2tgba.cc: Adjust.
    • Alexandre Duret-Lutz's avatar
      simulation: get rid of the "don't care" simulation reductions · 01590273
      Alexandre Duret-Lutz authored
      Those where never really publicized because they were slow and we failed
      to fix what we hopped to fix with them.  They where never used by
      default.  Getting rid of them will make it easier to cleanup the
      simulation code.
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Remove
      the simulation code.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
      src/tgbatest/ltl2tgba.cc: Do not call it.
      * src/bin/spot-x.cc: Update doc.
      * src/tgbatest/sim.test: Delete this file.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/spotlbtt.test, bench/ltl2tgba/tools.sim:
      Remove uses to don't care simulation.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba.html: document [:*i..j] · 1d724bea
      Alexandre Duret-Lutz authored
      For issue #51.
      * wrap/python/ajax/ltl2tgba.html: Here.
    • Alexandre Duret-Lutz's avatar
      ltl: rename is_X_free() into is_syntactic_stutter_invariant() · 34f1601b
      Alexandre Duret-Lutz authored
      and adjust it to detect siPSL formulas, as in the paper of Dax et
      al. (ATVA'09).  For issue #51.
      * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
      src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Rename
      the property, and adjust its computation on siSERE.
      * src/ltlvisit/remove_x.cc, src/ltlvisit/simplify.cc,
      src/tgbaalgos/stutter.cc: Adjust to new names.
      * src/bin/ltlfilt.cc: Add option --syntactic-sutter-invariant.
      * src/ltltest/kind.test: Update tests and add some new.
    • Alexandre Duret-Lutz's avatar
      psl: add support for the [:*i..j] operator · a79db4ee
      Alexandre Duret-Lutz authored
      This operator is to ':' what [*i..j] is to ';'.
      Part of issue #51.
      * doc/tl/tl.tex: Document syntax, semantic, and trivial
      * doc/tl/spotltl.sty: Add macros for new operators.
      * src/ltlast/bunop.cc, src/ltlast/bunop.hh: Implement it.
      * src/ltlast/multop.cc: Add some trivial simplifications.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse it.
      * src/ltltest/equals.test, src/ltltest/latex.test,
      src/tgbatest/ltl2tgba.test: Add more tests.
      * src/ltlvisit/randomltl.cc: Output this operator in
      random PSL formulas.
      * src/ltltest/rand.test: Adjust.
      * src/tgbaalgos/ltl2tgba_fm.cc: Add translation rules.
      * src/ltlvisit/tostring.cc: Add pretty printing code.
      * src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc: Adjust
      * NEWS: Mention the new operator.
    • Alexandre Duret-Lutz's avatar
      tl: formul\ae -> formulas · eebbcac2
      Alexandre Duret-Lutz authored
      * doc/tl/tl.tex: Use "formulas" everywhere in this file.
  2. 18 Jan, 2015 3 commits
  3. 14 Jan, 2015 2 commits
  4. 13 Jan, 2015 4 commits
  5. 12 Jan, 2015 1 commit
  6. 11 Jan, 2015 2 commits
  7. 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
  8. 08 Jan, 2015 5 commits