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 thedependencies
folder:
pip install dependencies/pylogics_modalities-0.2.2-py3-none-any.whl
pip install SymDFA2Aiger
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
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
Algorithm | Hash digest | |
---|---|---|
SHA256 | 32ca88d33c497d90fe864613f39d07578b1688315de79a591f4cf764cc4df9f0 |
|
MD5 | 3e53b35cdf40febee07b08b1c817213e |
|
BLAKE2b-256 | 812bdb54f2272d3bfe4544e6f8ac6ec225cae7a74eb237877617b70b53cbbf6c |
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
Algorithm | Hash digest | |
---|---|---|
SHA256 | 48217c3f0430c506082e0a9735e2eca7f8fa50ccd75f9fcfbaa0a2872e0bf312 |
|
MD5 | 60e8f142a0d7022d49cc85603cabc2c4 |
|
BLAKE2b-256 | 64955ed38a4e509d24073e22b2207c51fe44006fda8a5055e94fd45a0b716dcf |