1. 04 Jun, 2015 2 commits
    • 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
  2. 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
  3. 02 Jun, 2015 3 commits
  4. 01 Jun, 2015 7 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
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      randaut: rename -S as -Q for consistency · 0ac35a15
      Alexandre Duret-Lutz authored
      This way -S means --state-based-acc like with other tools
      producing automata.   This fixes #82.
      
      * src/bin/randaut.cc: Rename -S as -Q, rename --state-acc as
      --state-based-acc (with --sbacc as a synonym), and declare -S as the
      short version of --state-based-acc.
      * doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org,
      src/tests/isomorph.test, src/tests/randaut.test,
      src/tests/randtgba.test, src/tests/readsave.test, src/tests/uniq.test,
      wrap/python/tests/randaut.ipynb: Adjust all calls to randaut.
      0ac35a15
  5. 30 May, 2015 2 commits
  6. 27 May, 2015 1 commit
  7. 26 May, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      b87f24d7
    • Alexandre Duret-Lutz's avatar
      randaut: better generation of acceptance conditions · 88141b27
      Alexandre Duret-Lutz authored
      * src/bin/randaut.cc: Replace the --acc-type and --acc-sets
      options by a more general --acceptance option, that take either
      an acceptance formula, or an acceptance name parametred by ranges.
      Also accept a range for the number of atomic propositions.
      * src/twaalgos/randomgraph.cc (random_acceptance): Move...
      * src/twa/acc.cc, src/twa/acc.hh (random): ... here.
      (parse_acc_code): Generalize to accept ranges instead of
      numbers whenever sensible, and accept a 'random' acceptance.
      * src/tests/randaut.test: Adjust tests and add more.
      * wrap/python/tests/randaut.ipynb: Adjust call to randaut.
      88141b27
  8. 25 May, 2015 3 commits
  9. 24 May, 2015 1 commit
  10. 22 May, 2015 5 commits
  11. 21 May, 2015 2 commits
  12. 20 May, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      acc: recognize parity acceptance · 04171207
      Alexandre Duret-Lutz authored
      It has two modes: strict or not.  In strict mode (tested in
      hoaparse.test), the acceptance formula has to match exactly the one
      given in the HOA spec.  In non-strict mode (tested in accparse2.py)
      any equivalent formula is accepted.
      
      * src/twa/acc.cc, src/twa/acc.hh (acc_cond::is_parity): New method.
      * src/twaalgos/hoa.cc: Use it.
      * src/tests/hoaparse.test: Test it.
      * wrap/python/spot_impl.i: Bind it.
      * wrap/python/tests/accparse2.py: New file.
      * wrap/python/tests/Makefile.am: Add it.
      04171207
    • Alexandre Duret-Lutz's avatar
      acc: add support for generating parity conditions · 704eaf26
      Alexandre Duret-Lutz authored
      * src/twa/acc.cc, src/twa/acc.hh: Here.
      * wrap/python/tests/accparse.ipynb: Test it.
      704eaf26
    • Alexandre Duret-Lutz's avatar
      hoa: output acc-name for several acceptance types · d276f73e
      Alexandre Duret-Lutz authored
      So far the HOA output would emit an acc-name only
      for generalized-Buchi or inferior types (Buchi, all).
      It now knows about none, co-Buchi, generalized-co-Buchi,
      Rabin, Streett, and generalized-Rabin as well.
      
      * src/twa/acc.cc, src/twa/acc.hh: Add detection code.
      * src/twaalgos/hoa.cc: Use it.
      * src/tests/remfin.test, src/tests/maskacc.test,
      src/tests/complete.test, src/tests/sim3.test,
      src/tests/ltl2dstar.test: Adjust tests.
      * src/tests/hoaparse.test: Adjust and add more tests.
      d276f73e
  13. 18 May, 2015 6 commits