1. 15 Jun, 2015 2 commits
  2. 14 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      org: add utf-8 markers · 3e853eed
      Alexandre Duret-Lutz authored
      * doc/org/index.org, doc/org/ltl2tgta.org, doc/org/randltl.org,
      doc/org/satmin.org, doc/org/tut.org, doc/org/tut01.org,
      doc/org/tut02.org, doc/org/tut10.org, doc/org/tut20.org,
      doc/org/tut21.org, doc/org/tut22.org: Here.
      3e853eed
  3. 13 Jun, 2015 1 commit
  4. 12 Jun, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      org: new example · 89592881
      Alexandre Duret-Lutz authored
      Fixes #14.
      
      * doc/org/tut22.org: New file.
      * doc/Makefile.am, doc/org/tut.org: Add it.
      89592881
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Rename src/tests/ltl2tgba as src/tests/ikwiad. · 17dc2f86
      Alexandre Duret-Lutz authored
      Fixes #23.
      
      * src/tests/ltl2tgba.cc: Rename as ...
      * src/tests/ikwiad.cc: ... this.
      * src/tests/Makefile.am, src/tests/babiak.test, src/tests/checkta.cc,
      src/tests/complementation.test, src/tests/cycles.test,
      src/tests/dbacomp.test, src/tests/degendet.test,
      src/tests/degenid.test, src/tests/det.test, src/tests/dfs.test,
      src/tests/dstar.test, src/tests/dupexp.test, src/tests/emptchke.test,
      src/tests/kv.test, src/tests/ltl2neverclaim-lbtt.test,
      src/tests/ltl2neverclaim.test, src/tests/ltl2tgba.test,
      src/tests/ltlcounter.test, src/tests/ltlcross.test,
      src/tests/neverclaimread.test, src/tests/obligation.test,
      src/tests/parseaut.test, src/tests/randaut.test,
      src/tests/randpsl.test, src/tests/renault.test,
      src/tests/satmin2.test, src/tests/sccsimpl.test, src/tests/sim2.test,
      src/tests/simdet.test, src/tests/spotlbtt.test, src/tests/wdba.test,
      src/tests/wdba2.test, bench/emptchk/README, bench/emptchk/defs.in,
      bench/ltlclasses/run, bench/ltlcounter/run, bench/wdba/run: Adjust.
      17dc2f86
    • Alexandre Duret-Lutz's avatar
      org: new example · 4d848e98
      Alexandre Duret-Lutz authored
      * doc/org/tut21.org: New file.
      * doc/Makefile.am, doc/org/tut.org: Add it.
      4d848e98
  5. 11 Jun, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      graph: rename num_transitions() as num_edges() · af8634d8
      Alexandre Duret-Lutz authored
      And in fact, rename most "trans*" as "edges*", because that what they
      really are.
      
      * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/bin/randaut.cc,
      src/dstarparse/dra2ba.cc, src/dstarparse/dstarparse.yy,
      src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
      src/graph/graph.hh, src/graph/ngraph.hh, src/ltlvisit/exclusive.cc,
      src/parseaut/parseaut.yy, src/tests/complementation.cc,
      src/tests/graph.cc, src/tests/ltl2tgba.cc, src/tests/ngraph.cc,
      src/tests/twagraph.cc, src/twa/twagraph.cc, src/twa/twagraph.hh,
      src/twa/twamask.hh, src/twaalgos/are_isomorphic.cc,
      src/twaalgos/are_isomorphic.hh, src/twaalgos/canonicalize.cc,
      src/twaalgos/cleanacc.cc, src/twaalgos/complete.cc,
      src/twaalgos/compsusp.cc, src/twaalgos/cycles.cc,
      src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
      src/twaalgos/dtgbacomp.cc, src/twaalgos/dtgbasat.cc,
      src/twaalgos/dupexp.cc, src/twaalgos/emptiness.cc,
      src/twaalgos/isunamb.cc, src/twaalgos/isweakscc.cc,
      src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/mask.hh,
      src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
      src/twaalgos/powerset.cc, src/twaalgos/product.cc,
      src/twaalgos/randomgraph.cc, src/twaalgos/randomize.cc,
      src/twaalgos/randomize.hh, src/twaalgos/relabel.cc,
      src/twaalgos/remfin.cc, src/twaalgos/safety.cc, src/twaalgos/sbacc.cc,
      src/twaalgos/sccfilter.cc, src/twaalgos/sepsets.cc,
      src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
      src/twaalgos/totgba.cc: Rename these.
      af8634d8
    • Alexandre Duret-Lutz's avatar
      * doc/org/tut20.org: Cleanup. · a1ba0a89
      Alexandre Duret-Lutz authored
      a1ba0a89
    • Alexandre Duret-Lutz's avatar
      twa: forward num_sets() to acc_. · 6f500f3f
      Alexandre Duret-Lutz authored
      * src/twa/twa.hh (num_sets): New method.  Delegating to acc_.
      * src/twa/twagraph.hh, src/twa/twaproduct.cc, src/twa/twaproxy.cc,
      src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtgbacomp.cc,
      src/twaalgos/dtgbasat.cc, src/twaalgos/gv04.cc, src/twaalgos/hoa.cc,
      src/twaalgos/lbtt.cc, src/twaalgos/magic.cc, src/twaalgos/mask.cc,
      src/twaalgos/ndfs_result.hxx, src/twaalgos/postproc.cc,
      src/twaalgos/powerset.cc, src/twaalgos/product.cc,
      src/twaalgos/remfin.cc, src/twaalgos/se05.cc,
      src/twaalgos/simulation.cc, src/twaalgos/stats.cc,
      src/twaalgos/stutter.cc, src/twaalgos/tau03.cc,
      src/twaalgos/tau03opt.cc, src/twaalgos/totgba.cc: Simplify
      acc().num_sets() into num_sets().
      6f500f3f
    • Alexandre Duret-Lutz's avatar
      hoaparse: rename to parseaut · a86391ab
      Alexandre Duret-Lutz authored
      Because this parser is not specific to HOA anymore.
      
      * src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
      src/hoaparse/hoaparse.yy, src/hoaparse/parsedecl.hh,
      src/parseaut/public.hh, src/hoaparse/hoascan.ll,
      src/tests/hoaparse.test: Rename to...
      * src/parseaut/Makefile.am, src/parseaut/fmterror.cc,
      src/parseaut/parseaut.yy, src/parseaut/parsedecl.hh,
      src/hoaparse/public.hh, src/parseaut/scanaut.ll,
      src/tests/parseaut.test: ... these, and also adjust the name internally.
      For instance hoa_aut_ptr is now parsed_aut_ptr; hoa_stream_parser is now
      automaton_stream_parser, and hoa_parse() has become parse_aut().
      * NEWS, README, configure.ac, doc/org/tut20.org, src/Makefile.am,
      src/bin/autfilt.cc, src/bin/common_aoutput.cc,
      src/bin/common_aoutput.hh, src/bin/common_conv.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/Makefile.am,
      src/tests/complementation.cc, src/tests/ltl2tgba.cc,
      src/tests/readsave.test, wrap/python/ajax/spot.in,
      wrap/python/spot.py, wrap/python/spot_impl.i,
      wrap/python/tests/automata-io.ipynb, wrap/python/tests/parsetgba.py:
      Adjust.
      a86391ab
  6. 10 Jun, 2015 5 commits
  7. 09 Jun, 2015 1 commit
  8. 08 Jun, 2015 1 commit
  9. 07 Jun, 2015 6 commits
  10. 05 Jun, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      org: Update tut01 · a8f5e7fd
      Alexandre Duret-Lutz authored
      * doc/org/tut01.org: Update.
      * doc/org/g++wrap.in: Include BuDDy's header.
      a8f5e7fd
    • Alexandre Duret-Lutz's avatar
      adjust names for automata printers · 738f939f
      Alexandre Duret-Lutz authored
      The following renamings are made:
      
        never_claim_reachable -> print_never_claim
        hoa_reachable   -> print_hoa
        lbtt_reachable  -> print_lbtt
        dotty_reachable -> print_dot
        ltl::dotty      -> print_dot_psl
      
      Fixes #89.
      
      * src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh, src/taalgos/dotty.cc,
      src/taalgos/dotty.hh src/twaalgos/dotty.cc, src/twaalgos/dotty.hh:
      Rename...
      * src/ltlvisit/dot.cc, src/ltlvisit/dot.hh src/taalgos/dot.cc,
      src/taalgos/dot.hh src/twaalgos/dot.cc, src/twaalgos/dot.hh:
      ... those.
      * bench/stutter/stutter_invariance_randomgraph.cc,
      iface/ltsmin/modelcheck.cc, src/bin/common_aoutput.cc,
      src/bin/dstar2tgba.cc, src/bin/ltl2tgta.cc, src/dstarparse/dra2ba.cc,
      src/ltlvisit/Makefile.am, src/taalgos/Makefile.am,
      src/tests/checkpsl.cc, src/tests/checkta.cc,
      src/tests/complementation.cc, src/tests/emptchk.cc,
      src/tests/ltl2tgba.cc, src/tests/ltlprod.cc, src/tests/randtgba.cc,
      src/tests/readltl.cc, src/tests/taatgba.cc, src/tests/twagraph.cc,
      src/twa/twa.hh, src/twa/twasafracomplement.cc,
      src/twaalgos/Makefile.am, src/twaalgos/dtbasat.cc,
      src/twaalgos/dtgbasat.cc, src/twaalgos/dupexp.cc,
      src/twaalgos/lbtt.cc, src/twaalgos/lbtt.hh,
      src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/neverclaim.cc,
      src/twaalgos/neverclaim.hh, wrap/python/ajax/spot.in,
      wrap/python/spot.py, wrap/python/spot_impl.i,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/parsetgba.py: Adjust.
      738f939f
  11. 04 Jun, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlvisit: rename tostring.hh as print.hh and rename printer functions · 8fb7b279
      Alexandre Duret-Lutz authored
      This actually performs three related changes, but separating them
      would be quite inconvenient.
      
      1) rename tostring.hh to print.hh a welcome side-effect is that
      I could fix several files that included this file for not reason.
      
      2) de-overload some of the to_string functions, and rename them
      as follow:
      
        to_string -> print_psl, print_sere, str_psl, str_sere
        to_utf8_string -> print_utf8_psl, print_utf8_sere,
                          str_utf8_psl, str_utf8_sere
        to_spin_string -> print_spin_ltl, str_spin_ltl
        to_wring_string -> print_wring_ltl, str_wing_ltl
        to_lbt_string -> print_lbt_ltl, str_lbt_ltl
        to_latex_string -> print_latex_psl, str_latex_psl
        to_sclatex_string -> print_sclatex_psl, str_sclatex_psl
      
      Now it is clearer what these functions do, and their restrictions.
      
      3) all those print_* functions now take the stream to write onto
      as their first argument.  This fixes #88.
      
      * src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Rename into...
      * src/ltlvisit/print.cc, src/ltlvisit/print.hh: ... those, and make
      the changes listed above.
      * doc/org/tut01.org, src/bin/common_output.cc,
      src/bin/common_trans.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
      src/bin/randltl.cc, src/ltlparse/ltlparse.yy,
      src/ltlvisit/Makefile.am, src/ltlvisit/mark.cc,
      src/ltlvisit/relabel.cc, src/ltlvisit/simplify.cc,
      src/ltlvisit/snf.cc, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
      src/taalgos/tgba2ta.cc, src/tests/equalsf.cc, src/tests/ltl2tgba.cc,
      src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/reduc.cc,
      src/tests/syntimpl.cc, src/tests/tostring.cc, src/twa/bdddict.cc,
      src/twa/bddprint.cc, src/twa/taatgba.cc, src/twa/taatgba.hh,
      src/twa/twagraph.cc, src/twaalgos/compsusp.cc, src/twaalgos/lbtt.cc,
      src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/neverclaim.cc, src/twaalgos/remprop.cc,
      src/twaalgos/stats.cc, wrap/python/ajax/spot.in, wrap/python/spot.py,
      wrap/python/spot_impl.i: Adjust.
      8fb7b279
    • Alexandre Duret-Lutz's avatar
      stutter bench: fix so that is compile again · 0cf952e7
      Alexandre Duret-Lutz authored
      * bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc: Adjust after the
      tgba->twa changes.
      0cf952e7
    • Alexandre Duret-Lutz's avatar
      ltlparse: rename the main functions · 98790f53
      Alexandre Duret-Lutz authored
      parse         -> parse_infix_psl
      parse_lbt     -> parse_prefix_ltl
      parse_sere    -> parse_infix_sere
      parse_boolean -> parse_infix_boolean
      
      Fixes #87.
      
      * src/ltlparse/ltlparse.yy, src/ltlparse/public.hh:
      Do the above changes.
      * doc/mainpage.dox, doc/org/tut01.org, iface/ltsmin/modelcheck.cc,
      src/bin/common_finput.cc, src/hoaparse/hoaparse.yy,
      src/kripkeparse/kripkeparse.yy, src/tests/checkpsl.cc,
      src/tests/checkta.cc, src/tests/complementation.cc,
      src/tests/consterm.cc, src/tests/emptchk.cc, src/tests/equalsf.cc,
      src/tests/kind.cc, src/tests/length.cc, src/tests/ltl2tgba.cc,
      src/tests/ltlprod.cc, src/tests/ltlrel.cc, src/tests/randtgba.cc,
      src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
      src/tests/tostring.cc, wrap/python/ajax/spot.in,
      wrap/python/tests/alarm.py, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py: Adjust.
      98790f53
  12. 03 Jun, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlvisit: merge lbt.hh into tostring.hh · aedce810
      Alexandre Duret-Lutz authored
      Fixes #86.
      
      * src/ltlvisit/lbt.hh, src/ltlvisit/lbt.cc: Delete and move contents
      into...
      * src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc: ... these.
      * doc/org/tut01.org, src/bin/common_output.cc,
      src/bin/common_trans.cc, src/bin/ltlcross.cc,
      src/ltlvisit/Makefile.am, src/twaalgos/lbtt.cc,
      wrap/python/spot_impl.i: Adjust.
      aedce810
    • Alexandre Duret-Lutz's avatar
      org: add a first code example · 8de524ad
      Alexandre Duret-Lutz authored
      The difficulty is not the example, but setting up org-mode to allow
      Python and C++ example that use the local libraries, not those
      installed system-wide.
      
      * doc/org/.dir-locals.el: Rename as...
      * doc/org/.dir-locals.el.in: ... this, so we can easily define
      PYTHONPATH and other environment variables.
      * doc/org/init.el.in: Enable C++, and make sure but Python
      and C++ use the local libraries.
      * doc/org/g++wrap.in, doc/org/tut01.org: New files.
      * doc/Makefile.am, configure.ac: Adjust.
      * wrap/python/spot.py (to_str): Take a parenth argument.
      8de524ad
    • Alexandre Duret-Lutz's avatar
      acc: Do not restrict acceptance codes to small vectors. · 16336be3
      Alexandre Duret-Lutz authored
      * src/twa/acc.hh (acc_word): This is a 32-bit structure, so
      we can use short for both size and op.
      16336be3
  13. 02 Jun, 2015 3 commits
  14. 01 Jun, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      randaut: add a --colored option · 715805fa
      Alexandre Duret-Lutz authored
      Fixes #83.
      
      * src/bin/randaut.cc: Add option.
      * src/twaalgos/randomgraph.cc, src/twaalgos/randomgraph.hh: Honor it.
      * src/tests/randaut.test: Add tests.
      * doc/org/randaut.org: Document it.
      715805fa
    • Alexandre Duret-Lutz's avatar
      hoa: detect colored automata · 97665a58
      Alexandre Duret-Lutz authored
      Fixes #84.
      
      * src/twaalgos/hoa.cc: Detect and output the colored property.
      * src/tests/hoaparse.test, src/tests/satmin2.test: Update.
      97665a58
    • Alexandre Duret-Lutz's avatar
      random: fix rounding in barand() · a75a9c09
      Alexandre Duret-Lutz authored
      This fixes #85.
      
      * src/misc/random.hh (barand): Use round() before casting.
      * doc/org/oaut.org: Recompute example.
      * src/tests/randaut.test, wrap/python/tests/randaut.ipynb: Adjust.
      a75a9c09
    • Alexandre Duret-Lutz's avatar
      bin: clear temporary files on termination signals · eabed370
      Alexandre Duret-Lutz authored
      This is particularly important for src/tests/satmin.test, where ltl2tgba
      might be killed while writing a huge temporary file used for SAT-based
      minimization.  Before this patch, the temporary files would remain in
      src/tests/satmin.dir/, easily overflowing the 100GB limit of the docker
      containers we use on the build farm.
      
      * src/bin/common_setup.cc: Catch termination signals for all tools,
      even those that do not yet clear temporary files.
      * configure.ac: Check for sigaction.
      eabed370