1. 08 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      python: add bindings for bdd_to_formula() · 4e9303e3
      Alexandre Duret-Lutz authored
      Follow-up to an email from Ayrat Khalimov.
      
      * python/spot/impl.i: Include twa/formula2bdd.hh.
      * python/spot/__init__.py: Make the dictionnary
      optional.
      * spot/twa/formula2bdd.cc: Throw an exception instead of asserting.
      * tests/python/bdditer.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      4e9303e3
  2. 07 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · 2e763a08
      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.
      2e763a08
  3. 28 Feb, 2017 1 commit
  4. 20 Feb, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: add Python bindings · 289b2383
      Alexandre Duret-Lutz authored
      Related to #172, where we discussed that scc_info bindings were
      missing.
      
      * spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move...
      (spot::scc_info_node): ... here to help Swig.
      * python/spot/impl.i: Add bindings for scc_info.
      * tests/python/sccinfo.py: New file.
      * tests/Makefile.am: Add it.
      289b2383
  5. 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
  6. 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
  7. 12 Jan, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      minimize_wdba: fix handling of input with useless SCCs · c9918f64
      Alexandre Duret-Lutz authored
      * spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
      terminal SCCs that are incomplete, as if they had a non-accepting
      sink as successor.
      * spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
      (is_terminal_automaton): Add an option to ignore trivial SCC as we did
      before, since it matters for deciding membership to the guarantee
      class.
      (is_safety_mwdba): Rewrite as ...
      (is_safety_automaton): ... generalizating to any acceptance, and
      ignoring trivial SCCs.
      * bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
      tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
      is_safety_automaton().
      * tests/core/hierarchy.test: Add a problematic formula as test-case.
      * NEWS: Mention the bug.
      c9918f64
  8. 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
  9. 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
  10. 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
  11. 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
  12. 10 Oct, 2016 1 commit
  13. 29 Jul, 2016 1 commit
  14. 19 Jul, 2016 2 commits
  15. 11 Jul, 2016 1 commit
  16. 06 Jul, 2016 2 commits
  17. 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
  18. 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
  19. 10 May, 2016 2 commits
  20. 01 May, 2016 1 commit
  21. 22 Apr, 2016 2 commits
  22. 10 Apr, 2016 1 commit
  23. 08 Apr, 2016 1 commit
  24. 13 Mar, 2016 1 commit
  25. 10 Mar, 2016 2 commits
  26. 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
  27. 03 Mar, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      rename two confusing methods of emptiness_check_instantiator · ad08a585
      Alexandre Duret-Lutz authored
      * spot/twaalgos/emptiness.hh (emptiness_check_instantiator): rename
      min_acceptance_conditions and max_acceptance_conditions to
      min_sets and max_sets.
      * spot/twaalgos/emptiness.cc, python/ajax/spotcgi.in,
      tests/core/ikwiad.cc, tests/core/emptchk.cc, tests/core/randtgba.cc:
      Adjust.
      * doc/org/upgrade2.org, NEWS: Mention the change.
      ad08a585
  28. 01 Mar, 2016 1 commit