1. 07 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · cd4c326f
      Alexandre Duret-Lutz authored
      The goal is to improve coverage stats, but I discovered two issues
      while doing so.
      
      * tests/python/twagraph.py: New test case.
      * tests/Makefile.am: Add it.
      * spot/twa/twagraph.hh: Add fix typos in error messages.
      * python/spot/impl.i: Fix broken wrappers for state_from_number and
      state_acc_sets.
      cd4c326f
  2. 28 Feb, 2017 1 commit
  3. 18 Jan, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      python: render the M&P hierarchy in SVG · ff4c4a72
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py (show_mp_hierarchy, mp_hierarchy_svg): New
      functions.
      * tests/python/formulas.ipynb: Illustrate show_mp_hierarchy.
      * python/ajax/spotcgi.in: Use mp_hierarchy_svg.
      * python/ajax/css/trans.css: Adjust for possible overflows.
      * NEWS: Mention this new feature.
      ff4c4a72
  4. 14 Jan, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      hierarchy: expose mp_class to python · ebdb198b
      Alexandre Duret-Lutz authored
      * bin/common_output.cc: Move some of the printing code...
      * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: ... here, as new
        variants of mp_class...
      * python/spot/impl.i: ... that we can now call from Python.
      * python/ajax/spotcgi.in: Use those to simplify and extend
      the code printing class membership.
      ebdb198b
  5. 06 Jan, 2017 5 commits
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos: Set 'dicho' algo as default for SAT-based minimization · ef2355a5
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Handle options.
      * spot/twaalgos/dtwasat.cc: Handle options.
      * spot/twaalgos/postproc.cc: Handle options.
      * spot/twaalgos/postproc.hh: Handle options.
      * tests/core/satmin.test: Update tests.
      Now use 'sat-minimize=4' to use the naive algo.
      * tests/core/satmin2.test: Update tests.
      Now use --sat-minimize='naive' to use the naive algo.
      * tests/python/satmin.py: Update tests.
      Now use 'naive=True' to use the naive algo.
      ef2355a5
    • Alexandre GBAGUIDI AISSE's avatar
      spot: Add 'langmap' option with dichotomy (it helps to choose min val) · 67e3a4f2
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
      * spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
      * spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
      * spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
      * spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
      * spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
      * spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
      Handle options.
      * spot/twaalgos/postproc.cc: Handle options.
      * spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
      * tests/core/satmin2.test: Add tests for dichotomy.
      * tests/core/satmin.test: Add tests for dichotomy.
      * tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.
      67e3a4f2
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos: Implement language_map algo · 8a0eed6c
      Alexandre GBAGUIDI AISSE authored
      * python/spot/impl.i: Add python bindings.
      * spot/twaalgos/langmap.cc: Implement algo.
      * spot/twaalgos/langmap.hh: Declare algo.
      * spot/twaalgos/Makefile.am: Add new files.
      * tests/python/langmap.py: Add tests.
      * NEWS: Update.
      8a0eed6c
    • Alexandre GBAGUIDI AISSE's avatar
      spot: Implement dt*a_sat_minimize_assume(...) methods · 9a204b77
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Add 'assume' option.
      * spot/misc/satsolver.cc: Add function to handle assumptions.
      * spot/misc/satsolver.hh: Declare assumption function.
      * spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_assume.
      * spot/twaalgos/dtbasat.hh: Declare it.
      * spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_assume and
      handle options.
      * spot/twaalgos/dtwasat.hh: Declare it.
      * spot/twaalgos/postproc.cc: Handle options.
      * spot/twaalgos/postproc.hh: Use param_ var for incr and assume.
      * tests/core/satmin.test: Add tests for the new function.
      * tests/core/satmin2.test: Add tests for the new function.
      * tests/python/satmin.py: Add tests for the new function.
      9a204b77
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos: Implement dt*a_sat_minimize_incr(...) functions · ee17c2de
      Alexandre GBAGUIDI AISSE authored
      * python/spot/__init__.py: Add 'incr' boolean argument.
      * spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_incr(...).
      * spot/twaalgos/dtbasat.hh: Declare it.
      * spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_incr(...) and
      deal with options.
      * spot/twaalgos/dtwasat.hh: Declare it.
      * spot/twaalgos/postproc.cc: Add option --sat-minimize=incr.
      * spot/twaalgos/postproc.hh: Add incr parameter.
      * tests/core/satmin.test: Add tests for incremental version.
      Update expected result.
      * tests/core/satmin2.test: Add tests for incremental version.
      * tests/python/satmin.py: Add tests for incremental version.
      ee17c2de
  6. 27 Dec, 2016 3 commits
    • Alexandre Duret-Lutz's avatar
      alternation: add a states_and algorithm · 27ab631c
      Alexandre Duret-Lutz authored
      This should will come handy to implement the convertion from LTL to
      alternating automata, and to handle automata with multiple initial
      states.
      
      * spot/twaalgos/alternation.hh, spot/twaalgos/alternation.cc: New files.
      * spot/twaalgos/Makefile.am: Add them.
      * python/spot/impl.i: Add bindings.
      * tests/python/alternating.py: Test states_and.
      27ab631c
    • Alexandre Duret-Lutz's avatar
      twa_graph: add support for universal initial states · 48c812a5
      Alexandre Duret-Lutz authored
      The only missing point is that the HOA parser cannot deal with multiple
      universal initial states, as seen in parseaut.test.
      
      * spot/graph/graph.hh (new_univ_dests): New function, extracted from...
      (new_univ_edge): ... this one.
      * spot/twa/twagraph.hh (set_univ_init_state): Implement using
      new_univ_dests.
      * spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, python/spot/impl.i:
      Add support for universal initial states.
      * spot/parseaut/parseaut.yy: Add preliminary support for
      universal initial states.  Multiple universal initial states
      are still not supported.
      * tests/core/alternating.test, tests/core/parseaut.test,
      tests/python/alternating.py: Adjust tests and exercise this new feature.
      48c812a5
    • Alexandre Duret-Lutz's avatar
      twa_graph: add basic support for alternation · 6aad559c
      Alexandre Duret-Lutz authored
      This only allows creating universal edges, and reading the associated
      destinations.
      
      * spot/twa/twagraph.hh (new_univ_edges, univ_dests, is_alternating): New
      function.
      * python/spot/impl.i: Add Python bindings.
      * tests/python/alternating.py: New file.
      * tests/Makefile.am: Add it.
      6aad559c
  7. 15 Dec, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      spotcgi: correctly kill ltl3ba on timeout · 38fdb40e
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py (automata): Do not create a session for
      every command, this is only needed if automata() is run with a timeout
      parameter.
      * python/ajax/spotcgi.in: Adjust exclude the main process from
      the process group, so that only children are killed on SIGALRM.
      * NEWS: Mention the bug.
      38fdb40e
    • Alexandre Duret-Lutz's avatar
      spotcgi: correctly kill ltl3ba on timeout · cd348275
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py (automata): Do not create a session for
      every command, this is only needed if automata() is run with a timeout
      parameter.
      * python/ajax/spotcgi.in: Adjust exclude the main process from
      the process group, so that only children are killed on SIGALRM.
      * NEWS: Mention the bug.
      cd348275
  8. 05 Nov, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      from_ltlf: new LTL transformation. · 2e69e045
      Alexandre Duret-Lutz authored
      Fixes #187.
      
      * spot/tl/ltlf.cc, spot/tl/ltlf.hh: New files.
      * spot/tl/Makefile.am: Add them.
      * bin/ltlfilt.cc: Add a new option.
      * bin/man/ltlfilt.x: Add bibliographic reference.
      * tests/core/ltlfilt.test: Add more tests.
      * tests/python/ltlf.py: New file.
      * tests/Makefile.am: Add it.
      * python/spot/impl.i: Python bindings.
      * NEWS: Mention it.
      2e69e045
  9. 10 Oct, 2016 1 commit
  10. 29 Jul, 2016 1 commit
  11. 19 Jul, 2016 2 commits
  12. 12 Jun, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      python: add a %%pml magic · 272daf62
      Alexandre Duret-Lutz authored
      Fixes #162.
      
      * python/spot/ltsmin.i: Implement the magic.
      * NEWS: Mention it.
      * tests/python/ltsmin-pml.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * tests/python/ipnbdoctest.py: Adjust.
      272daf62
  13. 25 May, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      add binding for language_containment_checker and document them · b4088271
      Alexandre Duret-Lutz authored
      * spot/tl/contain.cc, spot/tl/contain.hh: Simplify the
      use of language_containment_checker by adding default argument.
      * python/spot/__init__.py, python/spot/impl.i: Bind it in Python.
      * doc/org/tut04.org: New file to illustrate it.
      * doc/org/tut.org, doc/Makefile.am: Add it.
      * NEWS: Mention those changes.
      b4088271
  14. 01 May, 2016 1 commit
  15. 22 Apr, 2016 2 commits
  16. 08 Apr, 2016 1 commit
  17. 10 Mar, 2016 1 commit
    • Laurent XU's avatar
      python: add wrapper on twa_graph::edges() · 1eee12b8
      Laurent XU authored
      * spot/twa/twagraph.hh (edges): Do not hide from SWIG.
      * spot/graph/graph.hh: Hide stuff that SWIG do not understand.
      * python/spot/impl.i: Add some typemaps and fragment to
      iterate over the result of twa_graph::edges().
      1eee12b8
  18. 07 Mar, 2016 1 commit
    • Amaury Fauchille's avatar
      word: implement twa word parsing · 1fd76ee9
      Amaury Fauchille authored
      * spot/twaalgos/word.hh: add parse_word method and a new constructor
      * spot/twaalgos/word.cc: implement word parsing
      * python/spot/__init__.py: add parse_word method binding
      * tests/python/word.ipynb: add word parsing tests
      1fd76ee9
  19. 17 Feb, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      parsetl: change the interface to return a parsed_formula · 22f442f7
      Alexandre Duret-Lutz authored
      This gets the interface of all the functions parsing formula in line
      with the interface of the automaton parser: both return a "parsed_*"
      object (parsed_formula or parsed_automaton) that contains the said
      object and its list of errors.  Doing so avoid having to declare the
      parse_error_list in advance.
      
      * spot/tl/parse.hh, spot/parsetl/parsetl.yy: Do the change.
      * spot/parsetl/fmterror.cc: Adjust the error printer.
      * NEWS: Document it.
      * bin/common_finput.cc, bin/common_finput.hh, bin/ltlcross.cc,
      bin/ltldo.cc, bin/ltlfilt.cc, doc/org/tut01.org, doc/org/tut02.org,
      doc/org/tut10.org, doc/org/tut20.org, python/ajax/spotcgi.in,
      python/spot/impl.i, spot/parseaut/parseaut.yy, tests/core/checkpsl.cc,
      tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
      tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
      tests/core/length.cc, tests/core/ltlprod.cc, tests/core/ltlrel.cc,
      tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
      tests/core/safra.cc, tests/core/syntimpl.cc, tests/core/tostring.cc,
      tests/ltsmin/modelcheck.cc, tests/python/alarm.py,
      tests/python/interdep.py, tests/python/ltl2tgba.py,
      tests/python/ltlparse.py: Adjust all uses.
      22f442f7
  20. 16 Feb, 2016 3 commits
    • Alexandre Duret-Lutz's avatar
      cleanup ltsmin bindings · 9692d734
      Alexandre Duret-Lutz authored
      * python/spot/aux.py (rm_f): new function.
      * python/spot/ltsmin.i: Replace the %require magic by a simple function.
      Rewrite the %%dve magic.
      * tests/python/otfcrash.py: Simplify using spot.ltsmin.require()
      * tests/python/ltsmin.ipynb: Likewise, also add more text for the
      documentation.
      * NEWS: Adjust.
      9692d734
    • Alexandre Duret-Lutz's avatar
      python: report dot errors · 22af7aef
      Alexandre Duret-Lutz authored
      * python/spot/aux.py: Catch errors from dot and signal them.
      * tests/python/_aux.ipynb: New file.
      * tests/Makefile.am: Add it.
      * tests/sanity/ipynb.pl: Support the convention that tests starting with
      '_' should not be published on the web site.
      22af7aef
    • Alexandre Duret-Lutz's avatar
      python: move auxiliary functions in a separate module · c093b7b7
      Alexandre Duret-Lutz authored
      * python/spot/aux.py: New file, with function extracted from...
      * python/spot/__init__.py: ... here.
      * python/.gitignore, python/Makefile.am: Adjust.
      c093b7b7
  21. 15 Feb, 2016 1 commit
  22. 12 Feb, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      get read of twa_safra_complement · 6a662a6d
      Alexandre Duret-Lutz authored
      * spot/twa/twasafracomplement.cc, spot/twa/twasafracomplement.hh,
      tests/core/complementation.cc: Delete.
      * tests/Makefile.am, spot/twa/Makefile.am: Adjust.
      * tests/core/complementation.test: Rewrite using the new determinization
      code.
      * python/spot/impl.i: Do not mention twa_safra_complement anymore.
      * NEWS: Mention the removal.
      6a662a6d
    • Alexandre Duret-Lutz's avatar
      python: fix translate's doc string · 0d9019ea
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py (translate): Mention 'generic' in doc string.
      0d9019ea
  23. 05 Feb, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      dot: add option C(COLOR) · 77b0b5b3
      Alexandre Duret-Lutz authored
      This fixes the output gliches visible in the previous patches,
      where highlighting a state would remove its fill color.
      
      * spot/twaalgos/dot.cc, spot/taalgos/dot.cc: Implement option C(COLOR).
      * bin/common_aoutput.cc, doc/org/oaut.org: Document it.
      * doc/org/.dir-locals.el.in, doc/org/init.el.in,
      python/spot/__init__.py: Use it.
      * tests/python/automata-io.ipynb, tests/python/automata.ipynb,
      tests/python/highlighting.ipynb: Test it.
      * tests/core/readsave.test: Adjust.
      * NEWS: Mention recent changes.
      77b0b5b3
    • Alexandre Duret-Lutz's avatar
      python: highlighting functions for edges and states · 23c2cbf4
      Alexandre Duret-Lutz authored
      * python/spot/impl.i (highlight_state, highlight_edge): New function.
      * python/spot/__init__.py (highlight_states, highlight_edges): New
      functions.
      * spot/twaalgos/dot.cc: Add a '#' option.
      * spot/taalgos/dot.cc: Ignore '#'.
      * tests/python/highlighting.ipynb: New file to illustrate everything.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      23c2cbf4
  24. 31 Jan, 2016 1 commit
  25. 29 Jan, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: add a <N option · b11c07b3
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Implement it.
      * spot/taalgos/dot.cc: Ignore it.
      * spot/twaalgos/copy.cc, spot/twaalgos/copy.hh: Add option
      to limit the number of states.
      * tests/python/ltsmin.ipynb: Improve test case.
      * tests/Makefile.am: Cleanup the files generated by ltsmin.ipynb.
      * python/spot/__init__.py (setup): Add a max_states argument
      that default to 50.
      * bin/common_aoutput.cc: Mention the <INT option.
      * NEWS: Likewise.
      b11c07b3
  26. 26 Jan, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      ltsmin: add accessors for variable names and types · db1e842a
      Alexandre Duret-Lutz authored
      * spot/ltsmin/ltsmin.hh, spot/ltsmin/ltsmin.cc: Expose more of the
      ltsmin interface.
      * python/spot/ltsmin.i: Add some helper functions on top of this
      new interface.
      * tests/python/ltsmin.ipynb: Test them.
      * NEWS: Mention it.
      db1e842a
    • Alexandre Duret-Lutz's avatar
      ltsmin: implement a two-step loading · 907b72fb
      Alexandre Duret-Lutz authored
      * spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: Split load_ltsmin() into
      ltsmin_model::load() and ltsmin_model::kripke().  Report errors using
      exceptions instead of on std::cerr.
      * python/spot/ltsmin.i: Deal with exceptions.
      * tests/ltsmin/modelcheck.cc, tests/python/ltsmin.ipynb: Adjust.
      907b72fb