| Name | SymDFA2AIGER JSON |
| Version |
1.1.6
JSON |
| download |
| home_page | None |
| Summary | This package takes a symbolic DFA and produces an AIGER file of type aag |
| upload_time | 2024-08-22 13:36:09 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | >=3.8 |
| license | None |
| keywords |
|
| VCS |
 |
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# 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
```python
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](https://github.com/danielaisen/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`
```bash
pip install SymDFA2Aiger
Raw data
{
"_id": null,
"home_page": null,
"name": "SymDFA2AIGER",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.8",
"maintainer_email": null,
"keywords": null,
"author": null,
"author_email": "Daniel Bachmann Aisen <danielmaxaisen@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/81/2b/db54f2272d3bfe4544e6f8ac6ec225cae7a74eb237877617b70b53cbbf6c/symdfa2aiger-1.1.6.tar.gz",
"platform": null,
"description": "# SymDFA2Aiger\n\n## Description\n\nSymDFA2Aiger is a tool for converting a symbolic deterministic finite automaton (SDFA) into an AIGER file (.aag). The main function provided is `SymDFA2Aiger`. \nAn example input file is included in this directory to illustrate the expected format for the function.\n\n#### Personal Note\nThis tool was created by Daniel Bachmann Aisen as part of his master\u2019s thesis. \nIn 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. \nMay we look forward to better days.\n\n## Inputs\n\nThe tool requires five inputs corresponding to SDFA properties:\n\n- `sigma_controlled`: `set[Formula]`\n- `sigma_environment`: `set[Formula]`\n- `state_variables`: `set[Formula]`\n- `initial_state`: `PLTLAnd`\n- `transition_system`: `dict`\n\n### Optional Inputs\n\n- `file_name`: `str` (default: `\"SymbDFA_AIGER.aag\"`)\n- `state_variables_return_dict`: `dict` (default: `None`)\n\n### Example Usage\n\n```python\nfrom SymDFA2AIGER import SymDFA2AIGER\n\na = parse_pltl(\"a\")\nb = parse_pltl(\"b\")\nc = parse_pltl(\"c\")\nd = parse_pltl(\"d\")\n_x1 = parse_pltl(\"x_var1\")\n_x2 = parse_pltl(\"x_var2\")\n_x3 = parse_pltl(\"x_var3\")\n_x4 = parse_pltl(\"x_var4\")\n\nsigma_controlled = {a, c}\nsigma_environment = {b, d}\n\ninitial_state_input = PLTLAnd(_x1, PLTLNot(_x2), _x3, _x4)\nfinal_state_variable = PLTLAnd(_x1, _x2, PLTLNot(_x3), PLTLNot(_x4))\nstate_variables_input = [_x1, _x2, _x3, _x4]\n\ntransition_system_input = {}\ntransition_system_input[\"x_var1_prime\"] = parse_pltl(\"a\")\ntransition_system_input[\"x_var2_prime\"] = parse_pltl(\"b\")\ntransition_system_input[\"x_var3_prime\"] = parse_pltl(\"(false|a|(b&d)|!c)\")\ntransition_system_input[\"x_var4_prime\"] = parse_pltl(\" ((! a) & ! c )\")\n\nSymDFA2AIGER(sigma_controlled, sigma_environment, state_variables_input, initial_state_input, transition_system_input, final_state_variable, \"experiment_aiger.aag\")\n```\n\n\n## Installation and Dependencies\n\nThis tool requires two external libraries: [pylogics_modalities](https://github.com/danielaisen/pylogics_modalities) and `multipledispatch`.\n\n- **pylogics_modalities**: This library extends the pylogics library by whitemech. To install it, use the `.whl` file provided in the `dependencies` folder:\n\n`pip install dependencies/pylogics_modalities-0.2.2-py3-none-any.whl`\n\n```bash\npip install SymDFA2Aiger\n",
"bugtrack_url": null,
"license": null,
"summary": "This package takes a symbolic DFA and produces an AIGER file of type aag",
"version": "1.1.6",
"project_urls": {
"Homepage": "https://github.com/danielaisen/SymDFA2Aiger",
"Issues": "https://github.com/danielaisen/SymDFA2Aiger/issues"
},
"split_keywords": [],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "64955ed38a4e509d24073e22b2207c51fe44006fda8a5055e94fd45a0b716dcf",
"md5": "60e8f142a0d7022d49cc85603cabc2c4",
"sha256": "48217c3f0430c506082e0a9735e2eca7f8fa50ccd75f9fcfbaa0a2872e0bf312"
},
"downloads": -1,
"filename": "symdfa2aiger-1.1.6-py3-none-any.whl",
"has_sig": false,
"md5_digest": "60e8f142a0d7022d49cc85603cabc2c4",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8",
"size": 6200,
"upload_time": "2024-08-22T13:36:07",
"upload_time_iso_8601": "2024-08-22T13:36:07.441706Z",
"url": "https://files.pythonhosted.org/packages/64/95/5ed38a4e509d24073e22b2207c51fe44006fda8a5055e94fd45a0b716dcf/symdfa2aiger-1.1.6-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "812bdb54f2272d3bfe4544e6f8ac6ec225cae7a74eb237877617b70b53cbbf6c",
"md5": "3e53b35cdf40febee07b08b1c817213e",
"sha256": "32ca88d33c497d90fe864613f39d07578b1688315de79a591f4cf764cc4df9f0"
},
"downloads": -1,
"filename": "symdfa2aiger-1.1.6.tar.gz",
"has_sig": false,
"md5_digest": "3e53b35cdf40febee07b08b1c817213e",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8",
"size": 80111,
"upload_time": "2024-08-22T13:36:09",
"upload_time_iso_8601": "2024-08-22T13:36:09.276380Z",
"url": "https://files.pythonhosted.org/packages/81/2b/db54f2272d3bfe4544e6f8ac6ec225cae7a74eb237877617b70b53cbbf6c/symdfa2aiger-1.1.6.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-08-22 13:36:09",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "danielaisen",
"github_project": "SymDFA2Aiger",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "symdfa2aiger"
}
