Skip to main content

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

Project description

SymbSyntDec

Description

SymbSyntDec is a tool designed to convert a DECLARE specification of a system into an AIGER file (.aag). This conversion is achieved through a novel transformation into a symbolic deterministic finite automaton (SDFA), which is then used as input for the SymDFA2AIGER tool. The main function provided is SymbSyntDec. An example input file is included in this directory to demonstrate 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 four inputs corresponding to full DECLARE specification of a system:

  • sigma_controlled_str: set[str]
  • sigma_environment_str: set[str]
  • specification_env_phiE_str: set[str]
  • specification_con_phiC_str: set[str]

Optional Inputs

  • file_name: str (default: "SymbSyntDec_master_thesis.aag")

Example Usage

sigma_environment_str = {"set", "pay", "cancel"}
sigma_controlled_str = {"ship", "refund"}

specification_env_phiE_str = {"absence2(pay)", "absence2(cancel)", "resp-existence(pay,set)", "neg-succession(ship,cancel)", "neg-succession(ship,set)"}
specification_con_phiC_str = {"precedence(set, ship)", "precedence(pay, ship)", "precedence(pay, refund)", "response(pay, ship | refund)", "neg-succession(cancel, ship)"
}

symbolicDFA = SymbSyntDec(sigma_controlled_str, sigma_environment_str, specification_env_phiE_str, specification_con_phiC_str, "SymbSyntDec_master_thesis.aag")

Installation and Dependencies

This tool requires three external libraries: pylogics_modalities, SymDFA2Aiger 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 pip install multipledispatch

pip install SymbSyntDec

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

symbsyntdec-1.0.9.tar.gz (455.7 kB view details)

Uploaded Source

Built Distribution

symbsyntdec-1.0.9-py3-none-any.whl (11.8 kB view details)

Uploaded Python 3

File details

Details for the file symbsyntdec-1.0.9.tar.gz.

File metadata

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

File hashes

Hashes for symbsyntdec-1.0.9.tar.gz
Algorithm Hash digest
SHA256 a001b71cbcce8bbf1ab5ebb9fad3919c1ba85f0f23ad1abb5f47c90f912af902
MD5 aaf543351c9fcf5492d9550bb2aa9619
BLAKE2b-256 d05b65c61dff9ad64e1d2f8601d17feff0c8e16b5927bd0581a5cda5e0772fd4

See more details on using hashes here.

File details

Details for the file symbsyntdec-1.0.9-py3-none-any.whl.

File metadata

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

File hashes

Hashes for symbsyntdec-1.0.9-py3-none-any.whl
Algorithm Hash digest
SHA256 23040dc0195cb02d03a844f2e602f065bd43dcf4e1bac20b1e78553aa107f494
MD5 5a613d44ce8a1ba3f525fbabc519dc20
BLAKE2b-256 c0bf31303ca08bf6ec982e929170015e1d5befd4062afb0275af288219a58651

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