Skip to main content

DFAx

A JAX-compatible Python implementation of a Deterministic Finite Automaton (DFA).

Installation

Install using pip.

pip install dfax

Usage

Create DFAs by specifying a start state, transitions matrix, which is max number of states by number of alphabet symbols, and the associated labels for each state.

from dfax import DFAx

# Use the static class constructor to create a DFAx object
dfax = DFAx.create(
	start=0, # State referred to as 0 is the initial state
	transitions=jnp.array([
		[1, 2, 0, 0, 0],
		[1, 1, 1, 1, 1],
		[2, 2, 2, 2, 2],
	]), # Max number of states is 3 and number of tokens is 5
	labels=jnp.array([False, True, False]) # State labels
) # Returns a DFA

Take transitions on the DFA using a given symbol.

dfax = dfax.advance(0) # Returns the resulting DFA after reading the symbol referred to as 0

Minimize DFAs.

dfax = dfax.minimize() # Returns a canonical minimal DFA

Canonicalize DFAs by relabeling states based on a BFS search.

dfax = dfax.canonicalize() # Returns a canonical DFA

Mutate DFAs by randomly toggling entries in the transition matrix.

import jax

key = jax.random.PRNGKey(0)
dfax = dfax.mutate(key) # Returns a mutated DFA

Perform syntactic equality check between DFAs.

dfax1 == dfax2

Perform semantic equality check between DFAs.

dfax1.minimize() == dfax2.minimize()

Use DFAs as reward functions. With ternary semantics, reward is (i) +1 if the start state has label True, (ii) -1 if the start state has label False and is a sink state, and (iii) 0 otherwise. With binary semantics, 0 is returned instead of -1.

dfax.reward() # Returns a ternary reward
dfax.reward(binary=True) # Returns a binary reward

Sample from different DFA distributions: Reach samples DFAs ordering alphabet symbols, ReachAvoid samples Reach DFAs but also includes Avoid constraints, ReachAvoidDerived samples randomly mutated Reach and ReachAvoid DFAs, and Mixture samples from Reach, ReachAvoid, and ReachAvoidDerived with given probabilities (uniform by default).

import jax
from dfax.samplers import ReachSampler, ReachAvoidSampler, RADSampler, MixtureSampler

key = jax.random.PRNGKey(0)
sampler = ReachAvoidSampler()

dfax = sampler.sample(key)

sampler = MixtureSampler(probs=(0.5, 0.25, 0.25)) # Reach, ReachAvoid, ReachAvoidDerived
dfax = sampler.sample(key)

Define your own DFA samplers by overloading DFASampler .

@struct.dataclass
class MySampler(DFASampler):
    @partial(jax.jit, static_argnums=(0,))
    def sample(self, key: chex.PRNGKey) -> DFAx:
        # Write sampling code and return sampled DFA

Visualize DFAs.

from dfax.utils import visualize
visualize(dfax)

This project is a JAX extension of dfa. Therefore, we include helper methods for translating DFAx objects to and from DFA objects.

from dfax import dfa2dfax, dfax2dfa

dfa = dfax2dfa(dfax) # Create DFA from DFAx
dfax = dfa2dfax(dfa) # Create DFAx from DFA

In progress

Currently, we are working on implementing Boolean operations on DFAx objects, e.g., conjunction, disjunction, etc. If there are other functionalities you would like to have in this package, create pull request or contact us to work together!

Metadata

Release files for dfax 0.1.22

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for dfax 0.1.22
File Size Uploaded Provenance
dfax-0.1.22.tar.gz 719.6 kB Without provenance Details

Built distribution (wheel)

Table of built distributions (wheels) for dfax 0.1.22
File Interpreter ABI Platform
dfax-0.1.22-py3-none-any.whl Python 3 none any Details

Total release size: 1.3 MB

Release files / dfax-0.1.22.tar.gz

Download URL dfax-0.1.22.tar.gz
Size 719.6 kB
Tags Source
SHA-256 checksum
How to use checksums
7c6476b71a1a36f0d9bb899cf5a3057f955f5dfdab99c75286d19db51e119413
BLAKE2b-256 checksum
How to use checksums
e22153a7aa24fa2f50079c0b11f0d8d1c14e2e0ecaeeb145e9c2d1e854a84de3
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via uv/0.12.12 {"installer":{"name":"uv","version":"0.12.12","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"macOS","version":null,"id":null,"libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}

Release files / dfax-0.1.22-py3-none-any.whl

Download URL dfax-0.1.22-py3-none-any.whl
Size 601.8 kB
Tags Python 3
SHA-256 checksum
How to use checksums
e8b247b9e471ee9184eb2625819714daf8e6cab1db41e1d098ca2fdcb99246a8
BLAKE2b-256 checksum
How to use checksums
f5cd007db2525b7c463a1b54fc4bcd63aed1fc2a1357bd47ab7a8b2be5e503a8
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via uv/0.12.12 {"installer":{"name":"uv","version":"0.12.12","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"macOS","version":null,"id":null,"libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}

Security for dfax 0.1.22

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.

To learn more about protecting yourself from malicious actors, visit our package security documentation.

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page