LTLf2DFA

https://github.com/whitemech/ltlf2dfa
Admin
LTLf2DFA is a tool that transforms an LTLf or a PPLTL formula into a minimal Deterministic Finite...
Tokens:2,432
Snippets:42
Trust Score:8.5
Update:3 months ago
Show doc for...
Tokens:
Raw
### Install Development Dependencies with Poetry

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Set up the development environment by cloning the repository and installing dependencies using Poetry. This is for contributors to the project.

```bash
git clone https://github.com/whitemech/LTLf2DFA.git
cd LTLf2DFA
poetry shell && poetry install
```

--------------------------------

### Install ltlf2dfa from source

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Install the ltlf2dfa package directly from the GitHub repository using pip. This is useful for development or to get the latest changes.

```bash
pip install git+https://github.com/whitemech/LTLf2DFA.git
```

--------------------------------

### Install ltlf2dfa from cloned repository

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Clone the ltlf2dfa repository and install it locally. This method is suitable for development purposes.

```bash
git clone https://github.com/whitemech/LTLf2DFA.git
cd ltlf2dfa
pip install .
```

--------------------------------

### Install ltlf2dfa from PyPI

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Install the ltlf2dfa package using pip. This is the recommended method for most users.

```bash
pip install ltlf2dfa
```

--------------------------------

### Serve Documentation Locally with MkDocs

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Build and serve the project's documentation locally using MkDocs. This allows you to preview the documentation in a web browser at http://localhost:8000.

```bash
mkdocs serve
```

--------------------------------

### Build Documentation with MkDocs

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Build the project's documentation using MkDocs. The generated documentation will be placed in the 'site' directory.

```bash
mkdocs build
```

--------------------------------

### LTLf2DFA CLI Usage

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Command-line interface for LTLf2DFA. Specify the formula language (ltlf or ppltl) and the path to the formula file.

```bash
ltlf2dfa -l {ltlf | ppltl} -f <path/to/formula>
```

--------------------------------

### Run All Tests with Tox

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Execute all tests for the ltlf2dfa project using the tox testing tool. This ensures the project's integrity.

```bash
tox
```

--------------------------------

### Run Code Tests with Tox

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Run only the code-related tests for the ltlf2dfa project using tox, specifying the Python version.

```bash
tox -e py38
```

--------------------------------

### Run Code Style Checks with Tox

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Execute only the code style checks (flake8) for the ltlf2dfa project using tox.

```bash
tox -e flake8
```

--------------------------------

### LTLf Grammar

Source: https://github.com/whitemech/ltlf2dfa/blob/main/docs/grammars.md

This is the Lark grammar for parsing LTLf (Linear Temporal Logic over Finite Traces) expressions. It includes temporal operators like Next, Until, and Release.

```lark
True: "True"
False: "False"

// Basic operators
NOT: "~"
AND: "&"
OR: "|"
XOR: "^"
IMPLIES: "->"
EQUIV: "<->"

// Temporal operators
NEXT: "X"
UNTIL: "U"
RELEASE: "R"

// Parentheses
LPAR: "("
RPAR: ")"

// Variables
VAR: /[a-zA-Z_][a-zA-Z0-9_]*/

%import common.WS
%ignore WS

// Rules

start: expr

?expr: term (EQUIV term)?

?term: factor (IMPLIES factor)?

?factor: disjunction (XOR disjunction)?

?disjunction: conjunction (OR conjunction)*

?conjunction: temporal (AND temporal)*

?temporal:
    atom
    | "~" temporal
    | "X" temporal
    | "(" temporal "U" temporal ")"
    | "(" temporal "R" temporal ")"

?atom:
    "(" expr ")"
    | True
    | False
    | VAR

```

--------------------------------

### Translate Formula to DFA using Python Library

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Convert a parsed LTLf or PPLTL formula object into its corresponding Deterministic Finite Automaton (DFA). The DFA is output in DOT format.

```python
dfa = formula.to_dfa()
print(dfa)                          # prints the DFA in DOT format
```

--------------------------------

### Propositional Logic Grammar

Source: https://github.com/whitemech/ltlf2dfa/blob/main/docs/grammars.md

This is the Lark grammar for parsing Propositional Logic expressions. It defines the syntax for basic logical operators and propositions.

```lark
True: "True"
False: "False"

// Basic operators
NOT: "~"
AND: "&"
OR: "|"
XOR: "^"
IMPLIES: "->"
EQUIV: "<->"

// Parentheses
LPAR: "("
RPAR: ")"

// Variables
VAR: /[a-zA-Z_][a-zA-Z0-9_]*/

%import common.WS
%ignore WS

// Rules

start: expr

?expr: term (EQUIV term)?

?term: factor (IMPLIES factor)?

?factor: disjunction (XOR disjunction)?

?disjunction: conjunction (OR conjunction)*

?conjunction: atom (AND atom)*

?atom:
    "(" expr ")"
    | "~" atom
    | True
    | False
    | VAR

```

--------------------------------

### Parse PPLTL Formula using Python Library

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Use the PPLTLParser from the ltlf2dfa library to parse a PPLTL formula string into a PPLTLFormula object. The parsed formula can then be printed or further processed.

```python
from ltlf2dfa.parser.ppltl import PPLTLParser

parser = PPLTLParser()
formula_str = "H(a -> Y b)"
formula = parser(formula_str)       # returns a PPLTLFormula

print(formula)                      # prints "H(a -> Y (b))"
```

--------------------------------

### Parse LTLf Formula using Python Library

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

Use the LTLfParser from the ltlf2dfa library to parse an LTLf formula string into an LTLfFormula object. The parsed formula can then be printed or further processed.

```python
from ltlf2dfa.parser.ltlf import LTLfParser

parser = LTLfParser()
formula_str = "G(a -> X b)"
formula = parser(formula_str)       # returns an LTLfFormula

print(formula)                      # prints "G(a -> X (b))"
```

--------------------------------

### BibTeX Citation for LTLf2DFA

Source: https://github.com/whitemech/ltlf2dfa/blob/main/README.md

BibTeX entry for citing the LTLf2DFA tool in academic research. Includes author, title, publisher, version, DOI, and URLs.

```bibtex
@software{fuggitti-ltlf2dfa,
  author       = {Francesco Fuggitti},
  title        = {LTLf2DFA},
  month        = {March},
  year         = {2019},
  publisher    = {Zenodo},
  version      = {1.0.3},
  doi          = {10.5281/zenodo.3888410},
  url_code    = {https://github.com/whitemech/LTLf2DFA},
  url_website = {http://ltlf2dfa.diag.uniroma1.it},
}
```
Tokens:
Raw