1. 20 May, 2015 2 commits
    • 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
  2. 18 May, 2015 10 commits
    • Alexandre Duret-Lutz's avatar
      acc: parse standard acceptance names · 8e1c8469
      Alexandre Duret-Lutz authored
      * src/twa/acc.cc, src/twa/acc.hh: Add method to create
      standard acceptance conditions, and adjust the parse_acc_code
      to recognize them
      * wrap/python/spot_impl.i (acc_cond::acc_code): Add a printer.
      * wrap/python/tests/accparse.ipynb: New test file.
      * wrap/python/tests/Makefile.am: Add it.
      * src/tests/satmin2.test: Use the new syntax.
      8e1c8469
    • Alexandre Duret-Lutz's avatar
      sat-minimize: add a max-states option · 7880b25a
      Alexandre Duret-Lutz authored
      * src/twaalgos/dtbasat.cc, src/twaalgos/dtbasat.hh,
      src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Add it.
      * src/tests/satmin2.test: Add couple of tests.
      7880b25a
    • Alexandre Duret-Lutz's avatar
      sat-minimize: ignore silly histories · 91f68ab1
      Alexandre Duret-Lutz authored
      If the target acceptance is Fin(0)&Inf(1), there is no need to
      distinguish between an history of {0,1} and an history of {0}, as a
      cycle with either history will be rejected.  This implements this
      simplification.  If both the canditate and reference automata
      are Rabin automata with n pairs, then we now use at most
        Q * Q' * Q * Q' * 3^n * 3^n
      variables to encode the partial cycles histories, versus
        Q * Q' * Q * Q' * 4^n * 4^n
      before.
      
      * src/twaalgos/dtgbasat.cc: Implement this.
      * src/tests/satmin2.test: More tests.
      91f68ab1
    • Alexandre Duret-Lutz's avatar
      python: export the sat-minimization routines · 9480669e
      Alexandre Duret-Lutz authored
      * wrap/python/spot_impl.i: Here.
      9480669e
    • Alexandre Duret-Lutz's avatar
      ec49398e
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      sat-minimize: allow different acceptances as input and output · 0ede9687
      Alexandre Duret-Lutz authored
      * src/twaalgos/dtgbasat.cc (sat_minimize): Use any arbitrary
      acceptance condition passed via the "acc" option.
      * src/twa/acc.hh (mark_t::max_set): New method.
      * src/tests/satmin2.test: Add two test cases with DRA as input
      and DSA as output.
      0ede9687
    • Alexandre Duret-Lutz's avatar
      acc: preserve input order in parse_acc_code() · 3efeacb6
      Alexandre Duret-Lutz authored
      * src/twa/acc.cc: Here.
      * src/tests/acc.test: Adjust.
      3efeacb6
    • Alexandre Duret-Lutz's avatar
      sat-minimize: omit impossible histories · b4881579
      Alexandre Duret-Lutz authored
      When the reference acceptance condition is complex enough, some
      accepting SCCs may not use all acceptance sets.  In that case
      we don't have to encode all possible histories for this SCC.
      
      * src/twaalgos/dtgbasat.cc: Improve the encoding by omitting
      histories involving sets that are not used in a reference SCC.
      b4881579
    • Alexandre Duret-Lutz's avatar
      sat-minimize: generalize to any acceptance · 08749805
      Alexandre Duret-Lutz authored
      This is still missing tests.
      
      * src/bin/autfilt.cc: Add a --sat-minimize option.
      * src/misc/optionmap.cc, src/misc/optionmap.hh: Allow passing strings.
      * src/twa/acc.cc, src/twa/acc.hh: Add helper functions needed
      by the SAT-encoder.
      * src/twaalgos/complete.hh: Typos.
      * src/twaalgos/dtbasat.hh: Adjust comment.
      * src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Generalize
      to take the target acceptance as input.
      * src/twaalgos/postproc.cc, src/tests/ltl2tgba.cc: Adjust calls.
      * src/twaalgos/sbacc.cc, src/twaalgos/sbacc.hh: Don't pass
      the pointer by reference.
      * src/tests/acc.cc, src/tests/acc.test: More tests
      for the acceptance helper function.
      08749805
  3. 15 May, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: rewrite translate() to deal with unambiguous and sbacc · 19a27392
      Alexandre Duret-Lutz authored
      and make it easier to extend and use.
      
      * src/twaalgos/postproc.hh, src/twaalgos/translate.cc,
      src/twaalgos/translate.hh: Incorporate the Unambiguous option
      with the other preferences.  It's cleaner this way, and the
      previous setup did not work well with Python.
      * src/bin/ltl2tgba.cc: Adjust to this change.
      * wrap/python/spot.py (translate): Rewrite.
      * wrap/python/tests/automata.ipynb: Adjust existing cases, and
      add more as well as some comments.
      19a27392
  4. 14 May, 2015 6 commits
    • Alexandre Duret-Lutz's avatar
      translate: remove arbitrary restriction on -U and -D · 1ef3e5f3
      Alexandre Duret-Lutz authored
      * src/twaalgos/translate.cc, src/bin/ltl2tgba.cc: Do not assume that
      unambiguous is incompatible with deterministic.
      1ef3e5f3
    • Alexandre Duret-Lutz's avatar
      postproc: add a SBAcc option · 0786e068
      Alexandre Duret-Lutz authored
      Producing state-based acceptance is now part of the postprocessing
      routines.  That means we can more easily simplify automata with
      state-based acceptance (using autfilt -S --small --high, for instance)
      and as as side-effect, ltl2tgba can produce GBA.  However the result of
      ltl2tgba -S is often larger than that of ltl2tgba -B.
      
      * src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Implement
      the SBAcc option.
      * src/bin/common_post.cc, src/bin/common_post.hh: Implement -S.
      * src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
      src/bin/ltl2tgta.cc, src/bin/ltldo.cc: Adjust.
      * src/tests/sim3.test: Augment test case.
      * NEWS, doc/org/ltl2tgba.org, doc/org/autfilt.org: Document it -S.
      0786e068
    • Alexandre Duret-Lutz's avatar
      wdba: adjust to work on any TωA · dd87bdf8
      Alexandre Duret-Lutz authored
      * src/twaalgos/minimize.cc, src/twaalgos/safety.cc,
      src/twaalgos/safety.hh: Adjust.
      * src/tests/wdba2.test: More tests.
      dd87bdf8
    • Alexandre Duret-Lutz's avatar
      simulation: work on TωA · 80808133
      Alexandre Duret-Lutz authored
      * src/twaalgos/simulation.cc, src/twaalgos/simulation.hh: Adjust
      to work on TωA.  This only require separate acceptance sets.
      * src/tests/sim3.test: New test.
      * src/tests/Makefile.am: Add it.
      80808133
    • Alexandre Duret-Lutz's avatar
      ltldo: preserve generic acceptance · 0e04b253
      Alexandre Duret-Lutz authored
      * src/bin/ltldo.cc: Default to generic acceptance.
      * src/tests/ltl2dstar.test: Add a test.
      0e04b253
    • Alexandre Duret-Lutz's avatar
      autfilt: new --separate-sets option · 3d1ccdc4
      Alexandre Duret-Lutz authored
      * src/twaalgos/sepsets.cc, src/twaalgos/sepsets.hh: New files.
      * src/twaalgos/Makefile.am: Add them.
      * src/twa/acc.hh (get_acceptance): Add a non-const version.
      * src/bin/autfilt.cc: Add the --separate-sets option.
      * src/tests/sepsets.test: New file.
      * src/tests/Makefile.am: Add it.
      3d1ccdc4
  5. 13 May, 2015 5 commits
  6. 12 May, 2015 5 commits
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: produce unambiguous automata for PSL as well · 5d76b912
      Alexandre Duret-Lutz authored
      * src/twaalgos/ltl2tgba_fm.cc: Fix the PSL operators.
      * src/tests/unambig.test: Add more tests.
      5d76b912
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: make it easier to preserve state names · 778d8fe9
      Alexandre Duret-Lutz authored
      * src/twa/twagraph.cc, src/twa/twagraph.hh (create_formula_namer,
      release_formula_namer): New functions.
      * src/twaalgos/ltl2tgba_fm.cc: Use it.
      778d8fe9
    • Alexandre Duret-Lutz's avatar
      bin: add --check=unambiguous · 487a86d0
      Alexandre Duret-Lutz authored
      * src/bin/common_aoutput.cc: Add --check=unambiguous.
      * src/twa/twa.hh: New unambiguous property.
      * src/twaalgos/hoa.cc: Print it.
      * src/twaalgos/ltl2tgba_fm.cc: Set it.
      * src/twaalgos/isunamb.cc, src/twaalgos/isunamb.hh
      (check_unambiguous): New function.
      * src/tests/unambig.test: More tests.
      487a86d0
    • Alexandre Duret-Lutz's avatar
      Add an is_unambiguous() function, use it in ltlcross and autfilt · 98de84f3
      Alexandre Duret-Lutz authored
      * src/twaalgos/isunamb.hh, src/twaalgos/isunamb.cc: New files.
      * src/twaalgos/Makefile.am: Add them.
      * src/tests/unambig.test: New file.
      * src/tests/Makefile.am: Add it.
      * src/bin/ltlcross.cc: Record whether each produced automaton is
      ambiguous.
      * src/bin/autfilt.cc: Add a --is-unambiguous option.
      * NEWS: Mention it.
      98de84f3
    • Alexandre Duret-Lutz's avatar
      Add support for unambiguous automata · 9f3a7a49
      Alexandre Duret-Lutz authored
      * src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/ltl2tgba_fm.cc: Implement
      generation of unambiguous automata.
      * src/tests/ltl2tgba.cc: Add option -fu to test it.
      * src/bin/common_post.cc: Adjust the group of options so we can easily
      add more from ltl2tgba.cc.
      * src/bin/ltl2tgba.cc: Add support for -U and --unambigous.
      * src/twaalgos/translate.cc, src/twaalgos/translate.hh: Add support
      for Unambiguous.
      * src/tests/ltlcross.test, src/tests/ltlcross2.test: Test both
      bin/ltl2tgba and tgbatest/ltl2tgba.
      * NEWS: Mention the change.
      9f3a7a49
  7. 11 May, 2015 5 commits
  8. 10 May, 2015 3 commits
  9. 05 May, 2015 1 commit
  10. 04 May, 2015 1 commit
  11. 28 Apr, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: heuristic to switch between circles and ellipses · a4b63e8e
      Alexandre Duret-Lutz authored
      * src/twaalgos/dotty.cc: Add an option (e) to force elliptic shape, and
      a heuristic to choose between circle and ellipse by default.
      * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document 'e'.
      * src/taalgos/dotty.cc: Ignore 'e'.
      * wrap/python/spot.py (setup): Do not force circular states.  The
      default should be fine.
      * src/tests/det.test, src/tests/dstar.test, src/tests/monitor.test,
      src/tests/neverclaimread.test, src/tests/readsave.test,
      src/tests/sccdot.test, src/tests/tgbagraph.test: Adjust expected
      results.
      * NEWS: Adjust.
      a4b63e8e