Merge branch 'master' of github.com:khovanskiy/verification-course

Merged

Author: Alexander Loboda

data/LTLParser.ltl.correct

@@ -1 +1,4 @@
-G(('E(variable)' | 'E(array)') -> F'S(VOC)')
+true
+'S(state0)' -> FG true
+G(('E(variable)' | 'E(array)') -> F'S(VOC)')
+G(('E(see_minus)' | 'E(vertical_line)') -> (F'S(NestedMachine)' | F'S(ForkMachine)' | F'S(NameWithArrow)' | F'S(Fork)'))

data/LTLParser.ltl.incorrect

@@ -1 +1,3 @@
-G(('E(see_minus)' | 'E(vertical_line)') -> (F'S(NestedMachine)' | F'S(ForkMachine)'))
+false
+G('E(machine_name)' -> F'A(WriteToken)')
+G(('E(see_minus)' | 'E(vertical_line)') -> (F'S(NestedMachine)' | F'S(ForkMachine)'))

src/main/antlr4/model/ltl/LTL.g4

@@ -57,9 +57,9 @@ primary returns [Formula<String> f]
     {
         $f = $ltl.f;
     }
-    |   NOT primary
+    |   NOT ltl
     {
-        $f = LTL.not($primary.f);
+        $f = LTL.not($ltl.f);
     }
     ;