Skip to main content

This package takes a symbolic DFA and produces an AIGER file of type aag

Project description

SymDFA2Aiger

Description

SymDFA2Aiger is a tool for converting a symbolic deterministic finite automaton (SDFA) into an AIGER file (.aag). The main function provided is SymDFA2Aiger. An example input file is included in this directory to illustrate the expected format for the function.

Personal Note

This tool was created by Daniel Bachmann Aisen as part of his master’s thesis. In 2024, amidst challenging times, this project is dedicated to the safe return of all hostages, to the soldiers safeguarding my friends, family, and me, and in memory of those who have fallen. May we look forward to better days.

Inputs

The tool requires five inputs corresponding to SDFA properties:

  • sigma_controlled: set[Formula]
  • sigma_environment: set[Formula]
  • state_variables: set[Formula]
  • initial_state: PLTLAnd
  • transition_system: dict

Optional Inputs

  • file_name: str (default: "SymbDFA_AIGER.aag")
  • state_variables_return_dict: dict (default: None)

Example Usage

from SymDFA2AIGER import SymDFA2AIGER

a = parse_pltl("a")
b = parse_pltl("b")
c = parse_pltl("c")
d = parse_pltl("d")
_x1 = parse_pltl("x_var1")
_x2 = parse_pltl("x_var2")
_x3 = parse_pltl("x_var3")
_x4 = parse_pltl("x_var4")

sigma_controlled = {a, c}
sigma_environment = {b, d}

initial_state_input = PLTLAnd(_x1, PLTLNot(_x2), _x3, _x4)
final_state_variable = PLTLAnd(_x1, _x2, PLTLNot(_x3), PLTLNot(_x4))
state_variables_input = [_x1, _x2, _x3, _x4]

transition_system_input = {}
transition_system_input["x_var1_prime"] = parse_pltl("a")
transition_system_input["x_var2_prime"] = parse_pltl("b")
transition_system_input["x_var3_prime"] = parse_pltl("(false|a|(b&d)|!c)")
transition_system_input["x_var4_prime"] = parse_pltl(" ((! a) & ! c )")

SymDFA2AIGER(sigma_controlled, sigma_environment, state_variables_input, initial_state_input, transition_system_input, final_state_variable, "experiment_aiger.aag")

Installation and Dependencies

This tool requires two external libraries: pylogics_modalities and multipledispatch.

  • pylogics_modalities: This library extends the pylogics library by whitemech. To install it, use the .whl file provided in the dependencies folder:

pip install dependencies/pylogics_modalities-0.2.2-py3-none-any.whl

pip install SymDFA2Aiger

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

symdfa2aiger-1.1.6.tar.gz (80.1 kB view details)

Uploaded Source

Built Distribution

symdfa2aiger-1.1.6-py3-none-any.whl (6.2 kB view details)

Uploaded Python 3

File details

Details for the file symdfa2aiger-1.1.6.tar.gz.

File metadata

  • Download URL: symdfa2aiger-1.1.6.tar.gz
  • Upload date:
  • Size: 80.1 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.1.1 CPython/3.10.12

File hashes

Hashes for symdfa2aiger-1.1.6.tar.gz
Algorithm Hash digest
SHA256 32ca88d33c497d90fe864613f39d07578b1688315de79a591f4cf764cc4df9f0
MD5 3e53b35cdf40febee07b08b1c817213e
BLAKE2b-256 812bdb54f2272d3bfe4544e6f8ac6ec225cae7a74eb237877617b70b53cbbf6c

See more details on using hashes here.

File details

Details for the file symdfa2aiger-1.1.6-py3-none-any.whl.

File metadata

  • Download URL: symdfa2aiger-1.1.6-py3-none-any.whl
  • Upload date:
  • Size: 6.2 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.1.1 CPython/3.10.12

File hashes

Hashes for symdfa2aiger-1.1.6-py3-none-any.whl
Algorithm Hash digest
SHA256 48217c3f0430c506082e0a9735e2eca7f8fa50ccd75f9fcfbaa0a2872e0bf312
MD5 60e8f142a0d7022d49cc85603cabc2c4
BLAKE2b-256 64955ed38a4e509d24073e22b2207c51fe44006fda8a5055e94fd45a0b716dcf

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page