Commit ad2f5524 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

doc: add tut90.org about bdd_dict

Fixes #372.

* doc/org/tut90.org: New file.
* doc/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention it.
* python/spot/__init__.py: Allow make_twa_graph with
default bdd_dict.
parent 7f48a08e
Pipeline #10349 passed with stages
in 208 minutes and 33 seconds
......@@ -30,6 +30,11 @@ New in spot 2.7.5.dev (not yet released)
amongst "Inf(0)", "t", or "f", and persistance properties have an
acceptance condition among "Fin(0)", "t", or "f".
Documentation:
- https://spot.lrde.epita.fr/tut90.html is a new file that explains
the purpose of the =spot::bdd_dict= object.
Library:
- Add generic_accepting_run() as a variant of generic_emptiness_check() that
......
......@@ -115,6 +115,7 @@ ORG_FILES = \
org/tut50.org \
org/tut51.org \
org/tut52.org \
org/tut90.org \
org/upgrade2.org \
org/satmin.org \
org/satmin.tex \
......
......@@ -38,6 +38,8 @@ three interfaces supported by Spot: shell commands, Python, or C++.
- [[file:tut23.org][Creating an alternating automaton by adding states and transitions]]
- [[file:tut24.org][Iterating over alternating automata]]
- [[file:tut52.org][Creating an explicit Kripke structure]]
- [[file:tut90.org][Using the =bdd_dict= to associate atomic proposition to BDD
variables, or allocate anonymous BDD variables (advanced)]]
* Examples in C++ only
......
This diff is collapsed.
......@@ -200,6 +200,12 @@ class twa_graph:
from IPython.display import SVG
return SVG(_ostream_to_svg(ostr))
def make_twa_graph(*args):
from spot.impl import make_twa_graph as mtg
if len(args) == 0:
return mtg(_bdd_dict)
return mtg(*args)
@_extend(formula)
class formula:
def __init__(self, str):
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment