whitemech / pythomata

A Python package for automata theory.

Pythomata

Python implementation of automata theory.

Links

• GitHub: https://github.com/whitemech/pythomata
• PyPI: https://pypi.org/project/pythomata/
• Documentation: https://whitemech.github.io/pythomata
• Changelog: https://whitemech.github.io/pythomata/release-history/
• Issue Tracker:https://github.com/whitemech/pythomata/issues
• Download: https://pypi.org/project/pythomata/#files

Install

• from PyPI:

pip install pythomata

• or, from source (e.g. develop branch):

pip install git+https://github.com/whitemech/pythomata.git@develop

• or, clone the repository and install:

git clone https://github.com/whitemech/pythomata.git
cd pythomata
pip install .

How to use

• Define an automaton:

from pythomata import SimpleDFA
alphabet = {"a", "b", "c"}
states = {"s1", "s2", "s3"}
initial_state = "s1"
accepting_states = {"s3"}
transition_function = {
    "s1": {
        "b" : "s1",
        "a" : "s2"
    },
    "s2": {
        "a" : "s2",
        "b" : "s1",
        "c" : "s3",
    },
    "s3":{
        "c" : "s3"
    }
}
dfa = SimpleDFA(states, alphabet, initial_state, accepting_states, transition_function)

• Test word acceptance:

# a word is a list of symbols
word = "bbbac"
dfa.accepts(word)        # True

# without the last symbol c, the final state is not reached
dfa.accepts(word[:-1])   # False

• Operations such as minimization and trimming:

dfa_minimized = dfa.minimize()
dfa_trimmed = dfa.trim()

• Translate into a graphviz.Digraph instance:

graph = dfa.minimize().trim().to_graphviz()

To print the automaton:

graph.render("path_to_file")

For that you will need to install Graphviz. Please look at their download page for detailed instructions depending on your system.

The output looks like the following:

Features

• Basic DFA and NFA support;
• Algorithms for DFA minimization and trimming;
• Algorithm for NFA determinization;
• Translate automata into Graphviz objects.
• Support for Symbolic Automata.

Tests

To run the tests:

tox

To run only the code style checks:

tox -e flake8 -e mypy

Docs

To build the docs:

mkdocs build

To view documentation in a browser

mkdocs serve

and then go to http://localhost:8000

License

Pythomata is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).

Copyright 2018-2020 WhiteMech

pythomata's Issues

Implement `BddDfa`

Is your feature request related to a problem? Please describe.

SymbolicDFA is actually explicit in the state space and symbolic in the transition guards.

Describe the solution you'd like

Implement a fully symbolic version of the DFA, where all the components are represented symbolically.

Describe alternatives you've considered
n/a

Additional context
n/a

Minimized DFA not minimal

Describe the bug
Minimized DFA does not appear to be minimal.

To Reproduce
To reproduce, run conv_rust2pyth_min.py in test.zip. Observe that the output DFA (rendered in test.svg in the zip file) has a cluster of trivial accept states below state 9.

Expected behavior
Expected to obtain the unique minimal DFA recognizing the same language, but looking at the DFA in test.svg, we could add self-loops for all characters to state 9, remove all other accepting states below, and decide the same language.

Screenshots
The DFA is too large to screenshot well. Please see test.svg in the zip file above.

Implement boolean operations over `SymbolicDFA`

Is your feature request related to a problem? Please describe.
SymbolicDFA currently does not support boolean operations.

Describe the solution you'd like
Implement them.

• intersection
• union
• complementation

References:

• Applications of Symbolic Finite Automata: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/ciaa13.pdf
• Symbolic Automata Constraint Solving: https://link.springer.com/chapter/10.1007%2F978-3-642-16242-8_45
• Rex: Symbolic Regular Expression Explorer: https://www.microsoft.com/en-us/research/wp-content/uploads/2010/04/rex-ICST.pdf

Describe alternatives you've considered
n/a

Additional context
Add any other context or screenshots about the feature request here.

Unexpected behavior of dfa.minimize method

• Pythomata version: clone from master commit id b42e5e3
• Python version: CPython 3.5.3
• Operating System: MacOS

Description

Unexpected behavior of dfa.minimize function
( Am I not understanding it right )

What I Did

I have a DFA automata like this:

Let's call it dfa1

I call the following function on it

dfa3 = dfa2.minimize()

And I end up with this

Questions:

 - Why there are transitions coming from state 2 on the same symbols.  There is transition on symbol 'E' that  leads both state 2 and state 1

 - The minimized automata will accept words that original automate will not accept, because the order of sequence of states is lost.   Dfa2 will only accept single word 'HELO'   DFa3 will also accept words 'HHO'  'ELLHO' etc... basically [HEL]+O

Making accept method faster

The accept method for accepting a string could be made faster by stopping the iteration over the string symbols when the DFA is in a sink state. Here is my custom solution that should work:

    ...
    current_states = reduce(set.union, map(lambda x: dfa.get_successors(x, temp), current_states),set(),)

    sink_state = all(is_sink(dfa, state) for state in current_states)
    if sink_state:
        break
is_accepted = any(dfa.is_accepting(state) for state in current_states)

where

def is_sink(dfa: SymbolicDFA, current_state: int):
    sink = True
    for output_state in dfa._transition_function[current_state].keys():
        if output_state != current_state:
            sink = False
    return sink

Hope it will be useful. My 2 cents.

Ivan

Implement serialization/deserialization into/from several formats

Is your feature request related to a problem? Please describe.
Would be useful to have serialization to several formats (e.g. JSON, HOA etc.)

Describe the solution you'd like
Provide utilities to serialize-/deserialize automata.

Describe alternatives you've considered
n/a

Additional context
n/a

Make `Simulator.step` use the sink state if a bad symbol is provided.

Is your feature request related to a problem? Please describe.

When using DFASimulator.step with a bad symbol, the current state is set to None.

Describe the solution you'd like

The current state should be set to the sink state, which does exist since the DFASimulator completes the DFA.

Describe alternatives you've considered

Additional context

A SimpleNFA isn't initialized by states consisting of two symbols, e. g. "s0", "s1" etc.

Describe the bug
A SimpleNFA isn't initialized by states consisting of two symbols, e. g. "s0", "s1" etc.

To Reproduce
Steps to reproduce the behavior:

1. Create a file .py
2. Run the following code snippet:

from pythomata import SimpleNFA
from IPython.display import Image

alphabet = {'0', '1'}
states = {'q0', 'q1', 'q2', 'q3'}
initial_state = 'q0'
accepting_states = {'q3'}
transition_function = {
    'q0' : {
        '0' : 'q0',
        '1' : 'q0',
        '0' : 'q1',
        '1' : 'q2'
    },
    'q1' : {
        '0' : 'q3'
    },
    'q2' : {
        '1' : 'q3'
    }
}
nfa = SimpleNFA(states, alphabet, initial_state, accepting_states, transition_function)

picture = nfa.to_graphviz()
picture.format = 'png'
Image(filename=picture.render("./new_nfa")) 

Expected behavior
The NFA generated by the previous code and similar to this NFA

Screenshots

Desktop (please complete the following information):

• OS: Linux Mint
• Browser Chome

Generate a random DFA of size N

I train Neural Network to recognize DFA given accept / not accept strings. It would be nice to have a method that samples random DFA with maximum size N and K strings that are accepted and K strings that are not accepted by this automaton.

Add SymbolicAutomata examples in docs.

Is your feature request related to a problem? Please describe.

Provide more examples of the usage of SymbolicAutomata.

Describe the solution you'd like

Describe alternatives you've considered

Additional context

Basic example from readme does not work: ...word = "bbbac" is not accepted

from pythomata import SimpleDFA
alphabet = {"a", "b", "c"}
states = {"s1", "s2", "s3"}
initial_state = "s1"
accepting_states = {"s3"}
transition_function = {
    "s1": {
        "b" : "s1",
        "a" : "s2"
    },
    "s2": {
        "a" : "s3",
        "b" : "s1"
    },
    "s3":{
        "c" : "s3"
    }
}
dfa = SimpleDFA(states, alphabet, initial_state, accepting_states, transition_function)

word = "bbbac"
dfa.accepts(word) 

Returns False.

Python 3.7.13, pythomata==0.3.2

Problems in `levels_to_accepting_states()`

• Pythomata version: 0.1.5.post1
• Python version: Python 3.5
• Operating System: Linux (Ubuntu)

Description

I have the following DFA:

The function levels_to_accepting_states() gives me:
{1: 2, 0: 2}

whereas I was expecting:
{1:0, 0:1}

because 1 is a final state and from 0 we need one step.

What I Did

Here how to replicate the issue:

    a, b, ab, empty = Symbol("a"), Symbol("b"), Symbol("ab"), Symbol("{}")
    alphabet = Alphabet({a, b, ab, empty})
    states = frozenset({"s1", "s2"})
    initial_state = "s1"
    accepting_states = frozenset({"s2"})
    transition_function = {
        "s1": {
            a: "s1",
            ab: "s1",
            empty: "s1",
            b: "s2"
        },
        "s2": {
            a: "s2",
            ab: "s2",
            empty: "s2",
            b: "s2"
        }
    }
    dfa = DFA(alphabet, states, initial_state, accepting_states, transition_function)
    levels = dfa.levels_to_accepting_states()

levels should be {"s2":0, "s1":1}

Permission error while saving graphs using graphvix

Hi, I was using your library for minimizing a 3 variable DFA and while using graph.render it shows permission error as the graph below.

Implement boolean operations of `SimpleDFA`

Is your feature request related to a problem? Please describe.
Currently, SimpleDFA does not support boolean operations like intersection, union, negation etc.

Describe the solution you'd like
Implement them.

• intersection
• union
• complement

Boolean binary operations should be implemented using the same code to compute the product; they only differ in the condition for a state to be accepting.

Describe alternatives you've considered
n/a

Additional context

The reference can be any textbook on automata theory, e.g. https://en.wikipedia.org/wiki/Introduction_to_Automata_Theory,_Languages,_and_Computation

DFA equality

Is there a way to compare two minimized DFAs for equality?

What I really want to do is compare two LTLf terms. I'm hoping to parse them with logaut, minimize them, and check for DFA equality.

Add `SimpleNFA` examples in docs.

Is your feature request related to a problem? Please describe.

There is no thorough documentation regarding non-deterministic finite automata.

Describe the solution you'd like

Add examples for SimpleNFA.

Describe alternatives you've considered

Additional context

`SymbolicAutomaton.determinize()` does not work correctly when initial state is accepting.

Subject of the issue

SymbolicAutomaton.determinize() does not work correctly when initial state is accepting.

Your environment

• OS: Ubuntu 19.10
• Python version: 3.7
• Package Version: 0.3.1

Steps to reproduce

• Install the package:
  pip install pythomata==0.3.1
• Run the following code snippet:

import sympy
from pythomata import SymbolicAutomaton
a = sympy.symbols("a")
aut = SymbolicAutomaton()
aut.create_state()
aut.set_accepting_state(0, True)
aut.set_accepting_state(1, False)
aut.add_transition((0, a, 1))
aut.to_graphviz().render("automaton_1")
aut.determinize().to_graphviz().render("automaton_1_determinized")

"automaton_1" gives:

The determinized version (which should yield the same automaton) gives:

Expected behaviour

Both automata, the original and the determinized one, are the same.

Actual behaviour

The initial state is not accepting anymore.

I believe the guilty lines are these:

pythomata/pythomata/impl/symbolic.py

Lines 337 to 338 in 3b83dc0

	if s == initial_state:
	continue

That is, the initial state is ignored, whether it is an accepting state or not. Before the if, there should be the check for acceptance of that state.

Support translation from/to regular expressions.

Is your feature request related to a problem? Please describe.

Sometimes it is hard to build automata by thinking of states and transitions,
whereas it is trivial to think in terms of an equivalent regular expression.

Describe the solution you'd like

Provide translations from/to regular expressions for some automata implementation.

Describe alternatives you've considered

Additional context

Typo in example of README

Describe the bug
In the "How to use" section of the README, the example is not correct (README at the commit: https://github.com/whitemech/pythomata/blob/cb521b8c98a63069ebc7a36e3ac43d47ab2941e6/README.md).

By replacing the transition:

(s2, a, s3)

With the transition:

(s2, c, s3)

It works again.

The code snippet becomes:

from pythomata import SimpleDFA
alphabet = {"a", "b", "c"}
states = {"s1", "s2", "s3"}
initial_state = "s1"
accepting_states = {"s3"}
transition_function = {
    "s1": {
        "b" : "s1",
        "a" : "s2"
    },
    "s2": {
        "c" : "s3",
        "b" : "s1"
    },
    "s3":{
        "c" : "s3"
    }
}
dfa = SimpleDFA(states, alphabet, initial_state, accepting_states, transition_function)

Make SymbolicDFA accept SymPy symbols as keys of propositional interpretations

Is your feature request related to a problem? Please describe.
The following code does not work:

from pythomata.impl.symbolic import SymbolicDFA
from sympy import symbols
a = symbols("a")
dfa = SymbolicDFA()
dfa.create_state()
dfa.add_transition((0, a, 1))
dfa.set_accepting_state(1, True)

# returns True, correctly
dfa.accepts([{"a": True}])

# it raises ValueError: Symbol {a: True} is not valid.
dfa.accepts([{a: True}])

The reason is that SymbolicDFA.accepts accepts only PropositionalInterpretation whose labels are of type str and not sympy.Symbol.

Describe the solution you'd like
Make it work. That is, try to be more flexible on the data validation in SymbolicDFA.accepts.

Describe alternatives you've considered
n/a

Additional context
n/a

Implement symbolic transitions.

Is your feature request related to a problem? Please describe.

With the current implementation, all the transitions must be stated explicitly and with the alphabet as arc labels.

Describe the solution you'd like

A way to specify a broader set of possible transitions expressed by propositional formulas, e.g. true to specify any symbol (even not present in the alphabet), false the opposite, a to indicate that the proposition a must be true.

Describe alternatives you've considered

Additional context

Provide documentation for Simulator APIs

Is your feature request related to a problem? Please describe.

The Simulator API is not well documented.

Describe the solution you'd like

Provide documentation and examples for the Simulator API.

Describe alternatives you've considered

Additional context

Update documentation after #72

Is your feature request related to a problem? Please describe.
After #72, many parts of the documentation are obsolete.

Describe the solution you'd like
Update docs and code examples after API refactoring of #72.

Describe alternatives you've considered

Additional context