Metadata-Version: 2.4
Name: octopas
Version: 0.1.1
Summary: Python interface to OctoPAs, a library for parametric automata and transducers
Author-email: Oliver Markgraf <markgraf@cs.uni-kl.de>, Hongjian Jiang <hongjian.jiang@rptu.de>, Franziska Alber <franziska.alber@informatik.uni-regensburg.de>, Philipp Rümmer <philipp.ruemmer@it.uu.se>
License-Expression: MIT
Project-URL: Homepage, https://arg-git.informatik.uni-kl.de/pub/octopas
Project-URL: Source, https://arg-git.informatik.uni-kl.de/pub/octopas
Keywords: automata,symbolic automata,parametric automata,transducers,formal verification
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Java
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Libraries
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: JPype1>=1.5
Provides-Extra: plot
Requires-Dist: graphviz; extra == "plot"
Provides-Extra: test
Requires-Dist: pytest; extra == "test"
Dynamic: license-file

# OctoPAs for Python

A Python interface to [OctoPAs](https://arg-git.informatik.uni-kl.de/pub/octopas),
a library for parametric automata and transducers. OctoPAs runs on the JVM,
and this package drives it in-process through
[JPype](https://jpype.readthedocs.io).

## Install

```bash
pip install octopas             # or "octopas[plot]" for drawing automata
```

You need Python 3.9 or newer and Java 17 or newer. The OctoPAs library is
bundled with the package, so nothing else has to be built. If Java is not
found, set `JAVA_HOME` to your JDK. Plotting also needs the Graphviz `dot`
executable.

## Parametric automata

A guard constrains the current symbol `x`. A parameter has one value for the
whole accepting run:

```python
import octopas as oc
from octopas import x

pa = oc.interval()
y = pa.parameter("y")

# Words whose last letter is strictly larger than all earlier ones.
a2 = pa.automaton(0, [1], [(0, x < y, 0), (0, x == y, 1)])
a2.accepts("abz")            # True
a2.witness("abz")            # {y: 122}

lower = pa.star_of(oc.between("a", "z"))
(a2 & lower).accepted_run()  # ([97], {y: 97})
```

To write guards, use `x < y`, `x == y + 1`, `(x >= "a") & (x <= y)`,
`oc.between(lo, hi)` or `oc.any_symbol()`. A bound can be an integer, a
one-character string, a parameter plus an offset, or `None` for infinity.

These are the operators and methods on automata:

| Python | Meaning |
| --- | --- |
| `a & b`, `a \| b`, `a + b` | intersection, union, and concatenation, with shared parameters |
| `~a` | pointwise complement, for every fixed parameter valuation |
| `a <= b`, `a.equivalent(b)` | pointwise inclusion and equivalence |
| `a.is_empty()`, `a.accepted_run()` | exact emptiness, and a witness word with its parameter values |
| `a.star()`, `a.reverse()`, `a.determinize()`, `a.reduce()`, `a.prune()` | the usual constructions |
| `a.projected_complement()` | complement after projecting the parameters away |
| `a.accepts_under(w, {y: 5})` | acceptance under exactly these parameter values |
| `pa.direct_intersect(a, b)`, etc. | variants that rename clashing parameters of `b` apart |

## Linear guards

`oc.linear()` builds automata whose guards are Boolean combinations of
comparisons between `x`, parameters plus offsets, and constants. Unlike an
interval guard, a linear guard can constrain parameters on their own:

```python
from octopas.linear import cmp

la = oc.linear()
p, q = la.parameter("p"), la.parameter("q")
a = la.automaton(0, [1], [(0, (x == p) & cmp(p, "<", q), 1)])
a.accepts_under([3], {p: 3, q: 4})   # True
a.accepts_under([3], {p: 3, q: 3})   # False
```

Interval guards such as `x < p` also work here. Combine guards with `&`, `|`
and `~`. The automata support `&`, `|`, `~` (pointwise complement),
`equivalent`, `accepted_run`, `accepts` and `accepts_under`.

## Active learning (PL\*)

`octopas.learning` learns a parametrized automaton from membership queries
under fixed parameter values and pointwise equivalence queries.

```python
from octopas.learning import learn

target = la.automaton(0, [1], [(0, x < p, 0), (0, x == p, 1)])
result = learn(target)
result.hypothesis.equivalent(target)   # True
result.stats                            # queries, slices, time
```

By default the vocabulary is the set of terms in the target's guards. Pass
`Vocabulary.from_terms(...)` to use another one.

## Transducers

```python
upper = pa.transducer(0, [0], [(0, oc.between("a", "z"), [x - 32], 0)])
upper.output_on("abc")       # [65, 66, 67]
image = upper(a2 & lower)    # exact image; guards become offsets of y
upper.preimage(image)
upper.then(other)            # composition: upper first, then other
```

An output is a sum of `x`, parameters, and constants. An exact operation that
OctoPAs cannot represent raises `oc.Unsupported`. That is different from an
empty result.

## UTF-16 automata

These are parameter-free automata over code units `0..65535`. They support
exact complement and minimisation.

```python
s = oc.utf16()
ident = s.range("a", "z") + s.range("a", "z").star()
(~ident).example()           # a word outside the language
(ident - s.word("abc")).accepts("abc")   # False
ident.minimize()
```

## Plotting

`a.plot("a.svg")` writes a drawing. Without a file name, it returns a
`graphviz.Source`, and automata also display inline in Jupyter. Highlighting
follows Mata's Python binding:

```python
a2.plot("a2.svg",
        node_highlight=[(lambda aut, q: q in aut.finals, {"fillcolor": "red"})],
        edge_highlight=[(lambda aut, e: e.guard == "{y}", {"style": "dashed"})])
```

## Development

To work on the binding itself, build the JAR from source. You need a JDK
(17 or newer) and sbt:

```bash
sbt pythonJar                # in the repository root: builds python/octopas/_jars/octopas-all.jar
python3 -m venv .venv        # a Python 3 environment; plain `pip` may be Python 2
source .venv/bin/activate
pip install -e "python[plot,test]"
python -m pytest python/tests
```

To use a JAR from somewhere else, set `OCTOPAS_JAR=/path/to/octopas-all.jar`.

## License

MIT. See `LICENSE`.
