Merge pull request #71 from whitemech/develop

Release 0.1.0
whitemech · Jun 7, 2021 · ea1949c · ea1949c
2 parents 8b3f7d9 + c04fc5e
commit ea1949c
Show file tree

Hide file tree

Showing 33 changed files with 1,101 additions and 712 deletions.
diff --git a/HISTORY.md b/HISTORY.md
@@ -1,12 +1,27 @@
 # History
 
-## 0.1.0a0
+## 0.1.0 (2021-06-07)
 
-- Support for Propositional Logic parsing, 
+- Improved to the behaviour of `Not`:
+  - Make `Not` to simplify when argument is a boolean formula. If `Not` is applied to `TrueFormula`, then the output is `FalseFormula`; 
+    likewise, if it is applied to `FalseFormula`, the output is `TrueFormula`.
+  - Fix: replace `__neg__` with `__invert__`
+- Improved simplification of monotone operators: check also
+  the presence of `phi OP ~phi` and reduce according to the 
+  binary operator involved.
+- Added tests to check consistency between code and documentation.
+- Updated grammars so to be compliant with 
+  version `0.2.0` of [this standard](https://marcofavorito.me/tl-grammars/v/7d9a17267fbf525d9a6a1beb92a46f05cf652db6/).
+
+
+
+## 0.1.0a0 (2021-04-23)
+
+- Added support for Propositional Logic parsing, 
   syntax representation and parsing.
-- Support for Linear Temporal Logic
+- Added support for Linear Temporal Logic
   parsing and syntax representation.
-- Support for Past Linear Temporal Logic
+- Added support for Past Linear Temporal Logic
   parsing and syntax representation.
-- Support for Linear Dynamic Logic 
+- Added support for Linear Dynamic Logic 
   parsing and syntax representation.
diff --git a/README.md b/README.md
@@ -58,7 +58,7 @@ A Python library for logic formalisms representation and manipulation.
 
 To install the package from PyPI:
 ```
-pip install pylogics==0.1.0a0
+pip install pylogics
 ```
 
 ## Tests

diff --git a/docs/grammars.md b/docs/grammars.md
@@ -18,24 +18,24 @@ start: propositional_formula
 ?prop_and: prop_not (AND prop_not)*
 ?prop_not: NOT* prop_wrapped
 ?prop_wrapped: prop_atom
-            | LSEPARATOR propositional_formula RSEPARATOR
+            | LEFT_PARENTHESIS propositional_formula RIGHT_PARENTHESIS
 ?prop_atom: atom
-	     | prop_true
-	     | prop_false
+         | prop_true
+         | prop_false
 
 atom: SYMBOL_NAME
 prop_true: TRUE
 prop_false: FALSE
 
-LSEPARATOR : "("
-RSEPARATOR : ")"
+LEFT_PARENTHESIS : "("
+RIGHT_PARENTHESIS : ")"
 EQUIVALENCE : "<->"
 IMPLY : ">>"|"->"
 OR: "||"|"|"
 AND: "&&"|"&"
 NOT: "!"|"~"
-TRUE.2: /(?i:true)/
-FALSE.2: /(?i:false)/
+TRUE.2: /true/
+FALSE.2: /false/
 
 // Symbols cannot contain uppercase letters, because these are reserved
 // Moreover, any word between quotes is a symbol
@@ -76,28 +76,35 @@ start: ltlf_formula
 ?ltlf_weak_next:   WEAK_NEXT ltlf_unaryop
 ?ltlf_not:         NOT ltlf_unaryop
 ?ltlf_wrapped:     ltlf_atom
-             |     LSEPARATOR ltlf_formula RSEPARATOR
+             |     LEFT_PARENTHESIS ltlf_formula RIGHT_PARENTHESIS
 ?ltlf_atom:        ltlf_symbol
           |        ltlf_true
           |        ltlf_false
+          |        ltlf_tt
+          |        ltlf_ff
           |        ltlf_last
 
 ltlf_symbol: SYMBOL_NAME
 ltlf_true: prop_true
 ltlf_false: prop_false
+ltlf_tt: TT
+ltlf_ff: FF
 ltlf_last: LAST
 
 UNTIL.2: "U"
-RELEASE.2: "R"
+RELEASE.2:  /R|V/
 ALWAYS.2: "G"
 EVENTUALLY.2: "F"
-NEXT.2: "X"
-WEAK_NEXT.2: "N"
+NEXT.2: "X[!]"
+WEAK_NEXT.2: "X"
 WEAK_UNTIL.2: "W"
 STRONG_RELEASE.2: "M"
 
-END.2: /(?i:end)/
-LAST.2: /(?i:last)/
+END.2: /end/
+LAST.2: /last/
+
+TT.2: /tt/
+FF.2: /ff/
 
 %ignore /\s+/
 
@@ -109,8 +116,8 @@ LAST.2: /(?i:last)/
 %import  .pl.AND -> AND
 %import  .pl.EQUIVALENCE -> EQUIVALENCE
 %import  .pl.IMPLY -> IMPLY
-%import  .pl.LSEPARATOR -> LSEPARATOR
-%import  .pl.RSEPARATOR -> RSEPARATOR
+%import  .pl.LEFT_PARENTHESIS -> LEFT_PARENTHESIS
+%import  .pl.RIGHT_PARENTHESIS -> RIGHT_PARENTHESIS
 ```
 
 ## Past Linear Temporal Logic
@@ -140,23 +147,30 @@ start: pltlf_formula
 ?pltlf_before:       BEFORE pltlf_unaryop
 ?pltlf_not:          NOT pltlf_unaryop
 ?pltlf_wrapped:      pltlf_atom
-             |       LSEPARATOR pltlf_formula RSEPARATOR
+             |       LEFT_PARENTHESIS pltlf_formula RIGHT_PARENTHESIS
 ?pltlf_atom:       pltlf_symbol
            |       pltlf_true
            |       pltlf_false
+           |       pltlf_tt
+           |       pltlf_ff
            |       pltlf_start
+           |       pltlf_first
 
 pltlf_symbol: SYMBOL_NAME
 pltlf_true: prop_true
 pltlf_false: prop_false
+pltlf_tt: TT
+pltlf_ff: FF
 pltlf_start: START
+pltlf_first: FIRST
 
 // Operators must not be part of a word
 SINCE.2: "S"
 HISTORICALLY.2: "H"
 ONCE.2: "O"
 BEFORE.2: "Y"
-START.2: /(?i:start)/
+FIRST.2: /first/
+START.2: /start/
 
 %ignore /\s+/
 
@@ -168,8 +182,10 @@ START.2: /(?i:start)/
 %import  .pl.AND -> AND
 %import  .pl.EQUIVALENCE -> EQUIVALENCE
 %import  .pl.IMPLY -> IMPLY
-%import  .pl.LSEPARATOR -> LSEPARATOR
-%import  .pl.RSEPARATOR -> RSEPARATOR
+%import  .pl.LEFT_PARENTHESIS -> LEFT_PARENTHESIS
+%import  .pl.RIGHT_PARENTHESIS -> RIGHT_PARENTHESIS
+%import  .ltl.TT -> TT
+%import  .ltl.FF -> FF
 ```
 
 ## Linear Dynamic Logic
@@ -181,32 +197,26 @@ and it is reported below:
 ```lark
 start: ldlf_formula
 
-?ldlf_formula:  ldlf_equivalence
+?ldlf_formula:     ldlf_equivalence
 ?ldlf_equivalence: ldlf_implication (EQUIVALENCE ldlf_implication)*
 ?ldlf_implication: ldlf_or (IMPLY ldlf_or)*
-?ldlf_or: ldlf_and (OR ldlf_and)*
-?ldlf_and: ldlf_unaryop (AND ldlf_unaryop)*
+?ldlf_or:          ldlf_and (OR ldlf_and)*
+?ldlf_and:         ldlf_unaryop (AND ldlf_unaryop)*
 
 ?ldlf_unaryop:     ldlf_box
              |     ldlf_diamond
              |     ldlf_not
              |     ldlf_wrapped
-?ldlf_box: BOXLSEPARATOR regular_expression BOXRSEPARATOR ldlf_unaryop
-?ldlf_diamond: DIAMONDLSEPARATOR regular_expression DIAMONDRSEPARATOR ldlf_unaryop
-?ldlf_not: NOT ldlf_unaryop
+?ldlf_box:         LEFT_SQUARE_BRACKET regular_expression RIGHT_SQUARE_BRACKET ldlf_unaryop
+?ldlf_diamond:     LEFT_ANGLE_BRACKET regular_expression RIGHT_ANGLE_BRACKET ldlf_unaryop
+?ldlf_not:         NOT ldlf_unaryop
 ?ldlf_wrapped:    ldlf_atom
-             |    LSEPARATOR ldlf_formula RSEPARATOR
-?ldlf_atom:   ldlf_tt
-          |   ldlf_ff
-          |   ldlf_last
-          |   ldlf_end
-          |   ldlf_prop_true
-          |   ldlf_prop_false
-          |   ldlf_prop_atom
-
-ldlf_prop_true: TRUE
-ldlf_prop_false: FALSE
-ldlf_prop_atom: SYMBOL_NAME
+             |    LEFT_PARENTHESIS ldlf_formula RIGHT_PARENTHESIS
+?ldlf_atom:       ldlf_tt
+          |       ldlf_ff
+          |       ldlf_last
+          |       ldlf_end
+
 
 ldlf_tt: TT
 ldlf_ff: FF
@@ -218,23 +228,21 @@ regular_expression: re_union
 ?re_union:      re_sequence (UNION re_sequence)*
 ?re_sequence:   re_star (SEQ re_star)*
 ?re_star:       re_test STAR?
-?re_test:       TEST ldlf_formula
+?re_test:       ldlf_formula TEST
         |       re_wrapped
 ?re_wrapped:    re_propositional
-           |    LSEPARATOR regular_expression RSEPARATOR
+           |    LEFT_PARENTHESIS regular_expression RIGHT_PARENTHESIS
 re_propositional: propositional_formula
 
 
-BOXLSEPARATOR: "["
-BOXRSEPARATOR: "]"
-DIAMONDLSEPARATOR: "<"
-DIAMONDRSEPARATOR: ">"
+LEFT_SQUARE_BRACKET: "["
+RIGHT_SQUARE_BRACKET: "]"
+LEFT_ANGLE_BRACKET: "<"
+RIGHT_ANGLE_BRACKET: ">"
 UNION: "+"
 SEQ: ";"
 TEST: "?"
 STAR: "*"
-TT.2: /(?i:tt)/
-FF.2: /(?i:ff)/
 
 %ignore /\s+/
 
@@ -247,8 +255,10 @@ FF.2: /(?i:ff)/
 %import  .pl.OR -> OR
 %import  .pl.AND -> AND
 %import  .pl.NOT -> NOT
-%import  .pl.LSEPARATOR -> LSEPARATOR
-%import  .pl.RSEPARATOR -> RSEPARATOR
-%import .ltl.LAST -> LAST
-%import .ltl.END -> END
+%import  .pl.LEFT_PARENTHESIS -> LEFT_PARENTHESIS
+%import  .pl.RIGHT_PARENTHESIS -> RIGHT_PARENTHESIS
+%import  .ltl.LAST -> LAST
+%import  .ltl.END -> END
+%import  .ltl.TT -> TT
+%import  .ltl.FF -> FF
 ```
diff --git a/docs/introduction.md b/docs/introduction.md
@@ -9,7 +9,7 @@ on [temporal logics](https://plato.stanford.edu/entries/logic-temporal/).
 > API might be broken frequently or may contain bugs :bug:.
 
 > :warning: Docs are not thorough and might be inaccurate.
-> Apologizes.
+> Apologies.
 
 ## Quickstart
 

diff --git a/docs/parsing.md b/docs/parsing.md
@@ -17,6 +17,11 @@ The library uses [Lark](https://lark-parser.readthedocs.io/en/latest/)
 to generate the parser automatically.
 The grammar files are reported at [this page](grammars.md).
 
+The syntax for `LTL`, `PLTL` and `LDL`
+aims to be compliant with 
+[this specification](https://marcofavorito.me/tl-grammars/v/7d9a17267fbf525d9a6a1beb92a46f05cf652db6/).
+
+
 ## Symbols
 
 A symbol is determined by the following regular expression:
@@ -45,8 +50,8 @@ pl_formula: pl_formula <-> pl_formula  // equivalence
           | pl_formula &&  pl_formula  // conjunction 
           | !pl_formula                // negation
           | ( pl_formula )             // brackets 
-          | true                       // boolean constant
-          | false                      // boolean constant
+          | true                       // boolean propositional constant
+          | false                      // boolean propositional constant
           | SYMBOL                     // prop. atom
 ```
 
@@ -81,20 +86,26 @@ ltl_formula: ltl_formula <-> ltl_formula  // equivalence
            | ltl_formula M ltl_formula    // strong release 
            | F ltl_formula                // eventually 
            | G ltl_formula                // always 
-           | X ltl_formula                // next 
-           | N ltl_formula                // weak next 
-           | true                         // boolean constant
-           | false                        // boolean constant
-           | SYMBOL                       // prop. atom
+           | X[!] ltl_formula             // next 
+           | X ltl_formula                // weak next 
+           | true                         // boolean propositional constant
+           | false                        // boolean propositional constant
+           | tt                           // boolean logical constant
+           | ff                           // boolean logical constant
+           | SYMBOL                       // propositional atom
 ```
 
 Some examples:
 ```python
 from pylogics.parsers import parse_ltl
+parse_ltl("tt")
+parse_ltl("ff")
+parse_ltl("true")
+parse_ltl("false")
 parse_ltl("a")
 parse_ltl("b")
 parse_ltl("X(a)")
-parse_ltl("N(b)")
+parse_ltl("X[!](b)")
 parse_ltl("F(a)")
 parse_ltl("G(b)")
 parse_ltl("G(a -> b)")
@@ -118,14 +129,20 @@ pltl_formula: pltl_formula <-> pltl_formula  // equivalence
             | H pltl_formula                 // historically
             | O pltl_formula                 // once 
             | Y pltl_formula                 // before 
-            | true                           // boolean constant
-            | false                          // boolean constant
-            | SYMBOL                         // prop. atom
+            | true                           // boolean propositional constant
+            | false                          // boolean propositional constant
+            | tt                             // boolean logical constant
+            | ff                             // boolean logical constant
+            | SYMBOL                         // propositional atom
 ```
 
 Some examples:
 ```python
 from pylogics.parsers import parse_pltl
+parse_pltl("tt")
+parse_pltl("ff")
+parse_pltl("true")
+parse_pltl("false")
 parse_pltl("a")
 parse_pltl("b")
 parse_pltl("Y(a)")
@@ -172,5 +189,5 @@ parse_ldl("<a + b>tt")
 parse_ldl("<a ; b><c>tt")
 parse_ldl("<(a ; b)*><c>tt")
 parse_ldl("<true><a>tt")  # Next a
-parse_ldl("<(?<a>tt;true)*>(<b>tt)")  # (a Until b) in LDLf
+parse_ldl("<(<a>tt?;true)*>(<b>tt)")  # (a Until b) in LDLf
 ```
diff --git a/docs/syntax.md b/docs/syntax.md
@@ -91,8 +91,8 @@ described above.
 For LDL, you can use the following classes,
 defined in `pylogics.syntax.ldl`:
 
-- `LDLTrue`, the boolean positive constant `tt`
-- `LDLFalse`, the boolean negative constant `ff`
+- `TrueFormula(logic=Logic.LDL)`, the boolean positive constant `tt`
+- `FalseFormula(logic=Logic.LDL)`, the boolean negative constant `ff`
 - `Diamond(regex, ldlf_formula)`
 - `Box(regex, ldlf_formula)`
 

diff --git a/mkdocs.yml b/mkdocs.yml
@@ -1,6 +1,7 @@
 site_name: PyLogics Docs
+site_url: "https://whitemech.github.io/pylogics/"
 repo_name: 'marcofavorito/pylogics'
-repo_url: https://github.com/marcofavorito/pylogics
+repo_url: "https://github.com/marcofavorito/pylogics"
 
 nav:
 - Home: index.md