Temporal Logic Parser

The Temporal Logic Parser or tlparser takes something like this as input:

G((y and u == 9) --> F(not y or i < 3))

And returns some statistics about it:

json { "agg": { "aps": 3, "cops": 2, "lops": 4, "tops": 2 }, "ap": [ "i_lt_3", "u_eq_9", "y" ], "asth": 5, "cops": { "eq": 1, "geq": 0, "gt": 0, "leq": 0, "lt": 1, "neq": 0 }, "entropy": { "lops": 1, "lops_tops": 2.585, "tops": 2 }, "lops": { "and": 1, "impl": 1, "not": 1, "or": 1 }, "tops": { "A": 0, "E": 0, "F": 1, "G": 1, "R": 0, "U": 0, "X": 0 } }

How to use

First, git clone this repository and cd into the folder. Listing the contents of this directory (e.g., using ls -la on Unix or dir /a on Windows) should return the following items:

bash . ├── .git (folder) ├── .github (folder) ├── .gitignore ├── .vscode (folder) ├── LICENSE ├── README.md ├── data (folder) ├── pyproject.toml ├── pytest.ini ├── tests (folder) └── tlparser (folder)

[!NOTE]
This tool requires Python 3.10 or later. Ensure you have the correct version installed.

Next, create a new virtual environment using the following commands:

bash python3 -m venv venv && source venv/bin/activate

Install and test the dependencies:

bash pip3 install --upgrade pip && pip3 install -e '.[test]' && python3 -m pytest

Now you are ready to start the tlparser. Test it by printing the help message.

bash tlparser --help

You can parse the spacewire requirements using the following command:

bash tlparser digest ./data/spacewire.json

The resulting Excel file serves as basis for generating the plots. It contains the following columns:

| Column | Meaning | |------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------| | id | Unique requirement identifier | | text | Requirement in human language | | type | Temporal logic (supported are INV, LTL, MTLb, MITL, TPTL, CTLS, STL) | | reasoning | Thought decisive for formalizing the requirement in this logic | | translation | Specified whether the requirement can theoretically be formalized in (translated to) another logic (possible values are self, yes, no, unknown) | | translation class | Category name derived by concatenating first letters of all translation cases per requirement | | stats.formularaw | Formalization with comparison operators (e.g. G((x <= 7) --> (not (y)))) | | stats.formulaparsable | Formalization without comparison operators (e.g. G((x_leq_7) --> (not (y)))) | | stats.formulaparsed | Interpreted formalization using pyModelChecking (e.g. `G((xleq_7 --> not y))) | | stats.asth | Height (or *depth* or *nesting*) of the abstract syntax tree | | stats.ap | Set of all atomic propositions | | stats.cops.eq | Number of==(equals) comparisons | | stats.cops.ge | Number of>=(greater-or-equal-than) comparisons | | stats.cops.gt | Number of>(greater-than) comparisons | | stats.cops.leq | Number of<=less-or-equal-than comparisons | | stats.cops.lt | Number of<(less-than) comparisons | | stats.cops.ne | Number of!=(not-equals) comparisons | | stats.lops.and | Number of∧(and) operators | | stats.lops.imp | Number of-->(implies) operators | | stats.lops.not | Number of¬(not) operators | | stats.lops.or | Number of∨(or) operators | | stats.tops.A | Number offor all pathsoperators | | stats.tops.E | Number ofthere exists a pathoperators | | stats.tops.F | Number ofeventually(diamond symbol) operators | | stats.tops.G | Number ofglobally(square symbol) operators | | stats.tops.R | Number ofreleaseoperators | | stats.tops.U | Number ofuntiloperators | | stats.tops.X | Number ofnextoperators | | stats.agg.aps | Total number of atomic propositions | | stats.agg.cops | Total number of comparison operators (==,!=,<,>,=>,<=) | | stats.agg.lops | Total number of logical operators (∧,∨,-->,¬) | | stats.agg.tops | Total number of temporal operators (A,E,F,G,R,U,X`) |

To generate all plots of the latest Excel file execute the following command:

bash tlparser visualize -l -p all

All plots are saved to ./tlparser/workingdir/.

To clean-up all generated files again, execute the following command and confirm with y:

bash tlparser cleanup

Exit the virtual environment again using this command:

bash deactivate

To activate it again, simply execute this command in the root folder of the repository:

bash source venv/bin/activate