Repository: whitemech/LTLf2DFA (language: python)

Issue:
Prepare Release



Discussion / hints:

Fix patch:
diff --git a/.github/ISSUE_TEMPLATE/bug-report.md b/.github/ISSUE_TEMPLATE/bug-report.md
new file mode 100644
index 0000000..a62acc2
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/bug-report.md
@@ -0,0 +1,18 @@
+### Subject of the issue
+Describe your issue here.
+
+### Your environment
+- OS: [e.g. iOS]
+- Python version: [e.g. 3.7.2]
+- Package Version [e.g. 0.1.2]
+- Anything else you consider helpful.
+
+### Steps to reproduce
+Tell us how to reproduce this issue.
+
+### Expected behaviour
+Tell us what should happen
+
+### Actual behaviour
+Tell us what happens instead
+
diff --git a/.github/ISSUE_TEMPLATE/feature-request.md b/.github/ISSUE_TEMPLATE/feature-request.md
new file mode 100644
index 0000000..bbcbbe7
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/feature-request.md
@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
new file mode 100644
index 0000000..da01625
--- /dev/null
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -0,0 +1,30 @@
+## Proposed changes
+
+Describe the big picture of your changes here to communicate to the maintainers why we should accept this pull request.
+
+## Fixes
+
+If it fixes a bug or resolves a feature request, be sure to link to that issue.
+
+## Types of changes
+
+What types of changes does your code introduce to agents-tac?
+_Put an `x` in the boxes that apply_
+
+- [ ] Bugfix (non-breaking change which fixes an issue)
+- [ ] New feature (non-breaking change which adds functionality)
+- [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
+
+## Checklist
+
+_Put an `x` in the boxes that apply._
+
+- [ ] I have read the [CONTRIBUTING](../master/CONTRIBUTING.rst) doc
+- [ ] I am making a pull request against the `develop` branch (left side). Also you should start your branch off our `develop`.
+- [ ] Lint and unit tests pass locally with my changes
+- [ ] I have added tests that prove my fix is effective or that my feature works
+
+## Further comments
+
+If this is a relatively large or complex change, kick off the discussion by explaining why you chose the solution you did and what alternatives you considered, etc...
+
diff --git a/.github/RELEASE_PR.md b/.github/RELEASE_PR.md
new file mode 100644
index 0000000..c58c535
--- /dev/null
+++ b/.github/RELEASE_PR.md
@@ -0,0 +1,29 @@
+## Release summary
+
+Version number: [e.g. 1.0.1]
+
+## Release details
+
+Describe in short the main changes with the new release.
+
+## Checklist
+
+_Put an `x` in the boxes that apply._
+
+- [ ] I have read the [CONTRIBUTING](../master/CONTRIBUTING.rst) doc
+- [ ] I am making a pull request against the `master` branch (left side), from `develop`
+- [ ] I've updated the dependencies versions in `Pipfile` to the latest, wherever is possible.
+- [ ] Lint and unit tests pass locally
+- [ ] I built the documentation and updated it with the latest changes
+- [ ] I've added an item in `HISTORY.md` for this release
+- [ ] I bumped the version number in the `__version__.py` file.
+- [ ] I published the latest version on TestPyPI and checked that the following command work:
+       ```pip install ltlf2dfa==<version-number> --index-url https://testpypi.org/simple --force --no-cache-dir --no-deps```
+- [ ] After merging the PR, I'll publish the build also on PyPI. Then, I'll make sure the following
+      command will work:
+      ```pip install ltlf2dfa==<version_number> --force --no-cache-dir --no-deps```  
+
+
+## Further comments
+
+Write here any other comment about the release, if any.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
new file mode 100644
index 0000000..cabaa53
--- /dev/null
+++ b/.github/workflows/docs.yml
@@ -0,0 +1,29 @@
+name: docs
+
+on:
+  push:
+    branches:
+      - develop
+      - master
+  pull_request:
+
+jobs:
+  run:
+    runs-on: ${{ matrix.os }}
+
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        python-version: [3.7]
+
+    timeout-minutes: 30
+
+    steps:
+    - uses: actions/checkout@master
+    - uses: actions/setup-python@master
+      with:
+        python-version: ${{ matrix.python-version }}
+    - name: Install dependencies
+      run:  pip install tox
+    - name: Generate Documentation
+      run: tox -e docs
\ No newline at end of file
diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml
new file mode 100644
index 0000000..35cc831
--- /dev/null
+++ b/.github/workflows/lint.yml
@@ -0,0 +1,41 @@
+name: lint
+
+on:
+  push:
+    branches:
+      - develop
+      - master
+  pull_request:
+
+jobs:
+  run:
+    runs-on: ${{ matrix.os }}
+
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        python-version: [3.7]
+
+    timeout-minutes: 30
+
+    steps:
+    - uses: actions/checkout@master
+    - uses: actions/setup-python@master
+      with:
+        python-version: ${{ matrix.python-version }}
+    - name: Install dependencies
+      run:  pip install tox
+    - name: Code style check
+      run: |
+        tox -e black-check
+        tox -e isort-check
+        tox -e flake8
+        tox -e vulture
+    - name: Static type check
+      run: tox -e mypy
+    - name: Check copyright
+      run: tox -e check-copyright
+    - name: Misc checks
+      run: |
+        tox -e bandit
+        tox -e safety
\ No newline at end of file
diff --git a/HISTORY.md b/HISTORY.md
index c0bb682..3a523d3 100644
--- a/HISTORY.md
+++ b/HISTORY.md
@@ -1,5 +1,11 @@
 # History
 
+## 1.0.1 (2020-07-03)
+* Introduce optional argument to `to_dfa()` method for DFA in MONA output
+* Add parsing support for `LTLfLast()` and `PLTLfStart()` keywords
+* Some fixes
+* Increase code coverage
+
 ## 1.0.0.post0 (2020-06-05)
 
 * Include *.lark files in the package build
diff --git a/Pipfile b/Pipfile
index f12a101..c66276b 100644
--- a/Pipfile
+++ b/Pipfile
@@ -14,12 +14,17 @@ pydocstyle = "*"
 mypy = "*"
 tox = "*"
 coverage = "*"
-black = "==19.3b0"
 mkdocs = "*"
 markdown-include = "*"
+mkdocs-material = "*"
 pymdown-extensions = "*"
+ipython = "*"
+codecov = "*"
+tox-travis = "*"
+black = "==19.10b0"
+isort = "*"
+
+[packages]
 
 [requires]
 python_version = "3.7"
-
-[packages]
\ No newline at end of file
diff --git a/Pipfile.lock b/Pipfile.lock
index 3484f04..b114ccd 100644
--- a/Pipfile.lock
+++ b/Pipfile.lock
@@ -1,7 +1,7 @@
 {
     "_meta": {
         "hash": {
-            "sha256": "4a79c429b339f33a4837aca5cd5296136063b98d6b1e5d28680921cbce90adda"
+            "sha256": "eaeb3126f973c8e48b920701aaefb1953099887a90aa096c32042c60411ec35c"
         },
         "pipfile-spec": 6,
         "requires": {
@@ -24,20 +24,49 @@
             ],
             "version": "==1.4.4"
         },
+        "appnope": {
+            "hashes": [
+                "sha256:5b26757dc6f79a3b7dc9fab95359328d5747fcb2409d331ea66d0272b90ab2a0",
+                "sha256:8b995ffe925347a2138d7ac0fe77155e4311a0ea6d6da4f5128fe4b3cbe5ed71"
+            ],
+            "markers": "sys_platform == 'darwin'",
+            "version": "==0.1.0"
+        },
         "attrs": {
             "hashes": [
-                "sha256:31b2eced602aa8423c2aea9c76a724617ed67cf9513173fd3a4f03e3a929c7e6",
-                "sha256:832aa3cde19744e49938b91fea06d69ecb9e649c93ba974535d08ad92164f700"
+                "sha256:0ef97238856430dcf9228e07f316aefc17e8939fc8507e18c6501b761ef1a42a",
+                "sha256:2867b7b9f8326499ab5b0e2d12801fa5c98842d2cbd22b35112ae04bf85b4dff"
+            ],
+            "version": "==20.1.0"
+        },
+        "backcall": {
+            "hashes": [
+                "sha256:5cbdbf27be5e7cfadb448baf0aa95508f91f2bbc6c6437cd9cd06e2a4c215e1e",
+                "sha256:fbbce6a29f263178a1f7915c1940bde0ec2b2a967566fe1c65c1dfb7422bd255"
             ],
-            "version": "==20.3.0"
+            "version": "==0.2.0"
         },
         "black": {
             "hashes": [
-                "sha256:09a9dcb7c46ed496a9850b76e4e825d6049ecd38b611f1224857a79bd985a8cf",
-                "sha256:68950ffd4d9169716bcb8719a56c07a2f4485354fec061cdd5910aa07369731c"
+                "sha256:1b30e59be925fafc1ee4565e5e08abef6b03fe455102883820fe5ee2e4734e0b",
+                "sha256:c2edb73a08e9e0e6f65a0e6af18b059b8b1cdd5bef997d7a0b181df93dc81539"
             ],
             "index": "pypi",
-            "version": "==19.3b0"
+            "version": "==19.10b0"
+        },
+        "certifi": {
+            "hashes": [
+                "sha256:5930595817496dd21bb8dc35dad090f1c2cd0adfaf21204bf6732ca5d8ee34d3",
+                "sha256:8fc0819f1f30ba15bdb34cceffb9ef04d99f420f68eb75d901e9560b8749fc41"
+            ],
+            "version": "==2020.6.20"
+        },
+        "chardet": {
+            "hashes": [
+                "sha256:84ab92ed1c4d4f16916e05906b6b75a6c0fb5db821cc65e70cbd64a3e2a5eaae",
+                "sha256:fc323ffcaeaed0e0a02bf4d117757b98aed530d9ed4531e3e15460124c106691"
+            ],
+            "version": "==3.0.4"
         },
         "click": {
             "hashes": [
@@ -46,42 +75,60 @@
             ],
             "version": "==7.1.2"
         },
+        "codecov": {
+            "hashes": [
+                "sha256:24545847177a893716b3455ac5bfbafe0465f38d4eb86ea922c09adc7f327e65",
+                "sha256:355fc7e0c0b8a133045f0d6089bde351c845e7b52b99fec5903b4ea3ab5f6aab"
+            ],
+            "index": "pypi",
+            "version": "==2.1.9"
+        },
         "coverage": {
             "hashes": [
-                "sha256:00f1d23f4336efc3b311ed0d807feb45098fc86dee1ca13b3d6768cdab187c8a",
-                "sha256:01333e1bd22c59713ba8a79f088b3955946e293114479bbfc2e37d522be03355",
-                "sha256:0cb4be7e784dcdc050fc58ef05b71aa8e89b7e6636b99967fadbdba694cf2b65",
-                "sha256:0e61d9803d5851849c24f78227939c701ced6704f337cad0a91e0972c51c1ee7",
-                "sha256:1601e480b9b99697a570cea7ef749e88123c04b92d84cedaa01e117436b4a0a9",
-                "sha256:2742c7515b9eb368718cd091bad1a1b44135cc72468c731302b3d641895b83d1",
-                "sha256:2d27a3f742c98e5c6b461ee6ef7287400a1956c11421eb574d843d9ec1f772f0",
-                "sha256:402e1744733df483b93abbf209283898e9f0d67470707e3c7516d84f48524f55",
-                "sha256:5c542d1e62eece33c306d66fe0a5c4f7f7b3c08fecc46ead86d7916684b36d6c",
-                "sha256:5f2294dbf7875b991c381e3d5af2bcc3494d836affa52b809c91697449d0eda6",
-                "sha256:6402bd2fdedabbdb63a316308142597534ea8e1895f4e7d8bf7476c5e8751fef",
-                "sha256:66460ab1599d3cf894bb6baee8c684788819b71a5dc1e8fa2ecc152e5d752019",
-                "sha256:782caea581a6e9ff75eccda79287daefd1d2631cc09d642b6ee2d6da21fc0a4e",
-                "sha256:79a3cfd6346ce6c13145731d39db47b7a7b859c0272f02cdb89a3bdcbae233a0",
-                "sha256:7a5bdad4edec57b5fb8dae7d3ee58622d626fd3a0be0dfceda162a7035885ecf",
-                "sha256:8fa0cbc7ecad630e5b0f4f35b0f6ad419246b02bc750de7ac66db92667996d24",
-                "sha256:a027ef0492ede1e03a8054e3c37b8def89a1e3c471482e9f046906ba4f2aafd2",
-                "sha256:a3f3654d5734a3ece152636aad89f58afc9213c6520062db3978239db122f03c",
-                "sha256:a82b92b04a23d3c8a581fc049228bafde988abacba397d57ce95fe95e0338ab4",
-                "sha256:acf3763ed01af8410fc36afea23707d4ea58ba7e86a8ee915dfb9ceff9ef69d0",
-                "sha256:adeb4c5b608574a3d647011af36f7586811a2c1197c861aedb548dd2453b41cd",
-                "sha256:b83835506dfc185a319031cf853fa4bb1b3974b1f913f5bb1a0f3d98bdcded04",
-                "sha256:bb28a7245de68bf29f6fb199545d072d1036a1917dca17a1e75bbb919e14ee8e",
-                "sha256:bf9cb9a9fd8891e7efd2d44deb24b86d647394b9705b744ff6f8261e6f29a730",
-                "sha256:c317eaf5ff46a34305b202e73404f55f7389ef834b8dbf4da09b9b9b37f76dd2",
-                "sha256:dbe8c6ae7534b5b024296464f387d57c13caa942f6d8e6e0346f27e509f0f768",
-                "sha256:de807ae933cfb7f0c7d9d981a053772452217df2bf38e7e6267c9cbf9545a796",
-                "sha256:dead2ddede4c7ba6cb3a721870f5141c97dc7d85a079edb4bd8d88c3ad5b20c7",
-                "sha256:dec5202bfe6f672d4511086e125db035a52b00f1648d6407cc8e526912c0353a",
-                "sha256:e1ea316102ea1e1770724db01998d1603ed921c54a86a2efcb03428d5417e489",
-                "sha256:f90bfc4ad18450c80b024036eaf91e4a246ae287701aaa88eaebebf150868052"
+                "sha256:098a703d913be6fbd146a8c50cc76513d726b022d170e5e98dc56d958fd592fb",
+                "sha256:16042dc7f8e632e0dcd5206a5095ebd18cb1d005f4c89694f7f8aafd96dd43a3",
+                "sha256:1adb6be0dcef0cf9434619d3b892772fdb48e793300f9d762e480e043bd8e716",
+                "sha256:27ca5a2bc04d68f0776f2cdcb8bbd508bbe430a7bf9c02315cd05fb1d86d0034",
+                "sha256:28f42dc5172ebdc32622a2c3f7ead1b836cdbf253569ae5673f499e35db0bac3",
+                "sha256:2fcc8b58953d74d199a1a4d633df8146f0ac36c4e720b4a1997e9b6327af43a8",
+                "sha256:304fbe451698373dc6653772c72c5d5e883a4aadaf20343592a7abb2e643dae0",
+                "sha256:30bc103587e0d3df9e52cd9da1dd915265a22fad0b72afe54daf840c984b564f",
+                "sha256:40f70f81be4d34f8d491e55936904db5c527b0711b2a46513641a5729783c2e4",
+                "sha256:4186fc95c9febeab5681bc3248553d5ec8c2999b8424d4fc3a39c9cba5796962",
+                "sha256:46794c815e56f1431c66d81943fa90721bb858375fb36e5903697d5eef88627d",
+                "sha256:4869ab1c1ed33953bb2433ce7b894a28d724b7aa76c19b11e2878034a4e4680b",
+                "sha256:4f6428b55d2916a69f8d6453e48a505c07b2245653b0aa9f0dee38785939f5e4",
+                "sha256:52f185ffd3291196dc1aae506b42e178a592b0b60a8610b108e6ad892cfc1bb3",
+                "sha256:538f2fd5eb64366f37c97fdb3077d665fa946d2b6d95447622292f38407f9258",
+                "sha256:64c4f340338c68c463f1b56e3f2f0423f7b17ba6c3febae80b81f0e093077f59",
+                "sha256:675192fca634f0df69af3493a48224f211f8db4e84452b08d5fcebb9167adb01",
+                "sha256:700997b77cfab016533b3e7dbc03b71d33ee4df1d79f2463a318ca0263fc29dd",
+                "sha256:8505e614c983834239f865da2dd336dcf9d72776b951d5dfa5ac36b987726e1b",
+                "sha256:962c44070c281d86398aeb8f64e1bf37816a4dfc6f4c0f114756b14fc575621d",
+                "sha256:9e536783a5acee79a9b308be97d3952b662748c4037b6a24cbb339dc7ed8eb89",
+                "sha256:9ea749fd447ce7fb1ac71f7616371f04054d969d412d37611716721931e36efd",
+                "sha256:a34cb28e0747ea15e82d13e14de606747e9e484fb28d63c999483f5d5188e89b",
+                "sha256:a3ee9c793ffefe2944d3a2bd928a0e436cd0ac2d9e3723152d6fd5398838ce7d",
+                "sha256:aab75d99f3f2874733946a7648ce87a50019eb90baef931698f96b76b6769a46",
+                "sha256:b1ed2bdb27b4c9fc87058a1cb751c4df8752002143ed393899edb82b131e0546",
+                "sha256:b360d8fd88d2bad01cb953d81fd2edd4be539df7bfec41e8753fe9f4456a5082",
+                "sha256:b8f58c7db64d8f27078cbf2a4391af6aa4e4767cc08b37555c4ae064b8558d9b",
+                "sha256:c1bbb628ed5192124889b51204de27c575b3ffc05a5a91307e7640eff1d48da4",
+                "sha256:c2ff24df02a125b7b346c4c9078c8936da06964cc2d276292c357d64378158f8",
+                "sha256:c890728a93fffd0407d7d37c1e6083ff3f9f211c83b4316fae3778417eab9811",
+                "sha256:c96472b8ca5dc135fb0aa62f79b033f02aa434fb03a8b190600a5ae4102df1fd",
+                "sha256:ce7866f29d3025b5b34c2e944e66ebef0d92e4a4f2463f7266daa03a1332a651",
+                "sha256:e26c993bd4b220429d4ec8c1468eca445a4064a61c74ca08da7429af9bc53bb0"
             ],
             "index": "pypi",
-            "version": "==5.1"
+            "version": "==5.2.1"
+        },
+        "decorator": {
+            "hashes": [
+                "sha256:41fa54c2a0cc4ba648be4fd43cff00aedf5b9465c9bf18d64325bc225f08f760",
+                "sha256:e3a62f0520172440ca0dcc823749319382e377f37f140a0b99ef45fecb84bfe7"
+            ],
+            "version": "==4.4.2"
         },
         "distlib": {
             "hashes": [
@@ -99,11 +146,11 @@
         },
         "flake8": {
             "hashes": [
-                "sha256:6c1193b0c3f853ef763969238f6c81e9e63ace9d024518edc020d5f1d6d93195",
-                "sha256:ea6623797bf9a52f4c9577d780da0bb17d65f870213f7b5bcc9fca82540c31d5"
+                "sha256:15e351d19611c887e482fb960eae4d44845013cc142d42896e9862f775d8cf5c",
+                "sha256:f04b9fcbac03b0a3e58c0ab3a0ecc462e023a9faf046d57794184028123aa208"
             ],
             "index": "pypi",
-            "version": "==3.8.1"
+            "version": "==3.8.3"
         },
         "flake8-bugbear": {
             "hashes": [
@@ -127,6 +174,13 @@
             ],
             "version": "==0.18.2"
         },
+        "idna": {
+            "hashes": [
+                "sha256:b307872f855b18632ce0c21c5e45be78c0ea7ae4c15c828c20788b26921eb3f6",
+                "sha256:b97d804b1e9b523befed77c48dacec60e6dcb0b5391d57af6a65a312a90648c0"
+            ],
+            "version": "==2.10"
+        },
         "importlib-metadata": {
             "hashes": [
                 "sha256:90bb658cdbbf6d1735b6341ce708fc7024a3e14e99ffdc5783edea9f9b077f83",
@@ -135,6 +189,43 @@
             "markers": "python_version < '3.8'",
             "version": "==1.7.0"
         },
+        "iniconfig": {
+            "hashes": [
+                "sha256:80cf40c597eb564e86346103f609d74efce0f6b4d4f30ec8ce9e2c26411ba437",
+                "sha256:e5f92f89355a67de0595932a6c6c02ab4afddc6fcdc0bfc5becd0d60884d3f69"
+            ],
+            "version": "==1.0.1"
+        },
+        "ipython": {
+            "hashes": [
+                "sha256:2e22c1f74477b5106a6fb301c342ab8c64bb75d702e350f05a649e8cb40a0fb8",
+                "sha256:a331e78086001931de9424940699691ad49dfb457cea31f5471eae7b78222d5e"
+            ],
+            "index": "pypi",
+            "version": "==7.18.1"
+        },
+        "ipython-genutils": {
+            "hashes": [
+                "sha256:72dd37233799e619666c9f639a9da83c34013a73e8bbc79a7a6348d93c61fab8",
+                "sha256:eb2e116e75ecef9d4d228fdc66af54269afa26ab4463042e33785b887c628ba8"
+            ],
+            "version": "==0.2.0"
+        },
+        "isort": {
+            "hashes": [
+                "sha256:60a1b97e33f61243d12647aaaa3e6cc6778f5eb9f42997650f1cc975b6008750",
+                "sha256:d488ba1c5a2db721669cc180180d5acf84ebdc5af7827f7aaeaa75f73cf0e2b8"
+            ],
+            "index": "pypi",
+            "version": "==5.4.2"
+        },
+        "jedi": {
+            "hashes": [
+                "sha256:86ed7d9b750603e4ba582ea8edc678657fb4007894a12bcf6f4bb97892f31d20",
+                "sha256:98cc583fa0f2f8304968199b01b6b4b94f469a1f4a74c1560506ca2a211378b5"
+            ],
+            "version": "==0.17.2"
+        },
         "jinja2": {
             "hashes": [
                 "sha256:03e47ad063331dd6a3f04a43eddca8a966a26ba0c5b7207a9a9e4e08f1b29419",
@@ -144,10 +235,10 @@
         },
         "joblib": {
             "hashes": [
-                "sha256:9c17567692206d2f3fb9ecf5e991084254fe631665c450b443761c4186a613f7",
-                "sha256:feeb1ec69c4d45129954f1b7034954241eedfd6ba39b5e9e4b6883be3332d5e5"
+                "sha256:8f52bf24c64b608bf0b2563e0e47d6fcf516abc8cfafe10cfd98ad66d94f92d6",
+                "sha256:d348c5d4ae31496b2aa060d6d9b787864dd204f9480baaa52d18850cb43e9f49"
             ],
-            "version": "==1.0.1"
+            "version": "==0.16.0"
         },
         "livereload": {
             "hashes": [
@@ -174,10 +265,10 @@
         },
         "markdown-include": {
             "hashes": [
-                "sha256:72a45461b589489a088753893bc95c5fa5909936186485f4ed55caa57d10250f"
+                "sha256:6f5d680e36f7780c7f0f61dca53ca581bd50d1b56137ddcd6353efafa0c3e4a2"
             ],
             "index": "pypi",
-            "version": "==0.5.1"
+            "version": "==0.6.0"
         },
         "markupsafe": {
             "hashes": [
@@ -251,32 +342,47 @@
             "index": "pypi",
             "version": "==1.1.2"
         },
+        "mkdocs-material": {
+            "hashes": [
+                "sha256:9b2225af305668f422a01d4b41ddb7ebb938b1c43a0dde7aae3b00475e6c9ae3",
+                "sha256:d956fba4b3e27b40490aa457678083e0c26fe4ea1b307d8322c3df3412a0b485"
+            ],
+            "index": "pypi",
+            "version": "==5.5.12"
+        },
+        "mkdocs-material-extensions": {
+            "hashes": [
+                "sha256:09569c3694b5acc1e8334c9730e52b4bcde65fc9d613cc20e49af131ef1a9ca0",
+                "sha256:17d7491e189af75700310b7ec33c6c48a22060b8b445001deca040cb60471cde"
+            ],
+            "version": "==1.0"
+        },
         "more-itertools": {
             "hashes": [
-                "sha256:5652a9ac72209ed7df8d9c15daf4e1aa0e3d2ccd3c87f8265a0673cd9cbc9ced",
-                "sha256:c5d6da9ca3ff65220c3bfd2a8db06d698f05d4d2b9be57e1deb2be5a45019713"
+                "sha256:6f83822ae94818eae2612063a5101a7311e68ae8002005b5e05f03fd74a86a20",
+                "sha256:9b30f12df9393f0d28af9210ff8efe48d10c94f73e5daf886f10c4b0b0b4f03c"
             ],
-            "version": "==8.7.0"
+            "version": "==8.5.0"
         },
         "mypy": {
             "hashes": [
-                "sha256:15b948e1302682e3682f11f50208b726a246ab4e6c1b39f9264a8796bb416aa2",
-                "sha256:219a3116ecd015f8dca7b5d2c366c973509dfb9a8fc97ef044a36e3da66144a1",
-                "sha256:3b1fc683fb204c6b4403a1ef23f0b1fac8e4477091585e0c8c54cbdf7d7bb164",
-                "sha256:3beff56b453b6ef94ecb2996bea101a08f1f8a9771d3cbf4988a61e4d9973761",
-                "sha256:7687f6455ec3ed7649d1ae574136835a4272b65b3ddcf01ab8704ac65616c5ce",
-                "sha256:7ec45a70d40ede1ec7ad7f95b3c94c9cf4c186a32f6bacb1795b60abd2f9ef27",
-                "sha256:86c857510a9b7c3104cf4cde1568f4921762c8f9842e987bc03ed4f160925754",
-                "sha256:8a627507ef9b307b46a1fea9513d5c98680ba09591253082b4c48697ba05a4ae",
-                "sha256:8dfb69fbf9f3aeed18afffb15e319ca7f8da9642336348ddd6cab2713ddcf8f9",
-                "sha256:a34b577cdf6313bf24755f7a0e3f3c326d5c1f4fe7422d1d06498eb25ad0c600",
-                "sha256:a8ffcd53cb5dfc131850851cc09f1c44689c2812d0beb954d8138d4f5fc17f65",
-                "sha256:b90928f2d9eb2f33162405f32dde9f6dcead63a0971ca8a1b50eb4ca3e35ceb8",
-                "sha256:c56ffe22faa2e51054c5f7a3bc70a370939c2ed4de308c690e7949230c995913",
-                "sha256:f91c7ae919bbc3f96cd5e5b2e786b2b108343d1d7972ea130f7de27fdd547cf3"
+                "sha256:2c6cde8aa3426c1682d35190b59b71f661237d74b053822ea3d748e2c9578a7c",
+                "sha256:3fdda71c067d3ddfb21da4b80e2686b71e9e5c72cca65fa216d207a358827f86",
+                "sha256:5dd13ff1f2a97f94540fd37a49e5d255950ebcdf446fb597463a40d0df3fac8b",
+                "sha256:6731603dfe0ce4352c555c6284c6db0dc935b685e9ce2e4cf220abe1e14386fd",
+                "sha256:6bb93479caa6619d21d6e7160c552c1193f6952f0668cdda2f851156e85186fc",
+                "sha256:81c7908b94239c4010e16642c9102bfc958ab14e36048fa77d0be3289dda76ea",
+                "sha256:9c7a9a7ceb2871ba4bac1cf7217a7dd9ccd44c27c2950edbc6dc08530f32ad4e",
+                "sha256:a4a2cbcfc4cbf45cd126f531dedda8485671545b43107ded25ce952aac6fb308",
+                "sha256:b7fbfabdbcc78c4f6fc4712544b9b0d6bf171069c6e0e3cb82440dd10ced3406",
+                "sha256:c05b9e4fb1d8a41d41dec8786c94f3b95d3c5f528298d769eb8e73d293abc48d",
+                "sha256:d7df6eddb6054d21ca4d3c6249cae5578cb4602951fd2b6ee2f5510ffb098707",
+                "sha256:e0b61738ab504e656d1fe4ff0c0601387a5489ca122d55390ade31f9ca0e252d",
+                "sha256:eff7d4a85e9eea55afa34888dfeaccde99e7520b51f867ac28a48492c0b1130c",
+                "sha256:f05644db6779387ccdb468cc47a44b4356fc2ffa9287135d05b70a98dc83b89a"
             ],
             "index": "pypi",
-            "version": "==0.770"
+            "version": "==0.782"
         },
         "mypy-extensions": {
             "hashes": [
@@ -299,6 +405,35 @@
             ],
             "version": "==20.9"
         },
+        "parso": {
+            "hashes": [
+                "sha256:97218d9159b2520ff45eb78028ba8b50d2bc61dcc062a9682666f2dc4bd331ea",
+                "sha256:caba44724b994a8a5e086460bb212abc5a8bc46951bf4a9a1210745953622eb9"
+            ],
+            "version": "==0.7.1"
+        },
+        "pathspec": {
+            "hashes": [
+                "sha256:7d91249d21749788d07a2d0f94147accd8f845507400749ea19c1ec9054a12b0",
+                "sha256:da45173eb3a6f2a5a487efba21f050af2b41948be6ab52b6a1e3ff22bb8b7061"
+            ],
+            "version": "==0.8.0"
+        },
+        "pexpect": {
+            "hashes": [
+                "sha256:0b48a55dcb3c05f3329815901ea4fc1537514d6ba867a152b581d69ae3710937",
+                "sha256:fc65a43959d153d0114afe13997d439c22823a27cefceb5ff35c2178c6784c0c"
+            ],
+            "markers": "sys_platform != 'win32'",
+            "version": "==4.8.0"
+        },
+        "pickleshare": {
+            "hashes": [
+                "sha256:87683d47965c1da65cdacaf31c8441d12b8044cdec9aca500cd78fc2c683afca",
+                "sha256:9649af414d74d4df115d5d718f82acb59c9d418196b7b4290ed47a12ce62df56"
+            ],
+            "version": "==0.7.5"
+        },
         "pluggy": {
             "hashes": [
                 "sha256:15b2acde666561e1298d71b523007ed7364de07029219b604cf808bfa1c765b0",
@@ -306,12 +441,26 @@
             ],
             "version": "==0.13.1"
         },
+        "prompt-toolkit": {
+            "hashes": [
+                "sha256:822f4605f28f7d2ba6b0b09a31e25e140871e96364d1d377667b547bb3bf4489",
+                "sha256:83074ee28ad4ba6af190593d4d4c607ff525272a504eb159199b6dd9f950c950"
+            ],
+            "version": "==3.0.7"
+        },
+        "ptyprocess": {
+            "hashes": [
+                "sha256:923f299cc5ad920c68f2bc0bc98b75b9f838b93b599941a6b63ddbc2476394c0",
+                "sha256:d7cc528d76e76342423ca640335bd3633420dc1366f258cb31d05e865ef5ca1f"
+            ],
+            "version": "==0.6.0"
+        },
         "py": {
             "hashes": [
-                "sha256:21b81bda15b66ef5e1a777a21c4dcd9c20ad3efd0b3f817e7a809035269e1bd3",
-                "sha256:3b80836aa6d1feeaa108e046da6423ab8f6ceda6468545ae8d02d9d58d18818a"
+                "sha256:366389d1db726cd2fcfc79732e75410e5fe4d31db13692115529d34069a043c2",
+                "sha256:9ca6883ce56b4e8da7e79ac18787889fa5206c79dcc67fb065376cd2fe03f342"
             ],
-            "index": "pypi",
+            "version": "==1.9.0"
         },
         "pycodestyle": {
             "hashes": [
@@ -322,11 +471,11 @@
         },
         "pydocstyle": {
             "hashes": [
-                "sha256:da7831660b7355307b32778c4a0dbfb137d89254ef31a2b2978f50fc0b4d7586",
-                "sha256:f4f5d210610c2d153fae39093d44224c17429e2ad7da12a8b419aba5c2f614b5"
+                "sha256:19b86fa8617ed916776a11cd8bc0197e5b9856d5433b777f51a3defe13075325",
+                "sha256:aca749e190a01726a4fb472dd4ef23b5c9da7b9205c0a7857c06533de13fd678"
             ],
             "index": "pypi",
-            "version": "==5.0.2"
+            "version": "==5.1.1"
         },
         "pyflakes": {
             "hashes": [
@@ -335,13 +484,20 @@
             ],
             "version": "==2.2.0"
         },
+        "pygments": {
+            "hashes": [
+                "sha256:647344a061c249a3b74e230c739f434d7ea4d8b1d5f3721bc0f3558049b38f44",
+                "sha256:ff7a40b4860b727ab48fad6360eb351cc1b33cbf9b15a0f689ca5353e9463324"
+            ],
+            "version": "==2.6.1"
+        },
         "pymdown-extensions": {
             "hashes": [
-                "sha256:5bf93d1ccd8281948cd7c559eb363e59b179b5373478e8a7195cf4b78e3c11b6",
-                "sha256:8f415b21ee86d80bb2c3676f4478b274d0a8ccb13af672a4c86b9ffd22bd005c"
+                "sha256:440b0db9823b89f9917482ce3ab3d32ac18e60f2e186770ac37836830d5e7256",
+                "sha256:c3b18b719adc3a441c4edbcf691157998dbd333384a8e2caf0690985a6e586f0"
             ],
             "index": "pypi",
-            "version": "==7.1"
+            "version": "==8.0"
         },
         "pyparsing": {
             "hashes": [
@@ -352,27 +508,27 @@
         },
         "pytest": {
             "hashes": [
-                "sha256:95c710d0a72d91c13fae35dce195633c929c3792f54125919847fdcdf7caa0d3",
-                "sha256:eb2b5e935f6a019317e455b6da83dd8650ac9ffd2ee73a7b657a30873d67a698"
+                "sha256:85228d75db9f45e06e57ef9bf4429267f81ac7c0d742cc9ed63d09886a9fe6f4",
+                "sha256:8b6007800c53fdacd5a5c192203f4e531eb2a1540ad9c752e052ec0f7143dbad"
             ],
             "index": "pypi",
-            "version": "==5.4.2"
+            "version": "==6.0.1"
         },
         "pytest-cov": {
             "hashes": [
-                "sha256:cc6742d8bac45070217169f5f72ceee1e0e55b0221f54bcf24845972d3a47f2b",
-                "sha256:cdbdef4f870408ebdbfeb44e63e07eb18bb4619fae852f6e760645fa36172626"
+                "sha256:45ec2d5182f89a81fc3eb29e3d1ed3113b9e9a873bcddb2a71faaab066110191",
+                "sha256:47bd0ce14056fdd79f93e1713f88fad7bdcc583dcd7783da86ef2f085a0bb88e"
             ],
             "index": "pypi",
-            "version": "==2.8.1"
+            "version": "==2.10.1"
         },
         "pytest-randomly": {
             "hashes": [
-                "sha256:568b6a3bd251b566e8d99fc7bcb15c3c39561babd07e16412563b7dab1b0290a",
-                "sha256:9b06429c877b3aab360c7cf698f2a65dbe75db1b1ed0ab02dc3bb47f3487e469"
+                "sha256:2c4df1390db72a33a4f44fac0c780e7883cd5968238efa2a2bdbdd54e3fc6681",
+                "sha256:5fd0dbeeb218a7ce029690a8100453cd8d6a7972cf9d8e657690352692e92c69"
             ],
             "index": "pypi",
-            "version": "==3.3.1"
+            "version": "==3.4.1"
         },
         "pyyaml": {
             "hashes": [
@@ -410,49 +566,36 @@
         },
         "regex": {
             "hashes": [
-                "sha256:01afaf2ec48e196ba91b37451aa353cb7eda77efe518e481707e0515025f0cd5",
-                "sha256:11d773d75fa650cd36f68d7ca936e3c7afaae41b863b8c387a22aaa78d3c5c79",
-                "sha256:18c071c3eb09c30a264879f0d310d37fe5d3a3111662438889ae2eb6fc570c31",
-                "sha256:1e1c20e29358165242928c2de1482fb2cf4ea54a6a6dea2bd7a0e0d8ee321500",
-                "sha256:281d2fd05555079448537fe108d79eb031b403dac622621c78944c235f3fcf11",
-                "sha256:314d66636c494ed9c148a42731b3834496cc9a2c4251b1661e40936814542b14",
-                "sha256:32e65442138b7b76dd8173ffa2cf67356b7bc1768851dded39a7a13bf9223da3",
-                "sha256:339456e7d8c06dd36a22e451d58ef72cef293112b559010db3d054d5560ef439",
-                "sha256:3916d08be28a1149fb97f7728fca1f7c15d309a9f9682d89d79db75d5e52091c",
-                "sha256:3a9cd17e6e5c7eb328517969e0cb0c3d31fd329298dd0c04af99ebf42e904f82",
-                "sha256:47bf5bf60cf04d72bf6055ae5927a0bd9016096bf3d742fa50d9bf9f45aa0711",
-                "sha256:4c46e22a0933dd783467cf32b3516299fb98cfebd895817d685130cc50cd1093",
-                "sha256:4c557a7b470908b1712fe27fb1ef20772b78079808c87d20a90d051660b1d69a",
-                "sha256:52ba3d3f9b942c49d7e4bc105bb28551c44065f139a65062ab7912bef10c9afb",
-                "sha256:563085e55b0d4fb8f746f6a335893bda5c2cef43b2f0258fe1020ab1dd874df8",
-                "sha256:598585c9f0af8374c28edd609eb291b5726d7cbce16be6a8b95aa074d252ee17",
-                "sha256:619d71c59a78b84d7f18891fe914446d07edd48dc8328c8e149cbe0929b4e000",
-                "sha256:67bdb9702427ceddc6ef3dc382455e90f785af4c13d495f9626861763ee13f9d",
-                "sha256:6d1b01031dedf2503631d0903cb563743f397ccaf6607a5e3b19a3d76fc10480",
-                "sha256:741a9647fcf2e45f3a1cf0e24f5e17febf3efe8d4ba1281dcc3aa0459ef424dc",
-                "sha256:7c2a1af393fcc09e898beba5dd59196edaa3116191cc7257f9224beaed3e1aa0",
-                "sha256:7d9884d86dd4dd489e981d94a65cd30d6f07203d90e98f6f657f05170f6324c9",
-                "sha256:90f11ff637fe8798933fb29f5ae1148c978cccb0452005bf4c69e13db951e765",
-                "sha256:919859aa909429fb5aa9cf8807f6045592c85ef56fdd30a9a3747e513db2536e",
-                "sha256:96fcd1888ab4d03adfc9303a7b3c0bd78c5412b2bfbe76db5b56d9eae004907a",
-                "sha256:97f29f57d5b84e73fbaf99ab3e26134e6687348e95ef6b48cfd2c06807005a07",
-                "sha256:980d7be47c84979d9136328d882f67ec5e50008681d94ecc8afa8a65ed1f4a6f",
-                "sha256:a91aa8619b23b79bcbeb37abe286f2f408d2f2d6f29a17237afda55bb54e7aac",
-                "sha256:ade17eb5d643b7fead300a1641e9f45401c98eee23763e9ed66a43f92f20b4a7",
-                "sha256:b9c3db21af35e3b3c05764461b262d6f05bbca08a71a7849fd79d47ba7bc33ed",
-                "sha256:bd28bc2e3a772acbb07787c6308e00d9626ff89e3bfcdebe87fa5afbfdedf968",
-                "sha256:bf5824bfac591ddb2c1f0a5f4ab72da28994548c708d2191e3b87dd207eb3ad7",
-                "sha256:c0502c0fadef0d23b128605d69b58edb2c681c25d44574fc673b0e52dce71ee2",
-                "sha256:c38c71df845e2aabb7fb0b920d11a1b5ac8526005e533a8920aea97efb8ec6a4",
-                "sha256:ce15b6d103daff8e9fee13cf7f0add05245a05d866e73926c358e871221eae87",
-                "sha256:d3029c340cfbb3ac0a71798100ccc13b97dddf373a4ae56b6a72cf70dfd53bc8",
-                "sha256:e512d8ef5ad7b898cdb2d8ee1cb09a8339e4f8be706d27eaa180c2f177248a10",
-                "sha256:e8e5b509d5c2ff12f8418006d5a90e9436766133b564db0abaec92fd27fcee29",
-                "sha256:ee54ff27bf0afaf4c3b3a62bcd016c12c3fdb4ec4f413391a90bd38bc3624605",
-                "sha256:fa4537fb4a98fe8fde99626e4681cc644bdcf2a795038533f9f711513a862ae6",
-                "sha256:fd45ff9293d9274c5008a2054ecef86a9bfe819a67c7be1afb65e69b405b3042"
-            ],
-            "version": "==2021.4.4"
+                "sha256:0dc64ee3f33cd7899f79a8d788abfbec168410be356ed9bd30bbd3f0a23a7204",
+                "sha256:1269fef3167bb52631ad4fa7dd27bf635d5a0790b8e6222065d42e91bede4162",
+                "sha256:14a53646369157baa0499513f96091eb70382eb50b2c82393d17d7ec81b7b85f",
+                "sha256:3a3af27a8d23143c49a3420efe5b3f8cf1a48c6fc8bc6856b03f638abc1833bb",
+                "sha256:46bac5ca10fb748d6c55843a931855e2727a7a22584f302dd9bb1506e69f83f6",
+                "sha256:4c037fd14c5f4e308b8370b447b469ca10e69427966527edcab07f52d88388f7",
+                "sha256:51178c738d559a2d1071ce0b0f56e57eb315bcf8f7d4cf127674b533e3101f88",
+                "sha256:5ea81ea3dbd6767873c611687141ec7b06ed8bab43f68fad5b7be184a920dc99",
+                "sha256:6961548bba529cac7c07af2fd4d527c5b91bb8fe18995fed6044ac22b3d14644",
+                "sha256:75aaa27aa521a182824d89e5ab0a1d16ca207318a6b65042b046053cfc8ed07a",
+                "sha256:7a2dd66d2d4df34fa82c9dc85657c5e019b87932019947faece7983f2089a840",
+                "sha256:8a51f2c6d1f884e98846a0a9021ff6861bdb98457879f412fdc2b42d14494067",
+                "sha256:9c568495e35599625f7b999774e29e8d6b01a6fb684d77dee1f56d41b11b40cd",
+                "sha256:9eddaafb3c48e0900690c1727fba226c4804b8e6127ea409689c3bb492d06de4",
+                "sha256:bbb332d45b32df41200380fff14712cb6093b61bd142272a10b16778c418e98e",
+                "sha256:bc3d98f621898b4a9bc7fecc00513eec8f40b5b83913d74ccb445f037d58cd89",
+                "sha256:c11d6033115dc4887c456565303f540c44197f4fc1a2bfb192224a301534888e",
+                "sha256:c50a724d136ec10d920661f1442e4a8b010a4fe5aebd65e0c2241ea41dbe93dc",
+                "sha256:d0a5095d52b90ff38592bbdc2644f17c6d495762edf47d876049cfd2968fbccf",
+                "sha256:d6cff2276e502b86a25fd10c2a96973fdb45c7a977dca2138d661417f3728341",
+                "sha256:e46d13f38cfcbb79bfdb2964b0fe12561fe633caf964a77a5f8d4e45fe5d2ef7"
+            ],
+            "version": "==2020.7.14"
+        },
+        "requests": {
+            "hashes": [
+                "sha256:b3559a131db72c33ee969480840fff4bb6dd111de7dd27c8ee1f820f4f00231b",
+                "sha256:fe75cc94a9443b9246fc7049224f75604b113c36acb93f87b80ed42c44cbb898"
+            ],
+            "version": "==2.24.0"
         },
         "six": {
             "hashes": [
@@ -523,18 +666,33 @@
         },
         "tox": {
             "hashes": [
-                "sha256:322dfdf007d7d53323f767badcb068a5cfa7c44d8aabb698d131b28cf44e62c4",
-                "sha256:8c9ad9b48659d291c5bc78bcabaa4d680d627687154b812fa52baedaa94f9f83"
+                "sha256:e6318f404aff16522ff5211c88cab82b39af121735a443674e4e2e65f4e4637b",
+                "sha256:eb629ddc60e8542fd4a1956b2462e3b8771d49f1ff630cecceacaa0fbfb7605a"
             ],
             "index": "pypi",
-            "version": "==3.15.1"
+            "version": "==3.20.0"
+        },
+        "tox-travis": {
+            "hashes": [
+                "sha256:442c96b078333c94e272d0e90e4582e35e0529ea98bcd2f7f96053d690c4e7a4",
+                "sha256:465cd8f71ad878962a3fce0e9e2e213994e0ae4e0c30f87fe6af1b04ea282dc4"
+            ],
+            "index": "pypi",
+            "version": "==0.12"
         },
         "tqdm": {
             "hashes": [
-                "sha256:daec693491c52e9498632dfbe9ccfc4882a557f5fa08982db1b4d3adbe0887c3",
-                "sha256:ebdebdb95e3477ceea267decfc0784859aa3df3e27e22d23b83e9b272bf157ae"
+                "sha256:1a336d2b829be50e46b84668691e0a2719f26c97c62846298dd5ae2937e4d5cf",
+                "sha256:564d632ea2b9cb52979f7956e093e831c28d441c11751682f84c86fc46e4fd21"
+            ],
+            "version": "==4.48.2"
+        },
+        "traitlets": {
+            "hashes": [
+                "sha256:0d9c4005506b306b0a99551e96174b8bedc675c2dd048f92b3bbbb7d86ac93a9",
+                "sha256:62a037f12ccb823fb05823afbe35fe0273bc18fa3202d0cf0ea8f24e97e464be"
             ],
-            "version": "==4.60.0"
+            "version": "==5.0.0"
         },
         "typed-ast": {
             "hashes": [
@@ -579,12 +737,19 @@
             ],
             "version": "==3.7.4.3"
         },
+        "urllib3": {
+            "hashes": [
+                "sha256:91056c15fa70756691db97756772bb1eb9678fa585d9184f24534b100dc60f4a",
+                "sha256:e7983572181f5e1522d9c98453462384ee92a0be7fac5f1413a1e35c56cc0461"
+            ],
+            "version": "==1.25.10"
+        },
         "virtualenv": {
             "hashes": [
-                "sha256:09c61377ef072f43568207dc8e46ddeac6bcdcaf288d49011bda0e7f4d38c4a2",
-                "sha256:a935126db63128861987a7d5d30e23e8ec045a73840eeccb467c148514e29535"
+                "sha256:43add625c53c596d38f971a465553f6318decc39d98512bc100fa1b1e839c8dc",
+                "sha256:e0305af10299a7fb0d69393d8f04cb2965dda9351140d11ac8db4e5e3970451b"
             ],
-            "version": "==20.4.4"
+            "version": "==20.0.31"
         },
         "wcwidth": {
             "hashes": [
diff --git a/README.md b/README.md
index a2695a2..fc7bef1 100644
--- a/README.md
+++ b/README.md
@@ -1,20 +1,70 @@
-# LTL<sub>f</sub>2DFA
-[![](https://img.shields.io/pypi/v/ltlf2dfa.svg)](https://pypi.python.org/pypi/ltlf2dfa)
-[![](https://img.shields.io/pypi/pyversions/ltlf2dfa.svg)](https://pypi.python.org/pypi/ltlf2dfa)
-[![LTLf2DFA CI pipeline](
-  https://github.com/whitemech/LTLf2DFA/workflows/LTLf2DFA%20CI%20pipeline./badge.svg)](
-  https://github.com/whitemech/LTLf2DFA/actions?query=workflow%3A%22LTLf2DFA+CI+pipeline.%22)
-[![](https://img.shields.io/badge/docs-mkdocs-9cf)](https://www.mkdocs.org/)
-[![](https://img.shields.io/badge/status-development-orange.svg)](https://img.shields.io/badge/status-development-orange.svg)
-[![codecov](https://codecov.io/gh/whitemech/LTLf2DFA/branch/master/graph/badge.svg)](https://codecov.io/gh/whitemech/LTLf2DFA)
-[![](https://img.shields.io/badge/flake8-checked-blueviolet)](https://img.shields.io/badge/flake8-checked-blueviolet)
-[![](https://img.shields.io/badge/mypy-checked-blue)](https://img.shields.io/badge/mypy-checked-blue)
-[![](https://img.shields.io/badge/license-LGPLv3%2B-blue)](https://img.shields.io/badge/license-LGPLv3%2B-blue)
+<h1 align="center">
+  <img src="http://ltlf2dfa.diag.uniroma1.it/static/images/logo-ltlf2dfa.svg">
+</h1>
+
+<p align="center">
+  <a href="https://pypi.org/project/ltlf2dfa">
+    <img alt="PyPI" src="https://img.shields.io/pypi/v/ltlf2dfa">
+  </a>
+  <a href="https://pypi.org/project/ltlf2dfa">
+    <img alt="PyPI - Python Version" src="https://img.shields.io/pypi/pyversions/ltlf2dfa" />
+  </a>
+  <a href="">
+    <img alt="PyPI - Implementation" src="https://img.shields.io/pypi/implementation/ltlf2dfa">
+  </a>
+  <a href="https://github.com/whitemech/ltlf2dfa/blob/master/LICENSE">
+    <img alt="GitHub" src="https://img.shields.io/badge/license-LGPLv3%2B-blue">
+  </a>  
+  <a href="">
+    <img alt="PyPI - Wheel" src="https://img.shields.io/pypi/wheel/ltlf2dfa">
+  </a>
+</p>
+<p align="center">
+  <a href="">
+    <img alt="test" src="https://github.com/whitemech/ltlf2dfa/workflows/test/badge.svg">
+  </a>
+  <a href="">
+    <img alt="lint" src="https://github.com/whitemech/ltlf2dfa/workflows/lint/badge.svg">
+  </a>
+  <a href="">
+    <img alt="docs" src="https://github.com/whitemech/ltlf2dfa/workflows/docs/badge.svg">
+  </a>
+  <a href="https://codecov.io/gh/whitemech/pddl">
+    <img alt="codecov" src="https://codecov.io/gh/whitemech/ltlf2dfa/branch/master/graph/badge.svg">
+  </a>
+  <a href="">
+    <img alt="PyPI - Status" src="https://img.shields.io/pypi/status/ltlf2dfa" />
+  </a>
+</p>
+<p align="center">
+  <a href="https://img.shields.io/badge/flake8-checked-blueviolet">
+    <img alt="" src="https://img.shields.io/badge/flake8-checked-blueviolet">
+  </a>
+  <a href="https://img.shields.io/badge/mypy-checked-blue">
+    <img alt="" src="https://img.shields.io/badge/mypy-checked-blue">
+  </a>
+  <a href="https://img.shields.io/badge/isort-checked-yellow">
+    <img alt="isort" src="https://img.shields.io/badge/isort-checked-yellow" />
+  </a>
+  <a href="https://img.shields.io/badge/code%20style-black-black">
+    <img alt="black" src="https://img.shields.io/badge/code%20style-black-black" />
+  </a>
+  <a href="https://www.mkdocs.org/">
+    <img alt="" src="https://img.shields.io/badge/docs-mkdocs-9cf">
+</p>
+<p align="center">
+  </a>
+    <a href="https://zenodo.org/badge/DOI/10.5281/zenodo.3888410.svg">
+    <img alt="" src="https://zenodo.org/badge/DOI/10.5281/zenodo.3888410.svg">
+  </a>
+</p>
+
+---
 
 LTL<sub>f</sub>2DFA is a tool that transforms an LTL<sub>f</sub> or a PLTL<sub>f</sub> formula into a minimal 
 Deterministic Finite state Automaton (DFA) using [MONA](http://www.brics.dk/mona/).
 
-It is also available online at [ltlf2dfa.diag.uniroma1.it](http://ltlf2dfa.diag.uniroma1.it).
+It is also available online at [http://ltlf2dfa.diag.uniroma1.it](http://ltlf2dfa.diag.uniroma1.it).
 
 ## Prerequisites
 
@@ -23,8 +73,8 @@ your system following the instructions [here](http://www.brics.dk/mona/download.
 
 This tool is also based on the following libraries:
 
-- [lark-parser 0.8.5](https://pypi.org/project/lark-parser/)
-- [sympy 1.5.1](https://pypi.org/project/sympy/)
+- [lark-parser 0.9.0](https://pypi.org/project/lark-parser/)
+- [sympy 1.6.1](https://pypi.org/project/sympy/)
 
 They are automatically added while installing LTL<sub>f</sub>2DFA.
 
@@ -41,7 +91,7 @@ pip install git+https://github.com/whitemech/LTLf2DFA.git
 
 - or, clone the repository and install:
 ```
-git clone htts://github.com/whitemech/LTLf2DFA.git
+git clone https://github.com/whitemech/LTLf2DFA.git
 cd ltlf2dfa
 pip install .
 ```
@@ -88,7 +138,7 @@ have only past, only future or none operators.
 
 To run tests: `tox`
 
-To run only the code tests: `tox -e py37`
+To run only the code tests: `tox -e py3.7`
 
 To run only the code style checks: `tox -e flake8`
 
@@ -103,7 +153,10 @@ and then go to [http://localhost:8000](http://localhost:8000)
 
 LTL<sub>f</sub>2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).
 
-Copyright 2018-2020 WhiteMech
+Copyright 2018-2020 WhiteMech @ Sapienza University
+
+## Citing
+If you are interested in this tool, and you use it in your own work, please consider citing it.
 
 ## Author
 
diff --git a/docs/changelog.md b/docs/changelog.md
new file mode 100644
index 0000000..a36f2f3
--- /dev/null
+++ b/docs/changelog.md
@@ -0,0 +1,1 @@
+{!../HISTORY.md!}
\ No newline at end of file
diff --git a/ltlf2dfa/__init__.py b/ltlf2dfa/__init__.py
index 11a4d2c..4632c5a 100644
--- a/ltlf2dfa/__init__.py
+++ b/ltlf2dfa/__init__.py
@@ -1,6 +1,31 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """Top-level package for ltlf2dfa."""
 
-from .__version__ import __title__, __description__, __url__, __version__
-from .__version__ import __author__, __author_email__, __license__, __copyright__
+from .__version__ import (
+    __author__,
+    __author_email__,
+    __copyright__,
+    __description__,
+    __license__,
+    __title__,
+    __url__,
+    __version__,
+)
diff --git a/ltlf2dfa/__version__.py b/ltlf2dfa/__version__.py
index 11741e4..c672cdf 100644
--- a/ltlf2dfa/__version__.py
+++ b/ltlf2dfa/__version__.py
@@ -1,11 +1,28 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Declaration of metadata for the package."""
 
 __title__ = "ltlf2dfa"
 __description__ = "LTLf and PLTLf to Deterministic Finite-state Automata (DFA)"
 __url__ = "https://github.com/whitemech/ltlf2dfa.git"
-__version__ = "1.0.0.post0"
+__version__ = "1.0.1"
 __author__ = "Francesco Fuggitti"
-__author_email__ = "fuggitti@eecs.yorku.ca"
+__author_email__ = "fuggitti@diag.uniroma1.it"
 __license__ = "GNU Lesser General Public License v3 or later (LGPLv3+)"
-__copyright__ = "2018-2020 WhiteMech"
+__copyright__ = "2018-2021 WhiteMech"
diff --git a/ltlf2dfa/base.py b/ltlf2dfa/base.py
index e9016be..b044832 100644
--- a/ltlf2dfa/base.py
+++ b/ltlf2dfa/base.py
@@ -1,13 +1,30 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """Base classes for the implementation of a generic syntax tree."""
-
-from abc import abstractmethod, ABC
-from typing import Sequence, Set, Tuple, TypeVar, Generic, cast, Union, Optional, Any
+import functools
 import re
+from abc import ABC, abstractmethod
+from typing import Any, Generic, List, Optional, Sequence, Tuple, TypeVar, Union, cast
 
-from ltlf2dfa.symbols import Symbols, OpSymbol
 from ltlf2dfa.helpers import Hashable, Wrapper
+from ltlf2dfa.symbols import OpSymbol, Symbols
 
 AtomSymbol = Union["QuotedFormula", str]
 
@@ -16,8 +33,8 @@ class Formula(Hashable, ABC):
     """Abstract class for a formula."""
 
     @abstractmethod
-    def find_labels(self) -> Set[AtomSymbol]:
-        """Return the set of symbols."""
+    def find_labels(self) -> List[AtomSymbol]:
+        """Return the list of symbols."""
 
     def to_nnf(self) -> "Formula":
         """Transform the formula in NNF."""
@@ -69,9 +86,9 @@ def __str__(self):
         """Get the string representation."""
         return str(self.s)
 
-    def find_labels(self) -> Set[AtomSymbol]:
-        """Return the set of symbols."""
-        return {self.s}
+    def find_labels(self) -> List[AtomSymbol]:
+        """Return the list of symbols."""
+        return [self.s]
 
 
 class QuotedFormula(Wrapper):
@@ -101,8 +118,8 @@ def __repr__(self):
 class MonaProgram:
     """Implements a MONA program."""
 
-    header = "m2l-str"
-    vars: Set[str] = set()
+    HEADER = "var2 $ where ~ex1 p where true: p notin $ & p+1 in $;\nallpos $"
+    vars: List[str] = list()
 
     def __init__(self, f: Formula):
         """Initialize.
@@ -111,11 +128,11 @@ def __init__(self, f: Formula):
         :param i: instant of evaluation in the trace.
         """
         self.formula = f
-        self._set_vars()
+        self._vars()
 
-    def _set_vars(self):
-        """Set MONA vars."""
-        self.vars = set([v.upper() for v in self.formula.find_labels()])
+    def _vars(self):
+        """List MONA vars."""
+        self.vars = [v.upper() for v in self.formula.find_labels()]
 
     def __repr__(self):
         """Nice representation."""
@@ -126,13 +143,13 @@ def mona_program(self) -> str:
         if self.vars:
             return "#{};\n{};\nvar2 {};\n{};\n".format(
                 str(self.formula),
-                self.header,
+                self.HEADER,
                 ", ".join(self.vars),
                 self.formula.to_mona(),
             )
         else:
             return "#{};\n{};\n{};\n".format(
-                str(self.formula), self.header, self.formula.to_mona()
+                str(self.formula), self.HEADER, self.formula.to_mona()
             )
 
 
@@ -181,8 +198,8 @@ def __lt__(self, other):
         """Compare the formula with another formula."""
         return self.f.__lt__(other.f)
 
-    def find_labels(self) -> Set[AtomSymbol]:
-        """Return the set of symbols."""
+    def find_labels(self) -> List[AtomSymbol]:
+        """Return the list of symbols."""
         return cast(Formula, self.f).find_labels()
 
 
@@ -210,10 +227,43 @@ def __str__(self):
     def _members(self) -> Tuple[OpSymbol, OperatorChildren]:
         return self.operator_symbol, self.formulas
 
-    def find_labels(self) -> Set[AtomSymbol]:
-        """Return the set of symbols."""
-        return set.union(*map(lambda f: f.find_labels(), self.formulas))
+    def find_labels(self) -> List[AtomSymbol]:
+        """Return the list of symbols."""
+        # return set.union(*map(lambda f: f.find_labels(), self.formulas))))
+        # seen = set()
+        # result = []
+        # for f in self.formulas:
+        #     for lab in f.find_labels():
+        #         if lab not in seen:
+        #             result.append(lab)
+        #             seen.add(lab)
+        # return result
+        return flatten(self.formulas)
 
     def to_nnf(self):
         """Transform in NNF."""
         return type(self)([f.to_nnf() for f in self.formulas])
+
+
+@functools.singledispatch
+def flatten(lst) -> List:
+    """Flatten a list of lists."""
+    return [item for sublist in lst for item in sublist.find_labels()]
+
+
+def _flatten_as_set(lst):
+    """Flatten a list of lists removing duplicates."""
+    seen = set()
+    result = []
+    for f in lst:
+        for lab in f.find_labels():
+            if lab not in seen:
+                result.append(lab)
+                seen.add(lab)
+    return result
+
+
+@flatten.register(tuple)
+def _(lst: Tuple[Formula]):
+    """Flatten a list of lists of formulas."""
+    return _flatten_as_set(lst)
diff --git a/ltlf2dfa/helpers.py b/ltlf2dfa/helpers.py
index e6d90fd..cb43186 100644
--- a/ltlf2dfa/helpers.py
+++ b/ltlf2dfa/helpers.py
@@ -1,17 +1,27 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """Helpers module."""
 
 from abc import ABC, abstractmethod
 from copy import copy
 
-# from itertools import chain, combinations
-# from typing import Iterable, Set, FrozenSet, List
-
-# from pythomata import PropositionalInterpretation as PropInt
-# from sympy import Symbol
-# from sympy.logic.boolalg import Boolean, BooleanFalse, BooleanTrue
-
 from ltlf2dfa.symbols import Symbols
 
 ParsingError = ValueError("Parsing error.")
@@ -107,38 +117,6 @@ def wrapped(self):
         return self.__obj
 
 
-# def powerset(s: Set) -> FrozenSet:
-#     """
-#     Compute the power set of a set.
-#
-#     >>> sorted(map(tuple, powerset({1,2,3})))
-#     [(), (1,), (1, 2), (1, 2, 3), (1, 3), (2,), (2, 3), (3,)]
-#
-#
-#     :param s: the set of elements on which to compute the power set.
-#     :return: the power set of the set provided in input.
-#     """
-#     combs = iter_powerset(s)
-#     res = frozenset(frozenset(x) for x in combs)
-#     return res
-
-
-# def iter_powerset(s: Set) -> Iterable:
-#     """
-#     Compute the generative version of the power set function.
-#
-#     >>> sorted(map(tuple, powerset({1,2,3})))
-#     [(), (1,), (1, 2), (1, 2, 3), (1, 3), (2,), (2, 3), (3,)]
-#
-#     :param s: the set of elements on which to compute the power set.
-#     :return: the generator that generates the poweset.
-#     """
-#     s_list = list(s)  # type: List
-#     combs = chain.from_iterable(combinations(s_list, r) for r in range(len(s_list) + 1))
-#     for c in combs:
-#         yield c
-
-
 def new_var(prev_var: str) -> str:
     """Compute next variable."""
     if prev_var == "0" or prev_var == "max($)":
@@ -158,28 +136,4 @@ def sym2regexp(sym: Symbols):
         return s
 
 
-# def evaluate(formula: Boolean, i: PropInt) -> bool:
-#     """
-#     Evaluate a SymPy boolean expression against a propositional interpretation.
-#
-#     The symbols not present in the propositional interpretation will be considered False.
-#
-#     >>> from sympy.parsing.sympy_parser import parse_expr
-#     >>> evaluate(parse_expr("a & b"), {"a": True})
-#     False
-#
-#     >>> evaluate(parse_expr("a | b"), {"b": True})
-#     True
-#
-#     >>> evaluate(parse_expr("a"), {"b": True})
-#     False
-#
-#     :param formula: a sympy.logic.boolalg.Boolean.
-#     :param i: a propositional interpretation,
-#               i.e. a mapping from symbol identifiers to True/False
-#     :return: True if the formula is true in the interpretation, False o/w.
-#     """
-#     return formula.subs(i).replace(Symbol, BooleanFalse) == BooleanTrue()
-
-
 MAX_CACHE_SIZE = 1024
diff --git a/ltlf2dfa/ltlf.py b/ltlf2dfa/ltlf.py
index c2c829d..24a9540 100644
--- a/ltlf2dfa/ltlf.py
+++ b/ltlf2dfa/ltlf.py
@@ -1,22 +1,39 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """This module contains the implementation of Linear Temporal Logic on finite traces."""
 
-from abc import abstractmethod, ABC
-from typing import Set, Optional, Any
 import re
+from abc import ABC, abstractmethod
+from typing import Any, List, Optional
 
 from ltlf2dfa.base import (
-    Formula,
     AtomicFormula,
-    UnaryOperator,
-    BinaryOperator,
     AtomSymbol,
+    BinaryOperator,
+    Formula,
+    UnaryOperator,
 )
+from ltlf2dfa.helpers import new_var
 from ltlf2dfa.ltlf2dfa import to_dfa
 from ltlf2dfa.pl import PLAtomic
-from ltlf2dfa.symbols import Symbols, OpSymbol
-from ltlf2dfa.helpers import new_var
+from ltlf2dfa.symbols import OpSymbol, Symbols
 
 
 class LTLfFormula(Formula, ABC):
@@ -48,9 +65,13 @@ def to_ldlf(self):
         :return: an LDLf formula.
         """
 
-    def to_dfa(self) -> str:
-        """Translate into a DFA."""
-        return to_dfa(self)
+    def to_dfa(self, mona_dfa_out: bool = False) -> str:
+        """
+        Translate into a DFA.
+
+        :param mona_dfa_out: flag for DFA output in MONA syntax.
+        """
+        return to_dfa(self, mona_dfa_out)
 
 
 class LTLfUnaryOperator(UnaryOperator[LTLfFormula], LTLfFormula, ABC):
@@ -70,7 +91,7 @@ def negate(self):
         """Negate the formula."""
         return LTLfNot(self)
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
         return PLAtomic(self.s).find_labels()
 
@@ -97,9 +118,9 @@ def negate(self):
         """Negate the formula."""
         return LTLfFalse()
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def to_mona(self, v="0") -> str:
         """Return the MONA encoding for False."""
@@ -121,9 +142,9 @@ def negate(self):
         """Negate the formula."""
         return LTLfTrue()
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def to_mona(self, v="0") -> str:
         """Return the MONA encoding for False."""
@@ -292,11 +313,13 @@ def to_mona(self, v="0") -> str:
         """Return the MONA encoding of an LTLf Next formula."""
         ex_var = new_var(v)
         if v != "0":
-            return "(ex1 {0}: {0}={1}+1 & {2})".format(
+            return "(ex1 {0}: {0} in $ & {0}={1}+1 & {2})".format(
                 ex_var, v, self.f.to_mona(ex_var)
             )
         else:
-            return "(ex1 {0}: {0}=1 & {1})".format(ex_var, self.f.to_mona(ex_var))
+            return "(ex1 {0}: {0} in $ & {0}=1 & {1})".format(
+                ex_var, self.f.to_mona(ex_var)
+            )
 
     # def to_ldlf(self):
     #     """Convert the formula to LDLf."""
@@ -326,11 +349,11 @@ def to_mona(self, v="0") -> str:
         """Return the MONA encoding of an LTLf WeakNext formula."""
         ex_var = new_var(v)
         if v != "0":
-            return "((0 = max($)) | (ex1 {0}: {0}={1}+1 & {2}))".format(
+            return "(({1} = max($)) | (ex1 {0}: {0} in $ & {0}={1}+1 & {2}))".format(
                 ex_var, v, self.f.to_mona(ex_var)
             )
         else:
-            return "((0 = max($)) | (ex1 {0}: {0}=1 & {1}))".format(
+            return "((0 = max($)) | (ex1 {0}: {0} in $ & {0}=1 & {1}))".format(
                 ex_var, self.f.to_mona(ex_var)
             )
 
@@ -367,18 +390,12 @@ def to_mona(self, v="0") -> str:
             if len(self.formulas) > 2
             else self.formulas[1].to_mona(v=ex_var)
         )
-        if v != "0":
-            return (
-                "(ex1 {0}: {1}<={0}&{0}<=max($) & {2} & "
-                "(all1 {3}: {1}<={3}&{3}<{0} => {4}))".format(
-                    ex_var, v, f2, all_var, f1
-                )
-            )
-        else:
-            return (
-                "(ex1 {0}: 0<={0}&{0}<=max($) & {1} & "
-                "(all1 {2}: 0<={2}&{2}<{0} => {3}))".format(ex_var, f2, all_var, f1)
+        return (
+            "(ex1 {0}: {0} in $ & {1}<={0}&{0}<=max($) & {2} & "
+            "(all1 {3}: {3} in $ & {1}<={3}&{3}<{0} => {4}))".format(
+                ex_var, v, f2, all_var, f1
             )
+        )
 
     # def to_ldlf(self):
     #     """Convert the formula to LDLf."""
@@ -420,18 +437,13 @@ def to_mona(self, v="0") -> str:
             if len(self.formulas) > 2
             else self.formulas[1].to_mona(v=all_var)
         )
-        if v != "0":
-            return (
-                "((ex1 {0}: {1}<={0}&{0}<=max($) & {2} & "
-                "(all1 {3}: {1}<={3}&{3}<={0} => {4})) | (all1 {3}: "
-                "{1}<={3}&{3}<=max($) => {4}))".format(ex_var, v, f1, all_var, f2)
-            )
-        else:
-            return (
-                "((ex1 {0}: 0<={0}&{0}<=max($) & {1} & "
-                "(all1 {2}: 0<={2}&{2}<={0} => {3})) | (all1 {2}: "
-                "0<={2}&{2}<=max($) => {3}))".format(ex_var, f1, all_var, f2)
+        return (
+            "((ex1 {0}: {0} in $ & {1}<={0}&{0}<=max($) & {2} & "
+            "(all1 {3}: {3} in $ & {1}<={3}&{3}<={0} => {4})) | (all1 {3}: "
+            "{3} in $ & {1}<={3}&{3}<=max($) => {4}))".format(
+                ex_var, v, f1, all_var, f2
             )
+        )
 
     # def to_ldlf(self):
     #     """Convert the formula to LDLf."""
@@ -516,9 +528,9 @@ def negate(self) -> LTLfFormula:
         """Negate the formula."""
         return self.to_nnf().negate()
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def _members(self):
         return (Symbols.LAST.value,)
@@ -527,6 +539,10 @@ def __str__(self):
         """Get the string representation."""
         return Symbols.LAST.value
 
+    def to_mona(self, v="0") -> str:
+        """Return the MONA encoding of an LTLf Last formula."""
+        return LTLfWeakNext(LTLfFalse()).to_mona(v)
+
     # def to_ldlf(self):
     #     """Convert the formula to LDLf."""
     #     return LDLfDiamond(RegExpPropositional(PLTrue()), LDLfEnd())
@@ -535,9 +551,9 @@ def __str__(self):
 class LTLfEnd(LTLfFormula):
     """Class for the LTLf End formula."""
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def _members(self):
         return (Symbols.END.value,)
diff --git a/ltlf2dfa/ltlf2dfa.py b/ltlf2dfa/ltlf2dfa.py
index f7bdcc2..303bbfb 100644
--- a/ltlf2dfa/ltlf2dfa.py
+++ b/ltlf2dfa/ltlf2dfa.py
@@ -1,14 +1,31 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """Main module of the pakage."""
 
 import itertools as it
-from subprocess import PIPE, Popen, TimeoutExpired
 import os
 import re
 import signal
+from subprocess import PIPE, Popen, TimeoutExpired
 
-from sympy import symbols, And, Not, Or, simplify
+from sympy import And, Not, Or, simplify, symbols
 
 from ltlf2dfa.base import MonaProgram
 
@@ -57,10 +74,7 @@ def ter2symb(ap, ternary):
 
 def simplify_guard(guards):
     """Make a big OR among guards and simplify them."""
-    final = Or()
-    for g in guards:
-        final = Or(final, g)
-    return simplify(final)
+    return simplify(Or(*guards))
 
 
 def parse_mona(mona_output):
@@ -160,7 +174,7 @@ def createMonafile(p: str):
 
 def invoke_mona():
     """Execute the MONA tool."""
-    command = "mona -q -w {}/automa.mona".format(PACKAGE_DIR)
+    command = "mona -q -u -w {}/automa.mona".format(PACKAGE_DIR)
     process = Popen(
         args=command,
         stdout=PIPE,
@@ -185,10 +199,14 @@ def output2dot(mona_output):
         return parse_mona(mona_output)
 
 
-def to_dfa(f) -> str:
+def to_dfa(f, mona_dfa_out=False) -> str:
     """Translate to deterministic finite-state automaton."""
     p = MonaProgram(f)
     mona_p_string = p.mona_program()
     createMonafile(mona_p_string)
     mona_dfa = invoke_mona()
-    return output2dot(mona_dfa)
+    if mona_dfa_out:
+        return mona_dfa
+    else:
+        assert mona_dfa_out is False
+        return output2dot(mona_dfa)
diff --git a/ltlf2dfa/parser/__init__.py b/ltlf2dfa/parser/__init__.py
index 90a7185..50867ae 100644
--- a/ltlf2dfa/parser/__init__.py
+++ b/ltlf2dfa/parser/__init__.py
@@ -1,4 +1,21 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """This module contains the implementation of the parsers for the supported logic formalisms."""
 import inspect
 import os
diff --git a/ltlf2dfa/parser/ltlf.py b/ltlf2dfa/parser/ltlf.py
index 388a6e3..1101374 100644
--- a/ltlf2dfa/parser/ltlf.py
+++ b/ltlf2dfa/parser/ltlf.py
@@ -1,4 +1,21 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Implementation of the LTLf parser."""
 
 from pathlib import Path
@@ -7,21 +24,21 @@
 
 from ltlf2dfa.helpers import ParsingError
 from ltlf2dfa.ltlf import (
+    LTLfAlways,
+    LTLfAnd,
+    LTLfAtomic,
     LTLfEquivalence,
+    LTLfEventually,
+    LTLfFalse,
     LTLfImplies,
-    LTLfOr,
-    LTLfAnd,
+    LTLfLast,
+    LTLfNext,
     LTLfNot,
-    LTLfUntil,
+    LTLfOr,
     LTLfRelease,
-    LTLfAlways,
-    LTLfEventually,
-    LTLfNext,
-    LTLfWeakNext,
     LTLfTrue,
-    LTLfAtomic,
-    LTLfFalse,
-    LTLfLast,
+    LTLfUntil,
+    LTLfWeakNext,
 )
 from ltlf2dfa.parser import CUR_DIR
 from ltlf2dfa.parser.pl import PLTransformer
diff --git a/ltlf2dfa/parser/pl.py b/ltlf2dfa/parser/pl.py
index 61f06a4..f06a0c4 100644
--- a/ltlf2dfa/parser/pl.py
+++ b/ltlf2dfa/parser/pl.py
@@ -1,4 +1,21 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Implementation of the PL parser."""
 
 from pathlib import Path
@@ -8,14 +25,14 @@
 from ltlf2dfa.helpers import ParsingError
 from ltlf2dfa.parser import CUR_DIR
 from ltlf2dfa.pl import (
-    PLNot,
-    PLAtomic,
-    PLOr,
     PLAnd,
-    PLImplies,
+    PLAtomic,
     PLEquivalence,
-    PLTrue,
     PLFalse,
+    PLImplies,
+    PLNot,
+    PLOr,
+    PLTrue,
 )
 
 
diff --git a/ltlf2dfa/parser/pltlf.lark b/ltlf2dfa/parser/pltlf.lark
index 0126b00..4d08432 100644
--- a/ltlf2dfa/parser/pltlf.lark
+++ b/ltlf2dfa/parser/pltlf.lark
@@ -22,12 +22,12 @@ start: pltlf_formula
 ?pltlf_atom:       pltlf_symbol
            |       pltlf_true
            |       pltlf_false
-           |       pltlf_last
+           |       pltlf_start
 
 pltlf_symbol: SYMBOL_NAME
 pltlf_true: prop_true
 pltlf_false: prop_false
-pltlf_last: START
+pltlf_start: START
 
 // Operators must not be part of a word
 SINCE.2: /S(?=[^a-z]|$)/
diff --git a/ltlf2dfa/parser/pltlf.py b/ltlf2dfa/parser/pltlf.py
index 0d2cbe6..ef3f248 100644
--- a/ltlf2dfa/parser/pltlf.py
+++ b/ltlf2dfa/parser/pltlf.py
@@ -1,4 +1,21 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Implementation of the PLTLf parser."""
 
 from pathlib import Path
@@ -6,23 +23,23 @@
 from lark import Lark, Transformer
 
 from ltlf2dfa.helpers import ParsingError
+from ltlf2dfa.parser import CUR_DIR
+from ltlf2dfa.parser.pl import PLTransformer
 from ltlf2dfa.pltlf import (
+    PLTLfAnd,
+    PLTLfAtomic,
+    PLTLfBefore,
     PLTLfEquivalence,
+    PLTLfFalse,
+    PLTLfHistorically,
     PLTLfImplies,
-    PLTLfOr,
-    PLTLfAnd,
     PLTLfNot,
-    PLTLfSince,
-    PLTLfHistorically,
     PLTLfOnce,
-    PLTLfBefore,
-    PLTLfAtomic,
+    PLTLfOr,
+    PLTLfSince,
+    PLTLfStart,
     PLTLfTrue,
-    PLTLfFalse,
-    PLTLfLast,
 )
-from ltlf2dfa.parser import CUR_DIR
-from ltlf2dfa.parser.pl import PLTransformer
 
 
 class PLTLfTransformer(Transformer):
@@ -156,9 +173,9 @@ def pltlf_false(self, args):
         """Parse PLTLf False."""
         return PLTLfFalse()
 
-    def pltlf_last(self, args):
+    def pltlf_start(self, args):
         """Parse PLTLf Last."""
-        return PLTLfLast()
+        return PLTLfStart()
 
     # def pltlf_end(self, args):
     #     raise NotImplementedError("PLTLf end not supported, yet")
diff --git a/ltlf2dfa/pl.py b/ltlf2dfa/pl.py
index f41d9e0..5e29e26 100644
--- a/ltlf2dfa/pl.py
+++ b/ltlf2dfa/pl.py
@@ -1,17 +1,30 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """This module provides support for Propositional Logic."""
 
 import functools
-from abc import abstractmethod, ABC
-from typing import Set, Any, Optional
+from abc import ABC, abstractmethod
+from typing import Any, List, Optional, Set
 
-# import sympy
-# from sympy.logic.boolalg import Boolean, BooleanTrue, BooleanFalse
-# from pythomata import PropositionalInterpretation
-
-from ltlf2dfa.base import Formula, AtomicFormula, BinaryOperator, UnaryOperator
-from ltlf2dfa.symbols import Symbols, OpSymbol
+from ltlf2dfa.base import AtomicFormula, BinaryOperator, Formula, UnaryOperator
+from ltlf2dfa.symbols import OpSymbol, Symbols
 
 
 class PLFormula(Formula):
@@ -54,54 +67,12 @@ def to_mona(self, v: Optional[Any] = None) -> str:
         """
 
 
-# def to_sympy(
-#     formula: Formula, replace: Optional[Dict[AtomSymbol, sympy.Symbol]] = None
-# ) -> Boolean:
-#     """
-#     Translate a PLFormula object into a SymPy expression.
-#
-#     :param formula: the formula to translate.
-#     :param replace: an optional mapping from symbols to replace to other replacement symbols.
-#     :return: the SymPy formula object equivalent to the formula.
-#     """
-#     if replace is None:
-#         replace = {}
-#
-#     if isinstance(formula, PLTrue):
-#         return BooleanTrue()
-#     elif isinstance(formula, PLFalse):
-#         return BooleanFalse()
-#     elif isinstance(formula, PLAtomic):
-#         symbol = replace.get(formula.s, formula.s)
-#         return sympy.Symbol(symbol)
-#     elif isinstance(formula, PLNot):
-#         return sympy.Not(to_sympy(formula.f, replace=replace))
-#     elif isinstance(formula, PLOr):
-#         return sympy.simplify(
-#             sympy.Or(*[to_sympy(f, replace=replace) for f in formula.formulas])
-#         )
-#     elif isinstance(formula, PLAnd):
-#         return sympy.simplify(
-#             sympy.And(*[to_sympy(f, replace=replace) for f in formula.formulas])
-#         )
-#     elif isinstance(formula, PLImplies):
-#         return sympy.simplify(
-#             sympy.Implies(*[to_sympy(f, replace=replace) for f in formula.formulas])
-#         )
-#     elif isinstance(formula, PLEquivalence):
-#         return sympy.simplify(
-#             sympy.Equivalent(*[to_sympy(f, replace=replace) for f in formula.formulas])
-#         )
-#     else:
-#         raise ValueError("Formula is not valid.")
-
-
 class PLAtomic(AtomicFormula, PLFormula):
     """A class to represent propositional atomic formulas."""
 
-    def find_labels(self) -> Set[Any]:
-        """Return the set of symbols."""
-        return {self.s}
+    def find_labels(self) -> List[Any]:
+        """Return the list of symbols."""
+        return [self.s]
 
     def _find_atomics(self):
         return {self}
@@ -112,10 +83,7 @@ def negate(self) -> PLFormula:
 
     def to_mona(self, v="0") -> str:
         """Return the MONA encoding of a PL atomic formula."""
-        if v != "0":
-            return "({} in {})".format(v, self.s.upper())
-        else:
-            return "(0 in {})".format(self.s.upper())
+        return f"({v} in {self.s.upper()})"
 
 
 class PLBinaryOperator(BinaryOperator[PLFormula], PLFormula, ABC):
@@ -138,14 +106,18 @@ def negate(self) -> "PLFalse":
         """Negate the formula."""
         return PLFalse()
 
-    def find_labels(self) -> Set[Any]:
-        """Return the set of symbols."""
-        return set()
+    def find_labels(self) -> List[Any]:
+        """Return the list of symbols."""
+        return list()
 
     def to_nnf(self):
         """Transform in NNF."""
         return self
 
+    def to_mona(self, v="0") -> str:
+        """Return the MONA encoding of a PL atomic formula."""
+        return Symbols.TRUE.value
+
 
 class PLFalse(PLAtomic):
     """Propositional false."""
@@ -158,14 +130,18 @@ def negate(self) -> "PLTrue":
         """Negate the formula."""
         return PLTrue()
 
-    def find_labels(self) -> Set[Any]:
-        """Return the set of symbols."""
-        return set()
+    def find_labels(self) -> List[Any]:
+        """Return the list of symbols."""
+        return list()
 
     def to_nnf(self):
         """Transform in NNF."""
         return self
 
+    def to_mona(self, v="0") -> str:
+        """Return the MONA encoding of a PL atomic formula."""
+        return Symbols.FALSE.value
+
 
 class PLNot(UnaryOperator[PLFormula], PLFormula):
     """Propositional Not."""
diff --git a/ltlf2dfa/pltlf.py b/ltlf2dfa/pltlf.py
index d2d99d9..2f8bb5f 100644
--- a/ltlf2dfa/pltlf.py
+++ b/ltlf2dfa/pltlf.py
@@ -1,22 +1,39 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """This module contains the implementation of Past Linear Temporal Logic on finite traces."""
 
-from abc import abstractmethod, ABC
-from typing import Set, Optional, Any
 import re
+from abc import ABC, abstractmethod
+from typing import Any, List, Optional
 
 from ltlf2dfa.base import (
-    Formula,
     AtomicFormula,
-    UnaryOperator,
-    BinaryOperator,
     AtomSymbol,
+    BinaryOperator,
+    Formula,
+    UnaryOperator,
 )
+from ltlf2dfa.helpers import new_var
 from ltlf2dfa.ltlf2dfa import to_dfa
 from ltlf2dfa.pl import PLAtomic
-from ltlf2dfa.symbols import Symbols, OpSymbol
-from ltlf2dfa.helpers import new_var
+from ltlf2dfa.symbols import OpSymbol, Symbols
 
 
 class PLTLfFormula(Formula, ABC):
@@ -41,16 +58,20 @@ def to_mona(self, v: Optional[Any] = None) -> str:
         :return: a string.
         """
 
-    # def to_ldlf(self):
+    # def to_pldlf(self):
     #     """
     #     Tranform the formula into an equivalent LDLf formula.
     #
     #     :return: an LDLf formula.
     #     """
 
-    def to_dfa(self) -> str:
-        """Translate into a DFA."""
-        return to_dfa(self)
+    def to_dfa(self, mona_dfa_out: bool = False) -> str:
+        """
+        Translate into a DFA.
+
+        :param mona_dfa_out: flag for DFA output in MONA syntax.
+        """
+        return to_dfa(self, mona_dfa_out)
 
 
 class PLTLfUnaryOperator(UnaryOperator[PLTLfFormula], PLTLfFormula, ABC):
@@ -70,7 +91,7 @@ def negate(self):
         """Negate the formula."""
         return PLTLfNot(self)
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
         return PLAtomic(self.s).find_labels()
 
@@ -79,9 +100,9 @@ def to_mona(self, v="max($)") -> str:
         if v != "max($)":
             return "({} in {})".format(v, self.s.upper())
         else:
-            return PLAtomic(self.s).to_mona()
+            return PLAtomic(self.s).to_mona(v="max($)")
 
-    # def to_ldlf(self):
+    # def to_pldlf(self):
     #     return LDLfPropositional(PLAtomic(self.s)).convert()
 
 
@@ -96,9 +117,9 @@ def negate(self):
         """Negate the formula."""
         return PLTLfFalse()
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding for True."""
@@ -116,9 +137,9 @@ def negate(self):
         """Negate the formula."""
         return PLTLfTrue()
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding for False."""
@@ -148,8 +169,8 @@ def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding of a PLTLf Not formula."""
         return "~({})".format(self.f.to_mona(v))
 
-    # def to_ldlf(self):
-    #     return LDLfNot(self.f.to_ldlf())
+    # def to_pldlf(self):
+    #     return LDLfNot(self.f.to_pldlf())
 
 
 class PLTLfAnd(PLTLfBinaryOperator):
@@ -168,8 +189,8 @@ def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding of a PLTLf And formula."""
         return "({})".format(" & ".join([f.to_mona(v) for f in self.formulas]))
 
-    # def to_ldlf(self):
-    #     return LDLfAnd([f.to_ldlf() for f in self.formulas])
+    # def to_pldlf(self):
+    #     return LDLfAnd([f.to_pldlf() for f in self.formulas])
 
 
 class PLTLfOr(PLTLfBinaryOperator):
@@ -255,24 +276,24 @@ def to_nnf(self) -> PLTLfFormula:
 
     def negate(self) -> PLTLfFormula:
         """Negate the formula."""
-        return PLTLfNot(self.f.negate())
+        return PLTLfNot(self)
 
     def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding of a PLTLf Before formula."""
         ex_var = new_var(v)
         if v != "max($)":
-            return "(ex1 {0}: {0}={1}-1 & {0}>=0 & {2})".format(
+            return "(ex1 {0}: {0} in $ & {0}={1}-1 & {1}>0 & {2})".format(
                 ex_var, v, self.f.to_mona(ex_var)
             )
         else:
-            return "(ex1 {0}: {0}=max($)-1 & max($)>0 & {1})".format(
+            return "(ex1 {0}: {0} in $ & {0}=max($)-1 & max($)>0 & {1})".format(
                 ex_var, self.f.to_mona(ex_var)
             )
 
-    # def to_ldlf(self):
+    # def to_pldlf(self):
     #     return LDLfDiamond(
     #         RegExpPropositional(PLTrue()),
-    #         LDLfAnd([self.f.to_ldlf(), LDLfNot(LDLfEnd())]),
+    #         LDLfAnd([self.f.to_pldlf(), LDLfNot(LDLfEnd())]),
     #     )
 
 
@@ -290,7 +311,7 @@ def to_nnf(self):
 
     def negate(self):
         """Negate the formula."""
-        return PLTLfNot([f.negate() for f in self.formulas])
+        return PLTLfNot(self)
 
     def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding of a PLTLf Since formula."""
@@ -302,27 +323,19 @@ def to_mona(self, v="max($)") -> str:
             if len(self.formulas) > 2
             else self.formulas[1].to_mona(v=ex_var)
         )
-        if v != "max($)":
-            return (
-                "(ex1 {0}: 0<={0}&{0}<={1} & {2} & "
-                "(all1 {3}: {0}<{3}&{3}<={1} => {4}))".format(
-                    ex_var, v, f2, all_var, f1
-                )
-            )
-        else:
-            return (
-                "(ex1 {0}: 0<={0}&{0}<=max($) & {1} & "
-                "(all1 {2}: {0}<{2}&{2}<=max($) => {3}))".format(
-                    ex_var, f2, all_var, f1
-                )
+        return (
+            "(ex1 {0}: {0} in $ & 0<={0}&{0}<={1} & {2} & "
+            "(all1 {3}: {3} in $ & {0}<{3}&{3}<={1} => {4}))".format(
+                ex_var, v, f2, all_var, f1
             )
+        )
 
-    # def to_ldlf(self):
-    #     f1 = self.formulas[0].to_ldlf()
+    # def to_pldlf(self):
+    #     f1 = self.formulas[0].to_pldlf()
     #     f2 = (
-    #         PLTLfSince(self.formulas[1:]).to_ldlf()
+    #         PLTLfSince(self.formulas[1:]).to_pldlf()
     #         if len(self.formulas) > 2
-    #         else self.formulas[1].to_ldlf()
+    #         else self.formulas[1].to_pldlf()
     #     )
     #     return LDLfDiamond(
     #         RegExpStar(RegExpSequence([RegExpTest(f1), RegExpPropositional(PLTrue())])),
@@ -350,10 +363,10 @@ def to_mona(self, v="max($)") -> str:
         """Return the MONA encoding of a PLTLf Once formula."""
         return PLTLfSince([PLTLfTrue(), self.f]).to_mona(v)
 
-    # def to_ldlf(self):
+    # def to_pldlf(self):
     #     return LDLfDiamond(
     #         RegExpStar(RegExpPropositional(PLTrue())),
-    #         LDLfAnd([self.f.to_ldlf(), LDLfNot(LDLfEnd())]),
+    #         LDLfAnd([self.f.to_pldlf(), LDLfNot(LDLfEnd())]),
     #     )
 
 
@@ -365,9 +378,9 @@ def operator_symbol(self) -> OpSymbol:
         """Get the operator symbol."""
         return Symbols.HISTORICALLY.value
 
-    # def to_nnf(self) -> PLTLfFormula:
-    #     """Transform to NNF."""
-    #     return PLTLfRelease([PLTLfFalse(), self.f.to_nnf()])
+    def to_nnf(self) -> PLTLfFormula:
+        """Transform to NNF."""
+        return PLTLfNot(PLTLfSince([PLTLfTrue(), PLTLfNot(self.f.to_nnf())]))
 
     def negate(self) -> PLTLfFormula:
         """Negate the formula."""
@@ -378,8 +391,8 @@ def to_mona(self, v="max($)") -> str:
         return PLTLfNot(PLTLfOnce(PLTLfNot(self.f))).to_mona(v)
 
 
-class PLTLfLast(PLTLfFormula):
-    """Class for the PLTLf Last formula."""
+class PLTLfStart(PLTLfFormula):
+    """Class for the PLTLf Start formula."""
 
     # def to_nnf(self) -> PLTLfFormula:
     #     """Transform to NNF."""
@@ -389,24 +402,28 @@ def negate(self) -> PLTLfFormula:
         """Negate the formula."""
         return self.to_nnf().negate()
 
-    def find_labels(self) -> Set[AtomSymbol]:
+    def find_labels(self) -> List[AtomSymbol]:
         """Find the labels."""
-        return set()
+        return list()
 
     def _members(self):
-        return (Symbols.LAST.value,)
+        return (Symbols.START.value,)
 
     def __str__(self):
         """Get the string representation."""
-        return Symbols.LAST.value
+        return Symbols.START.value
+
+    def to_mona(self, v="max($)") -> str:
+        """Return the MONA encoding of an LTLf Last formula."""
+        return PLTLfNot(PLTLfBefore(PLTLfTrue())).to_mona(v)
 
 
 # class PLTLfEnd(PLTLfFormula):
 #     """Class for the PLTLf End formula."""
 #
-#     def find_labels(self) -> Set[AtomSymbol]:
+#     def find_labels(self) -> List[AtomSymbol]:
 #         """Find the labels."""
-#         return set()
+#         return list()
 #
 #     def _members(self):
 #         return (Symbols.END.value,)
diff --git a/ltlf2dfa/symbols.py b/ltlf2dfa/symbols.py
index bbdc083..17f2634 100644
--- a/ltlf2dfa/symbols.py
+++ b/ltlf2dfa/symbols.py
@@ -1,9 +1,26 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
+
 """This module contains the definition to deal with symbols."""
 from enum import Enum
 from typing import Set
 
-
 OpSymbol = str
 
 
@@ -29,6 +46,7 @@ class Symbols(Enum):
     ROUND_BRACKET_LEFT = "("
     ROUND_BRACKET_RIGHT = ")"
     LAST = "last"
+    START = "start"
     END = "end"
     TRUE = "true"
     FALSE = "false"
diff --git a/mkdocs.yml b/mkdocs.yml
index edcfe12..95f29cc 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -1,12 +1,32 @@
 site_name: LTLf2DFA
+site_url: "https://whitemech.github.io/LTLf2DFA/"
+repo_name: 'whitemech/LTLf2DFA'
+repo_url: "https://github.com/whitemech/LTLf2DFA"
+
 nav:
     - Home: index.md
     - Credits: authors.md
-    - How to contribute: contributing.md
     - Grammars: grammars.md
+    - Change Log: changelog.md
+    - How to contribute: contributing.md
     - References: references.md
 
-theme: readthedocs
+plugins:
+- search
+
+theme:
+  name: material
+
 markdown_extensions:
-    - markdown_include.include:
-        base_path: docs
+- codehilite
+- pymdownx.arithmatex
+- pymdownx.highlight
+- pymdownx.superfences
+- pymdownx.emoji:
+    emoji_index: !!python/name:materialx.emoji.twemoji
+    emoji_generator: !!python/name:materialx.emoji.to_svg
+- markdown_include.include:
+    base_path: docs
+
+extra_javascript:
+- 'https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-MML-AM_CHTML'
diff --git a/scripts/check_copyright.py b/scripts/check_copyright.py
new file mode 100644
index 0000000..1f01809
--- /dev/null
+++ b/scripts/check_copyright.py
@@ -0,0 +1,104 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
+
+"""
+This script checks that all the Python files of the repository have:
+- (optional) the Python shebang
+- the encoding header;
+- the copyright notice;
+
+It is assumed the script is run from the repository root.
+"""
+
+import itertools
+import re
+import sys
+from pathlib import Path
+
+HEADER_REGEX = r"""(#!/usr/bin/env python3
+)?# -\*- coding: utf-8 -\*-
+#
+# This file is part of ltlf2dfa\.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# \(at your option\) any later version\.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE\.  See the
+# GNU General Public License for more details\.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa\.  If not, see <https://www\.gnu\.org/licenses/>\.
+#
+"""
+
+
+def check_copyright(file: Path) -> bool:
+    """
+    Given a file, check if the header stuff is in place.
+
+    Return True if the files has the encoding header and the copyright notice,
+    optionally prefixed by the shebang. Return False otherwise.
+
+    :param file: the file to check.
+    :return True if the file is compliant with the checks, False otherwise.
+    """
+    content = file.read_text()
+    header_regex = re.compile(HEADER_REGEX, re.MULTILINE)
+    return re.match(header_regex, content) is not None
+
+
+def parse_args():
+    """Parse arguments."""
+    import argparse  # pylint: disable=import-outside-toplevel
+
+    parser = argparse.ArgumentParser("check_copyright_notice")
+    parser.add_argument(
+        "--directory", type=str, default=".", help="The path to the repository root."
+    )
+
+
+if __name__ == "__main__":
+    python_files = set(
+        itertools.chain(
+            Path("ltlf2dfa").glob("**/*.py"),
+            Path("tests").glob("**/*.py"),
+            Path("scripts").glob("**/*.py"),
+            [Path("setup.py")],
+        )
+    )
+
+    ignore_files = {}
+
+    bad_files = {
+        filepath
+        for filepath in python_files.difference(ignore_files)
+        if not check_copyright(filepath)
+    }
+
+    if len(bad_files) > 0:
+        print("The following files are not well formatted:")
+        print("\n".join(map(str, bad_files)))
+        sys.exit(1)
+    else:
+        print("OK!")
+        sys.exit(0)
diff --git a/setup.cfg b/setup.cfg
index babfc0a..d508f66 100644
--- a/setup.cfg
+++ b/setup.cfg
@@ -31,15 +31,25 @@ per-file-ignores =
 python_version = 3.7
 strict_optional = True
 
+[isort]
+multi_line_output=3
+include_trailing_comma=True
+force_grid_wrap=0
+use_parentheses=True
+line_length=88
+
 # Per-module options:
 
-[mypy-lark.*]
+[mypy-lark]
 ignore_missing_imports = True
 
-[mypy-sympy.*]
+[mypy-sympy]
 ignore_missing_imports = True
 
 # Per-module options for tests dir:
 
 [mypy-pytest]
 ignore_missing_imports = True
+
+[mypy-pytest.*]
+ignore_missing_imports = True
diff --git a/setup.py b/setup.py
index c89da15..48b62e1 100644
--- a/setup.py
+++ b/setup.py
@@ -1,5 +1,21 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 
 """The setup script."""
 import os
@@ -20,7 +36,7 @@
 
 
 install_requires = [
-    "lark-parser",
+    "lark-parser>=0.9.0,<1",
     "sympy"
 ]
 
@@ -34,7 +50,7 @@
     long_description=readme + '\n\n' + history,
     long_description_content_type="text/markdown",
     classifiers=[
-        'Development Status :: 2 - Pre-Alpha',
+        'Development Status :: 2 - Alpha',
         'Intended Audience :: Education',
         'License :: OSI Approved :: GNU Lesser General Public License v3 or later (LGPLv3+)',
         'Natural Language :: English',
diff --git a/tox.ini b/tox.ini
index 86f69f6..5f902b3 100644
--- a/tox.ini
+++ b/tox.ini
@@ -1,5 +1,5 @@
 [tox]
-envlist = black, docs, flake8, mypy, py3.8, py3.7, py3.6
+envlist = bandit, safety, vulture, check-copyright, black-check, isort-check, docs, flake8, mypy, py3.8, py3.7, py3.6
 
 [testenv]
 setenv =
@@ -8,7 +8,9 @@ deps =
     pytest
     pytest-cov
     pytest-randomly
-
+    ; Main dependencies
+    sympy
+    lark-parser
 commands =
     pytest --basetemp={envtmpdir} --doctest-modules \
         ltlf2dfa tests/ \
@@ -27,42 +29,90 @@ basepython = python3.7
 basepython = python3.8
 
 [testenv:flake8]
+skip_install = True
 deps =
     flake8
-    flake8-docstrings
     flake8-bugbear
+    flake8-docstrings
+    flake8-isort
     pydocstyle
 commands =
     flake8 ltlf2dfa
 
 [testenv:mypy]
+skip_install = True
 deps =
     mypy
 commands =
     mypy ltlf2dfa tests
 
 [testenv:black]
+skip_install = True
 deps = black==19.10b0
-commands = black ltlf2dfa tests
+commands = black ltlf2dfa tests scripts
 
 [testenv:black-check]
+skip_install = True
 deps = black==19.10b0
 commands = black ltlf2dfa tests --check --verbose
 
+[testenv:isort]
+skip_install = True
+deps = isort
+commands = isort ltlf2dfa tests
+
+[testenv:isort-check]
+skip_install = True
+deps = isort
+commands = isort --check-only ltlf2dfa tests
+
+[testenv:bandit]
+skipsdist = True
+skip_install = True
+deps = bandit
+commands = bandit ltlf2dfa tests scripts
+
+[testenv:safety]
+skipsdist = True
+skip_install = True
+deps = safety
+commands = safety check
+
 [testenv:docs]
+skip_install = True
 deps =
     mkdocs
+    mkdocs-material
     markdown-include
     pymdown-extensions
+    markdown==3.2.2
+    mknotebooks==0.6.0.post0.dev2
+    mkdocs-bibtex
 commands =
     mkdocs build --clean
 
 [testenv:docs-serve]
+skip_install = True
 deps =
     mkdocs
+    mkdocs-material
     markdown-include
     pymdown-extensions
+    markdown==3.2.2
+    mknotebooks==0.6.0.post0.dev2
+    mkdocs-bibtex
 commands =
     mkdocs build --clean
     python -c 'print("###### Starting local server. Press Control+C to stop server ######")'
-    mkdocs serve
\ No newline at end of file
+    mkdocs serve
+
+[testenv:check-copyright]
+skip_install = True
+deps =
+commands = python scripts/check_copyright.py
+
+[testenv:vulture]
+skipsdist = True
+skip_install = True
+deps = vulture
+commands = vulture ltlf2dfa --min-confidence 65


Test patch:
diff --git a/.github/workflows/pythonpackage.yml b/.github/workflows/test.yml
similarity index 77%
rename from .github/workflows/pythonpackage.yml
rename to .github/workflows/test.yml
index 317a22e..ab82e42 100644
--- a/.github/workflows/pythonpackage.yml
+++ b/.github/workflows/test.yml
@@ -1,4 +1,4 @@
-name: LTLf2DFA CI pipeline.
+name: test
 
 on:
   push:
@@ -27,12 +27,6 @@ jobs:
         python-version: ${{ matrix.python-version }}
     - name: Install dependencies
       run:  pip install tox
-    - name: Code style check
-      run: |
-        tox -e black
-        tox -e flake8
-    - name: Static type check
-      run: tox -e mypy
     - name: Unit tests and coverage
       run: |
         tox -e py${{ matrix.python-version }}
@@ -44,6 +38,4 @@ jobs:
         flags: unittests
         name: codecov-umbrella
         yml: ./codecov.yml
-        fail_ci_if_error: true
-    - name: Generate Documentation
-      run: tox -e docs
+        fail_ci_if_error: true
\ No newline at end of file
diff --git a/tests/__init__.py b/tests/__init__.py
index c039b2b..ae2a18e 100644
--- a/tests/__init__.py
+++ b/tests/__init__.py
@@ -1,2 +1,19 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """This module contains the tests for the ltlf2dfa tool."""
diff --git a/tests/conftest.py b/tests/conftest.py
index 18a5102..73596ae 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -1,4 +1,21 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """This module contains the configurations for the tests."""
 import inspect
 import os
diff --git a/tests/parsing.py b/tests/parsing.py
index 8bf2bd9..518ed11 100644
--- a/tests/parsing.py
+++ b/tests/parsing.py
@@ -1,9 +1,27 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Small helper class to check the correct parsing."""
 
+from typing import List, Optional, Tuple
+
 from lark import Lark
-from lark.lexer import Token
-from typing import List, Tuple, Optional
+from lark.lexer import Token  # type: ignore
 
 
 class ParsingCheck:
diff --git a/tests/test_ltlf.py b/tests/test_ltlf.py
index 73d8e56..180c108 100644
--- a/tests/test_ltlf.py
+++ b/tests/test_ltlf.py
@@ -1,32 +1,51 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Test LTLf."""
-import pytest
 import os
+
 import lark
+import pytest
 
 from ltlf2dfa.ltlf import (
-    LTLfAtomic,
+    LTLfAlways,
     LTLfAnd,
+    LTLfAtomic,
     LTLfEquivalence,
-    LTLfOr,
-    LTLfNot,
-    LTLfImplies,
     LTLfEventually,
-    LTLfAlways,
-    LTLfUntil,
-    LTLfRelease,
+    LTLfFalse,
+    LTLfImplies,
+    LTLfLast,
     LTLfNext,
-    LTLfWeakNext,
+    LTLfNot,
+    LTLfOr,
+    LTLfRelease,
     LTLfTrue,
-    LTLfFalse,
+    LTLfUntil,
+    LTLfWeakNext,
 )
 from ltlf2dfa.parser.ltlf import LTLfParser
 
-# from ltlf2dfa.pl import PLAtomic, PLTrue, PLFalse, PLAnd, PLOr
-
 # from .conftest import LTLfFixtures
 from .parsing import ParsingCheck
 
+# from ltlf2dfa.pl import PLAtomic, PLTrue, PLFalse, PLAnd, PLOr
+
 
 def test_parser():
     parser = LTLfParser()
@@ -56,6 +75,8 @@ def test_parser():
         ]
     )
 
+    assert parser("a & last") == LTLfAnd([a, LTLfLast()])
+
 
 def test_names():
 
@@ -130,42 +151,56 @@ def test_mona():
         == "((~((0 in A)) | ~((0 in B))) & ((0 in A) | (0 in B)))"
     )
 
+    f = parser("a & last")
+    assert (
+        f.to_mona(v="0")
+        == "((0 in A) & ((0 = max($)) | (ex1 v_1: v_1 in $ & v_1=1 & false)))"
+    )
+
     # Next and Weak Next
     f = parser("X(a & b)")
-    assert f.to_mona(v="0") == "(ex1 v_1: v_1=1 & ((v_1 in A) & (v_1 in B)))"
+    assert f.to_mona(v="0") == "(ex1 v_1: v_1 in $ & v_1=1 & ((v_1 in A) & (v_1 in B)))"
+
+    f = parser("WX(a)")
+    assert (
+        f.to_mona(v="0") == "((0 = max($)) | (ex1 v_1: v_1 in $ & v_1=1 & (v_1 in A)))"
+    )
+
+    # f = parser("F(b & WX false) -> F(a & (WX false | X(WX false)))")
+    # assert f.to_mona(v="0") == ""
 
     f = parser("WX (a & b)")
     assert (
         f.to_mona(v="0")
-        == "((0 = max($)) | (ex1 v_1: v_1=1 & ((v_1 in A) & (v_1 in B))))"
+        == "((0 = max($)) | (ex1 v_1: v_1 in $ & v_1=1 & ((v_1 in A) & (v_1 in B))))"
     )
 
     # Until and Release
     f = parser("a U b")
     assert (
         f.to_mona(v="0")
-        == "(ex1 v_1: 0<=v_1&v_1<=max($) & (v_1 in B) & (all1 v_2: 0<=v_2&v_2<v_1"
+        == "(ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & (v_1 in B) & (all1 v_2: v_2 in $ & 0<=v_2&v_2<v_1"
         " => (v_2 in A)))"
     )
     f = parser("a R b")
     assert (
         f.to_mona(v="0")
-        == "((ex1 v_1: 0<=v_1&v_1<=max($) & (v_1 in A) & (all1 v_2: 0<=v_2&v_2<=v_1"
-        " => (v_2 in B))) | (all1 v_2: 0<=v_2&v_2<=max($) => (v_2 in B)))"
+        == "((ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & (v_1 in A) & (all1 v_2: v_2 in $ & 0<=v_2&v_2<=v_1"
+        " => (v_2 in B))) | (all1 v_2: v_2 in $ & 0<=v_2&v_2<=max($) => (v_2 in B)))"
     )
 
     # Eventually and Always
     f = parser("F(a & b)")
     assert (
         f.to_mona(v="0")
-        == "(ex1 v_1: 0<=v_1&v_1<=max($) & ((v_1 in A) & (v_1 in B)) & (all1 v_2: "
-        "0<=v_2&v_2<v_1 => true))"
+        == "(ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & ((v_1 in A) & (v_1 in B)) & (all1 v_2: "
+        "v_2 in $ & 0<=v_2&v_2<v_1 => true))"
     )
     f = parser("G(a | b)")
     assert (
         f.to_mona(v="0")
-        == "((ex1 v_1: 0<=v_1&v_1<=max($) & false & (all1 v_2: 0<=v_2&v_2<=v_1 => "
-        "((v_2 in A) | (v_2 in B)))) | (all1 v_2: 0<=v_2&v_2<=max($) => ((v_2 in A) "
+        == "((ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & false & (all1 v_2: v_2 in $ & 0<=v_2&v_2<=v_1 => "
+        "((v_2 in A) | (v_2 in B)))) | (all1 v_2: v_2 in $ & 0<=v_2&v_2<=max($) => ((v_2 in A) "
         "| (v_2 in B))))"
     )
 
diff --git a/tests/test_ltlf2dfa.py b/tests/test_ltlf2dfa.py
index a0e7b73..bd12d3b 100644
--- a/tests/test_ltlf2dfa.py
+++ b/tests/test_ltlf2dfa.py
@@ -1,6 +1,26 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Test the ltlf2dfa tool."""
 
+from sympy import And, Not, Or, Symbol, simplify, symbols
+
+from ltlf2dfa.ltlf2dfa import simplify_guard, ter2symb
 from ltlf2dfa.parser.ltlf import LTLfParser
 from ltlf2dfa.parser.pltlf import PLTLfParser
 
@@ -9,7 +29,8 @@ def test_ltlf_dfa():
     parser = LTLfParser()
 
     f = parser("a")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
+    mona_dfa = f.to_dfa(mona_dfa_out=True)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -25,10 +46,33 @@ def test_ltlf_dfa():
  2 -> 2 [label="true"];
  3 -> 3 [label="true"];
 }"""
+    expected_mona = """DFA for formula with free variables: A 
+Initial state: 0
+Accepting states: 3 
+Rejecting states: 0 1 2 
+
+Automaton has 4 states and 4 BDD-nodes
+Transitions:
+State 0: X -> state 1
+State 1: 0 -> state 2
+State 1: 1 -> state 3
+State 2: X -> state 2
+State 3: X -> state 3
+A counter-example of least length (0) is:
+A               X 
+
+A = {}
+
+A satisfying example of least length (1) is:
+A               X 1
+
+A = {0}"""
+
     assert dfa == expected
+    assert mona_dfa == expected_mona
 
     f = parser("true")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -44,7 +88,7 @@ def test_ltlf_dfa():
     assert dfa == expected
 
     f = parser("false")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -60,47 +104,43 @@ def test_ltlf_dfa():
     assert dfa == expected
 
     f = parser("G a")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 3;
+ node [shape = doublecircle]; 1;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
  1 -> 2 [label="~a"];
- 1 -> 3 [label="a"];
+ 1 -> 1 [label="a"];
  2 -> 2 [label="true"];
- 3 -> 2 [label="~a"];
- 3 -> 3 [label="a"];
 }"""
     assert dfa == expected
 
     f = parser("F(a & b)")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 3;
+ node [shape = doublecircle]; 2;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
- 1 -> 2 [label="~a | ~b"];
- 1 -> 3 [label="a & b"];
- 2 -> 2 [label="~a | ~b"];
- 2 -> 3 [label="a & b"];
- 3 -> 3 [label="true"];
+ 1 -> 1 [label="~a | ~b"];
+ 1 -> 2 [label="a & b"];
+ 2 -> 2 [label="true"];
 }"""
     assert dfa == expected
 
     f = parser("X(a)")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -120,7 +160,7 @@ def test_ltlf_dfa():
     assert dfa == expected
 
     f = parser("a U b")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected1 = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -162,54 +202,149 @@ def test_ltlf_dfa():
     assert dfa == expected1 or expected2
 
     f = parser("G(a) & F(b)")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 4;
+ node [shape = doublecircle]; 3;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
  1 -> 2 [label="~a"];
- 1 -> 3 [label="a & ~b"];
- 1 -> 4 [label="a & b"];
+ 1 -> 1 [label="a & ~b"];
+ 1 -> 3 [label="a & b"];
  2 -> 2 [label="true"];
  3 -> 2 [label="~a"];
- 3 -> 3 [label="a & ~b"];
- 3 -> 4 [label="a & b"];
- 4 -> 2 [label="~a"];
- 4 -> 4 [label="a"];
+ 3 -> 3 [label="a"];
 }"""
     assert dfa == expected
 
 
+def test_ltlf_mona_dfa():
+    parser = LTLfParser()
+
+    f = parser("a")
+    mona_dfa = f.to_dfa(mona_dfa_out=True)
+    expected_mona = """DFA for formula with free variables: A 
+Initial state: 0
+Accepting states: 3 
+Rejecting states: 0 1 2 
+
+Automaton has 4 states and 4 BDD-nodes
+Transitions:
+State 0: X -> state 1
+State 1: 0 -> state 2
+State 1: 1 -> state 3
+State 2: X -> state 2
+State 3: X -> state 3
+A counter-example of least length (0) is:
+A               X 
+
+A = {}
+
+A satisfying example of least length (1) is:
+A               X 1
+
+A = {0}"""
+
+    assert mona_dfa == expected_mona
+
+    f = parser("true")
+    mona_dfa = f.to_dfa(mona_dfa_out=True)
+    expected_mona = """DFA for formula with free variables: 
+Initial state: 0
+Accepting states: 1 
+Rejecting states: 0 
+
+Automaton has 2 states and 1 BDD-node
+Transitions:
+State 0:  -> state 1
+State 1:  -> state 1
+Formula is valid
+A satisfying example of least length (0) is:"""
+    assert mona_dfa == expected_mona
+
+    f = parser("false")
+    mona_dfa = f.to_dfa(mona_dfa_out=True)
+    expected_mona = """DFA for formula with free variables: 
+Initial state: 0
+Accepting states: 
+Rejecting states: 0 
+
+Automaton has 1 state and 1 BDD-node
+Transitions:
+State 0:  -> state 0
+Formula is unsatisfiable
+
+A counter-example of least length (0) is:"""
+    assert mona_dfa == expected_mona
+
+    f = parser("G a")
+    mona_dfa = f.to_dfa(mona_dfa_out=True)
+    expected_mona = """DFA for formula with free variables: A 
+Initial state: 0
+Accepting states: 1 
+Rejecting states: 0 2 
+
+Automaton has 3 states and 3 BDD-nodes
+Transitions:
+State 0: X -> state 1
+State 1: 0 -> state 2
+State 1: 1 -> state 1
+State 2: X -> state 2
+A counter-example of least length (1) is:
+A               X 0
+
+A = {}
+
+A satisfying example of least length (0) is:
+A               X 
+
+A = {}"""
+    assert mona_dfa == expected_mona
+
+    f1 = parser("F(WX(false))")
+    f2 = parser("F(!(X(!(false))))")
+    mona_dfa_1 = f1.to_dfa(mona_dfa_out=True)
+    mona_dfa_2 = f2.to_dfa(mona_dfa_out=True)
+    assert mona_dfa_1 == mona_dfa_2
+
+    f1 = parser("F(b & WX false) -> F(a & (WX false | X(WX false)))")
+    f2 = parser(
+        "((! (F (! ((! b) || (X (! false)))))) || (F (! ((! a) || (! ((! (X (! false))) || (X (! (X (! false))))))))))"
+    )
+    mona_dfa_1 = f1.to_dfa(mona_dfa_out=True)
+    mona_dfa_2 = f2.to_dfa(mona_dfa_out=True)
+    assert mona_dfa_1 == mona_dfa_2
+
+
 def test_pltlf_dfa():
     parser = PLTLfParser()
 
     f = parser("a")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 3;
+ node [shape = doublecircle]; 2;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
- 1 -> 2 [label="~a"];
- 1 -> 3 [label="a"];
- 2 -> 2 [label="true"];
- 3 -> 3 [label="true"];
+ 1 -> 1 [label="~a"];
+ 1 -> 2 [label="a"];
+ 2 -> 1 [label="~a"];
+ 2 -> 2 [label="a"];
 }"""
     assert dfa == expected
 
     f = parser("true")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -225,7 +360,7 @@ def test_pltlf_dfa():
     assert dfa == expected
 
     f = parser("false")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
@@ -241,111 +376,271 @@ def test_pltlf_dfa():
     assert dfa == expected
 
     f = parser("H a")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 3;
+ node [shape = doublecircle]; 1;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
  1 -> 2 [label="~a"];
- 1 -> 3 [label="a"];
+ 1 -> 1 [label="a"];
  2 -> 2 [label="true"];
- 3 -> 2 [label="~a"];
- 3 -> 3 [label="a"];
 }"""
     assert dfa == expected
 
     f = parser("O(a & b)")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 3;
+ node [shape = doublecircle]; 2;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
- 1 -> 2 [label="~a | ~b"];
- 1 -> 3 [label="a & b"];
- 2 -> 2 [label="~a | ~b"];
- 2 -> 3 [label="a & b"];
- 3 -> 3 [label="true"];
+ 1 -> 1 [label="~a | ~b"];
+ 1 -> 2 [label="a & b"];
+ 2 -> 2 [label="true"];
 }"""
     assert dfa == expected
 
     f = parser("Y(a)")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 4; 5;
+ node [shape = doublecircle]; 3; 4;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
- 1 -> 2 [label="~a"];
- 1 -> 3 [label="a"];
- 2 -> 2 [label="~a"];
- 2 -> 3 [label="a"];
- 3 -> 4 [label="~a"];
- 3 -> 5 [label="a"];
- 4 -> 2 [label="~a"];
- 4 -> 3 [label="a"];
- 5 -> 4 [label="~a"];
- 5 -> 5 [label="a"];
+ 1 -> 1 [label="~a"];
+ 1 -> 2 [label="a"];
+ 2 -> 3 [label="~a"];
+ 2 -> 4 [label="a"];
+ 3 -> 1 [label="~a"];
+ 3 -> 2 [label="a"];
+ 4 -> 3 [label="~a"];
+ 4 -> 4 [label="a"];
 }"""
     assert dfa == expected
 
     f = parser("a S b")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 3;
+ node [shape = doublecircle]; 2;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
- 1 -> 2 [label="~b"];
- 1 -> 3 [label="b"];
- 2 -> 2 [label="~b"];
- 2 -> 3 [label="b"];
- 3 -> 2 [label="~a & ~b"];
- 3 -> 3 [label="a | b"];
+ 1 -> 1 [label="~b"];
+ 1 -> 2 [label="b"];
+ 2 -> 1 [label="~a & ~b"];
+ 2 -> 2 [label="a | b"];
 }"""
     assert dfa == expected
 
     f = parser("H(a) & O(b)")
-    dfa = f.to_dfa()
+    dfa = f.to_dfa(mona_dfa_out=False)
     expected = """digraph MONA_DFA {
  rankdir = LR;
  center = true;
  size = "7.5,10.5";
  edge [fontname = Courier];
  node [height = .5, width = .5];
- node [shape = doublecircle]; 4;
+ node [shape = doublecircle]; 3;
  node [shape = circle]; 1;
  init [shape = plaintext, label = ""];
  init -> 1;
  1 -> 2 [label="~a"];
- 1 -> 3 [label="a & ~b"];
- 1 -> 4 [label="a & b"];
+ 1 -> 1 [label="a & ~b"];
+ 1 -> 3 [label="a & b"];
  2 -> 2 [label="true"];
  3 -> 2 [label="~a"];
- 3 -> 3 [label="a & ~b"];
- 3 -> 4 [label="a & b"];
- 4 -> 2 [label="~a"];
- 4 -> 4 [label="a"];
+ 3 -> 3 [label="a"];
+}"""
+    assert dfa == expected
+
+    f = parser("a & O(b)")
+
+    dfa = f.to_dfa(mona_dfa_out=False)
+    expected = """digraph MONA_DFA {
+ rankdir = LR;
+ center = true;
+ size = "7.5,10.5";
+ edge [fontname = Courier];
+ node [height = .5, width = .5];
+ node [shape = doublecircle]; 3;
+ node [shape = circle]; 1;
+ init [shape = plaintext, label = ""];
+ init -> 1;
+ 1 -> 1 [label="~b"];
+ 1 -> 2 [label="b & ~a"];
+ 1 -> 3 [label="a & b"];
+ 2 -> 2 [label="~a"];
+ 2 -> 3 [label="a"];
+ 3 -> 2 [label="~a"];
+ 3 -> 3 [label="a"];
 }"""
     assert dfa == expected
+
+    f = parser("H(Y(a))")
+
+    dfa = f.to_dfa(mona_dfa_out=False)
+    expected = """digraph MONA_DFA {
+ rankdir = LR;
+ center = true;
+ size = "7.5,10.5";
+ edge [fontname = Courier];
+ node [height = .5, width = .5];
+ node [shape = doublecircle]; 1;
+ node [shape = circle]; 1;
+ init [shape = plaintext, label = ""];
+ init -> 1;
+ 1 -> 2 [label="true"];
+ 2 -> 2 [label="true"];
+}"""
+    assert dfa == expected
+
+
+def test_ter2symb():
+    ap = symbols("a b c")
+
+    tern_0 = "X"
+    actual = ter2symb(None, tern_0)
+    expected = And()
+    assert expected == actual
+
+    tern_1 = "0X"
+    actual = ter2symb(ap, tern_1)
+    expected = And(Not(Symbol("a")))
+    assert expected == actual
+
+    tern_2 = "10"
+    actual = ter2symb(ap, tern_2)
+    expected = And(Symbol("a"), Not(Symbol("b")))
+    assert expected == actual
+
+    tern_3 = "0X1"
+    actual = ter2symb(ap, tern_3)
+    expected = And(Not(Symbol("a")), Symbol("c"))
+    assert expected == actual
+
+    ap = symbols("a b c d e f g h i")
+    tern_4 = "0X110XX01"
+    actual = ter2symb(ap, tern_4)
+    expected = And(
+        Not(Symbol("a")),
+        Symbol("c"),
+        Symbol("d"),
+        Not(Symbol("e")),
+        Not(Symbol("h")),
+        Symbol("i"),
+    )
+    assert expected == actual
+
+
+def test_simplify_guard():
+    ap = symbols("a b c")
+
+    tern_1 = "0XX"
+    tern_2 = "10X"
+    tern_3 = "110"
+    sym_1 = ter2symb(ap, tern_1)
+    sym_2 = ter2symb(ap, tern_2)
+    sym_3 = ter2symb(ap, tern_3)
+
+    actual = simplify_guard([sym_1, sym_2, sym_3])
+    expected = Or(Not(Symbol("a")), Not(Symbol("b")), Not(Symbol("c")))
+    assert expected == actual
+
+    ap = symbols("a b c d e f g h")
+
+    tern_1 = "0XXXXXXX"
+    tern_2 = "10XXXXXX"
+    tern_3 = "110XXXXX"
+    tern_4 = "1110XXXX"
+    tern_5 = "11110XXX"
+    tern_6 = "111110XX"
+    tern_7 = "1111110X"
+    tern_8 = "11111110"
+    sym_1 = ter2symb(ap, tern_1)
+    sym_2 = ter2symb(ap, tern_2)
+    sym_3 = ter2symb(ap, tern_3)
+    sym_4 = ter2symb(ap, tern_4)
+    sym_5 = ter2symb(ap, tern_5)
+    sym_6 = ter2symb(ap, tern_6)
+    sym_7 = ter2symb(ap, tern_7)
+    sym_8 = ter2symb(ap, tern_8)
+
+    actual = simplify_guard([sym_1, sym_2, sym_3, sym_4, sym_5, sym_6, sym_7, sym_8])
+    expected = Or(
+        Not(Symbol("a")),
+        Not(Symbol("b")),
+        Not(Symbol("c")),
+        Not(Symbol("d")),
+        Not(Symbol("e")),
+        Not(Symbol("f")),
+        Not(Symbol("g")),
+        Not(Symbol("h")),
+    )
+    assert expected == actual
+
+    sym_1 = Not(Symbol("a"))
+    sym_2 = And(Symbol("a"), Not(Symbol("b")))
+    sym_3 = And(Symbol("a"), Symbol("b"), Not(Symbol("c")))
+    sym_4 = And(Symbol("a"), Symbol("b"), Symbol("c"), Not(Symbol("d")))
+    sym_5 = And(Symbol("a"), Symbol("b"), Symbol("c"), Symbol("d"), Not(Symbol("e")))
+    sym_6 = And(
+        Symbol("a"),
+        Symbol("b"),
+        Symbol("c"),
+        Symbol("d"),
+        Symbol("e"),
+        Not(Symbol("f")),
+    )
+    sym_7 = And(
+        Symbol("a"),
+        Symbol("b"),
+        Symbol("c"),
+        Symbol("d"),
+        Symbol("e"),
+        Symbol("f"),
+        Not(Symbol("g")),
+    )
+    sym_8 = And(
+        Symbol("a"),
+        Symbol("b"),
+        Symbol("c"),
+        Symbol("d"),
+        Symbol("e"),
+        Symbol("f"),
+        Symbol("g"),
+        Not(Symbol("h")),
+    )
+
+    actual = simplify_guard([sym_1, sym_2, sym_3, sym_4, sym_5, sym_6, sym_7, sym_8])
+    expected = Or(
+        Not(Symbol("a")),
+        Not(Symbol("b")),
+        Not(Symbol("c")),
+        Not(Symbol("d")),
+        Not(Symbol("e")),
+        Not(Symbol("f")),
+        Not(Symbol("g")),
+        Not(Symbol("h")),
+    )
+    assert expected == actual
diff --git a/tests/test_misc.py b/tests/test_misc.py
index 2583d8b..e450965 100644
--- a/tests/test_misc.py
+++ b/tests/test_misc.py
@@ -1,4 +1,21 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Misc tests."""
 import os
 
@@ -11,7 +28,7 @@ def test_ltlf_example_readme():
     parsed_formula = parser(formula)
 
     assert str(parsed_formula) == "G((a -> X(b)))"
-    assert parsed_formula.find_labels() == {c for c in "ab"}
+    assert parsed_formula.find_labels() == [c for c in "ab"]
 
     # dfa = parsed_formula.to_dfa()
 
@@ -24,15 +41,16 @@ def test_pltlf_example_readme():
     parsed_formula = parser(formula)
 
     assert str(parsed_formula) == "H((a -> Y(b)))"
-    assert parsed_formula.find_labels() == {c for c in "ab"}
+    assert parsed_formula.find_labels() == [c for c in "ab"]
 
     # dfa = parsed_formula.to_dfa()
 
 
 def test_hash_consistency_after_pickling():
-    from ltlf2dfa.parser.ltlf import LTLfParser
     import pickle
 
+    from ltlf2dfa.parser.ltlf import LTLfParser
+
     parser = LTLfParser()
     formula = "F (a & !b)"
     old_obj = parser(formula)
@@ -49,8 +67,8 @@ def test_hash_consistency_after_pickling():
 
 def test_QuotedFormula():
     from ltlf2dfa.base import QuotedFormula
+    from ltlf2dfa.ltlf import LTLfAnd, LTLfAtomic
     from ltlf2dfa.parser.ltlf import LTLfParser
-    from ltlf2dfa.ltlf import LTLfAtomic, LTLfAnd
 
     f = LTLfParser()("!(G a)")
     qf = QuotedFormula(f)
diff --git a/tests/test_pl.py b/tests/test_pl.py
index b8a40e1..7769cbd 100644
--- a/tests/test_pl.py
+++ b/tests/test_pl.py
@@ -1,45 +1,99 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Test the Propositional Logic."""
 import os
-import pytest
+
 import lark
+import pytest
 
 from ltlf2dfa.parser.pl import PLParser
 from ltlf2dfa.pl import (
     PLAnd,
     PLAtomic,
-    PLNot,
     PLEquivalence,
-    PLOr,
-    PLImplies,
     PLFalse,
+    PLImplies,
+    PLNot,
+    PLOr,
     PLTrue,
 )
+
 from .parsing import ParsingCheck
 
 
 def test_parser():
     parser = PLParser()
-    sa, sb = "A", "B"
-    a, b = PLAtomic(sa), PLAtomic(sb)
+    sa, sb, sc = "A", "B", "C"
+    a, b, c = PLAtomic(sa), PLAtomic(sb), PLAtomic(sc)
+    parsed_a = parser("A")
+    assert parsed_a == a
+
+    parsed_b = parser("B")
+    assert parsed_b == b
+
+    parsed_not_a = parser("~A")
+    assert parsed_not_a == PLNot(a)
 
     a_and_b = parser("A & B")
     true_a_and_b = PLAnd([a, b])
     assert a_and_b == true_a_and_b
 
+    a_or_b = parser("A | B")
+    true_a_or_b = PLOr([a, b])
+    assert a_or_b == true_a_or_b
+
     material_implication = parser("!A | B <-> !(A & !B) <-> A->B")
     true_material_implication = PLEquivalence(
         [PLOr([PLNot(a), b]), PLNot(PLAnd([a, PLNot(b)])), PLImplies([a, b])]
     )
-
     assert material_implication == true_material_implication
 
+    a_imply_b = parser("A -> B")
+    true_a_imply_b = PLImplies([a, b])
+    assert a_imply_b == true_a_imply_b
+
+    a_imply_b_imply_c = parser("A -> B -> C")
+    true_a_imply_b_imply_c = PLImplies([a, b, c])
+    assert a_imply_b_imply_c == true_a_imply_b_imply_c
+
     true_a_and_false_and_true = PLAnd([a, PLFalse(), PLTrue()])
     a_and_false_and_true = parser("A & false & true")
-
     assert a_and_false_and_true == true_a_and_false_and_true
 
 
+def test_negate():
+    sa, sb, sc = "A", "B", "c"
+    a, b, c = PLAtomic(sa), PLAtomic(sb), PLAtomic(sc)
+
+    a_and_b = PLAnd([a, b])
+    not_a_or_not_b = PLOr([PLNot(a), PLNot(b)])
+    assert a_and_b.negate() == not_a_or_not_b
+
+    a_and_b_and_c = PLAnd([a, b, c])
+    not_a_or_not_b_or_not_c = PLOr([PLNot(a), PLNot(b), PLNot(c)])
+    assert a_and_b_and_c.negate() == not_a_or_not_b_or_not_c
+
+    a_or_b = PLOr([a, b])
+    not_a_and_not_b = PLAnd([PLNot(a), PLNot(b)])
+    assert a_or_b.negate() == not_a_and_not_b
+
+
 def test_nnf():
     parser = PLParser()
     sa, sb = "A", "B"
@@ -68,12 +122,46 @@ def test_find_labels():
     # complete formula
     f = "!A | B <-> !(A & !B) <-> A->B"
     formula = parser(f)
-    assert formula.find_labels() == {"A", "B"}
+    assert formula.find_labels() == ["A", "B"]
+
+    # more than one character
+    f = "!A & (!AB & !A0)"
+    formula = parser(f)
+    assert formula.find_labels() == [c for c in ["A", "AB", "A0"]]
+
+    # another formula
+    f = "!A | B <-> !(C & !B) <-> C->A"
+    formula = parser(f)
+    assert formula.find_labels() == ["A", "B", "C"]
+
+
+def test_find_atomics():
+    parser = PLParser()
+    sa, sb, sab, sa0 = "A", "B", "AB", "A0"
+    a, b, ab, a0 = PLAtomic(sa), PLAtomic(sb), PLAtomic(sab), PLAtomic(sa0)
+
+    # complete formula
+    f = "!A | B <-> !(A & !B) <-> A->B"
+    formula = parser(f)
+    assert formula.find_atomics() == {a, b}
 
     # more than one character
     f = "!A & (!AB & !A0)"
     formula = parser(f)
-    assert formula.find_labels() == {c for c in {"A", "AB", "A0"}}
+    assert formula.find_atomics() == {c for c in {a, ab, a0}}
+
+
+def test_mona():
+    # parser = PLParser()
+    a, b, c = [PLAtomic(c) for c in "abc"]
+    true = PLTrue()
+    false = PLFalse()
+
+    assert a.to_mona(v="0") == "(0 in A)"
+    assert b.to_mona(v="0") == "(0 in B)"
+    assert c.to_mona(v="0") == "(0 in C)"
+    assert true.to_mona(v="0") == "true"
+    assert false.to_mona(v="0") == "false"
 
 
 def test_names():
diff --git a/tests/test_pltlf.py b/tests/test_pltlf.py
index 85bba32..3d19464 100644
--- a/tests/test_pltlf.py
+++ b/tests/test_pltlf.py
@@ -1,30 +1,49 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
+#
+# This file is part of ltlf2dfa.
+#
+# ltlf2dfa is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# ltlf2dfa is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with ltlf2dfa.  If not, see <https://www.gnu.org/licenses/>.
+#
 """Test PLTLf."""
-import pytest
 import os
+
 import lark
+import pytest
 
+from ltlf2dfa.parser.pltlf import PLTLfParser
 from ltlf2dfa.pltlf import (
-    PLTLfAtomic,
     PLTLfAnd,
+    PLTLfAtomic,
+    PLTLfBefore,
     PLTLfEquivalence,
-    PLTLfOr,
-    PLTLfNot,
+    PLTLfFalse,
+    PLTLfHistorically,
     PLTLfImplies,
+    PLTLfNot,
     PLTLfOnce,
-    PLTLfHistorically,
+    PLTLfOr,
     PLTLfSince,
-    PLTLfBefore,
+    PLTLfStart,
     PLTLfTrue,
-    PLTLfFalse,
 )
-from ltlf2dfa.parser.pltlf import PLTLfParser
-
-# from ltlf2dfa.pl import PLAtomic, PLTrue, PLFalse, PLAnd, PLOr
 
 # from .conftest import LTLfFixtures
 from .parsing import ParsingCheck
 
+# from ltlf2dfa.pl import PLAtomic, PLTrue, PLFalse, PLAnd, PLOr
+
 
 def test_parser():
     parser = PLTLfParser()
@@ -40,6 +59,8 @@ def test_parser():
 
     assert parser("(Y a)") == PLTLfBefore(a)
 
+    assert parser("a & O(b)") == PLTLfAnd([a, PLTLfOnce(b)])
+
     assert parser("(O (a&b)) <-> !(H (!a | !b) )") == PLTLfEquivalence(
         [
             PLTLfOnce(PLTLfAnd([a, b])),
@@ -49,6 +70,34 @@ def test_parser():
 
     assert parser("(a S b S !c)") == PLTLfSince([a, b, PLTLfNot(c)])
 
+    assert parser("a & start") == PLTLfAnd([a, PLTLfStart()])
+
+
+def test_negate():
+    parser = PLTLfParser()
+    sa, sb, sc = "a", "b", "c"
+    a, b, c = PLTLfAtomic(sa), PLTLfAtomic(sb), PLTLfAtomic(sc)
+
+    a_and_b = PLTLfAnd([a, b])
+    not_a_or_not_b = PLTLfOr([PLTLfNot(a), PLTLfNot(b)])
+    assert a_and_b.negate() == not_a_or_not_b
+
+    a_and_b_and_c = PLTLfAnd([a, b, c])
+    not_a_or_not_b_or_not_c = PLTLfOr([PLTLfNot(a), PLTLfNot(b), PLTLfNot(c)])
+    assert a_and_b_and_c.negate() == not_a_or_not_b_or_not_c
+
+    before_a = PLTLfBefore(a)
+    not_before_a = PLTLfNot(PLTLfBefore(a))
+    assert before_a.negate() == not_before_a
+
+    once_a = PLTLfOnce(a)
+    not_true_since_a = PLTLfNot(PLTLfSince([PLTLfTrue(), a]))
+    assert once_a.negate() == not_true_since_a
+
+    historically_a = PLTLfHistorically(a)
+    true_since_not_a = PLTLfSince([PLTLfTrue(), PLTLfNot(a)])
+    assert historically_a.negate() == true_since_not_a
+
 
 def test_names():
 
@@ -107,36 +156,36 @@ def test_mona():
     tt = PLTLfTrue()
     ff = PLTLfFalse()
 
-    assert a.to_mona(v="max($)") == "(0 in A)"
-    assert b.to_mona(v="max($)") == "(0 in B)"
-    assert c.to_mona(v="max($)") == "(0 in C)"
+    assert a.to_mona(v="max($)") == "(max($) in A)"
+    assert b.to_mona(v="max($)") == "(max($) in B)"
+    assert c.to_mona(v="max($)") == "(max($) in C)"
     assert tt.to_mona(v="max($)") == "true"
     assert ff.to_mona(v="max($)") == "false"
 
     f = parser("!(a & !b)")
-    assert f.to_mona(v="max($)") == "~(((0 in A) & ~((0 in B))))"
+    assert f.to_mona(v="max($)") == "~(((max($) in A) & ~((max($) in B))))"
 
     f = parser("!(!a | b)")
-    assert f.to_mona(v="max($)") == "~((~((0 in A)) | (0 in B)))"
+    assert f.to_mona(v="max($)") == "~((~((max($) in A)) | (max($) in B)))"
 
     f = parser("!(a <-> b)")
     assert (
         f.to_nnf().to_mona(v="max($)")
-        == "((~((0 in A)) | ~((0 in B))) & ((0 in A) | (0 in B)))"
+        == "((~((max($) in A)) | ~((max($) in B))) & ((max($) in A) | (max($) in B)))"
     )
 
     # Before
     f = parser("Y(a & b)")
     assert (
         f.to_mona(v="max($)")
-        == "(ex1 v_1: v_1=max($)-1 & max($)>0 & ((v_1 in A) & (v_1 in B)))"
+        == "(ex1 v_1: v_1 in $ & v_1=max($)-1 & max($)>0 & ((v_1 in A) & (v_1 in B)))"
     )
 
     # Since
     f = parser("a S b")
     assert (
         f.to_mona(v="max($)")
-        == "(ex1 v_1: 0<=v_1&v_1<=max($) & (v_1 in B) & (all1 v_2: v_1<v_2&v_2<=max($)"
+        == "(ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & (v_1 in B) & (all1 v_2: v_2 in $ & v_1<v_2&v_2<=max($)"
         " => (v_2 in A)))"
     )
 
@@ -144,14 +193,20 @@ def test_mona():
     f = parser("O(a & b)")
     assert (
         f.to_mona(v="max($)")
-        == "(ex1 v_1: 0<=v_1&v_1<=max($) & ((v_1 in A) & (v_1 in B)) & (all1 v_2: "
-        "v_1<v_2&v_2<=max($) => true))"
+        == "(ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & ((v_1 in A) & (v_1 in B)) & (all1 v_2: "
+        "v_2 in $ & v_1<v_2&v_2<=max($) => true))"
+    )
+    f = parser("a & O(b)")
+    assert (
+        f.to_mona(v="max($)")
+        == "((max($) in A) & (ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & (v_1 in B) & (all1 v_2: v_2 in $ & v_1<v_2&v_2<=max($) => "
+        "true)))"
     )
     f = parser("H(a | b)")
     assert (
         f.to_mona(v="max($)")
-        == "~((ex1 v_1: 0<=v_1&v_1<=max($) & ~(((v_1 in A) | (v_1 in B))) & (all1 v_2: "
-        "v_1<v_2&v_2<=max($) => true)))"
+        == "~((ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & ~(((v_1 in A) | (v_1 in B))) & (all1 v_2: "
+        "v_2 in $ & v_1<v_2&v_2<=max($) => true)))"
     )