From feb33f601eb0c1611ef7345015f6708aa82c57ec Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Wed, 27 May 2015 12:12:16 +0200
Subject: [PATCH 01/36] Work in progress: New CTL grammar

---
 src/main/antlr4/CTL.g4    |  6 ++---
 src/main/antlr4/CTLnew.g4 | 57 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 3 deletions(-)
 create mode 100644 src/main/antlr4/CTLnew.g4

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 40a19ba..6e24375 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -2,7 +2,7 @@
 
 grammar CTL;
 
-@header { 
+@header {
 import cz.muni.fi.ctl.formula.Formula;
 import cz.muni.fi.ctl.formula.FormulaImpl;
 import cz.muni.fi.ctl.formula.operator.Operator;
@@ -16,14 +16,14 @@ import cz.muni.fi.ctl.formula.proposition.Tautology;
 import java.util.HashMap; 
 import java.util.List;
 import java.util.Map;
-} 
+}
 
 root locals [
     Map<String, Proposition> propositions = new HashMap<>(),
     Formula result
     ] : ctl; 
 
-ctl : 
+ctl :
       define ctl
     | property
 ;
diff --git a/src/main/antlr4/CTLnew.g4 b/src/main/antlr4/CTLnew.g4
new file mode 100644
index 0000000..39e2ced
--- /dev/null
+++ b/src/main/antlr4/CTLnew.g4
@@ -0,0 +1,57 @@
+
+grammar CTLnew;
+
+root :
+    | NEWLINE
+    | include root
+    | property root;
+
+PROP : '#property';
+INCL : '#include';
+
+include :
+    INCL QUOTE PATH QUOTE NEWLINE;
+
+property :
+    PROP VAR_NAME IS formula NEWLINE;
+
+formula:
+    bool | formula binary formula | EXISTS formula UNTIL formula | B_OPEN formula B_CLOSE;
+
+binary:
+    AND | OR | IMPL | EQIV;
+
+/* Terminals: */
+    bool : TRUE | FALSE ;
+    TRUE : 'True';
+    FALSE : 'False';
+
+    /* Boolean Operators */
+        NEG : '!';
+        AND : '&&';
+        OR : '||';
+        IMPL : '=>';
+        EQIV : '<=>';
+    /* Temporal Operators */
+        ALL : 'A';
+        EXISTS : 'E';
+        UNTIL : 'U';
+    /* Comparison operators */
+        EQ : '==';
+        N_EQ : '!=';
+        GT : '>';
+        LT : '<';
+        GT_EQ : '>=';
+        LT_EQ : '<=';
+    /* Brackets */
+        B_OPEN : '(';
+        B_CLOSE : ')';
+    /* Values */
+        VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
+        FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
+        PATH : [a-zA-Z/.]+[a-zA-Z0-9]*;
+
+        IS : '=';
+        QUOTE : '"';
+        NEWLINE: [\n]*;
+    WS : [ \t\n]+ -> skip ; // toss out whitespace
\ No newline at end of file

From 8b66821e2f09114d31745f27278e49ec16b2ae53 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 22:33:57 +0200
Subject: [PATCH 02/36] New grammar, supports imports, direction propositions,
 comments, lots of fancy stufff

---
 src/main/antlr4/CTL.g4    | 203 ++++++++++++++------------------------
 src/main/antlr4/CTLnew.g4 |  57 -----------
 2 files changed, 76 insertions(+), 184 deletions(-)
 delete mode 100644 src/main/antlr4/CTLnew.g4

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 6e24375..72fb51c 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -1,129 +1,78 @@
-/* Grammar for CTL parser */
-
-grammar CTL;
-
-@header {
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.FormulaImpl;
-import cz.muni.fi.ctl.formula.operator.Operator;
-import cz.muni.fi.ctl.formula.operator.BinaryOperator;
-import cz.muni.fi.ctl.formula.operator.UnaryOperator;
-import cz.muni.fi.ctl.formula.proposition.Contradiction;
-import cz.muni.fi.ctl.formula.proposition.FloatProposition;
-import cz.muni.fi.ctl.formula.proposition.Proposition;
-import cz.muni.fi.ctl.formula.proposition.Tautology;
-
-import java.util.HashMap; 
-import java.util.List;
-import java.util.Map;
-}
-
-root locals [
-    Map<String, Proposition> propositions = new HashMap<>(),
-    Formula result
-    ] : ctl; 
-
-ctl :
-      define ctl
-    | property
-;
-
-define : 
-           DEF 
-           VAR_NAME { String name = $VAR_NAME.text; } 
-           VAR_NAME { String prop = $VAR_NAME.text; } 
-           op_float 
-           FLOAT_VAL
-    {
-        if ($root::propositions.containsKey(name)) {
-            throw new IllegalArgumentException("Redefinition of proposition "+name);
-        }
-        $root::propositions.put( name,
-            new FloatProposition(
-                Double.parseDouble($FLOAT_VAL.text),
-                prop,
-                $op_float.op
-                )
-        );
-    }
-;
-
-property : PROP formula { $root::result = $property::formula().processed; };
-
-formula returns [ Formula processed ] : 
-          TRUE 
-          { $processed = Tautology.INSTANCE; }
-        | FALSE 
-          { $processed = Contradiction.INSTANCE; }
-        | VAR_NAME
-          { $processed = $root::propositions.get($VAR_NAME.text);
-            if ($processed == null) throw new IllegalArgumentException("Unknown proposition: "+$VAR_NAME.text);
-          }
-        | NEG formula
-          { $processed = new FormulaImpl(UnaryOperator.NEGATION, $formula.ctx.formula.processed ); }
-        | B_OPEN formula op_bool formula B_CLOSE
-          { $processed = new FormulaImpl($op_bool.op, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); }
-        | EXISTS B_OPEN formula UNTIL formula B_CLOSE
-          { $processed = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); }
-        | ALL B_OPEN formula UNTIL formula B_CLOSE
-          { $processed = new FormulaImpl(BinaryOperator.ALL_UNTIL, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); }
-        | temporal formula
-          { $processed = new FormulaImpl($temporal.op, $formula.ctx.formula(0).processed ); }
+
+grammar Playground;
+
+/* Main format structure */
+
+root : (statement break)*;
+
+statement : '#include' STRING                       # include
+          | VAR_NAME '=' formula                    # assign
+          | '#check' formula (',' formula)*         # check
+          ;
+
+break : NEWLINE+ | EOF;
+
+/* Formula and propositions */
+
+formula : VAR_NAME                                          #id
+        | (TRUE | FALSE)                                    #bool
+        | VAR_NAME ':' ('in'|'out') ('+'|'-')               #direction
+        | VAR_NAME float_op FLOAT_VAL                       #proposition
+        | '(' formula ')'                                   #parenthesis
+        | unary_op formula                                  #unary
+        | formula bool_op formula                           #binary
+        | 'E' formula 'U' formula                           #existUntil
+        | 'A' formula 'U' formula                           #allUntil
         ;
 
-temporal returns [ Operator op ] :                                     
-                                    'EX' { $op = UnaryOperator.EXISTS_NEXT; }
-                                    | 'AX' { $op = UnaryOperator.ALL_NEXT; }
-                                    | 'EF' { $op = UnaryOperator.EXISTS_FUTURE; }
-                                    | 'AF' { $op = UnaryOperator.ALL_FUTURE; }
-                                    | 'EG' { $op = UnaryOperator.EXISTS_GLOBAL; }
-                                    | 'AG' { $op = UnaryOperator.ALL_GLOBAL; }
-                                 ;
-
-op_bool returns [ Operator op ] : 
-          AND { $op = BinaryOperator.AND; } 
-        | OR { $op = BinaryOperator.OR; } 
-        | IMPL { $op = BinaryOperator.IMPLICATION; } 
-        | EQIV { $op = BinaryOperator.EQUIVALENCE; }
-;
-
-op_float returns [ FloatProposition.Operator op ] : 
-          EQ { $op = FloatProposition.Operator.EQ; } 
-        | N_EQ { $op = FloatProposition.Operator.NEQ; } 
-        | GT { $op = FloatProposition.Operator.GT; } 
-        | LT { $op = FloatProposition.Operator.LT; }
-        | GT_EQ { $op = FloatProposition.Operator.GT_EQ; } 
-        | LT_EQ { $op = FloatProposition.Operator.LT_EQ; }
-; 
-
-DEF : '#define';
-PROP : '#property';
-
-/* Terminals: */
-    bool : TRUE | FALSE ;
-    TRUE : 'True';
-    FALSE : 'False';
-    /* Boolean Operators */
-        NEG : '!';
-        AND : '&&';
-        OR : '||';
-        IMPL : '=>';
-        EQIV : '<=>';
-    /* Temporal Operators */
-        ALL : 'A';
-        EXISTS : 'E';
-        UNTIL : 'U';
-    /* Comparison operators */
-        EQ : '==';
-        N_EQ : '!=';
-        GT : '>';
-        LT : '<';
-        GT_EQ : '>=';
-        LT_EQ : '<=';
-    /* Brackets */
-        B_OPEN : '(';
-        B_CLOSE : ')';
-    /* Values */
-        VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
-        FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
-    WS : [ \t\n]+ -> skip ; // toss out whitespace
\ No newline at end of file
+/** Helper/Grouping parser rules **/
+
+unary_op : NEG | EX | EF | EG | AX | AF | AG;
+bool_op : CON | DIS | IMPL | EQIV;
+float_op : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
+
+/** Terminals **/
+
+TRUE : ([tT]'rue' | 'tt' | 'TT');
+FALSE : ([fF]'alse' | 'ff' | 'FF');
+
+IN : 'in';
+OUT : 'out';
+
+PLUS : '+';
+MINUS : '-';
+
+/** Operators **/
+
+EX : 'EX';
+EF : 'EF';
+EG : 'EG';
+AX : 'AX';
+AF : 'AF';
+AG : 'AG';
+
+EQ : '==';
+NEQ : '!=';
+GT : '>';
+LT : '<';
+GTEQ : '>=';
+LTEQ : '<=';
+
+NEG : '!';
+CON : '&&';
+DIS : '||';
+IMPL : '=>';
+EQIV : '<=>';
+
+/* Literals */
+
+STRING : ["].+?["]; //non-greedy match till next quotation mark
+VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
+FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
+
+NEWLINE : '\r'?'\n';
+
+WS : [ \t\u]+ -> channel(HIDDEN) ;
+
+Block_comment : '/*' (Block_comment|.)*? '*/' -> channel(HIDDEN) ; // nesting allow
+Line_comment : '//' .*? '\n' -> channel(HIDDEN) ;
\ No newline at end of file
diff --git a/src/main/antlr4/CTLnew.g4 b/src/main/antlr4/CTLnew.g4
deleted file mode 100644
index 39e2ced..0000000
--- a/src/main/antlr4/CTLnew.g4
+++ /dev/null
@@ -1,57 +0,0 @@
-
-grammar CTLnew;
-
-root :
-    | NEWLINE
-    | include root
-    | property root;
-
-PROP : '#property';
-INCL : '#include';
-
-include :
-    INCL QUOTE PATH QUOTE NEWLINE;
-
-property :
-    PROP VAR_NAME IS formula NEWLINE;
-
-formula:
-    bool | formula binary formula | EXISTS formula UNTIL formula | B_OPEN formula B_CLOSE;
-
-binary:
-    AND | OR | IMPL | EQIV;
-
-/* Terminals: */
-    bool : TRUE | FALSE ;
-    TRUE : 'True';
-    FALSE : 'False';
-
-    /* Boolean Operators */
-        NEG : '!';
-        AND : '&&';
-        OR : '||';
-        IMPL : '=>';
-        EQIV : '<=>';
-    /* Temporal Operators */
-        ALL : 'A';
-        EXISTS : 'E';
-        UNTIL : 'U';
-    /* Comparison operators */
-        EQ : '==';
-        N_EQ : '!=';
-        GT : '>';
-        LT : '<';
-        GT_EQ : '>=';
-        LT_EQ : '<=';
-    /* Brackets */
-        B_OPEN : '(';
-        B_CLOSE : ')';
-    /* Values */
-        VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
-        FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
-        PATH : [a-zA-Z/.]+[a-zA-Z0-9]*;
-
-        IS : '=';
-        QUOTE : '"';
-        NEWLINE: [\n]*;
-    WS : [ \t\n]+ -> skip ; // toss out whitespace
\ No newline at end of file

From 9e9cb44c3fb1b844c5f9859285992a73fd5fa5ce Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 22:34:53 +0200
Subject: [PATCH 03/36] Correctly mark generated sources root as project srcDir

---
 build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index 4a65eec..cc9bfee 100644
--- a/build.gradle
+++ b/build.gradle
@@ -31,7 +31,7 @@ antlr4 {
 compileJava.dependsOn antlr4
 
 // add the generated source files to the list of java sources
-sourceSets.main.java.srcDirs += antlr4.output
+sourceSets.main.java.srcDirs += new File('src/main/gen')
 
 // add antlr4 to classpath
 configurations {

From 74e4dcbd7e7c61cbf4208bfb4dac850a50cf3ce5 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 22:33:57 +0200
Subject: [PATCH 04/36] New grammar, supports imports, direction propositions,
 comments, lots of fancy stufff

---
 src/main/antlr4/CTL.g4    | 197 ++++++++++++++------------------------
 src/main/antlr4/CTLnew.g4 |  57 -----------
 2 files changed, 73 insertions(+), 181 deletions(-)
 delete mode 100644 src/main/antlr4/CTLnew.g4

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 6e24375..15412cd 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -1,129 +1,78 @@
-/* Grammar for CTL parser */
 
 grammar CTL;
 
-@header {
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.FormulaImpl;
-import cz.muni.fi.ctl.formula.operator.Operator;
-import cz.muni.fi.ctl.formula.operator.BinaryOperator;
-import cz.muni.fi.ctl.formula.operator.UnaryOperator;
-import cz.muni.fi.ctl.formula.proposition.Contradiction;
-import cz.muni.fi.ctl.formula.proposition.FloatProposition;
-import cz.muni.fi.ctl.formula.proposition.Proposition;
-import cz.muni.fi.ctl.formula.proposition.Tautology;
-
-import java.util.HashMap; 
-import java.util.List;
-import java.util.Map;
-}
-
-root locals [
-    Map<String, Proposition> propositions = new HashMap<>(),
-    Formula result
-    ] : ctl; 
-
-ctl :
-      define ctl
-    | property
-;
-
-define : 
-           DEF 
-           VAR_NAME { String name = $VAR_NAME.text; } 
-           VAR_NAME { String prop = $VAR_NAME.text; } 
-           op_float 
-           FLOAT_VAL
-    {
-        if ($root::propositions.containsKey(name)) {
-            throw new IllegalArgumentException("Redefinition of proposition "+name);
-        }
-        $root::propositions.put( name,
-            new FloatProposition(
-                Double.parseDouble($FLOAT_VAL.text),
-                prop,
-                $op_float.op
-                )
-        );
-    }
-;
-
-property : PROP formula { $root::result = $property::formula().processed; };
-
-formula returns [ Formula processed ] : 
-          TRUE 
-          { $processed = Tautology.INSTANCE; }
-        | FALSE 
-          { $processed = Contradiction.INSTANCE; }
-        | VAR_NAME
-          { $processed = $root::propositions.get($VAR_NAME.text);
-            if ($processed == null) throw new IllegalArgumentException("Unknown proposition: "+$VAR_NAME.text);
-          }
-        | NEG formula
-          { $processed = new FormulaImpl(UnaryOperator.NEGATION, $formula.ctx.formula.processed ); }
-        | B_OPEN formula op_bool formula B_CLOSE
-          { $processed = new FormulaImpl($op_bool.op, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); }
-        | EXISTS B_OPEN formula UNTIL formula B_CLOSE
-          { $processed = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); }
-        | ALL B_OPEN formula UNTIL formula B_CLOSE
-          { $processed = new FormulaImpl(BinaryOperator.ALL_UNTIL, $formula.ctx.formula(0).processed, $formula.ctx.formula(1).processed ); }
-        | temporal formula
-          { $processed = new FormulaImpl($temporal.op, $formula.ctx.formula(0).processed ); }
+/* Main format structure */
+
+root : (statement break)*;
+
+statement : '#include' STRING                       # include
+          | VAR_NAME '=' formula                    # assign
+          | '#check' formula (',' formula)*         # check
+          ;
+
+break : NEWLINE+ | EOF;
+
+/* Formula and propositions */
+
+formula : VAR_NAME                                          #id
+        | (TRUE | FALSE)                                    #bool
+        | VAR_NAME ':' ('in'|'out') ('+'|'-')               #direction
+        | VAR_NAME float_op FLOAT_VAL                       #proposition
+        | '(' formula ')'                                   #parenthesis
+        | unary_op formula                                  #unary
+        | formula bool_op formula                           #binary
+        | 'E' formula 'U' formula                           #existUntil
+        | 'A' formula 'U' formula                           #allUntil
         ;
 
-temporal returns [ Operator op ] :                                     
-                                    'EX' { $op = UnaryOperator.EXISTS_NEXT; }
-                                    | 'AX' { $op = UnaryOperator.ALL_NEXT; }
-                                    | 'EF' { $op = UnaryOperator.EXISTS_FUTURE; }
-                                    | 'AF' { $op = UnaryOperator.ALL_FUTURE; }
-                                    | 'EG' { $op = UnaryOperator.EXISTS_GLOBAL; }
-                                    | 'AG' { $op = UnaryOperator.ALL_GLOBAL; }
-                                 ;
-
-op_bool returns [ Operator op ] : 
-          AND { $op = BinaryOperator.AND; } 
-        | OR { $op = BinaryOperator.OR; } 
-        | IMPL { $op = BinaryOperator.IMPLICATION; } 
-        | EQIV { $op = BinaryOperator.EQUIVALENCE; }
-;
-
-op_float returns [ FloatProposition.Operator op ] : 
-          EQ { $op = FloatProposition.Operator.EQ; } 
-        | N_EQ { $op = FloatProposition.Operator.NEQ; } 
-        | GT { $op = FloatProposition.Operator.GT; } 
-        | LT { $op = FloatProposition.Operator.LT; }
-        | GT_EQ { $op = FloatProposition.Operator.GT_EQ; } 
-        | LT_EQ { $op = FloatProposition.Operator.LT_EQ; }
-; 
-
-DEF : '#define';
-PROP : '#property';
-
-/* Terminals: */
-    bool : TRUE | FALSE ;
-    TRUE : 'True';
-    FALSE : 'False';
-    /* Boolean Operators */
-        NEG : '!';
-        AND : '&&';
-        OR : '||';
-        IMPL : '=>';
-        EQIV : '<=>';
-    /* Temporal Operators */
-        ALL : 'A';
-        EXISTS : 'E';
-        UNTIL : 'U';
-    /* Comparison operators */
-        EQ : '==';
-        N_EQ : '!=';
-        GT : '>';
-        LT : '<';
-        GT_EQ : '>=';
-        LT_EQ : '<=';
-    /* Brackets */
-        B_OPEN : '(';
-        B_CLOSE : ')';
-    /* Values */
-        VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
-        FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
-    WS : [ \t\n]+ -> skip ; // toss out whitespace
\ No newline at end of file
+/** Helper/Grouping parser rules **/
+
+unary_op : NEG | EX | EF | EG | AX | AF | AG;
+bool_op : CON | DIS | IMPL | EQIV;
+float_op : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
+
+/** Terminals **/
+
+TRUE : ([tT]'rue' | 'tt' | 'TT');
+FALSE : ([fF]'alse' | 'ff' | 'FF');
+
+IN : 'in';
+OUT : 'out';
+
+PLUS : '+';
+MINUS : '-';
+
+/** Operators **/
+
+EX : 'EX';
+EF : 'EF';
+EG : 'EG';
+AX : 'AX';
+AF : 'AF';
+AG : 'AG';
+
+EQ : '==';
+NEQ : '!=';
+GT : '>';
+LT : '<';
+GTEQ : '>=';
+LTEQ : '<=';
+
+NEG : '!';
+CON : '&&';
+DIS : '||';
+IMPL : '=>';
+EQIV : '<=>';
+
+/* Literals */
+
+STRING : ["].+?["]; //non-greedy match till next quotation mark
+VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
+FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
+
+NEWLINE : '\r'?'\n';
+
+WS : [ \t\u]+ -> channel(HIDDEN) ;
+
+Block_comment : '/*' (Block_comment|.)*? '*/' -> channel(HIDDEN) ; // nesting allow
+Line_comment : '//' .*? '\n' -> channel(HIDDEN) ;
\ No newline at end of file
diff --git a/src/main/antlr4/CTLnew.g4 b/src/main/antlr4/CTLnew.g4
deleted file mode 100644
index 39e2ced..0000000
--- a/src/main/antlr4/CTLnew.g4
+++ /dev/null
@@ -1,57 +0,0 @@
-
-grammar CTLnew;
-
-root :
-    | NEWLINE
-    | include root
-    | property root;
-
-PROP : '#property';
-INCL : '#include';
-
-include :
-    INCL QUOTE PATH QUOTE NEWLINE;
-
-property :
-    PROP VAR_NAME IS formula NEWLINE;
-
-formula:
-    bool | formula binary formula | EXISTS formula UNTIL formula | B_OPEN formula B_CLOSE;
-
-binary:
-    AND | OR | IMPL | EQIV;
-
-/* Terminals: */
-    bool : TRUE | FALSE ;
-    TRUE : 'True';
-    FALSE : 'False';
-
-    /* Boolean Operators */
-        NEG : '!';
-        AND : '&&';
-        OR : '||';
-        IMPL : '=>';
-        EQIV : '<=>';
-    /* Temporal Operators */
-        ALL : 'A';
-        EXISTS : 'E';
-        UNTIL : 'U';
-    /* Comparison operators */
-        EQ : '==';
-        N_EQ : '!=';
-        GT : '>';
-        LT : '<';
-        GT_EQ : '>=';
-        LT_EQ : '<=';
-    /* Brackets */
-        B_OPEN : '(';
-        B_CLOSE : ')';
-    /* Values */
-        VAR_NAME : [a-zA-Z]+[a-zA-Z0-9]*;
-        FLOAT_VAL : [-]?[0-9]*[.]?[0-9]+;
-        PATH : [a-zA-Z/.]+[a-zA-Z0-9]*;
-
-        IS : '=';
-        QUOTE : '"';
-        NEWLINE: [\n]*;
-    WS : [ \t\n]+ -> skip ; // toss out whitespace
\ No newline at end of file

From 2ea305a95dcdb4e42ead6672ec353d3a9d70f8b7 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 22:34:53 +0200
Subject: [PATCH 05/36] Correctly mark generated sources root as project srcDir

---
 build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index 4a65eec..cc9bfee 100644
--- a/build.gradle
+++ b/build.gradle
@@ -31,7 +31,7 @@ antlr4 {
 compileJava.dependsOn antlr4
 
 // add the generated source files to the list of java sources
-sourceSets.main.java.srcDirs += antlr4.output
+sourceSets.main.java.srcDirs += new File('src/main/gen')
 
 // add antlr4 to classpath
 configurations {

From ea6d742472aeae2e444c2eb1086383758e923fb7 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 22:57:32 +0200
Subject: [PATCH 06/36] Fix break keyword conflict

---
 src/main/antlr4/CTL.g4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 15412cd..02af6d8 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -3,14 +3,14 @@ grammar CTL;
 
 /* Main format structure */
 
-root : (statement break)*;
+root : (statement fullstop)*;
 
 statement : '#include' STRING                       # include
           | VAR_NAME '=' formula                    # assign
           | '#check' formula (',' formula)*         # check
           ;
 
-break : NEWLINE+ | EOF;
+fullstop : NEWLINE+ | EOF;
 
 /* Formula and propositions */
 

From 58a0d08b8a1d8304da4852ddd6332846462a0b53 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 23:01:16 +0200
Subject: [PATCH 07/36] Rename rules to comply with java naming standards

---
 src/main/antlr4/CTL.g4 | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 02af6d8..378a2c9 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -3,33 +3,33 @@ grammar CTL;
 
 /* Main format structure */
 
-root : (statement fullstop)*;
+root : (statement fullStop)*;
 
 statement : '#include' STRING                       # include
           | VAR_NAME '=' formula                    # assign
           | '#check' formula (',' formula)*         # check
           ;
 
-fullstop : NEWLINE+ | EOF;
+fullStop : NEWLINE+ | EOF;
 
 /* Formula and propositions */
 
 formula : VAR_NAME                                          #id
         | (TRUE | FALSE)                                    #bool
         | VAR_NAME ':' ('in'|'out') ('+'|'-')               #direction
-        | VAR_NAME float_op FLOAT_VAL                       #proposition
+        | VAR_NAME floatOp FLOAT_VAL                        #proposition
         | '(' formula ')'                                   #parenthesis
-        | unary_op formula                                  #unary
-        | formula bool_op formula                           #binary
+        | unaryOp formula                                   #unary
+        | formula boolOp formula                            #binary
         | 'E' formula 'U' formula                           #existUntil
         | 'A' formula 'U' formula                           #allUntil
         ;
 
 /** Helper/Grouping parser rules **/
 
-unary_op : NEG | EX | EF | EG | AX | AF | AG;
-bool_op : CON | DIS | IMPL | EQIV;
-float_op : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
+unaryOp : NEG | EX | EF | EG | AX | AF | AG;
+boolOp : CON | DIS | IMPL | EQIV;
+floatOp : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
 
 /** Terminals **/
 

From 262fcc43efb10f3d85c75786ee3c6389052e0dff Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 23:07:45 +0200
Subject: [PATCH 08/36] Fix terminals not showing in listeners

---
 src/main/antlr4/CTL.g4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 378a2c9..6037cbf 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -16,7 +16,7 @@ fullStop : NEWLINE+ | EOF;
 
 formula : VAR_NAME                                          #id
         | (TRUE | FALSE)                                    #bool
-        | VAR_NAME ':' ('in'|'out') ('+'|'-')               #direction
+        | VAR_NAME ':' (IN | OUT) (PLUS | MINUS)            #direction
         | VAR_NAME floatOp FLOAT_VAL                        #proposition
         | '(' formula ')'                                   #parenthesis
         | unaryOp formula                                   #unary

From 22c8f4f23c2a25d65dbe5ed42832c1d26f465307 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 23:17:33 +0200
Subject: [PATCH 09/36] Remove redundant visibility declarations

---
 src/main/java/cz/muni/fi/ctl/formula/Formula.java         | 8 ++++----
 .../java/cz/muni/fi/ctl/formula/operator/Operator.java    | 2 +-
 .../muni/fi/ctl/formula/proposition/FloatProposition.java | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/main/java/cz/muni/fi/ctl/formula/Formula.java b/src/main/java/cz/muni/fi/ctl/formula/Formula.java
index be73689..86ef2fd 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/Formula.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/Formula.java
@@ -9,15 +9,15 @@
 public interface Formula {
 
     /** Get number of sub formulas. **/
-    public int getSubFormulaCount();
+    int getSubFormulaCount();
 
     /** Get sub formula at specified index. **/
-    public Formula getSubFormulaAt(int index);
+    Formula getSubFormulaAt(int index);
 
     @NotNull
-    public Collection<Formula> getSubFormulas();
+    Collection<Formula> getSubFormulas();
 
     @NotNull
-    public Operator getOperator();
+    Operator getOperator();
 
 }
diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java
index 7d4fb91..7f7163f 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java
@@ -2,6 +2,6 @@
 
 public interface Operator {
 
-    public int getCardinality();
+    int getCardinality();
 
 }
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
index c8ad358..f824d65 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
@@ -45,7 +45,7 @@ public String getVariable() {
         return variable;
     }
 
-    public static enum Operator {
+    public enum Operator {
         EQ("==", -1), NEQ("!=", -1), GT(">", 0), GT_EQ(">=", 2), LT("<", 1), LT_EQ("<=", 3);
 
         private final String val;

From 9fc8bb7ab58e81ebd23866d94507277ae65d4a7c Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 23:28:43 +0200
Subject: [PATCH 10/36] Remove evaluate method - useless

---
 .../formula/proposition/Contradiction.java    |  7 +------
 .../proposition/DirectionProposition.java     |  7 +++++++
 .../formula/proposition/FloatProposition.java | 21 +------------------
 .../ctl/formula/proposition/Proposition.java  |  4 +---
 .../fi/ctl/formula/proposition/Tautology.java |  7 +------
 5 files changed, 11 insertions(+), 35 deletions(-)
 create mode 100644 src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java

diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java
index ec64756..4062c38 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java
@@ -2,17 +2,12 @@
 
 import org.jetbrains.annotations.NotNull;
 
-public class Contradiction extends Proposition<Object> {
+public class Contradiction extends Proposition {
 
     public static final Contradiction INSTANCE = new Contradiction();
 
     private Contradiction() {}
 
-    @Override
-    public boolean evaluate(Object value) {
-        return false;
-    }
-
     @NotNull
     @Override
     public String toString() {
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
new file mode 100644
index 0000000..ee99304
--- /dev/null
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
@@ -0,0 +1,7 @@
+package cz.muni.fi.ctl.formula.proposition;
+
+/**
+ * Created by daemontus on 14/07/15.
+ */
+public class DirectionProposition {
+}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
index f824d65..9629eec 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
@@ -2,7 +2,7 @@
 
 import org.jetbrains.annotations.NotNull;
 
-public class FloatProposition extends Proposition<Double> {
+public class FloatProposition extends Proposition {
 
     private final double value;
     private final String variable;
@@ -14,25 +14,6 @@ public FloatProposition(double value, String variable, Operator operator) {
         this.variable = variable;
     }
 
-    @Override
-    public boolean evaluate(Double value) {
-        switch (operator) {
-            case LT:
-                return value < this.value;
-            case LT_EQ:
-                return value <= this.value;
-            case GT:
-                return value > this.value;
-            case GT_EQ:
-                return value >= this.value;
-            case NEQ:
-                return value != this.value;
-            case EQ:
-            default:
-                return value == this.value;
-        }
-    }
-
     public Operator getFloatOperator() {
         return operator;
     }
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java
index ba43736..0b66b73 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java
@@ -8,9 +8,7 @@
 import java.util.ArrayList;
 import java.util.Collection;
 
-public abstract class Proposition<T> implements Formula {
-
-    public abstract boolean evaluate(T value);
+public abstract class Proposition implements Formula {
 
     @Override
     public int getSubFormulaCount() {
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java
index 9162b89..1a4935d 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java
@@ -2,17 +2,12 @@
 
 import org.jetbrains.annotations.NotNull;
 
-public class Tautology extends Proposition<Object> {
+public class Tautology extends Proposition {
 
     public static final Tautology INSTANCE = new Tautology();
 
     private Tautology() {}
 
-    @Override
-    public boolean evaluate(Object value) {
-        return true;
-    }
-
     @NotNull
     @Override
     public String toString() {

From 7a4da4615c2938c36b65012554bd417a4d7b1944 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Tue, 14 Jul 2015 23:37:31 +0200
Subject: [PATCH 11/36] Create Direction Proposition

---
 .../proposition/DirectionProposition.java     | 67 +++++++++++++++++--
 1 file changed, 63 insertions(+), 4 deletions(-)

diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
index ee99304..1563e0e 100644
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
+++ b/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
@@ -1,7 +1,66 @@
 package cz.muni.fi.ctl.formula.proposition;
 
-/**
- * Created by daemontus on 14/07/15.
- */
-public class DirectionProposition {
+import org.jetbrains.annotations.NotNull;
+
+public class DirectionProposition extends Proposition {
+
+    public enum Direction { IN, OUT }
+    public enum Facet { POSITIVE, NEGATIVE }
+
+    @NotNull
+    private final String variable;
+    @NotNull
+    private final Direction direction;
+    @NotNull
+    private final Facet facet;
+
+    public DirectionProposition(@NotNull String variable, @NotNull Direction direction, @NotNull Facet facet) {
+        this.variable = variable;
+        this.direction = direction;
+        this.facet = facet;
+    }
+
+    @NotNull
+    public String getVariable() {
+        return variable;
+    }
+
+    @NotNull
+    public Direction getDirection() {
+        return direction;
+    }
+
+    @NotNull
+    public Facet getFacet() {
+        return facet;
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) return true;
+        if (!(o instanceof DirectionProposition)) return false;
+
+        DirectionProposition that = (DirectionProposition) o;
+
+        if (!variable.equals(that.variable)) return false;
+        if (direction != that.direction) return false;
+        return facet == that.facet;
+
+    }
+
+    @Override
+    public int hashCode() {
+        int result = variable.hashCode();
+        result = 31 * result + direction.hashCode();
+        result = 31 * result + facet.hashCode();
+        return result;
+    }
+
+    @Override
+    public String toString() {
+        return
+                variable + ":" +
+                (direction == Direction.IN ? "in" : "out") +
+                (facet == Facet.POSITIVE ? "+" : "-");
+    }
 }

From 07b25d905c7196dfe418d6b79d3402e4d99bfe3f Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 24 Jul 2015 15:53:21 +0200
Subject: [PATCH 12/36] Generate listeners

---
 build.gradle                                   | 2 +-
 src/main/java/cz/muni/fi/ctl/ParseContext.java | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 src/main/java/cz/muni/fi/ctl/ParseContext.java

diff --git a/build.gradle b/build.gradle
index cc9bfee..7920471 100644
--- a/build.gradle
+++ b/build.gradle
@@ -24,7 +24,7 @@ antlr4 {
     extraArgs=['-package', 'cz.muni.fi.ctl.antlr']
     output=new File('src/main/gen/cz/muni/fi/ctl/antlr')
     visitor=false
-    listener=false
+    listener=true
 }
 
 // make the Java compile task depend on the antlr4 task
diff --git a/src/main/java/cz/muni/fi/ctl/ParseContext.java b/src/main/java/cz/muni/fi/ctl/ParseContext.java
new file mode 100644
index 0000000..d05314f
--- /dev/null
+++ b/src/main/java/cz/muni/fi/ctl/ParseContext.java
@@ -0,0 +1,7 @@
+package cz.muni.fi.ctl;
+
+/**
+ * Created by daemontus on 14/07/15.
+ */
+public class ParseContext {
+}

From 62c0f5cf1d66ec20a9d93afdfcf7a5929acd7450 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Sat, 25 Jul 2015 16:25:06 +0200
Subject: [PATCH 13/36] Add Kotlin framework.

---
 build.gradle | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index 7920471..f58abdd 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,22 +1,25 @@
 //include antlr plugin
 buildscript {
+    ext.kotlin_version = '0.12.1218'
     repositories {
         maven {
             name 'JFrog OSS snapshot repo'
             url  'https://oss.jfrog.org/oss-snapshot-local/'
         }
         jcenter()
+        mavenCentral()
     }
 
     dependencies {
         classpath 'me.champeau.gradle:antlr4-gradle-plugin:0.1'
+        classpath "org.jetbrains.kotlin:kotlin-gradle-plugin:$kotlin_version"
     }
 }
 
 apply plugin: 'java'
+apply plugin: 'kotlin'
 apply plugin: 'me.champeau.gradle.antlr4'
 
-sourceCompatibility = 1.7
 version = '1.0'
 
 //antlr config
@@ -45,6 +48,7 @@ repositories {
 dependencies {
     testCompile group: 'junit', name: 'junit', version: '4.11'
     compile 'com.intellij:annotations:5.1'
+    compile "org.jetbrains.kotlin:kotlin-stdlib:$kotlin_version"
 }
 
 //create a single Jar with all dependencies
@@ -57,3 +61,7 @@ task fullJar(type: Jar) {
     from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
     with jar
 }
+sourceSets {
+    main.java.srcDirs += 'src/main/kotlin'
+    test.java.srcDirs += 'src/test/kotlin'
+}

From f903b4aa7593fa5b77bcc78dae837eba9372e113 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Sat, 25 Jul 2015 16:25:40 +0200
Subject: [PATCH 14/36] Operator and formula framework rewritten into Kotlin.

---
 .../cz/muni/fi/ctl/FormulaNormalizer.java     | 87 ------------------
 .../java/cz/muni/fi/ctl/FormulaParser.java    | 59 ------------
 .../java/cz/muni/fi/ctl/ParseContext.java     |  7 --
 .../java/cz/muni/fi/ctl/formula/Formula.java  | 23 -----
 .../cz/muni/fi/ctl/formula/FormulaImpl.java   | 81 ----------------
 .../ctl/formula/operator/BinaryOperator.java  | 12 ---
 .../ctl/formula/operator/NullaryOperator.java | 12 ---
 .../fi/ctl/formula/operator/Operator.java     |  7 --
 .../ctl/formula/operator/UnaryOperator.java   | 12 ---
 .../formula/proposition/Contradiction.java    | 17 ----
 .../proposition/DirectionProposition.java     | 66 -------------
 .../formula/proposition/FloatProposition.java | 75 ---------------
 .../ctl/formula/proposition/Proposition.java  | 35 -------
 .../fi/ctl/formula/proposition/Tautology.java | 16 ----
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt    | 92 +++++++++++++++++++
 src/main/kotlin/cz/muni/fi/ctl/Operators.kt   | 29 ++++++
 16 files changed, 121 insertions(+), 509 deletions(-)
 delete mode 100644 src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/FormulaParser.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/ParseContext.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/Formula.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java
 delete mode 100644 src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java
 create mode 100644 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
 create mode 100644 src/main/kotlin/cz/muni/fi/ctl/Operators.kt

diff --git a/src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java b/src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java
deleted file mode 100644
index f873ece..0000000
--- a/src/main/java/cz/muni/fi/ctl/FormulaNormalizer.java
+++ /dev/null
@@ -1,87 +0,0 @@
-package cz.muni.fi.ctl;
-
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.FormulaImpl;
-import cz.muni.fi.ctl.formula.operator.BinaryOperator;
-import cz.muni.fi.ctl.formula.operator.Operator;
-import cz.muni.fi.ctl.formula.operator.UnaryOperator;
-import cz.muni.fi.ctl.formula.proposition.Proposition;
-import cz.muni.fi.ctl.formula.proposition.Tautology;
-import org.jetbrains.annotations.NotNull;
-
-/**
- * <p>This class should transform formulas to normalized format processable by model checker.</p>
- * <p>Note: only one normal form is currently supported.</p>
- */
-public class FormulaNormalizer {
-
-    @NotNull
-    public Formula normalize(@NotNull Formula formula) {
-        //leave propositions unchanged
-        if (formula instanceof Proposition) return formula;
-        @NotNull Operator operator = formula.getOperator();
-        if (operator instanceof UnaryOperator) {
-            switch ((UnaryOperator) operator) {
-                case ALL_NEXT:
-                    // AX p = !EX !p
-                    return
-                            new FormulaImpl(UnaryOperator.NEGATION,
-                                    new FormulaImpl(UnaryOperator.EXISTS_NEXT,
-                                            new FormulaImpl(UnaryOperator.NEGATION,
-                                                    normalize(formula.getSubFormulaAt(0))
-                                            )));
-                case EXISTS_FUTURE:
-                    // EF p = E [ true U p ]
-                    return new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE,
-                                    normalize(formula.getSubFormulaAt(0))
-                            );
-                case ALL_FUTURE:
-                    // AF p = A [ true U p ]
-                    return
-                            new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE,
-                                    normalize(formula.getSubFormulaAt(0))
-                            );
-                case EXISTS_GLOBAL:
-                    // EG p = ! A [ true U ! p ]
-                    return new FormulaImpl(UnaryOperator.NEGATION,
-                            new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE,
-                                    new FormulaImpl(UnaryOperator.NEGATION,
-                                            normalize(formula.getSubFormulaAt(0))
-                                    )));
-                case ALL_GLOBAL:
-                    // AG p = ! E [ true U ! p ]
-                    return
-                            new FormulaImpl(UnaryOperator.NEGATION,
-                                    new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE,
-                                            new FormulaImpl(UnaryOperator.NEGATION,
-                                                    normalize(formula.getSubFormulaAt(0))
-                                            )));
-                default:
-                    return new FormulaImpl(formula.getOperator(), normalize(formula.getSubFormulaAt(0)));
-            }
-        } else if (operator instanceof BinaryOperator) {
-            switch ((BinaryOperator) operator) {
-                case IMPLICATION:
-                    // a => b = !a || b
-                    return new FormulaImpl(BinaryOperator.OR,
-                            new FormulaImpl(UnaryOperator.NEGATION,
-                                    normalize(formula.getSubFormulaAt(0))),
-                            normalize(formula.getSubFormulaAt(1))
-                            );
-                case EQUIVALENCE:
-                    // a <=> b = (a && b) || (!a && !b)
-                    return new FormulaImpl(BinaryOperator.OR,
-                            new FormulaImpl(BinaryOperator.AND, formula.getSubFormulaAt(0), formula.getSubFormulaAt(1)),
-                            new FormulaImpl(BinaryOperator.AND,
-                                    new FormulaImpl(UnaryOperator.NEGATION, formula.getSubFormulaAt(0)),
-                                    new FormulaImpl(UnaryOperator.NEGATION, formula.getSubFormulaAt(1))
-                            ));
-                default:
-                    return new FormulaImpl(formula.getOperator(), normalize(formula.getSubFormulaAt(0)), normalize(formula.getSubFormulaAt(1)));
-            }
-        } else {
-            throw new IllegalArgumentException("Unsupported operator type: " + operator);
-        }
-    }
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/FormulaParser.java b/src/main/java/cz/muni/fi/ctl/FormulaParser.java
deleted file mode 100644
index 8e13ef3..0000000
--- a/src/main/java/cz/muni/fi/ctl/FormulaParser.java
+++ /dev/null
@@ -1,59 +0,0 @@
-package cz.muni.fi.ctl;
-
-import cz.muni.fi.ctl.antlr.CTLLexer;
-import cz.muni.fi.ctl.antlr.CTLParser;
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.proposition.Proposition;
-import org.antlr.v4.runtime.ANTLRInputStream;
-import org.antlr.v4.runtime.BufferedTokenStream;
-import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
-
-import java.io.File;
-import java.io.FileInputStream;
-import java.io.IOException;
-import java.io.InputStream;
-import java.util.Collection;
-
-public class FormulaParser {
-
-    @NotNull
-    public Formula parse(@NotNull File input) throws IOException {
-        @Nullable InputStream inputStream = null;
-        try {
-            inputStream = new FileInputStream(input);
-            return parse(new ANTLRInputStream(inputStream));
-        } finally {
-            if (inputStream != null) {
-                inputStream.close();
-            }
-        }
-    }
-
-    @NotNull
-    public Formula parse(@NotNull String input) throws IllegalStateException {
-        return parse(new ANTLRInputStream(input.toCharArray(), input.length()));
-    }
-
-    private Formula parse(ANTLRInputStream is) {
-        CTLParser.RootContext root = new CTLParser(new BufferedTokenStream(new CTLLexer(is))).root();
-        Collection<Proposition> propositions = root.propositions.values();
-        Formula formula = root.result;
-        findUnusedPropositions(propositions, formula);
-        if (!propositions.isEmpty()) {
-            throw new IllegalArgumentException("Unused proposition: "+propositions.iterator().next().toString());
-        }
-        return formula;
-    }
-
-    private void findUnusedPropositions(Collection<Proposition> propositions, Formula formula) {
-        if (formula instanceof Proposition) {
-            propositions.remove(formula);
-            return;
-        }
-        for (Formula sub : formula.getSubFormulas()) {
-            findUnusedPropositions(propositions, sub);
-        }
-    }
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/ParseContext.java b/src/main/java/cz/muni/fi/ctl/ParseContext.java
deleted file mode 100644
index d05314f..0000000
--- a/src/main/java/cz/muni/fi/ctl/ParseContext.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package cz.muni.fi.ctl;
-
-/**
- * Created by daemontus on 14/07/15.
- */
-public class ParseContext {
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/Formula.java b/src/main/java/cz/muni/fi/ctl/formula/Formula.java
deleted file mode 100644
index 86ef2fd..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/Formula.java
+++ /dev/null
@@ -1,23 +0,0 @@
-package cz.muni.fi.ctl.formula;
-
-
-import cz.muni.fi.ctl.formula.operator.Operator;
-import org.jetbrains.annotations.NotNull;
-
-import java.util.Collection;
-
-public interface Formula {
-
-    /** Get number of sub formulas. **/
-    int getSubFormulaCount();
-
-    /** Get sub formula at specified index. **/
-    Formula getSubFormulaAt(int index);
-
-    @NotNull
-    Collection<Formula> getSubFormulas();
-
-    @NotNull
-    Operator getOperator();
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java b/src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java
deleted file mode 100644
index 8964b2a..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/FormulaImpl.java
+++ /dev/null
@@ -1,81 +0,0 @@
-package cz.muni.fi.ctl.formula;
-
-import cz.muni.fi.ctl.formula.operator.NullaryOperator;
-import cz.muni.fi.ctl.formula.operator.Operator;
-import org.jetbrains.annotations.NotNull;
-
-import java.util.*;
-
-public class FormulaImpl implements Formula {
-
-    @NotNull
-    private final Operator operator;
-    @NotNull
-    private final List<Formula> formulas = new ArrayList<>();
-
-    /**
-     * Utility constructor for nullary formulas.
-     */
-    public FormulaImpl() {
-        this.operator = NullaryOperator.INSTANCE;
-    }
-
-    /**
-     * Universal constructor for creating formulas with any cardinality.
-     * @param operator N-ary operator.
-     * @param formulas List of N formulas (empty list for nullary operator).
-     */
-    public FormulaImpl(@NotNull Operator operator, @NotNull Formula... formulas) {
-        this.operator = operator;
-        if (operator.getCardinality() != formulas.length) {
-            throw new IllegalArgumentException("Operator requires "+operator.getCardinality()+" subFormulas, "+formulas.length+" formulas provided");
-        }
-        this.formulas.addAll(Arrays.asList(formulas));
-    }
-
-    @Override
-    public int getSubFormulaCount() {
-        return operator.getCardinality();
-    }
-
-    @Override
-    public Formula getSubFormulaAt(int index) {
-        return formulas.get(index);
-    }
-
-    @NotNull
-    @Override
-    public Collection<Formula> getSubFormulas() {
-        return Collections.unmodifiableCollection(formulas);
-    }
-
-    @NotNull
-    @Override
-    public Operator getOperator() {
-        return operator;
-    }
-
-    @NotNull
-    @Override
-    public String toString() {
-        return operator + ": " + Arrays.toString(formulas.toArray());
-    }
-
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (!(o instanceof FormulaImpl)) return false;
-
-        @NotNull FormulaImpl formula = (FormulaImpl) o;
-
-        return formulas.equals(formula.formulas) && operator.equals(formula.operator);
-
-    }
-
-    @Override
-    public int hashCode() {
-        int result = operator.hashCode();
-        result = 31 * result + formulas.hashCode();
-        return result;
-    }
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java
deleted file mode 100644
index 527eb02..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/operator/BinaryOperator.java
+++ /dev/null
@@ -1,12 +0,0 @@
-package cz.muni.fi.ctl.formula.operator;
-
-public enum BinaryOperator implements Operator {
-    AND, OR, IMPLICATION, EQUIVALENCE, EXISTS_UNTIL, ALL_UNTIL
-    ;
-
-    @Override
-    public int getCardinality() {
-        return 2;
-    }
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java
deleted file mode 100644
index a1c022b..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/operator/NullaryOperator.java
+++ /dev/null
@@ -1,12 +0,0 @@
-package cz.muni.fi.ctl.formula.operator;
-
-public class NullaryOperator implements Operator {
-    public static final NullaryOperator INSTANCE = new NullaryOperator();
-
-    private NullaryOperator() {}
-
-    @Override
-    public int getCardinality() {
-        return 0;
-    }
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java
deleted file mode 100644
index 7f7163f..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/operator/Operator.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package cz.muni.fi.ctl.formula.operator;
-
-public interface Operator {
-
-    int getCardinality();
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java b/src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java
deleted file mode 100644
index 1ce45f4..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/operator/UnaryOperator.java
+++ /dev/null
@@ -1,12 +0,0 @@
-package cz.muni.fi.ctl.formula.operator;
-
-public enum UnaryOperator implements Operator {
-    NEGATION, EXISTS_NEXT, ALL_NEXT, EXISTS_FUTURE, ALL_FUTURE, EXISTS_GLOBAL, ALL_GLOBAL
-    ;
-
-    @Override
-    public int getCardinality() {
-        return 1;
-    }
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java
deleted file mode 100644
index 4062c38..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Contradiction.java
+++ /dev/null
@@ -1,17 +0,0 @@
-package cz.muni.fi.ctl.formula.proposition;
-
-import org.jetbrains.annotations.NotNull;
-
-public class Contradiction extends Proposition {
-
-    public static final Contradiction INSTANCE = new Contradiction();
-
-    private Contradiction() {}
-
-    @NotNull
-    @Override
-    public String toString() {
-        return "False";
-    }
-
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
deleted file mode 100644
index 1563e0e..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/DirectionProposition.java
+++ /dev/null
@@ -1,66 +0,0 @@
-package cz.muni.fi.ctl.formula.proposition;
-
-import org.jetbrains.annotations.NotNull;
-
-public class DirectionProposition extends Proposition {
-
-    public enum Direction { IN, OUT }
-    public enum Facet { POSITIVE, NEGATIVE }
-
-    @NotNull
-    private final String variable;
-    @NotNull
-    private final Direction direction;
-    @NotNull
-    private final Facet facet;
-
-    public DirectionProposition(@NotNull String variable, @NotNull Direction direction, @NotNull Facet facet) {
-        this.variable = variable;
-        this.direction = direction;
-        this.facet = facet;
-    }
-
-    @NotNull
-    public String getVariable() {
-        return variable;
-    }
-
-    @NotNull
-    public Direction getDirection() {
-        return direction;
-    }
-
-    @NotNull
-    public Facet getFacet() {
-        return facet;
-    }
-
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (!(o instanceof DirectionProposition)) return false;
-
-        DirectionProposition that = (DirectionProposition) o;
-
-        if (!variable.equals(that.variable)) return false;
-        if (direction != that.direction) return false;
-        return facet == that.facet;
-
-    }
-
-    @Override
-    public int hashCode() {
-        int result = variable.hashCode();
-        result = 31 * result + direction.hashCode();
-        result = 31 * result + facet.hashCode();
-        return result;
-    }
-
-    @Override
-    public String toString() {
-        return
-                variable + ":" +
-                (direction == Direction.IN ? "in" : "out") +
-                (facet == Facet.POSITIVE ? "+" : "-");
-    }
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
deleted file mode 100644
index 9629eec..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/FloatProposition.java
+++ /dev/null
@@ -1,75 +0,0 @@
-package cz.muni.fi.ctl.formula.proposition;
-
-import org.jetbrains.annotations.NotNull;
-
-public class FloatProposition extends Proposition {
-
-    private final double value;
-    private final String variable;
-    private final Operator operator;
-
-    public FloatProposition(double value, String variable, Operator operator) {
-        this.value = value;
-        this.operator = operator;
-        this.variable = variable;
-    }
-
-    public Operator getFloatOperator() {
-        return operator;
-    }
-
-    public double getThreshold() {
-        return value;
-    }
-
-    public String getVariable() {
-        return variable;
-    }
-
-    public enum Operator {
-        EQ("==", -1), NEQ("!=", -1), GT(">", 0), GT_EQ(">=", 2), LT("<", 1), LT_EQ("<=", 3);
-
-        private final String val;
-        //represents an integer passed to an enum inside a native library
-        private final int nativeIndex;
-
-        Operator(String val, int nativeIndex) {
-            this.val = val;
-            this.nativeIndex = nativeIndex;
-        }
-
-        @Override
-        public String toString() {
-            return val;
-        }
-
-        public int getOperatorIndex() {
-            return nativeIndex;
-        }
-    }
-
-    @NotNull
-    @Override
-    public String toString() {
-        return variable+" "+operator+" "+value;
-    }
-
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (!(o instanceof FloatProposition)) return false;
-
-        @NotNull FloatProposition that = (FloatProposition) o;
-
-        return Double.compare(that.value, value) == 0 && operator == that.operator && variable.equals(that.variable);
-
-    }
-
-    @Override
-    public int hashCode() {
-        long result = (value != +0.0f ? Double.doubleToLongBits(value) : 0);
-        result = 31 * result + variable.hashCode();
-        result = 31 * result + operator.hashCode();
-        return (int) result;
-    }
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java
deleted file mode 100644
index 0b66b73..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Proposition.java
+++ /dev/null
@@ -1,35 +0,0 @@
-package cz.muni.fi.ctl.formula.proposition;
-
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.operator.NullaryOperator;
-import cz.muni.fi.ctl.formula.operator.Operator;
-import org.jetbrains.annotations.NotNull;
-
-import java.util.ArrayList;
-import java.util.Collection;
-
-public abstract class Proposition implements Formula {
-
-    @Override
-    public int getSubFormulaCount() {
-        return 0;
-    }
-
-    @NotNull
-    @Override
-    public Formula getSubFormulaAt(int index) {
-        throw new IndexOutOfBoundsException("Requested index "+index+", size 0");
-    }
-
-    @NotNull
-    @Override
-    public Collection<Formula> getSubFormulas() {
-        return new ArrayList<>();
-    }
-
-    @NotNull
-    @Override
-    public Operator getOperator() {
-        return NullaryOperator.INSTANCE;
-    }
-}
diff --git a/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java b/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java
deleted file mode 100644
index 1a4935d..0000000
--- a/src/main/java/cz/muni/fi/ctl/formula/proposition/Tautology.java
+++ /dev/null
@@ -1,16 +0,0 @@
-package cz.muni.fi.ctl.formula.proposition;
-
-import org.jetbrains.annotations.NotNull;
-
-public class Tautology extends Proposition {
-
-    public static final Tautology INSTANCE = new Tautology();
-
-    private Tautology() {}
-
-    @NotNull
-    @Override
-    public String toString() {
-        return "True";
-    }
-}
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
new file mode 100644
index 0000000..ac34028
--- /dev/null
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -0,0 +1,92 @@
+package cz.muni.fi.ctl
+
+//Formulas
+public interface Formula {
+    val operator: Operator
+    val subFormulas: List<Formula>
+
+    public fun get(i: Int): Formula = subFormulas[i]
+}
+
+data class FormulaImpl (
+        override val operator: Operator = Operator.ATOM,
+        override val subFormulas: List<Formula> = listOf()
+) : Formula {
+
+    init {
+        if (subFormulas.size() != operator.cardinality) {
+            throw IllegalArgumentException(
+                    "Operator cardinality(${operator.cardinality}) and " +
+                    "number of sub formulas(${subFormulas.size()}) do not match")
+        }
+    }
+
+    constructor(operator: Operator, vararg formulas: Formula) : this(operator, formulas.toList())
+
+    override fun toString(): String = when (operator.cardinality) {
+        1 -> "$operator(${subFormulas[0]})"
+        2 -> "${subFormulas[0]} $operator ${subFormulas[1]}"
+        else -> "$operator($subFormulas)"
+    }
+
+}
+
+open class Atom : Formula {
+    final override val operator = Operator.ATOM
+    final override val subFormulas = listOf<Formula>()
+}
+
+//Boolean Atoms
+val True = object : Atom() {
+    override fun toString():String = "True"
+}
+
+val False = object : Atom() {
+    override fun toString():String = "False"
+}
+
+//Float atoms
+public data class FloatProposition (
+        val variable: String,
+        val floatOp: FloatOperator,
+        val value: Double
+) : Atom() {
+    override fun toString(): String = "$variable $floatOp $value"
+}
+
+//Direction atoms
+public data class DirectionProposition (
+        val variable: String,
+        val direction: DirectionProposition.Direction,
+        val facet: DirectionProposition.Facet
+) : Atom() {
+
+    override fun toString(): String = "$variable:$direction$facet"
+
+    enum class Direction(val str: String) {
+        IN("in"), OUT("out");
+        override fun toString(): String = str
+    }
+
+    enum class Facet(val str: String) {
+        POSITIVE("+"), NEGATIVE("-");
+        override fun toString(): String = str
+    }
+
+}
+
+
+//Simplified builders
+fun not(f: Formula) = FormulaImpl(Operator.NEGATION, f)
+fun EX(f: Formula) = FormulaImpl(Operator.EXISTS_NEXT, f)
+fun AX(f: Formula) = FormulaImpl(Operator.ALL_NEXT, f)
+fun EF(f: Formula) = FormulaImpl(Operator.EXISTS_FUTURE, f)
+fun AF(f: Formula) = FormulaImpl(Operator.ALL_FUTURE, f)
+fun EG(f: Formula) = FormulaImpl(Operator.EXISTS_GLOBAL, f)
+fun AG(f: Formula) = FormulaImpl(Operator.ALL_GLOBAL, f)
+fun Formula.or(f2: Formula): Formula = FormulaImpl(Operator.OR, this, f2)
+fun Formula.and(f2: Formula): Formula = FormulaImpl(Operator.AND, this, f2)
+fun Formula.implies(f2: Formula): Formula = FormulaImpl(Operator.IMPLICATION, this, f2)
+fun Formula.equals(f2: Formula): Formula = FormulaImpl(Operator.EQUIVALENCE, this, f2)
+fun Formula.EU(f2: Formula): Formula = FormulaImpl(Operator.EXISTS_UNTIL, this, f2)
+fun Formula.AU(f2: Formula): Formula = FormulaImpl(Operator.ALL_UNTIL, this, f2)
\ No newline at end of file
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
new file mode 100644
index 0000000..0e94da1
--- /dev/null
+++ b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
@@ -0,0 +1,29 @@
+package cz.muni.fi.ctl
+
+public enum class Operator(val cardinality: Int, val str: String) {
+    //nullary
+    ATOM(0,"null"),
+    //unary
+    NEGATION(1, "!"),
+    EXISTS_NEXT(1, "EX"),
+    ALL_NEXT(1, "AX"),
+    EXISTS_FUTURE(1, "EF"),
+    ALL_FUTURE(1, "AF"),
+    EXISTS_GLOBAL(1, "EG"),
+    ALL_GLOBAL(1, "AG"),
+    //binary
+    AND(2, "&&"),
+    OR(2, "||"),
+    IMPLICATION(2, "=>"),
+    EQUIVALENCE(2, "<=>"),
+    EXISTS_UNTIL(2, "EU"),
+    ALL_UNTIL(2, "AU");
+
+    override fun toString(): String = str
+}
+
+public enum class FloatOperator(val str: String) {
+    EQ("=="), NEQ("!="), GT(">"), GT_EQ(">="), LT("<"), LT_EQ("<=");
+
+    override fun toString(): String = str
+}
\ No newline at end of file

From 08e8cd0041cd1b3a1c78ebdd174015209ce41b2b Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Sat, 25 Jul 2015 16:27:00 +0200
Subject: [PATCH 15/36] Formula normalizer rewritten into Kotlin with support
 for various normal forms.

---
 src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt | 50 ++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
new file mode 100644
index 0000000..ae4d4c3
--- /dev/null
+++ b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
@@ -0,0 +1,50 @@
+package cz.muni.fi.ctl
+
+val untilNormalForm: Map<Operator, (Formula, (Formula) -> Formula) -> Formula> = mapOf(
+        Operator.ALL_NEXT to {
+            // AX p = !EX !p
+            f, x -> not( EX( not( x(f[0]) ) ) )
+        },
+        Operator.EXISTS_FUTURE to {
+            // EF p = E [ true U p ]
+            f, x -> True EU x(f[0])
+        },
+        Operator.ALL_FUTURE to {
+            // AF p = A [ true U p ]
+            f, x -> True AU x(f[0])
+        },
+        Operator.EXISTS_GLOBAL to {
+            // EG p = ! A [ true U ! p ]
+            f, x -> not( True AU not( x(f[0]) ) )
+        },
+        Operator.ALL_GLOBAL to {
+            // AG p = ! E [ true U ! p ]
+            f, x -> not( True EU not( x(f[0]) ) )
+        },
+        Operator.IMPLICATION to {
+            // a => b = !a || b
+            f, x -> not(x(f[0])) or x(f[1])
+        },
+        Operator.EQUIVALENCE to {
+            // a <=> b = (a && b) || (!a && !b)
+            f, x -> (x(f[0]) and x(f[1])) or (not(x(f[0])) and not(x(f[1])))
+        }
+)
+
+public class Normalizer(
+        normalForm: Map<Operator, (Formula, (Formula) -> Formula) -> Formula> = untilNormalForm
+) {
+
+    private val normalForm = normalForm
+
+    public fun normalize(f: Formula) : Formula {
+        if (f.operator.cardinality == 0) return f   //stop on propositions - we don't know how to handle them here
+
+        val normalize = { f: Formula -> normalize(f) }
+        val identity = { f: Formula, x: (Formula) -> Formula
+            -> FormulaImpl(f.operator, f.subFormulas.map(x)) }
+
+        return normalForm[f.operator]?.invoke(f, normalize) ?: identity(f, normalize)
+    }
+
+}
\ No newline at end of file

From 43c5101a45b10fa54902a4e34716bdea711fac28 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Sun, 26 Jul 2015 10:29:04 +0200
Subject: [PATCH 16/36] Simple formula optimizer based on boolean equality.

---
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt   | 37 +++++-----
 src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt | 22 +++---
 src/main/kotlin/cz/muni/fi/ctl/Operators.kt  |  8 ++-
 src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt  | 73 ++++++++++++++++++++
 4 files changed, 107 insertions(+), 33 deletions(-)
 create mode 100644 src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index ac34028..5b7a4dc 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -2,14 +2,14 @@ package cz.muni.fi.ctl
 
 //Formulas
 public interface Formula {
-    val operator: Operator
+    val operator: Op
     val subFormulas: List<Formula>
 
     public fun get(i: Int): Formula = subFormulas[i]
 }
 
 data class FormulaImpl (
-        override val operator: Operator = Operator.ATOM,
+        override val operator: Op = Op.ATOM,
         override val subFormulas: List<Formula> = listOf()
 ) : Formula {
 
@@ -21,7 +21,7 @@ data class FormulaImpl (
         }
     }
 
-    constructor(operator: Operator, vararg formulas: Formula) : this(operator, formulas.toList())
+    constructor(operator: Op, vararg formulas: Formula) : this(operator, formulas.toList())
 
     override fun toString(): String = when (operator.cardinality) {
         1 -> "$operator(${subFormulas[0]})"
@@ -32,7 +32,7 @@ data class FormulaImpl (
 }
 
 open class Atom : Formula {
-    final override val operator = Operator.ATOM
+    final override val operator = Op.ATOM
     final override val subFormulas = listOf<Formula>()
 }
 
@@ -48,7 +48,7 @@ val False = object : Atom() {
 //Float atoms
 public data class FloatProposition (
         val variable: String,
-        val floatOp: FloatOperator,
+        val floatOp: FloatOp,
         val value: Double
 ) : Atom() {
     override fun toString(): String = "$variable $floatOp $value"
@@ -77,16 +77,17 @@ public data class DirectionProposition (
 
 
 //Simplified builders
-fun not(f: Formula) = FormulaImpl(Operator.NEGATION, f)
-fun EX(f: Formula) = FormulaImpl(Operator.EXISTS_NEXT, f)
-fun AX(f: Formula) = FormulaImpl(Operator.ALL_NEXT, f)
-fun EF(f: Formula) = FormulaImpl(Operator.EXISTS_FUTURE, f)
-fun AF(f: Formula) = FormulaImpl(Operator.ALL_FUTURE, f)
-fun EG(f: Formula) = FormulaImpl(Operator.EXISTS_GLOBAL, f)
-fun AG(f: Formula) = FormulaImpl(Operator.ALL_GLOBAL, f)
-fun Formula.or(f2: Formula): Formula = FormulaImpl(Operator.OR, this, f2)
-fun Formula.and(f2: Formula): Formula = FormulaImpl(Operator.AND, this, f2)
-fun Formula.implies(f2: Formula): Formula = FormulaImpl(Operator.IMPLICATION, this, f2)
-fun Formula.equals(f2: Formula): Formula = FormulaImpl(Operator.EQUIVALENCE, this, f2)
-fun Formula.EU(f2: Formula): Formula = FormulaImpl(Operator.EXISTS_UNTIL, this, f2)
-fun Formula.AU(f2: Formula): Formula = FormulaImpl(Operator.ALL_UNTIL, this, f2)
\ No newline at end of file
+fun not(f: Formula) = FormulaImpl(Op.NEGATION, f)
+fun EX(f: Formula) = FormulaImpl(Op.EXISTS_NEXT, f)
+fun AX(f: Formula) = FormulaImpl(Op.ALL_NEXT, f)
+fun EF(f: Formula) = FormulaImpl(Op.EXISTS_FUTURE, f)
+fun AF(f: Formula) = FormulaImpl(Op.ALL_FUTURE, f)
+fun EG(f: Formula) = FormulaImpl(Op.EXISTS_GLOBAL, f)
+fun AG(f: Formula) = FormulaImpl(Op.ALL_GLOBAL, f)
+fun Formula.or(f2: Formula): Formula = FormulaImpl(Op.OR, this, f2)
+fun Formula.and(f2: Formula): Formula = FormulaImpl(Op.AND, this, f2)
+fun Formula.implies(f2: Formula): Formula = FormulaImpl(Op.IMPLICATION, this, f2)
+fun Formula.equals(f2: Formula): Formula = FormulaImpl(Op.EQUIVALENCE, this, f2)
+fun Formula.EU(f2: Formula): Formula = FormulaImpl(Op.EXISTS_UNTIL, this, f2)
+fun Formula.AU(f2: Formula): Formula = FormulaImpl(Op.ALL_UNTIL, this, f2)
+fun Formula.map(x: (Formula) -> Formula) = FormulaImpl(this.operator, this.subFormulas.map(x))
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
index ae4d4c3..4f6fd66 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
@@ -1,38 +1,38 @@
 package cz.muni.fi.ctl
 
-val untilNormalForm: Map<Operator, (Formula, (Formula) -> Formula) -> Formula> = mapOf(
-        Operator.ALL_NEXT to {
+val untilNormalForm: Map<Op, (Formula, (Formula) -> Formula) -> Formula> = mapOf(
+        Op.ALL_NEXT to {
             // AX p = !EX !p
             f, x -> not( EX( not( x(f[0]) ) ) )
         },
-        Operator.EXISTS_FUTURE to {
+        Op.EXISTS_FUTURE to {
             // EF p = E [ true U p ]
             f, x -> True EU x(f[0])
         },
-        Operator.ALL_FUTURE to {
+        Op.ALL_FUTURE to {
             // AF p = A [ true U p ]
             f, x -> True AU x(f[0])
         },
-        Operator.EXISTS_GLOBAL to {
+        Op.EXISTS_GLOBAL to {
             // EG p = ! A [ true U ! p ]
             f, x -> not( True AU not( x(f[0]) ) )
         },
-        Operator.ALL_GLOBAL to {
+        Op.ALL_GLOBAL to {
             // AG p = ! E [ true U ! p ]
             f, x -> not( True EU not( x(f[0]) ) )
         },
-        Operator.IMPLICATION to {
+        Op.IMPLICATION to {
             // a => b = !a || b
             f, x -> not(x(f[0])) or x(f[1])
         },
-        Operator.EQUIVALENCE to {
+        Op.EQUIVALENCE to {
             // a <=> b = (a && b) || (!a && !b)
             f, x -> (x(f[0]) and x(f[1])) or (not(x(f[0])) and not(x(f[1])))
         }
 )
 
 public class Normalizer(
-        normalForm: Map<Operator, (Formula, (Formula) -> Formula) -> Formula> = untilNormalForm
+        normalForm: Map<Op, (Formula, (Formula) -> Formula) -> Formula> = untilNormalForm
 ) {
 
     private val normalForm = normalForm
@@ -41,10 +41,8 @@ public class Normalizer(
         if (f.operator.cardinality == 0) return f   //stop on propositions - we don't know how to handle them here
 
         val normalize = { f: Formula -> normalize(f) }
-        val identity = { f: Formula, x: (Formula) -> Formula
-            -> FormulaImpl(f.operator, f.subFormulas.map(x)) }
 
-        return normalForm[f.operator]?.invoke(f, normalize) ?: identity(f, normalize)
+        return normalForm[f.operator]?.invoke(f, normalize) ?: f.map(normalize)
     }
 
 }
\ No newline at end of file
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
index 0e94da1..b717758 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
@@ -1,6 +1,6 @@
 package cz.muni.fi.ctl
 
-public enum class Operator(val cardinality: Int, val str: String) {
+public enum class Op(val cardinality: Int, val str: String) {
     //nullary
     ATOM(0,"null"),
     //unary
@@ -22,8 +22,10 @@ public enum class Operator(val cardinality: Int, val str: String) {
     override fun toString(): String = str
 }
 
-public enum class FloatOperator(val str: String) {
-    EQ("=="), NEQ("!="), GT(">"), GT_EQ(">="), LT("<"), LT_EQ("<=");
+public enum class FloatOp(val str: String, val neg: FloatOp) {
+    EQ("==", NEQ), NEQ("!=", EQ), GT(">", LT_EQ), GT_EQ(">=", LT), LT("<", GT_EQ), LT_EQ("<=", GT);
 
     override fun toString(): String = str
+
+
 }
\ No newline at end of file
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
new file mode 100644
index 0000000..4588239
--- /dev/null
+++ b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
@@ -0,0 +1,73 @@
+package cz.muni.fi.ctl
+
+
+public class Optimizer {
+
+    private val optimize = { f: Formula -> optimizeTree(f) }
+
+    fun optimizeTree(f: Formula): Formula = when {
+        f.operator.cardinality == 0 -> f
+        f.operator == Op.NEGATION ->
+            when {
+                // !True = False
+                f[0] == True -> False
+                // !False = True
+                f[0] == False -> True
+                // !a > 5 = a <= 5
+                f is FloatProposition -> f.copy(floatOp = f.floatOp.neg)
+                // !!a = a
+                f[0].operator == Op.NEGATION -> optimizeTree(f[0][0])
+                else -> f.map(optimize)
+            }
+        f.operator == Op.AND ->
+            when {
+                // a && False = False
+                False in f.subFormulas -> False
+                // a && True = a
+                f[0] == True -> optimizeTree(f[1])
+                f[1] == True -> optimizeTree(f[0])
+                //!a && !b = a || b
+                f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION ->
+                    optimizeTree(f[0][0]) and optimizeTree(f[1][0])
+                else -> f.map(optimize)
+            }
+        f.operator == Op.OR ->
+            when {
+                // a || True = True
+                True in f.subFormulas -> True
+                // a || False = a
+                f[0] == False -> optimizeTree(f[1])
+                f[1] == False -> optimizeTree(f[0])
+                // !a || !b = a && b
+                f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION ->
+                    optimizeTree(f[0][0]) and optimizeTree(f[1][0])
+                else -> f.map(optimize)
+            }
+        f.operator == Op.EXISTS_UNTIL ->
+            when {
+                // E a U True = True
+                f[1] == True -> True
+                // E a U False = False
+                f[1] == False -> False
+                else -> f.map(optimize)
+            }
+        f.operator == Op.ALL_UNTIL ->
+            when {
+                // A a U True = True
+                f[1] == True -> True
+                // A a U False = False
+                f[1] == False -> False
+                else -> f.map(optimize)
+            }
+        f.operator == Op.EXISTS_NEXT ->
+            when {
+                // EX True = True
+                f[0] == True -> True
+                // EX False = False
+                f[0] == False -> False
+                else -> f.map(optimize)
+            }
+        else ->
+            f.map(optimize)
+    }
+}
\ No newline at end of file

From 2ca625d0a9987eda056b8008fff7d90f9ec65cf2 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 15:12:34 +0200
Subject: [PATCH 17/36] Accept file starting with newlines

---
 src/main/antlr4/CTL.g4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 6037cbf..4fd50c6 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -3,7 +3,7 @@ grammar CTL;
 
 /* Main format structure */
 
-root : (statement fullStop)*;
+root : fullStop? (statement fullStop)*;
 
 statement : '#include' STRING                       # include
           | VAR_NAME '=' formula                    # assign

From 2d3e35926355c2d138822031ff26948b2184c7c8 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 15:13:43 +0200
Subject: [PATCH 18/36] FloatOp initializer fix.

---
 src/main/kotlin/cz/muni/fi/ctl/Operators.kt | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
index b717758..1eb6936 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
@@ -22,8 +22,18 @@ public enum class Op(val cardinality: Int, val str: String) {
     override fun toString(): String = str
 }
 
-public enum class FloatOp(val str: String, val neg: FloatOp) {
-    EQ("==", NEQ), NEQ("!=", EQ), GT(">", LT_EQ), GT_EQ(">=", LT), LT("<", GT_EQ), LT_EQ("<=", GT);
+public enum class FloatOp(val str: String) {
+    EQ("=="), NEQ("!="), GT(">"), GT_EQ(">="), LT("<"), LT_EQ("<=");
+
+    val neg: FloatOp
+        get() = when (this) {
+            EQ -> NEQ
+            NEQ -> EQ
+            GT -> LT_EQ
+            GT_EQ -> LT
+            LT -> GT_EQ
+            LT_EQ -> GT
+        }
 
     override fun toString(): String = str
 

From f2f3aa2691a88203c108b5d9a06863da63fc7ca7 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 15:14:56 +0200
Subject: [PATCH 19/36] Formula.map rewritten to Formula.treeMap -> map only on
 tree nodes, not leafs

---
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt   |  7 ++++++-
 src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt |  3 +--
 src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt  | 14 +++++++-------
 3 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index 5b7a4dc..42d9e57 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -90,4 +90,9 @@ fun Formula.implies(f2: Formula): Formula = FormulaImpl(Op.IMPLICATION, this, f2
 fun Formula.equals(f2: Formula): Formula = FormulaImpl(Op.EQUIVALENCE, this, f2)
 fun Formula.EU(f2: Formula): Formula = FormulaImpl(Op.EXISTS_UNTIL, this, f2)
 fun Formula.AU(f2: Formula): Formula = FormulaImpl(Op.ALL_UNTIL, this, f2)
-fun Formula.map(x: (Formula) -> Formula) = FormulaImpl(this.operator, this.subFormulas.map(x))
+fun Formula.treeMap(x: (Formula) -> Formula) =
+        if (this.operator.cardinality == 0) {
+            this
+        } else {
+            FormulaImpl(this.operator, this.subFormulas.map(x))
+        }
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
index 4f6fd66..efff5fb 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Normalizer.kt
@@ -38,11 +38,10 @@ public class Normalizer(
     private val normalForm = normalForm
 
     public fun normalize(f: Formula) : Formula {
-        if (f.operator.cardinality == 0) return f   //stop on propositions - we don't know how to handle them here
 
         val normalize = { f: Formula -> normalize(f) }
 
-        return normalForm[f.operator]?.invoke(f, normalize) ?: f.map(normalize)
+        return normalForm[f.operator]?.invoke(f, normalize) ?: f.treeMap(normalize)
     }
 
 }
\ No newline at end of file
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
index 4588239..85e836a 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
@@ -17,7 +17,7 @@ public class Optimizer {
                 f is FloatProposition -> f.copy(floatOp = f.floatOp.neg)
                 // !!a = a
                 f[0].operator == Op.NEGATION -> optimizeTree(f[0][0])
-                else -> f.map(optimize)
+                else -> f.treeMap(optimize)
             }
         f.operator == Op.AND ->
             when {
@@ -29,7 +29,7 @@ public class Optimizer {
                 //!a && !b = a || b
                 f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION ->
                     optimizeTree(f[0][0]) and optimizeTree(f[1][0])
-                else -> f.map(optimize)
+                else -> f.treeMap(optimize)
             }
         f.operator == Op.OR ->
             when {
@@ -41,7 +41,7 @@ public class Optimizer {
                 // !a || !b = a && b
                 f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION ->
                     optimizeTree(f[0][0]) and optimizeTree(f[1][0])
-                else -> f.map(optimize)
+                else -> f.treeMap(optimize)
             }
         f.operator == Op.EXISTS_UNTIL ->
             when {
@@ -49,7 +49,7 @@ public class Optimizer {
                 f[1] == True -> True
                 // E a U False = False
                 f[1] == False -> False
-                else -> f.map(optimize)
+                else -> f.treeMap(optimize)
             }
         f.operator == Op.ALL_UNTIL ->
             when {
@@ -57,7 +57,7 @@ public class Optimizer {
                 f[1] == True -> True
                 // A a U False = False
                 f[1] == False -> False
-                else -> f.map(optimize)
+                else -> f.treeMap(optimize)
             }
         f.operator == Op.EXISTS_NEXT ->
             when {
@@ -65,9 +65,9 @@ public class Optimizer {
                 f[0] == True -> True
                 // EX False = False
                 f[0] == False -> False
-                else -> f.map(optimize)
+                else -> f.treeMap(optimize)
             }
         else ->
-            f.map(optimize)
+            f.treeMap(optimize)
     }
 }
\ No newline at end of file

From 0ad49ab7e3f9a6168b9a7881a7668a285d377e94 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 15:16:19 +0200
Subject: [PATCH 20/36] Parser classes (references, includes, etc.)

---
 src/main/kotlin/cz/muni/fi/ctl/Parser.kt | 231 +++++++++++++++++++++++
 1 file changed, 231 insertions(+)
 create mode 100644 src/main/kotlin/cz/muni/fi/ctl/Parser.kt

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
new file mode 100644
index 0000000..bf26422
--- /dev/null
+++ b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
@@ -0,0 +1,231 @@
+package cz.muni.fi.ctl
+
+import cz.muni.fi.ctl.antlr.CTLBaseListener
+import cz.muni.fi.ctl.antlr.CTLLexer
+import cz.muni.fi.ctl.antlr.CTLParser
+import org.antlr.v4.runtime.ANTLRInputStream
+import org.antlr.v4.runtime.CommonTokenStream
+import org.antlr.v4.runtime.tree.ParseTree
+import org.antlr.v4.runtime.tree.ParseTreeProperty
+import org.antlr.v4.runtime.tree.ParseTreeWalker
+import java.io.File
+import java.util.ArrayList
+import java.util.HashMap
+import java.util.HashSet
+import java.util.Stack
+
+public class Parser {
+
+    public fun parse(input: String): List<Formula> = process(FileParser().process(input))
+
+    public fun parse(input: File): List<Formula> = process(FileParser().process(input))
+
+    fun process(ctx: ParserContext): List<Formula> {
+
+        val formulas = ctx.formulas
+        val checks = ctx.checks
+
+        // Resolve references
+
+        val references = HashMap(formulas)  //mutable copy
+        val replaced = Stack<String>()  //processing stack for cycle detection
+
+        fun replace(f: Formula): Formula = when (f) {
+            is Reference -> when {
+                f.name !in references ->
+                    throw IllegalStateException("Undefined reference: ${f.name}")
+                f.name in replaced ->
+                    throw IllegalStateException("Cyclic reference: ${f.name}")
+                else -> {
+                    replaced.push(f.name)
+                    val result = references[f.name].treeMap(::replace)
+                    replaced.pop()
+                    result
+                }
+            }
+            else -> f.treeMap(::replace)
+        }
+
+        for ((name, formula) in formulas) {
+            references[name] = formula.treeMap(::replace)
+        }
+
+        return checks.map(::replace)
+    }
+
+}
+
+class FileParser {
+
+    private val processed = HashSet<File>()
+
+    fun process(input: String): ParserContext {
+        val ctx = processString(input)
+        return ctx.includes.map { process(it) }.fold(ctx.toParseContext(), ParserContext::plus)
+    }
+
+    fun process(input: File): ParserContext {
+        val ctx = processFile(input)
+        processed.add(input)
+        return ctx.includes.
+                filter { it !in processed }.
+                map { process(it) }.
+                fold (ctx.toParseContext(), ParserContext::plus)
+    }
+
+    private fun processString(input: String): FileContext =
+            processStream(ANTLRInputStream(input.toCharArray(), input.length()), "input string")
+
+    private fun processFile(input: File): FileContext =
+            input.inputStream().use { processStream(ANTLRInputStream(it), input.getAbsolutePath()) }
+
+    private fun processStream(input: ANTLRInputStream, location: String): FileContext {
+        val root = CTLParser(CommonTokenStream(CTLLexer(input))).root()
+        val context = FileContext(location)
+        ParseTreeWalker().walk(context, root)
+        return context
+    }
+
+}
+
+data class ParserContext(
+        val assignments: List<Assignment>,
+        val checks: List<Formula> = listOf()
+) {
+
+    val formulas: Map<String, Formula>
+        get() = assignments.toMap({ it.name }, { it.formula} )
+
+    /**
+     * Checks for duplicate assignments received from parser
+     */
+    init {
+        for (one in assignments) {
+            for (two in assignments) {
+                if (one.name == two.name && one.location != two.location) {
+                    throw IllegalStateException(
+                            "Duplicate assignment for ${one.name} defined in ${one.location} and ${two.location}"
+                    )
+                }
+            }
+        }
+    }
+
+    fun plus(ctx: ParserContext): ParserContext {
+        return ParserContext(assignments + ctx.assignments, checks + ctx.checks)
+    }
+
+}
+
+class FileContext(val location: String) : CTLBaseListener() {
+
+    val includes = ArrayList<File>()
+    val assignments = ArrayList<Assignment>()
+    val checks = ArrayList<Formula>()
+
+    private val formulas = ParseTreeProperty<Formula>()
+
+    fun toParseContext() = ParserContext(assignments, checks)
+
+    override fun exitInclude(ctx: CTLParser.IncludeContext) {
+        val string = ctx.STRING().getText()!!
+        includes.add(File(string.substring(1, string.length() - 1)))    //remove quotes
+    }
+
+    override fun exitAssign(ctx: CTLParser.AssignContext) {
+        assignments.add(Assignment(
+                ctx.VAR_NAME().getText()!!,
+                formulas[ctx.formula()]!!,
+                location
+        ))
+    }
+
+    override fun exitCheck(ctx: CTLParser.CheckContext) {
+        for (context in ctx.formula()) {
+            checks.add(formulas[context]!!)
+        }
+    }
+
+    /** ------ Formula Parsing ------ **/
+
+    override fun exitId(ctx: CTLParser.IdContext) {
+        formulas[ctx] = Reference(ctx.getText()!!)
+    }
+
+    override fun exitBool(ctx: CTLParser.BoolContext) {
+        formulas[ctx] = if (ctx.TRUE() != null) True else False
+    }
+
+    override fun exitDirection(ctx: CTLParser.DirectionContext) {
+        formulas[ctx] = DirectionProposition(
+                variable = ctx.VAR_NAME().getText()!!,
+                direction = if (ctx.IN() != null) DirectionProposition.Direction.IN else DirectionProposition.Direction.OUT,
+                facet = if (ctx.PLUS() != null) DirectionProposition.Facet.POSITIVE else DirectionProposition.Facet.NEGATIVE
+        )
+    }
+
+    override fun exitProposition(ctx: CTLParser.PropositionContext) {
+        formulas[ctx] = FloatProposition(
+                variable = ctx.VAR_NAME().getText()!!,
+                floatOp = ctx.floatOp().toOperator(),
+                value = ctx.FLOAT_VAL().getText().toDouble()
+        )
+    }
+
+    override fun exitParenthesis(ctx: CTLParser.ParenthesisContext) {
+        formulas[ctx] = formulas[ctx.formula()]!!
+    }
+
+    override fun exitUnary(ctx: CTLParser.UnaryContext) {
+        formulas[ctx] = FormulaImpl(ctx.unaryOp().toOperator(), formulas[ctx.formula()]!!)
+    }
+
+    override fun exitBinary(ctx: CTLParser.BinaryContext) {
+        formulas[ctx] = FormulaImpl(ctx.boolOp().toOperator(), formulas[ctx.formula(0)]!!, formulas[ctx.formula(1)]!!)
+    }
+
+    override fun exitExistUntil(ctx: CTLParser.ExistUntilContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! EU formulas[ctx.formula(1)]!!
+    }
+
+    override fun exitAllUntil(ctx: CTLParser.AllUntilContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! AU formulas[ctx.formula(1)]!!
+    }
+}
+
+data class Assignment(val name: String, val formula: Formula, val location: String)
+
+data class Reference(val name: String) : Atom()
+
+//convenience methods
+
+fun CTLParser.BoolOpContext.toOperator(): Op = when {
+    CON() != null -> Op.AND
+    DIS() != null -> Op.OR
+    IMPL() != null -> Op.IMPLICATION
+    EQIV() != null -> Op.EQUIVALENCE
+    else -> throw IllegalStateException("Invalid binary operator: ${getText()}")
+}
+
+fun CTLParser.UnaryOpContext.toOperator(): Op = when {
+    NEG() != null -> Op.NEGATION
+    EX() != null -> Op.EXISTS_NEXT
+    AX() != null -> Op.ALL_NEXT
+    EF() != null -> Op.EXISTS_FUTURE
+    AF() != null -> Op.ALL_FUTURE
+    EG() != null -> Op.EXISTS_GLOBAL
+    AG() != null -> Op.ALL_GLOBAL
+    else -> throw IllegalStateException("Invalid unary operator: ${getText()}")
+}
+
+fun CTLParser.FloatOpContext.toOperator(): FloatOp = when {
+    EQ() != null -> FloatOp.EQ
+    NEQ() != null -> FloatOp.NEQ
+    LT() != null -> FloatOp.LT
+    LTEQ() != null -> FloatOp.LT_EQ
+    GT() != null -> FloatOp.GT
+    GTEQ() != null -> FloatOp.GT_EQ
+    else -> throw IllegalStateException("Invalid float operator: ${getText()}")
+}
+
+fun <T> ParseTreeProperty<T>.set(k: ParseTree, v: T) = this.put(k, v)

From 7e19509b9634803acfaad86a196060533e86974e Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 16:38:05 +0200
Subject: [PATCH 21/36]  Formula API refinement and map tests.

---
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt    |  32 ++--
 src/test/java/FormulaNormalizerTest.java      | 147 ------------------
 .../kotlin/cz/muni/fi/ctl/FormulasTest.kt     |  48 ++++++
 .../kotlin/cz/muni/fi/ctl/NormalizerTest.kt   |   5 +
 4 files changed, 70 insertions(+), 162 deletions(-)
 delete mode 100644 src/test/java/FormulaNormalizerTest.java
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index 42d9e57..1edf0c8 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -37,11 +37,11 @@ open class Atom : Formula {
 }
 
 //Boolean Atoms
-val True = object : Atom() {
+public val True: Formula = object : Atom() {
     override fun toString():String = "True"
 }
 
-val False = object : Atom() {
+public val False: Formula = object : Atom() {
     override fun toString():String = "False"
 }
 
@@ -77,19 +77,21 @@ public data class DirectionProposition (
 
 
 //Simplified builders
-fun not(f: Formula) = FormulaImpl(Op.NEGATION, f)
-fun EX(f: Formula) = FormulaImpl(Op.EXISTS_NEXT, f)
-fun AX(f: Formula) = FormulaImpl(Op.ALL_NEXT, f)
-fun EF(f: Formula) = FormulaImpl(Op.EXISTS_FUTURE, f)
-fun AF(f: Formula) = FormulaImpl(Op.ALL_FUTURE, f)
-fun EG(f: Formula) = FormulaImpl(Op.EXISTS_GLOBAL, f)
-fun AG(f: Formula) = FormulaImpl(Op.ALL_GLOBAL, f)
-fun Formula.or(f2: Formula): Formula = FormulaImpl(Op.OR, this, f2)
-fun Formula.and(f2: Formula): Formula = FormulaImpl(Op.AND, this, f2)
-fun Formula.implies(f2: Formula): Formula = FormulaImpl(Op.IMPLICATION, this, f2)
-fun Formula.equals(f2: Formula): Formula = FormulaImpl(Op.EQUIVALENCE, this, f2)
-fun Formula.EU(f2: Formula): Formula = FormulaImpl(Op.EXISTS_UNTIL, this, f2)
-fun Formula.AU(f2: Formula): Formula = FormulaImpl(Op.ALL_UNTIL, this, f2)
+public fun not(f: Formula): Formula = FormulaImpl(Op.NEGATION, f)
+public fun EX(f: Formula): Formula = FormulaImpl(Op.EXISTS_NEXT, f)
+public fun AX(f: Formula): Formula = FormulaImpl(Op.ALL_NEXT, f)
+public fun EF(f: Formula): Formula = FormulaImpl(Op.EXISTS_FUTURE, f)
+public fun AF(f: Formula): Formula = FormulaImpl(Op.ALL_FUTURE, f)
+public fun EG(f: Formula): Formula = FormulaImpl(Op.EXISTS_GLOBAL, f)
+public fun AG(f: Formula): Formula = FormulaImpl(Op.ALL_GLOBAL, f)
+public fun Formula.or(f2: Formula): Formula = FormulaImpl(Op.OR, this, f2)
+public fun Formula.and(f2: Formula): Formula = FormulaImpl(Op.AND, this, f2)
+public fun Formula.implies(f2: Formula): Formula = FormulaImpl(Op.IMPLICATION, this, f2)
+public fun Formula.equal(f2: Formula): Formula = FormulaImpl(Op.EQUIVALENCE, this, f2)
+public fun Formula.EU(f2: Formula): Formula = FormulaImpl(Op.EXISTS_UNTIL, this, f2)
+public fun Formula.AU(f2: Formula): Formula = FormulaImpl(Op.ALL_UNTIL, this, f2)
+
+//this is not typical map semantics -> don't make it public
 fun Formula.treeMap(x: (Formula) -> Formula) =
         if (this.operator.cardinality == 0) {
             this
diff --git a/src/test/java/FormulaNormalizerTest.java b/src/test/java/FormulaNormalizerTest.java
deleted file mode 100644
index 31f5b08..0000000
--- a/src/test/java/FormulaNormalizerTest.java
+++ /dev/null
@@ -1,147 +0,0 @@
-
-import cz.muni.fi.ctl.FormulaNormalizer;
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.FormulaImpl;
-import cz.muni.fi.ctl.formula.operator.BinaryOperator;
-import cz.muni.fi.ctl.formula.operator.UnaryOperator;
-import cz.muni.fi.ctl.formula.proposition.Contradiction;
-import cz.muni.fi.ctl.formula.proposition.FloatProposition;
-import cz.muni.fi.ctl.formula.proposition.Proposition;
-import cz.muni.fi.ctl.formula.proposition.Tautology;
-import org.junit.Test;
-
-import static org.junit.Assert.assertEquals;
-
-/**
- * Tests for FormulaNormalizer
- */
-public class FormulaNormalizerTest {
-
-    @Test
-    public void propositionTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        assertEquals(Tautology.INSTANCE, normalizer.normalize(Tautology.INSTANCE));
-        assertEquals(Contradiction.INSTANCE, normalizer.normalize(Contradiction.INSTANCE));
-        Proposition proposition = new FloatProposition(34.5, "aaa", FloatProposition.Operator.GT_EQ);
-        assertEquals(proposition, normalizer.normalize(proposition));
-    }
-
-    @Test
-    public void unchangedTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula ex = new FormulaImpl(UnaryOperator.EXISTS_NEXT, Tautology.INSTANCE);
-        assertEquals(ex, normalizer.normalize(ex));
-        Formula eu = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE);
-        assertEquals(eu, normalizer.normalize(eu));
-        Formula au = new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE);
-        assertEquals(au, normalizer.normalize(au));
-        Formula neg = new FormulaImpl(UnaryOperator.NEGATION, Tautology.INSTANCE);
-        assertEquals(neg, normalizer.normalize(neg));
-        Formula and = new FormulaImpl(BinaryOperator.AND, Tautology.INSTANCE, Contradiction.INSTANCE);
-        assertEquals(and, normalizer.normalize(and));
-        Formula or = new FormulaImpl(BinaryOperator.OR, Tautology.INSTANCE, Contradiction.INSTANCE);
-        assertEquals(or, normalizer.normalize(or));
-    }
-
-    @Test
-    public void allNextTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(UnaryOperator.NEGATION,
-                            new FormulaImpl(UnaryOperator.EXISTS_NEXT,
-                                    new FormulaImpl(UnaryOperator.NEGATION, Tautology.INSTANCE)));
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.ALL_NEXT, Tautology.INSTANCE)));
-    }
-
-
-    @Test
-    public void allFutureTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE);
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.ALL_FUTURE, Contradiction.INSTANCE)));
-    }
-
-    @Test
-    public void existsFutureTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE, Contradiction.INSTANCE);
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.EXISTS_FUTURE, Contradiction.INSTANCE)));
-    }
-
-    @Test
-    public void allGlobalTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(UnaryOperator.NEGATION,
-                new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE,
-                        new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE)));
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.ALL_GLOBAL, Contradiction.INSTANCE)));
-    }
-
-    @Test
-    public void existsGlobalTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(UnaryOperator.NEGATION,
-                new FormulaImpl(BinaryOperator.ALL_UNTIL, Tautology.INSTANCE,
-                        new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE)));
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(UnaryOperator.EXISTS_GLOBAL, Contradiction.INSTANCE)));
-    }
-
-    @Test
-    public void implicationTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(BinaryOperator.OR, new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE), Contradiction.INSTANCE);
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(BinaryOperator.IMPLICATION, Contradiction.INSTANCE, Contradiction.INSTANCE)));
-    }
-
-    @Test
-    public void equivalenceTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula norm = new FormulaImpl(BinaryOperator.OR,
-                new FormulaImpl(BinaryOperator.AND, Contradiction.INSTANCE, Contradiction.INSTANCE),
-                new FormulaImpl(BinaryOperator.AND,
-                        new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE),
-                        new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE)
-                ));
-        assertEquals(norm, normalizer.normalize(new FormulaImpl(BinaryOperator.EQUIVALENCE, Contradiction.INSTANCE, Contradiction.INSTANCE)));
-    }
-
-    @Test
-    public void nestedUnchanged() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula sample = new FormulaImpl(BinaryOperator.AND,
-                new FormulaImpl(BinaryOperator.OR,
-                        new FormulaImpl(BinaryOperator.ALL_UNTIL,
-                                new FormulaImpl(UnaryOperator.EXISTS_NEXT, Tautology.INSTANCE),
-                                new FormulaImpl(UnaryOperator.NEGATION, Tautology.INSTANCE)
-                        ),
-                        Contradiction.INSTANCE
-                ),
-                new FormulaImpl(BinaryOperator.EXISTS_UNTIL,
-                        Tautology.INSTANCE,
-                        Contradiction.INSTANCE
-                )
-        );
-        assertEquals(sample, normalizer.normalize(sample));
-    }
-
-    @Test
-    public void complexTest() {
-        FormulaNormalizer normalizer = new FormulaNormalizer();
-        Formula sample = new FormulaImpl(BinaryOperator.AND,
-                new FormulaImpl(BinaryOperator.IMPLICATION, Contradiction.INSTANCE, Contradiction.INSTANCE),
-                new FormulaImpl(UnaryOperator.EXISTS_FUTURE,
-                        new FormulaImpl(UnaryOperator.EXISTS_NEXT,
-                                new FormulaImpl(UnaryOperator.ALL_GLOBAL, Contradiction.INSTANCE)))
-        );
-        Formula expected = new FormulaImpl(BinaryOperator.AND,
-                new FormulaImpl(BinaryOperator.OR,
-                        new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE),
-                        Contradiction.INSTANCE),
-                new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE,
-                        new FormulaImpl(UnaryOperator.EXISTS_NEXT,
-                                new FormulaImpl(UnaryOperator.NEGATION,
-                                        new FormulaImpl(BinaryOperator.EXISTS_UNTIL, Tautology.INSTANCE,
-                                        new FormulaImpl(UnaryOperator.NEGATION, Contradiction.INSTANCE)))))
-        );
-        assertEquals(expected, normalizer.normalize(sample));
-    }
-}
diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
new file mode 100644
index 0000000..14ab1a6
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -0,0 +1,48 @@
+package cz.muni.fi.ctl
+
+import org.junit.Test
+import kotlin.test.assertEquals
+
+class MapTest {
+
+    val formula = EX( True EU (
+            FloatProposition("var", FloatOp.EQ, 13.3)
+                    or
+            DirectionProposition("val", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+        )
+    )
+
+    Test fun treeMapId() {
+
+        assertEquals(formula, formula.treeMap { it })
+
+    }
+
+    Test fun treeMapPropositions() {
+
+        formula.treeMap {
+            if (it.operator.cardinality == 0) throw IllegalStateException("Executing tree map on a leaf")
+            else it
+        }
+    }
+
+    Test fun treeMapComplex() {
+
+        fun transform(f: Formula): Formula = when(f.operator) {
+            Op.EXISTS_NEXT -> FormulaImpl(Op.ALL_NEXT, f.subFormulas.map(::transform))
+            Op.EXISTS_UNTIL -> FormulaImpl(Op.ALL_UNTIL, f.subFormulas.map(::transform))
+            Op.OR -> FormulaImpl(Op.AND, f.subFormulas.map(::transform))
+            else -> f.treeMap(::transform)
+        }
+
+        assertEquals(
+                AX( True AU (
+                FloatProposition("var", FloatOp.EQ, 13.3)
+                    and
+                DirectionProposition("val", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+                )
+        ), transform(formula))
+
+    }
+
+}
\ No newline at end of file
diff --git a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
new file mode 100644
index 0000000..1dbeec3
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
@@ -0,0 +1,5 @@
+package cz.muni.fi.ctl
+
+/**
+ * Created by daemontus on 31/07/15.
+ */

From 7a265380139e9facc2937de2ad20c225f02316de Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 17:17:05 +0200
Subject: [PATCH 22/36] Normalizer tests

---
 .../kotlin/cz/muni/fi/ctl/NormalizerTest.kt   | 144 +++++++++++++++++-
 1 file changed, 141 insertions(+), 3 deletions(-)

diff --git a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
index 1dbeec3..6fc14a7 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
@@ -1,5 +1,143 @@
 package cz.muni.fi.ctl
 
-/**
- * Created by daemontus on 31/07/15.
- */
+import org.junit.Test
+import kotlin.test.assertEquals
+
+class UntilNormalFormTest {
+
+    val p1 = Reference("p1")
+    val p2 = Reference("p2")
+    val p3 = Reference("p3")
+    val p4 = Reference("p4")
+
+    val normalizer = Normalizer()
+
+    Test fun complexTest() {
+
+        val f1 = FloatProposition("var1", FloatOp.NEQ, 14.3)
+        val f2 = FloatProposition("var2", FloatOp.LT, -15.3)
+        val d1 = DirectionProposition("var1", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+        val d2 = DirectionProposition("var2", DirectionProposition.Direction.OUT, DirectionProposition.Facet.POSITIVE)
+
+        val prop = EF( AF((EX(f1) AU False) equal not(d2)) implies AX( EG(f2) EU AG(d1)))
+        assertEquals(
+                True EU
+                        (not( True AU ((EX(f1) AU False and not(d2)) or (not(EX(f1) AU False) and not(not(d2)))))
+                                or
+                        not( EX( not( (not( True AU not(f2))) EU (not( True EU not(d1))) )))),
+                normalizer.normalize(prop)
+        )
+    }
+
+    Test fun nestingNoPropositions() {
+        val prop = EF( p1 implies AX( EG(p2) EU AG(p1)))
+        assertEquals(
+                True EU (not(p1) or not( EX( not( (not( True AU not(p2))) EU (not( True EU not(p1))) )))),
+                normalizer.normalize(prop)
+        )
+    }
+
+    Test fun nestingPreserve() {
+        val prop = (p1 and EX(not(p2))) EU ( not(p3) AU (p4 or p2))
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    //trivial cases
+
+    Test fun equivChange() {
+        val prop = p1 equal p2
+        val norm = normalizer.normalize(prop)
+        assertEquals( (p1 and p2) or (not(p1) and not(p2)), norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun implChange() {
+        val prop = p1 implies p2
+        val norm = normalizer.normalize(prop)
+        assertEquals(not(p1) or p2, norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun agChange() {
+        val prop = AG(p1)
+        val norm = normalizer.normalize(prop)
+        assertEquals(not( True EU  not(p1) ), norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun egChange() {
+        val prop = EG(p1)
+        val norm = normalizer.normalize(prop)
+        assertEquals(not( True AU not(p1) ), norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun afChange() {
+        val prop = AF(p1)
+        val norm = normalizer.normalize(prop)
+        assertEquals(True AU p1, norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun efChange() {
+        val prop = EF(p1)
+        val norm = normalizer.normalize(prop)
+        assertEquals(True EU p1, norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun axChange() {
+        val prop = AX(p1)
+        val norm = normalizer.normalize(prop)
+        assertEquals(not( EX( not(p1) ) ), norm)
+        assertEquals(norm, normalizer.normalize(norm))
+    }
+
+    Test fun auPreserve() {
+        val prop = p1 AU p2
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun euPreserve() {
+        val prop = p1 EU p2
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun orPreserve() {
+        val prop = p1 or p2
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun andPreserve() {
+        val prop = p1 and p2
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun negPreserve() {
+        val prop = not(p1)
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun exPreserve() {
+        val prop = EX(p1)
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun floatPreserve() {
+        val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2)
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+    Test fun booleanPreserve() {
+        assertEquals(True, normalizer.normalize(True))
+        assertEquals(False, normalizer.normalize(False))
+    }
+
+    Test fun directionPreserve() {
+        val prop = DirectionProposition("var", DirectionProposition.Direction.IN, DirectionProposition.Facet.POSITIVE)
+        assertEquals(prop, normalizer.normalize(prop))
+    }
+
+
+
+}
\ No newline at end of file

From 0383b17239f5e55242e633abcf92437f9ea01c8f Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 17:47:59 +0200
Subject: [PATCH 23/36] Optimizer bug fix and tests.

---
 src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt   |  31 +-
 src/test/java/FormulaParserTest.java          | 280 ------------------
 .../kotlin/cz/muni/fi/ctl/OptimizerTest.kt    |  73 +++++
 3 files changed, 95 insertions(+), 289 deletions(-)
 delete mode 100644 src/test/java/FormulaParserTest.java
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
index 85e836a..6a1ab42 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
@@ -3,22 +3,35 @@ package cz.muni.fi.ctl
 
 public class Optimizer {
 
+    public fun optimize(f: Formula): Formula {
+        //it's hard to optimize while formula at once, so we just compute it as a fix point
+        var one = optimizeTree(f)
+        var two = optimizeTree(one)
+        while(two != one) {
+            one = two
+            two = optimizeTree(two)
+        }
+        return two
+    }
+
     private val optimize = { f: Formula -> optimizeTree(f) }
 
     fun optimizeTree(f: Formula): Formula = when {
         f.operator.cardinality == 0 -> f
-        f.operator == Op.NEGATION ->
+        f.operator == Op.NEGATION -> {
+            val child = f[0]
             when {
                 // !True = False
-                f[0] == True -> False
+                child == True -> False
                 // !False = True
-                f[0] == False -> True
+                child == False -> True
                 // !a > 5 = a <= 5
-                f is FloatProposition -> f.copy(floatOp = f.floatOp.neg)
+                child is FloatProposition -> child.copy(floatOp = child.floatOp.neg)
                 // !!a = a
-                f[0].operator == Op.NEGATION -> optimizeTree(f[0][0])
+                child.operator == Op.NEGATION -> optimizeTree(child[0])
                 else -> f.treeMap(optimize)
             }
+        }
         f.operator == Op.AND ->
             when {
                 // a && False = False
@@ -26,9 +39,9 @@ public class Optimizer {
                 // a && True = a
                 f[0] == True -> optimizeTree(f[1])
                 f[1] == True -> optimizeTree(f[0])
-                //!a && !b = a || b
+                //!a && !b = !(a || b)
                 f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION ->
-                    optimizeTree(f[0][0]) and optimizeTree(f[1][0])
+                    not(optimizeTree(f[0][0]) or optimizeTree(f[1][0]))
                 else -> f.treeMap(optimize)
             }
         f.operator == Op.OR ->
@@ -38,9 +51,9 @@ public class Optimizer {
                 // a || False = a
                 f[0] == False -> optimizeTree(f[1])
                 f[1] == False -> optimizeTree(f[0])
-                // !a || !b = a && b
+                // !a || !b = !(a && b)
                 f[0].operator == Op.NEGATION && f[1].operator == Op.NEGATION ->
-                    optimizeTree(f[0][0]) and optimizeTree(f[1][0])
+                    not(optimizeTree(f[0][0]) and optimizeTree(f[1][0]))
                 else -> f.treeMap(optimize)
             }
         f.operator == Op.EXISTS_UNTIL ->
diff --git a/src/test/java/FormulaParserTest.java b/src/test/java/FormulaParserTest.java
deleted file mode 100644
index e50ff7f..0000000
--- a/src/test/java/FormulaParserTest.java
+++ /dev/null
@@ -1,280 +0,0 @@
-import cz.muni.fi.ctl.FormulaParser;
-import cz.muni.fi.ctl.formula.Formula;
-import cz.muni.fi.ctl.formula.operator.BinaryOperator;
-import cz.muni.fi.ctl.formula.operator.UnaryOperator;
-import cz.muni.fi.ctl.formula.proposition.Contradiction;
-import cz.muni.fi.ctl.formula.proposition.FloatProposition;
-import cz.muni.fi.ctl.formula.proposition.Tautology;
-import org.junit.Rule;
-import org.junit.Test;
-import org.junit.rules.ExpectedException;
-
-import static org.hamcrest.CoreMatchers.instanceOf;
-import static org.junit.Assert.assertEquals;
-import static org.junit.Assert.assertThat;
-
-/**
- * Tests for FormulaParser
- */
-public class FormulaParserTest {
-
-    private static final float TOLERANCE = 0.0001f;
-
-    @Rule
-    public final ExpectedException exception = ExpectedException.none();
-
-    @Test
-    public void propositionTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("#define a B > 3.0 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        FloatProposition proposition = (FloatProposition) formula;
-        assertEquals(proposition.getThreshold(), 3.0, TOLERANCE);
-        assertEquals(proposition.getVariable(), "B");
-        //long names
-        formula = parser.parse("#define someLongName ANOTHERlongNAME > 1234.5678 #property someLongName");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getThreshold(), 1234.5678, TOLERANCE);
-        assertEquals(proposition.getVariable(), "ANOTHERlongNAME");
-        //negative numbers
-        formula = parser.parse("#define a B > -23.4 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getThreshold(), -23.4, TOLERANCE);
-        assertEquals(proposition.getVariable(), "B");
-        //unused propositions
-        //this should produce an exception
-        exception.expect(IllegalArgumentException.class);
-        parser.parse("#define a B > 3.0 #define c C <= 23.4 #define z Z > 4.0 #property c");
-        //proposition redefinition
-        exception.expect(IllegalArgumentException.class);
-        parser.parse("#define a B > 3.0 #define a C <= 23.4 #define z Z > 4.0 #property c");
-        //unknown proposition
-        exception.expect(IllegalArgumentException.class);
-        parser.parse("#define a B > 3.0 #define a C <= 23.4 #define z Z > 4.0 #property D");
-    }
-
-    @Test
-    public void floatValuesTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("#define a B > 3 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        FloatProposition proposition = (FloatProposition) formula;
-        assertEquals(proposition.getVariable(), "B");
-        assertEquals(proposition.getThreshold(), 3, TOLERANCE);
-        formula = parser.parse("#define a B > -3 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getVariable(), "B");
-        assertEquals(proposition.getThreshold(), -3, TOLERANCE);
-        formula = parser.parse("#define a B > 0.2 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getVariable(), "B");
-        assertEquals(proposition.getThreshold(), 0.2, TOLERANCE);
-        formula = parser.parse("#define a B > -0.4 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getVariable(), "B");
-        assertEquals(proposition.getThreshold(), -0.4, TOLERANCE);
-        formula = parser.parse("#define a B > .3 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getVariable(), "B");
-        assertEquals(proposition.getThreshold(), 0.3, TOLERANCE);
-        formula = parser.parse("#define a B > -.9 #property a");
-        assertThat(formula, instanceOf(FloatProposition.class));
-        proposition = (FloatProposition) formula;
-        assertEquals(proposition.getVariable(), "B");
-        assertEquals(proposition.getThreshold(), -0.9, TOLERANCE);
-    }
-
-    @Test
-    public void booleanLiteralsTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("#property True");
-        assertThat(formula, instanceOf(Tautology.class));
-        formula = parser.parse("#property False");
-        assertThat(formula, instanceOf(Contradiction.class));
-    }
-
-    @Test
-    public void unaryTemporalOperatorTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("#property EX False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.EXISTS_NEXT);
-        formula = parser.parse("#property AX False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.ALL_NEXT);
-        formula = parser.parse("#property EF False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.EXISTS_FUTURE);
-        formula = parser.parse("#property AF False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.ALL_FUTURE);
-        formula = parser.parse("#property EG False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.EXISTS_GLOBAL);
-        formula = parser.parse("#property AG False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.ALL_GLOBAL);
-    }
-
-    @Test
-    public void binaryTemporalOperator() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("#property E (True U False)");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(BinaryOperator.class));
-        assertEquals(formula.getOperator(), BinaryOperator.EXISTS_UNTIL);
-        formula = parser.parse("#property A (True U False)");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(BinaryOperator.class));
-        assertEquals(formula.getOperator(), BinaryOperator.ALL_UNTIL);
-    }
-
-    @Test
-    public void booleanOperatorTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("#property ! False");
-        assertEquals(formula.getSubFormulaCount(), 1);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(UnaryOperator.class));
-        assertEquals(formula.getOperator(), UnaryOperator.NEGATION);
-        formula = parser.parse("#property (True && False)");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(BinaryOperator.class));
-        assertEquals(formula.getOperator(), BinaryOperator.AND);
-        formula = parser.parse("#property (True || False)");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(BinaryOperator.class));
-        assertEquals(formula.getOperator(), BinaryOperator.OR);
-        formula = parser.parse("#property (True => False)");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(BinaryOperator.class));
-        assertEquals(formula.getOperator(), BinaryOperator.IMPLICATION);
-        formula = parser.parse("#property (True <=> False)");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(Tautology.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(Contradiction.class));
-        assertThat(formula.getOperator(), instanceOf(BinaryOperator.class));
-        assertEquals(formula.getOperator(), BinaryOperator.EQUIVALENCE);
-    }
-
-    @Test
-    public void complexTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("" +
-                "#define first XY < 2.7 \n" +
-                "#define second aBx >= -0.01 \t \t \n" +
-                "#define Third zZ != 41234.45 \n" +
-                "#property E ( AF EX AG (first => True) U ( EF Third <=> A ( False U second ) ) ) ");
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertEquals(formula.getOperator(), BinaryOperator.EXISTS_UNTIL);
-        Formula af = formula.getSubFormulaAt(0);
-        assertEquals(af.getSubFormulaCount(), 1);
-        assertEquals(af.getOperator(), UnaryOperator.ALL_FUTURE);
-        Formula ex = af.getSubFormulaAt(0);
-        assertEquals(ex.getSubFormulaCount(), 1);
-        assertEquals(ex.getOperator(), UnaryOperator.EXISTS_NEXT);
-        Formula ag = ex.getSubFormulaAt(0);
-        assertEquals(ag.getSubFormulaCount(), 1);
-        assertEquals(ag.getOperator(), UnaryOperator.ALL_GLOBAL);
-        Formula impl = ag.getSubFormulaAt(0);
-        assertEquals(impl.getSubFormulaCount(), 2);
-        assertEquals(impl.getOperator(), BinaryOperator.IMPLICATION);
-        assertThat(impl.getSubFormulaAt(0), instanceOf(FloatProposition.class));
-        assertThat(impl.getSubFormulaAt(1), instanceOf(Tautology.class));
-        FloatProposition first = (FloatProposition) impl.getSubFormulaAt(0);
-        assertEquals(first.getVariable(), "XY");
-        assertEquals(first.getThreshold(), 2.7, TOLERANCE);
-        Formula equiv = formula.getSubFormulaAt(1);
-        assertEquals(equiv.getSubFormulaCount(), 2);
-        assertEquals(equiv.getOperator(), BinaryOperator.EQUIVALENCE);
-        Formula ef = equiv.getSubFormulaAt(0);
-        assertEquals(ef.getSubFormulaCount(), 1);
-        assertEquals(ef.getOperator(), UnaryOperator.EXISTS_FUTURE);
-        assertThat(ef.getSubFormulaAt(0), instanceOf(FloatProposition.class));
-        FloatProposition third = (FloatProposition) ef.getSubFormulaAt(0);
-        assertEquals(third.getVariable(), "zZ");
-        assertEquals(third.getThreshold(), 41234.45, TOLERANCE);
-        Formula au = equiv.getSubFormulaAt(1);
-        assertEquals(au.getSubFormulaCount(), 2);
-        assertEquals(au.getOperator(), BinaryOperator.ALL_UNTIL);
-        assertThat(au.getSubFormulaAt(0), instanceOf(Contradiction.class));
-        assertThat(au.getSubFormulaAt(1), instanceOf(FloatProposition.class));
-        FloatProposition second = (FloatProposition) au.getSubFormulaAt(1);
-        assertEquals(second.getVariable(), "aBx");
-        assertEquals(second.getThreshold(), -0.01, TOLERANCE);
-    }
-
-    @Test
-    public void whitespaceTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse("\t \n \n#define\t\ta\nx    < \t \n 1.0\n#define\n\n\nb   x\t>2.0 #property \t\t E(   a U \tb )\n\n\t");
-        assertEquals(formula.getOperator(), BinaryOperator.EXISTS_UNTIL);
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertThat(formula.getSubFormulaAt(0), instanceOf(FloatProposition.class));
-        assertThat(formula.getSubFormulaAt(1), instanceOf(FloatProposition.class));
-        FloatProposition a = (FloatProposition) formula.getSubFormulaAt(0);
-        FloatProposition b = (FloatProposition) formula.getSubFormulaAt(1);
-        assertEquals(a.getVariable(), "x");
-        assertEquals(b.getVariable(), "x");
-        assertEquals(a.getThreshold(), 1.0, TOLERANCE);
-        assertEquals(b.getThreshold(), 2.0, TOLERANCE);
-    }
-
-    @Test
-    public void realLifeTest() {
-        FormulaParser parser = new FormulaParser();
-        Formula formula = parser.parse( "#define a x < 4.9 \n" +
-                                        "#define b x > 5.1 \n" +
-                                        "#property ( EF AG a && EF AG b )"
-        );
-        assertEquals(formula.getSubFormulaCount(), 2);
-        assertEquals(formula.getOperator(), BinaryOperator.AND);
-        Formula ef1 = formula.getSubFormulaAt(0);
-        Formula ef2 = formula.getSubFormulaAt(1);
-        assertEquals(ef1.getOperator(), UnaryOperator.EXISTS_FUTURE);
-        assertEquals(ef2.getOperator(), UnaryOperator.EXISTS_FUTURE);
-        Formula ag1 = ef1.getSubFormulaAt(0);
-        Formula ag2 = ef2.getSubFormulaAt(0);
-        assertEquals(ag1.getOperator(), UnaryOperator.ALL_GLOBAL);
-        assertEquals(ag2.getOperator(), UnaryOperator.ALL_GLOBAL);
-        Formula aF = ag1.getSubFormulaAt(0);
-        Formula bF = ag2.getSubFormulaAt(0);
-        assertThat(aF, instanceOf(FloatProposition.class));
-        assertThat(bF, instanceOf(FloatProposition.class));
-        FloatProposition a = (FloatProposition) aF;
-        FloatProposition b = (FloatProposition) bF;
-        assertEquals(a.getVariable(), "x");
-        assertEquals(b.getVariable(), "x");
-        assertEquals(a.getThreshold(), 4.9, TOLERANCE);
-        assertEquals(b.getThreshold(), 5.1, TOLERANCE);
-    }
-
-}
diff --git a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
new file mode 100644
index 0000000..8868427
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
@@ -0,0 +1,73 @@
+package cz.muni.fi.ctl
+
+import org.junit.Test
+import kotlin.test.assertEquals
+
+class OptimizerTest {
+
+    val p1 = Reference("p1")
+    val p2 = Reference("p2")
+
+    val optimizer = Optimizer()
+
+    Test fun complexTest() {
+        val f1 = FloatProposition("var2", FloatOp.LT_EQ, -15.3)
+        val nf1 = FloatProposition("var2", FloatOp.GT, -15.3)
+        val d1 = DirectionProposition("var1", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+
+        val prop = EX(not(f1) EU not(True and ( not(d1) or (p1 AU False))))
+        val optimized = optimizer.optimize(prop)
+
+        assertEquals(EX(nf1 EU d1), optimized)
+        assertEquals(optimized, optimizer.optimize(optimized))
+    }
+
+    Test fun orNegation() {
+        assertEquals(not(p1 and p2), optimizer.optimize(not(p1) or not(p2)))
+    }
+
+    Test fun andNegation() {
+        assertEquals(not(p1 or p2), optimizer.optimize(not(p1) and not(p2)))
+    }
+
+    Test fun floatNegation() {
+        assertEquals(
+                FloatProposition("val", FloatOp.NEQ, 13.2),
+                optimizer.optimize(
+                        not(FloatProposition("val", FloatOp.EQ, 13.2))
+                )
+        )
+        assertEquals(
+                FloatProposition("val", FloatOp.LT_EQ, 13.2),
+                optimizer.optimize(
+                        not(FloatProposition("val", FloatOp.GT, 13.2))
+                )
+        )
+    }
+
+    Test fun doubleNegation() {
+        assertEquals(p1, optimizer.optimize(not(not(p1))))
+        assertEquals(not(p2), optimizer.optimize(not(not(not(p2)))))
+    }
+
+    Test fun booleanReduction() {
+        val prop = EX( not(False) and ( (True or False) EU (False AU True) ))
+        assertEquals(True, optimizer.optimize(prop))
+    }
+
+    Test fun floatPreserve() {
+        val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2)
+        assertEquals(prop, optimizer.optimize(prop))
+    }
+
+    Test fun booleanPreserve() {
+        assertEquals(True, optimizer.optimize(True))
+        assertEquals(False, optimizer.optimize(False))
+    }
+
+    Test fun directionPreserve() {
+        val prop = DirectionProposition("var", DirectionProposition.Direction.IN, DirectionProposition.Facet.POSITIVE)
+        assertEquals(prop, optimizer.optimize(prop))
+    }
+
+}
\ No newline at end of file

From c4e85ead66e1312e72adad0936363453b38a3f87 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 31 Jul 2015 23:29:32 +0200
Subject: [PATCH 24/36] A little coverage/visibility boost.

---
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt    |  6 ++--
 src/main/kotlin/cz/muni/fi/ctl/Operators.kt   |  4 +--
 .../kotlin/cz/muni/fi/ctl/FormulasTest.kt     | 35 +++++++++++++++++++
 .../kotlin/cz/muni/fi/ctl/OptimizerTest.kt    |  9 +++--
 4 files changed, 47 insertions(+), 7 deletions(-)

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index 1edf0c8..ba0dc38 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -26,7 +26,7 @@ data class FormulaImpl (
     override fun toString(): String = when (operator.cardinality) {
         1 -> "$operator(${subFormulas[0]})"
         2 -> "${subFormulas[0]} $operator ${subFormulas[1]}"
-        else -> "$operator($subFormulas)"
+        else -> "$operator($subFormulas)"   //this never happens
     }
 
 }
@@ -63,12 +63,12 @@ public data class DirectionProposition (
 
     override fun toString(): String = "$variable:$direction$facet"
 
-    enum class Direction(val str: String) {
+    enum class Direction(private val str: String) {
         IN("in"), OUT("out");
         override fun toString(): String = str
     }
 
-    enum class Facet(val str: String) {
+    enum class Facet(private val str: String) {
         POSITIVE("+"), NEGATIVE("-");
         override fun toString(): String = str
     }
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
index 1eb6936..de744cf 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
@@ -1,6 +1,6 @@
 package cz.muni.fi.ctl
 
-public enum class Op(val cardinality: Int, val str: String) {
+public enum class Op(val cardinality: Int, private val str: String) {
     //nullary
     ATOM(0,"null"),
     //unary
@@ -22,7 +22,7 @@ public enum class Op(val cardinality: Int, val str: String) {
     override fun toString(): String = str
 }
 
-public enum class FloatOp(val str: String) {
+public enum class FloatOp(private val str: String) {
     EQ("=="), NEQ("!="), GT(">"), GT_EQ(">="), LT("<"), LT_EQ("<=");
 
     val neg: FloatOp
diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
index 14ab1a6..ed526d9 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -45,4 +45,39 @@ class MapTest {
 
     }
 
+}
+
+class Misc {
+
+    Test fun booleanToString() {
+        assertEquals("True", True.toString())
+        assertEquals("False", False.toString())
+    }
+
+    Test fun formulaToString() {
+        assertEquals("True && EX(False EU True)", (True and EX(False EU True)).toString())
+    }
+
+    Test fun floatToString() {
+        assertEquals("prop > 5.3", FloatProposition("prop", FloatOp.GT, 5.3).toString())
+    }
+
+    Test fun directionToString() {
+        assertEquals("prop:in+", DirectionProposition("prop", DirectionProposition.Direction.IN, DirectionProposition.Facet.POSITIVE).toString())
+    }
+
+    Test fun emptyFormula() {
+        assertEquals("null([])",FormulaImpl().toString())
+    }
+
+    Test(expected = IllegalArgumentException::class)
+    fun notEnoughFormulas() {
+        FormulaImpl(Op.ALL_UNTIL, True)
+    }
+
+    Test(expected = IllegalArgumentException::class)
+    fun tooManyFormulas() {
+        FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
+    }
+
 }
\ No newline at end of file
diff --git a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
index 8868427..4a62c91 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
@@ -15,10 +15,10 @@ class OptimizerTest {
         val nf1 = FloatProposition("var2", FloatOp.GT, -15.3)
         val d1 = DirectionProposition("var1", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
 
-        val prop = EX(not(f1) EU not(True and ( not(d1) or (p1 AU False))))
+        val prop = p1 AU EX(not(f1) EU not(True and ( not(d1) or (p1 AU False))))
         val optimized = optimizer.optimize(prop)
 
-        assertEquals(EX(nf1 EU d1), optimized)
+        assertEquals(p1 AU EX(nf1 EU d1), optimized)
         assertEquals(optimized, optimizer.optimize(optimized))
     }
 
@@ -55,6 +55,11 @@ class OptimizerTest {
         assertEquals(True, optimizer.optimize(prop))
     }
 
+    Test fun preserveUnsupported() {
+        val prop = AX(EG(p1 implies p2))
+        assertEquals(prop, optimizer.optimize(prop))
+    }
+
     Test fun floatPreserve() {
         val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2)
         assertEquals(prop, optimizer.optimize(prop))

From aa532f18955850300455940b1b45e0c1e03560fa Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Wed, 5 Aug 2015 15:53:30 +0200
Subject: [PATCH 25/36] Remove #check clause and weird EU/AU syntax. Not really
 practical and universall -> confusing.

---
 src/main/antlr4/CTL.g4                        | 13 ++---
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt    | 14 +----
 src/main/kotlin/cz/muni/fi/ctl/Operators.kt   |  9 +++
 src/main/kotlin/cz/muni/fi/ctl/Parser.kt      | 55 +++++++++----------
 .../kotlin/cz/muni/fi/ctl/FormulasTest.kt     |  6 +-
 .../kotlin/cz/muni/fi/ctl/NormalizerTest.kt   |  6 +-
 .../kotlin/cz/muni/fi/ctl/OptimizerTest.kt    |  4 +-
 7 files changed, 51 insertions(+), 56 deletions(-)

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 4fd50c6..578b673 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -7,7 +7,6 @@ root : fullStop? (statement fullStop)*;
 
 statement : '#include' STRING                       # include
           | VAR_NAME '=' formula                    # assign
-          | '#check' formula (',' formula)*         # check
           ;
 
 fullStop : NEWLINE+ | EOF;
@@ -20,21 +19,19 @@ formula : VAR_NAME                                          #id
         | VAR_NAME floatOp FLOAT_VAL                        #proposition
         | '(' formula ')'                                   #parenthesis
         | unaryOp formula                                   #unary
-        | formula boolOp formula                            #binary
-        | 'E' formula 'U' formula                           #existUntil
-        | 'A' formula 'U' formula                           #allUntil
+        | formula binaryOp formula                          #binary
         ;
 
 /** Helper/Grouping parser rules **/
 
 unaryOp : NEG | EX | EF | EG | AX | AF | AG;
-boolOp : CON | DIS | IMPL | EQIV;
+binaryOp : EU | AU | CON | DIS | IMPL | EQIV;
 floatOp : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
 
 /** Terminals **/
 
-TRUE : ([tT]'rue' | 'tt' | 'TT');
-FALSE : ([fF]'alse' | 'ff' | 'FF');
+TRUE : ([tT]'rue' | 'tt');
+FALSE : ([fF]'alse' | 'ff');
 
 IN : 'in';
 OUT : 'out';
@@ -50,6 +47,8 @@ EG : 'EG';
 AX : 'AX';
 AF : 'AF';
 AG : 'AG';
+EU : 'EU';
+AU : 'AU';
 
 EQ : '==';
 NEQ : '!=';
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index ba0dc38..5f27cc1 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -57,22 +57,12 @@ public data class FloatProposition (
 //Direction atoms
 public data class DirectionProposition (
         val variable: String,
-        val direction: DirectionProposition.Direction,
-        val facet: DirectionProposition.Facet
+        val direction: Direction,
+        val facet: Facet
 ) : Atom() {
 
     override fun toString(): String = "$variable:$direction$facet"
 
-    enum class Direction(private val str: String) {
-        IN("in"), OUT("out");
-        override fun toString(): String = str
-    }
-
-    enum class Facet(private val str: String) {
-        POSITIVE("+"), NEGATIVE("-");
-        override fun toString(): String = str
-    }
-
 }
 
 
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
index de744cf..d651b67 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Operators.kt
@@ -37,5 +37,14 @@ public enum class FloatOp(private val str: String) {
 
     override fun toString(): String = str
 
+}
 
+public enum class Direction(private val str: String) {
+    IN("in"), OUT("out");
+    override fun toString(): String = str
+}
+
+public enum class Facet(private val str: String) {
+    POSITIVE("+"), NEGATIVE("-");
+    override fun toString(): String = str
 }
\ No newline at end of file
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
index bf26422..cf073ff 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
@@ -14,16 +14,27 @@ import java.util.HashMap
 import java.util.HashSet
 import java.util.Stack
 
+/**
+ * Workflow:
+ * Antlr constructs a parse tree that is transformed into FileContext.
+ * File context is a direct representation of a file.
+ * Using FileParser, includes in the file context are resolved and merged into a ParserContext.
+ * Duplicate assignments are checked at this stage.
+ * Lastly, Parser resolves references in ParserContext (checking for undefined or cyclic references)
+ * and returns a final map of valid assignments
+ */
+
 public class Parser {
 
-    public fun parse(input: String): List<Formula> = process(FileParser().process(input))
+    public fun formula(input: String): Formula = parse("val = $input").get("val")!!
+
+    public fun parse(input: String): Map<String, Formula> = process(FileParser().process(input))
 
-    public fun parse(input: File): List<Formula> = process(FileParser().process(input))
+    public fun parse(input: File): Map<String, Formula> = process(FileParser().process(input))
 
-    fun process(ctx: ParserContext): List<Formula> {
+    fun process(ctx: ParserContext): Map<String, Formula> {
 
         val formulas = ctx.formulas
-        val checks = ctx.checks
 
         // Resolve references
 
@@ -50,7 +61,7 @@ public class Parser {
             references[name] = formula.treeMap(::replace)
         }
 
-        return checks.map(::replace)
+        return references
     }
 
 }
@@ -89,8 +100,7 @@ class FileParser {
 }
 
 data class ParserContext(
-        val assignments: List<Assignment>,
-        val checks: List<Formula> = listOf()
+        val assignments: List<Assignment>
 ) {
 
     val formulas: Map<String, Formula>
@@ -112,7 +122,7 @@ data class ParserContext(
     }
 
     fun plus(ctx: ParserContext): ParserContext {
-        return ParserContext(assignments + ctx.assignments, checks + ctx.checks)
+        return ParserContext(assignments + ctx.assignments)
     }
 
 }
@@ -121,11 +131,10 @@ class FileContext(val location: String) : CTLBaseListener() {
 
     val includes = ArrayList<File>()
     val assignments = ArrayList<Assignment>()
-    val checks = ArrayList<Formula>()
 
     private val formulas = ParseTreeProperty<Formula>()
 
-    fun toParseContext() = ParserContext(assignments, checks)
+    fun toParseContext() = ParserContext(assignments)
 
     override fun exitInclude(ctx: CTLParser.IncludeContext) {
         val string = ctx.STRING().getText()!!
@@ -140,12 +149,6 @@ class FileContext(val location: String) : CTLBaseListener() {
         ))
     }
 
-    override fun exitCheck(ctx: CTLParser.CheckContext) {
-        for (context in ctx.formula()) {
-            checks.add(formulas[context]!!)
-        }
-    }
-
     /** ------ Formula Parsing ------ **/
 
     override fun exitId(ctx: CTLParser.IdContext) {
@@ -159,8 +162,8 @@ class FileContext(val location: String) : CTLBaseListener() {
     override fun exitDirection(ctx: CTLParser.DirectionContext) {
         formulas[ctx] = DirectionProposition(
                 variable = ctx.VAR_NAME().getText()!!,
-                direction = if (ctx.IN() != null) DirectionProposition.Direction.IN else DirectionProposition.Direction.OUT,
-                facet = if (ctx.PLUS() != null) DirectionProposition.Facet.POSITIVE else DirectionProposition.Facet.NEGATIVE
+                direction = if (ctx.IN() != null) Direction.IN else Direction.OUT,
+                facet = if (ctx.PLUS() != null) Facet.POSITIVE else Facet.NEGATIVE
         )
     }
 
@@ -181,16 +184,9 @@ class FileContext(val location: String) : CTLBaseListener() {
     }
 
     override fun exitBinary(ctx: CTLParser.BinaryContext) {
-        formulas[ctx] = FormulaImpl(ctx.boolOp().toOperator(), formulas[ctx.formula(0)]!!, formulas[ctx.formula(1)]!!)
-    }
-
-    override fun exitExistUntil(ctx: CTLParser.ExistUntilContext) {
-        formulas[ctx] = formulas[ctx.formula(0)]!! EU formulas[ctx.formula(1)]!!
+        formulas[ctx] = FormulaImpl(ctx.binaryOp().toOperator(), formulas[ctx.formula(0)]!!, formulas[ctx.formula(1)]!!)
     }
 
-    override fun exitAllUntil(ctx: CTLParser.AllUntilContext) {
-        formulas[ctx] = formulas[ctx.formula(0)]!! AU formulas[ctx.formula(1)]!!
-    }
 }
 
 data class Assignment(val name: String, val formula: Formula, val location: String)
@@ -199,7 +195,9 @@ data class Reference(val name: String) : Atom()
 
 //convenience methods
 
-fun CTLParser.BoolOpContext.toOperator(): Op = when {
+fun CTLParser.BinaryOpContext.toOperator(): Op = when {
+    EU() != null -> Op.EXISTS_UNTIL
+    AU() != null -> Op.ALL_UNTIL
     CON() != null -> Op.AND
     DIS() != null -> Op.OR
     IMPL() != null -> Op.IMPLICATION
@@ -219,13 +217,12 @@ fun CTLParser.UnaryOpContext.toOperator(): Op = when {
 }
 
 fun CTLParser.FloatOpContext.toOperator(): FloatOp = when {
-    EQ() != null -> FloatOp.EQ
     NEQ() != null -> FloatOp.NEQ
     LT() != null -> FloatOp.LT
     LTEQ() != null -> FloatOp.LT_EQ
     GT() != null -> FloatOp.GT
     GTEQ() != null -> FloatOp.GT_EQ
-    else -> throw IllegalStateException("Invalid float operator: ${getText()}")
+    else -> FloatOp.EQ
 }
 
 fun <T> ParseTreeProperty<T>.set(k: ParseTree, v: T) = this.put(k, v)
diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
index ed526d9..216aa78 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -8,7 +8,7 @@ class MapTest {
     val formula = EX( True EU (
             FloatProposition("var", FloatOp.EQ, 13.3)
                     or
-            DirectionProposition("val", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+            DirectionProposition("val", Direction.IN, Facet.NEGATIVE)
         )
     )
 
@@ -39,7 +39,7 @@ class MapTest {
                 AX( True AU (
                 FloatProposition("var", FloatOp.EQ, 13.3)
                     and
-                DirectionProposition("val", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+                DirectionProposition("val", Direction.IN, Facet.NEGATIVE)
                 )
         ), transform(formula))
 
@@ -63,7 +63,7 @@ class Misc {
     }
 
     Test fun directionToString() {
-        assertEquals("prop:in+", DirectionProposition("prop", DirectionProposition.Direction.IN, DirectionProposition.Facet.POSITIVE).toString())
+        assertEquals("prop:in+", DirectionProposition("prop", Direction.IN, Facet.POSITIVE).toString())
     }
 
     Test fun emptyFormula() {
diff --git a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
index 6fc14a7..fb766de 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
@@ -16,8 +16,8 @@ class UntilNormalFormTest {
 
         val f1 = FloatProposition("var1", FloatOp.NEQ, 14.3)
         val f2 = FloatProposition("var2", FloatOp.LT, -15.3)
-        val d1 = DirectionProposition("var1", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
-        val d2 = DirectionProposition("var2", DirectionProposition.Direction.OUT, DirectionProposition.Facet.POSITIVE)
+        val d1 = DirectionProposition("var1", Direction.IN, Facet.NEGATIVE)
+        val d2 = DirectionProposition("var2", Direction.OUT, Facet.POSITIVE)
 
         val prop = EF( AF((EX(f1) AU False) equal not(d2)) implies AX( EG(f2) EU AG(d1)))
         assertEquals(
@@ -134,7 +134,7 @@ class UntilNormalFormTest {
     }
 
     Test fun directionPreserve() {
-        val prop = DirectionProposition("var", DirectionProposition.Direction.IN, DirectionProposition.Facet.POSITIVE)
+        val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE)
         assertEquals(prop, normalizer.normalize(prop))
     }
 
diff --git a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
index 4a62c91..3eda50e 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
@@ -13,7 +13,7 @@ class OptimizerTest {
     Test fun complexTest() {
         val f1 = FloatProposition("var2", FloatOp.LT_EQ, -15.3)
         val nf1 = FloatProposition("var2", FloatOp.GT, -15.3)
-        val d1 = DirectionProposition("var1", DirectionProposition.Direction.IN, DirectionProposition.Facet.NEGATIVE)
+        val d1 = DirectionProposition("var1", Direction.IN, Facet.NEGATIVE)
 
         val prop = p1 AU EX(not(f1) EU not(True and ( not(d1) or (p1 AU False))))
         val optimized = optimizer.optimize(prop)
@@ -71,7 +71,7 @@ class OptimizerTest {
     }
 
     Test fun directionPreserve() {
-        val prop = DirectionProposition("var", DirectionProposition.Direction.IN, DirectionProposition.Facet.POSITIVE)
+        val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE)
         assertEquals(prop, optimizer.optimize(prop))
     }
 

From c0104af61b647105b3eb812a47f26735d62f9374 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Thu, 6 Aug 2015 00:18:40 +0200
Subject: [PATCH 26/36] Fix operator priority. Parser bugs and tests. Formula
 tostring format.

---
 src/main/antlr4/CTL.g4                        |   9 +-
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt    |   4 +-
 src/main/kotlin/cz/muni/fi/ctl/Parser.kt      |  40 +++--
 .../kotlin/cz/muni/fi/ctl/FormulasTest.kt     |  13 +-
 .../kotlin/cz/muni/fi/ctl/ParserBasicTest.kt  | 134 +++++++++++++++
 .../cz/muni/fi/ctl/ParserComplexTest.kt       | 112 ++++++++++++
 .../cz/muni/fi/ctl/ParserIncludeTest.kt       | 108 ++++++++++++
 .../cz/muni/fi/ctl/ParserReferencesTest.kt    | 160 ++++++++++++++++++
 8 files changed, 559 insertions(+), 21 deletions(-)
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 578b673..83af20f 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -19,13 +19,18 @@ formula : VAR_NAME                                          #id
         | VAR_NAME floatOp FLOAT_VAL                        #proposition
         | '(' formula ')'                                   #parenthesis
         | unaryOp formula                                   #unary
-        | formula binaryOp formula                          #binary
+        //we list operators explicitly, becuase writing them as a subrule broke operator priority
+        | formula CON formula                               #and
+        | formula DIS formula                               #or
+        | formula IMPL formula                              #implies
+        | formula EQIV formula                              #equal
+        | formula EU formula                                #EU
+        | formula AU formula                                #AU
         ;
 
 /** Helper/Grouping parser rules **/
 
 unaryOp : NEG | EX | EF | EG | AX | AF | AG;
-binaryOp : EU | AU | CON | DIS | IMPL | EQIV;
 floatOp : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
 
 /** Terminals **/
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index 5f27cc1..84f3fdc 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -24,8 +24,8 @@ data class FormulaImpl (
     constructor(operator: Op, vararg formulas: Formula) : this(operator, formulas.toList())
 
     override fun toString(): String = when (operator.cardinality) {
-        1 -> "$operator(${subFormulas[0]})"
-        2 -> "${subFormulas[0]} $operator ${subFormulas[1]}"
+        1 -> "$operator ${subFormulas[0]}"
+        2 -> "(${subFormulas[0]} $operator ${subFormulas[1]})"
         else -> "$operator($subFormulas)"   //this never happens
     }
 
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
index cf073ff..202e991 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
@@ -112,7 +112,7 @@ data class ParserContext(
     init {
         for (one in assignments) {
             for (two in assignments) {
-                if (one.name == two.name && one.location != two.location) {
+                if (one.name == two.name && (one.location != two.location || one.formula != two.formula)) {
                     throw IllegalStateException(
                             "Duplicate assignment for ${one.name} defined in ${one.location} and ${two.location}"
                     )
@@ -145,7 +145,7 @@ class FileContext(val location: String) : CTLBaseListener() {
         assignments.add(Assignment(
                 ctx.VAR_NAME().getText()!!,
                 formulas[ctx.formula()]!!,
-                location
+                location+":"+ctx.start.getLine()
         ))
     }
 
@@ -183,10 +183,29 @@ class FileContext(val location: String) : CTLBaseListener() {
         formulas[ctx] = FormulaImpl(ctx.unaryOp().toOperator(), formulas[ctx.formula()]!!)
     }
 
-    override fun exitBinary(ctx: CTLParser.BinaryContext) {
-        formulas[ctx] = FormulaImpl(ctx.binaryOp().toOperator(), formulas[ctx.formula(0)]!!, formulas[ctx.formula(1)]!!)
+    override fun exitOr(ctx: CTLParser.OrContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! or formulas[ctx.formula(1)]!!
     }
 
+    override fun exitAnd(ctx: CTLParser.AndContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! and formulas[ctx.formula(1)]!!
+    }
+
+    override fun exitImplies(ctx: CTLParser.ImpliesContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! implies formulas[ctx.formula(1)]!!
+    }
+
+    override fun exitEqual(ctx: CTLParser.EqualContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! equal  formulas[ctx.formula(1)]!!
+    }
+
+    override fun exitEU(ctx: CTLParser.EUContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! EU formulas[ctx.formula(1)]!!
+    }
+
+    override fun exitAU(ctx: CTLParser.AUContext) {
+        formulas[ctx] = formulas[ctx.formula(0)]!! AU formulas[ctx.formula(1)]!!
+    }
 }
 
 data class Assignment(val name: String, val formula: Formula, val location: String)
@@ -195,25 +214,14 @@ data class Reference(val name: String) : Atom()
 
 //convenience methods
 
-fun CTLParser.BinaryOpContext.toOperator(): Op = when {
-    EU() != null -> Op.EXISTS_UNTIL
-    AU() != null -> Op.ALL_UNTIL
-    CON() != null -> Op.AND
-    DIS() != null -> Op.OR
-    IMPL() != null -> Op.IMPLICATION
-    EQIV() != null -> Op.EQUIVALENCE
-    else -> throw IllegalStateException("Invalid binary operator: ${getText()}")
-}
-
 fun CTLParser.UnaryOpContext.toOperator(): Op = when {
-    NEG() != null -> Op.NEGATION
     EX() != null -> Op.EXISTS_NEXT
     AX() != null -> Op.ALL_NEXT
     EF() != null -> Op.EXISTS_FUTURE
     AF() != null -> Op.ALL_FUTURE
     EG() != null -> Op.EXISTS_GLOBAL
     AG() != null -> Op.ALL_GLOBAL
-    else -> throw IllegalStateException("Invalid unary operator: ${getText()}")
+    else -> Op.NEGATION
 }
 
 fun CTLParser.FloatOpContext.toOperator(): FloatOp = when {
diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
index 216aa78..a5707eb 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -55,7 +55,7 @@ class Misc {
     }
 
     Test fun formulaToString() {
-        assertEquals("True && EX(False EU True)", (True and EX(False EU True)).toString())
+        assertEquals("(True && EX (False EU True))", (True and EX(False EU True)).toString())
     }
 
     Test fun floatToString() {
@@ -80,4 +80,15 @@ class Misc {
         FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
     }
 
+    Test fun get() {
+        val float = FloatProposition("val", FloatOp.GT, 34.12)
+        assertEquals("val", float.variable)
+        assertEquals(FloatOp.GT, float.floatOp)
+        assertEquals(34.12, float.value)
+        val dir = DirectionProposition("var", Direction.IN, Facet.NEGATIVE)
+        assertEquals("var", dir.variable)
+        assertEquals(Direction.IN, dir.direction)
+        assertEquals(Facet.NEGATIVE, dir.facet)
+    }
+
 }
\ No newline at end of file
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt
new file mode 100644
index 0000000..d22251b
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt
@@ -0,0 +1,134 @@
+package cz.muni.fi.ctl
+
+import org.junit.Test
+import kotlin.test.assertEquals
+
+class Basic {
+
+    val parser = Parser()
+
+    Test fun parenthesis() {
+        assertEquals(
+                True,
+                parser.formula("(True)")
+        )
+    }
+
+    Test fun binaryOps() {
+        assertEquals(
+                True EU False,
+                parser.formula("True EU False")
+        )
+        assertEquals(
+                True AU False,
+                parser.formula("True AU False")
+        )
+        assertEquals(
+                True and False,
+                parser.formula("True && False")
+        )
+        assertEquals(
+                True or False,
+                parser.formula("True || False")
+        )
+        assertEquals(
+                True implies False,
+                parser.formula("True => False")
+        )
+        assertEquals(
+                True equal False,
+                parser.formula("True <=> False")
+        )
+    }
+
+    Test fun unaryOps() {
+        assertEquals(
+                not(True),
+                parser.formula("!True")
+        )
+        assertEquals(
+                EX(True),
+                parser.formula("EX True")
+        )
+        assertEquals(
+                AX(True),
+                parser.formula("AX True")
+        )
+        assertEquals(
+                EF(True),
+                parser.formula("EF True")
+        )
+        assertEquals(
+                AF(True),
+                parser.formula("AF True")
+        )
+        assertEquals(
+                EG(True),
+                parser.formula("EG True")
+        )
+        assertEquals(
+                AG(True),
+                parser.formula("AG True")
+        )
+    }
+
+    Test fun floats() {
+        assertEquals(
+                FloatProposition("var", FloatOp.EQ, 0.0),
+                parser.formula("var == 0")
+        )
+        assertEquals(
+                FloatProposition("var", FloatOp.EQ, 1.0),
+                parser.formula("var == 1")
+        )
+        assertEquals(
+                FloatProposition("var", FloatOp.NEQ, -1.0),
+                parser.formula("var != -1")
+        )
+        assertEquals(
+                FloatProposition("var", FloatOp.GT, 0.158),
+                parser.formula("var > 0.158")
+        )
+        assertEquals(
+                FloatProposition("var", FloatOp.GT_EQ, -0.9995),
+                parser.formula("var >= -0.9995")
+        )
+        assertEquals(
+                FloatProposition("var", FloatOp.LT, 1040.58),
+                parser.formula("var < 1040.58")
+        )
+        assertEquals(
+                FloatProposition("var", FloatOp.LT_EQ, -586.44),
+                parser.formula("var <= -586.44")
+        )
+    }
+
+    Test fun directions() {
+        assertEquals(
+                DirectionProposition("var", Direction.IN, Facet.POSITIVE),
+                parser.formula("var:in+")
+        )
+        assertEquals(
+                DirectionProposition("var", Direction.OUT, Facet.POSITIVE),
+                parser.formula("var:out+")
+        )
+        assertEquals(
+                DirectionProposition("var", Direction.IN, Facet.NEGATIVE),
+                parser.formula("var:in-")
+        )
+        assertEquals(
+                DirectionProposition("var", Direction.OUT, Facet.NEGATIVE),
+                parser.formula("var:out-")
+        )
+    }
+
+    Test fun booleans() {
+        assertEquals(True, parser.formula("true"))
+        assertEquals(True, parser.formula("True"))
+        assertEquals(True, parser.formula("tt"))
+        assertEquals(False, parser.formula("false"))
+        assertEquals(False, parser.formula("False"))
+        assertEquals(False, parser.formula("ff"))
+    }
+
+}
\ No newline at end of file
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
new file mode 100644
index 0000000..33b4c79
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
@@ -0,0 +1,112 @@
+package cz.muni.fi.ctl
+
+import org.junit.Test
+import java.io.File
+import kotlin.test.assertEquals
+
+class Complex {
+
+    val parser = Parser()
+
+
+    val p1 = FloatProposition("p1", FloatOp.EQ, 4.0)
+    val p2 = DirectionProposition("p2", Direction.IN, Facet.NEGATIVE)
+    val p3 = FloatProposition("p3", FloatOp.LT, -3.14)
+
+    Test fun complexFiles() {
+
+        val f1 = File.createTempFile("file", ".ctl")
+        val f2 = File.createTempFile("file2", ".ctl")
+        val f3 = File.createTempFile("file3", ".ctl")
+
+        f1.bufferedWriter().use {
+            it.write("c = p2:in- || EX p3 < -3.14 EU a")
+        }
+
+        f2.bufferedWriter().use {
+            it.write("#include \"${ f1.getAbsolutePath() }\" \n")
+            it.write("b = EX c <=> True \n")
+            it.write("d = e => e")
+        }
+
+        f3.bufferedWriter().use {
+            it.write("a = ! p1 == 4 \n")
+            it.write("#include \"${ f2.getAbsolutePath() }\" \n")
+            it.write("e = True && c || c && False")
+        }
+
+        val result = parser.parse(f3)
+
+        val a = not(p1)
+        val c = (p2 or EX(p3)) EU a
+        val b = EX(c) equal True
+        val e = (True and c) or (c and False)
+        val d = e implies e
+
+        assertEquals(5, result.size())
+        assertEquals(a, result.get("a"))
+        assertEquals(b, result.get("b"))
+        assertEquals(c, result.get("c"))
+        assertEquals(d, result.get("d"))
+        assertEquals(e, result.get("e"))
+
+        f1.delete()
+        f2.delete()
+        f3.delete()
+
+    }
+
+    Test fun complexString() {
+
+        val result = parser.parse("""
+            b = EX p3 < -3.14 EU a
+            a = (p1 == 4) && p2:in-
+            d = AG AX c
+            c = b <=> b
+            e = c && True || False && b
+        """)
+
+        val a = p1 and p2
+        val b = EX(p3) EU a
+        val c = b equal b
+        val d = AG(AX(c))
+        val e = (c and True) or (False and b)
+
+        assertEquals(5, result.size())
+        assertEquals(a, result.get("a"))
+        assertEquals(b, result.get("b"))
+        assertEquals(c, result.get("c"))
+        assertEquals(d, result.get("d"))
+        assertEquals(e, result.get("e"))
+
+    }
+
+    Test fun operatorPriority() {
+        assertEquals(
+                not(False) and not(True),
+                parser.formula("!False && !True")
+        )
+        assertEquals(
+                (True and False) or (False and True),
+                parser.formula("True && False || False && True")
+        )
+        assertEquals(
+                (True or False) implies (False or True),
+                parser.formula("True || False => False || True")
+        )
+        assertEquals(
+                (True implies False) equal (False implies True),
+                parser.formula("True => False <=> False => True")
+        )
+        assertEquals(
+                (True equal False) EU (False equal True),
+                parser.formula("True <=> False EU False <=> True")
+        )
+        assertEquals(
+                (True EU False) AU (False EU True),
+                parser.formula("True EU False AU False EU True")
+        )
+    }
+
+}
+
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt
new file mode 100644
index 0000000..463d119
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt
@@ -0,0 +1,108 @@
+package cz.muni.fi.ctl
+
+import org.junit.Test
+import java.io.File
+import java.io.FileNotFoundException
+import kotlin.test.assertEquals
+
+class Includes {
+
+    val parser = Parser()
+
+    Test(expected = FileNotFoundException::class)
+    fun invalidInclude() {
+        parser.parse("#include \"bogus.foo\" ")
+    }
+
+    Test fun duplicateInclude() {
+
+        val i1 = File.createTempFile("include1", ".ctl")
+        val i2 = File.createTempFile("include2", ".ctl")
+
+        i1.bufferedWriter().use {
+            it.write("val = True \n")
+            it.write("#include \"${ i1.getAbsolutePath() }\"")
+        }
+        i2.bufferedWriter().use {
+            it.write("#include \"${ i1.getAbsolutePath() }\" \n")
+            it.write("#include \"${ i2.getAbsolutePath() }\" \n")
+            it.write("val2 = False")
+        }
+
+        val result = parser.parse(
+                "#include \"${ i2.getAbsolutePath() }\" \n" +
+                        "#include \"${ i1.getAbsolutePath() }\" "
+        )
+
+        assertEquals(2, result.size())
+        assertEquals(True, result.get("val"))
+        assertEquals(False, result.get("val2"))
+
+        i1.delete()
+        i2.delete()
+
+    }
+
+    Test fun transitiveInclude() {
+
+        val i1 = File.createTempFile("include1", ".ctl")
+        val i2 = File.createTempFile("include2", ".ctl")
+
+        i1.bufferedWriter().use {
+            it.write("val = True")
+        }
+        i2.bufferedWriter().use {
+            it.write("#include \"${ i1.getAbsolutePath() }\"")
+        }
+
+        val result = parser.parse("#include \"${ i2.getAbsolutePath() }\"")
+
+        assertEquals(1, result.size())
+        assertEquals(True, result.get("val"))
+
+        i1.delete()
+        i2.delete()
+
+    }
+
+    Test fun simpleIncludeFromFile() {
+
+        val include = File.createTempFile("simpleInclude", ".ctl")
+
+        include.bufferedWriter().use {
+            it.write("val = True")
+        }
+
+        val file = File.createTempFile("simpleFile", ".ctl")
+        file.bufferedWriter().use {
+            it.write("#include \"${include.getAbsolutePath()}\"")
+        }
+
+        val result = parser.parse(file)
+
+        assertEquals(1, result.size())
+        assertEquals(True, result.get("val"))
+
+        file.delete()
+        include.delete()
+    }
+
+    Test fun simpleIncludeFromString() {
+
+        val file = File.createTempFile("simpleInclude", ".ctl")
+
+        file.bufferedWriter().use {
+            it.write("val = True")
+        }
+
+        val result = parser.parse(
+                "#include \"${ file.getAbsolutePath() }\""
+        )
+
+        assertEquals(1, result.size())
+        assertEquals(True, result.get("val"))
+
+        file.delete()
+    }
+
+}
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
new file mode 100644
index 0000000..0c462bd
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
@@ -0,0 +1,160 @@
+package cz.muni.fi.ctl
+
+import org.junit.Test
+import java.io.File
+import kotlin.test.assertEquals
+
+class References {
+
+    val parser = Parser()
+
+    Test(expected = IllegalStateException::class)
+    fun cyclicReferenceThroughFiles() {
+        val file = File.createTempFile("file", ".ctx")
+        try {
+
+            file.bufferedWriter().use {
+                it.write("k = m")
+            }
+
+            parser.parse("""
+                m = !k
+            """)
+        } finally {
+            file.delete()
+        }
+    }
+
+    Test(expected = IllegalStateException::class)
+    fun transitiveCyclicReference() {
+        parser.parse("""
+            k = EX l
+            l = AX m
+            m = ! k
+        """)
+    }
+
+    Test(expected = IllegalStateException::class)
+    fun simpleCyclicReference() {
+        parser.parse("k = !k")
+    }
+
+    Test(expected = IllegalStateException::class)
+    fun undefinedReference() {
+        parser.parse("k = EF m")
+    }
+
+    Test fun declarationOrderIndependence() {
+
+        val result = parser.parse("""
+            k = ! m
+            m = True
+        """)
+
+        assertEquals(2, result.size())
+        assertEquals(not(True), result.get("k"))
+        assertEquals(True, result.get("m"))
+
+    }
+
+    Test(expected = IllegalStateException::class)
+    fun duplicateDeclarationInFiles() {
+
+        val i1 = File.createTempFile("include1", ".ctl")
+
+        i1.bufferedWriter().use {
+            it.write("k = True")
+        }
+
+        try {
+            parser.parse(
+                    "#include \"${ i1.getAbsolutePath() }\" \n" +
+                            "k = False"
+            )
+        } finally {
+            i1.delete()
+        }
+    }
+
+    Test(expected = IllegalStateException::class)
+    fun duplicateDeclarationInString() {
+
+        parser.parse("""
+            k = True
+            l = False
+            k = False
+        """)
+    }
+
+    Test fun transitiveResolveInFiles() {
+
+        val i1 = File.createTempFile("include1", ".ctl")
+        val i2 = File.createTempFile("include2", ".ctl")
+
+        i1.bufferedWriter().use {
+            it.write("k = True")
+        }
+        i2.bufferedWriter().use {
+            it.write("l = EF k")
+        }
+
+        val result = parser.parse(
+                "m = !l \n" +
+                        "#include \"${ i1.getAbsolutePath() }\" \n" +
+                        "#include \"${ i2.getAbsolutePath() }\" \n"
+        )
+
+        assertEquals(3, result.size())
+        assertEquals(True, result.get("k"))
+        assertEquals(EF(True), result.get("l"))
+        assertEquals(not(EF(True)), result.get("m"))
+
+    }
+
+    Test fun transitiveResolveInString() {
+
+        val result = parser.parse("""
+                k = True
+                l = EF k
+                m = !l
+        """)
+
+        assertEquals(3, result.size())
+        assertEquals(True, result.get("k"))
+        assertEquals(EF(True), result.get("l"))
+        assertEquals(not(EF(True)), result.get("m"))
+
+    }
+
+    Test fun simpleResolveInInclude() {
+
+        val i = File.createTempFile("include", ".ctl")
+
+        i.bufferedWriter().use {
+            it.write("val = False")
+        }
+
+        val result = parser.parse(
+                "k = !val \n " +
+                        "#include \"${ i.getAbsoluteFile() }\" \n"
+        )
+
+        assertEquals(2, result.size())
+        assertEquals(False, result.get("val"))
+        assertEquals(not(False), result.get("k"))
+
+        i.delete()
+
+    }
+
+    Test fun simpleResolveInString() {
+        val result = parser.parse("""
+            k = True
+            l = !k
+        """)
+        assertEquals(2, result.size())
+        assertEquals(True, result.get("k"))
+        assertEquals(not(True), result.get("l"))
+    }
+
+}
\ No newline at end of file

From 487d6836fe7a1f9a3f360db13c2ac7345e8d5e96 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Thu, 6 Aug 2015 14:54:35 +0200
Subject: [PATCH 27/36] Fix right-associative operators.

---
 src/main/antlr4/CTL.g4                        |  6 +++---
 .../cz/muni/fi/ctl/ParserComplexTest.kt       | 19 +++++++++++++++++++
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 83af20f..3890b3d 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -22,10 +22,10 @@ formula : VAR_NAME                                          #id
         //we list operators explicitly, becuase writing them as a subrule broke operator priority
         | formula CON formula                               #and
         | formula DIS formula                               #or
-        | formula IMPL formula                              #implies
+        |<assoc=right> formula IMPL formula                              #implies
         | formula EQIV formula                              #equal
-        | formula EU formula                                #EU
-        | formula AU formula                                #AU
+        |<assoc=right> formula EU formula                                #EU
+        |<assoc=right> formula AU formula                                #AU
         ;
 
 /** Helper/Grouping parser rules **/
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
index 33b4c79..be1e75a 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
@@ -81,7 +81,26 @@ class Complex {
 
     }
 
+    Test fun operatorAssociativity() {
+        //These binary operators are by convention right-associative
+        //Other binary operators, such as &&, ||, <=> are associative,
+        //so it doesn't matter if we resolve them left to right or right to left
+        assertEquals(
+                True EU (False EU True),
+                parser.formula("True EU False EU True")
+        )
+        assertEquals(
+                True AU (False AU True),
+                parser.formula("True AU False AU True")
+        )
+        assertEquals(
+                True implies (False implies True),
+                parser.formula("True EU False EU True")
+        )
+    }
+
     Test fun operatorPriority() {
+        //we do not test every combination, since priority should be transitive
         assertEquals(
                 not(False) and not(True),
                 parser.formula("!False && !True")

From eb9cd5b06f7362d88782a7c446b1ef089490ccec Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Thu, 6 Aug 2015 14:54:35 +0200
Subject: [PATCH 28/36]  Fix right-associative operators.

---
 src/main/antlr4/CTL.g4                        |  6 +++---
 .../kotlin/cz/muni/fi/ctl/IntegrationTest.kt  |  5 +++++
 .../cz/muni/fi/ctl/ParserComplexTest.kt       | 19 +++++++++++++++++++
 3 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt

diff --git a/src/main/antlr4/CTL.g4 b/src/main/antlr4/CTL.g4
index 83af20f..3890b3d 100644
--- a/src/main/antlr4/CTL.g4
+++ b/src/main/antlr4/CTL.g4
@@ -22,10 +22,10 @@ formula : VAR_NAME                                          #id
         //we list operators explicitly, becuase writing them as a subrule broke operator priority
         | formula CON formula                               #and
         | formula DIS formula                               #or
-        | formula IMPL formula                              #implies
+        |<assoc=right> formula IMPL formula                              #implies
         | formula EQIV formula                              #equal
-        | formula EU formula                                #EU
-        | formula AU formula                                #AU
+        |<assoc=right> formula EU formula                                #EU
+        |<assoc=right> formula AU formula                                #AU
         ;
 
 /** Helper/Grouping parser rules **/
diff --git a/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
new file mode 100644
index 0000000..ce82ef6
--- /dev/null
+++ b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
@@ -0,0 +1,5 @@
+package cz.muni.fi.ctl
+
+/**
+ * Created by daemontus on 06/08/15.
+ */
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
index 33b4c79..fa5caf5 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
@@ -81,7 +81,26 @@ class Complex {
 
     }
 
+    Test fun operatorAssociativity() {
+        //These binary operators are by convention right-associative
+        //Other binary operators, such as &&, ||, <=> are associative,
+        //so it doesn't matter if we resolve them left to right or right to left
+        assertEquals(
+                True EU (False EU True),
+                parser.formula("True EU False EU True")
+        )
+        assertEquals(
+                True AU (False AU True),
+                parser.formula("True AU False AU True")
+        )
+        assertEquals(
+                True implies (False implies True),
+                parser.formula("True => False => True")
+        )
+    }
+
     Test fun operatorPriority() {
+        //we do not test every combination, since priority should be transitive
         assertEquals(
                 not(False) and not(True),
                 parser.formula("!False && !True")

From ad6fce3bd90a90c8824d0362367564087932cb3f Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Thu, 6 Aug 2015 15:26:41 +0200
Subject: [PATCH 29/36] Big complex integration test. Also usage example.

---
 src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt   |  2 +-
 .../kotlin/cz/muni/fi/ctl/IntegrationTest.kt  | 78 ++++++++++++++++++-
 2 files changed, 78 insertions(+), 2 deletions(-)

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
index 6a1ab42..8ae9c99 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Optimizer.kt
@@ -16,7 +16,7 @@ public class Optimizer {
 
     private val optimize = { f: Formula -> optimizeTree(f) }
 
-    fun optimizeTree(f: Formula): Formula = when {
+    private fun optimizeTree(f: Formula): Formula = when {
         f.operator.cardinality == 0 -> f
         f.operator == Op.NEGATION -> {
             val child = f[0]
diff --git a/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
index ce82ef6..46612bd 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
@@ -1,5 +1,81 @@
 package cz.muni.fi.ctl
 
+import org.junit.Test
+import java.io.File
+import kotlin.test.assertEquals
+
 /**
- * Created by daemontus on 06/08/15.
+ * Consider this an example of usage
  */
+class Integration {
+
+    Test fun test() {
+
+        val f1 = File.createTempFile("file", ".ctl")
+
+        val parser = Parser()
+        val normalizer = Normalizer()
+        val optimizer = Optimizer()
+
+        f1.bufferedWriter().use {
+            it.write("c = p2 > 3.14 <=> False \n")
+            it.write("pop = True EU c EU a \n")
+        }
+
+        val formulas = parser.parse(
+                "#include \"${ f1.getAbsolutePath() }\" \n" +
+        """
+            a = True && p1:out+
+            f = EF True && EG pop || AX a
+        """)
+
+        val p1 = DirectionProposition("p1", Direction.OUT, Facet.POSITIVE)
+        val p2 = FloatProposition("p2", FloatOp.GT, 3.14)
+        val np2 = FloatProposition("p2", FloatOp.LT_EQ, 3.14)
+
+        val a = True and p1
+        val c = p2 equal False
+        val pop = True EU (c EU a)
+        val f = (EF(True) and EG(pop)) or AX(a)
+
+        assertEquals(4, formulas.size())
+        assertEquals(a, formulas.get("a"))
+        assertEquals(c, formulas.get("c"))
+        assertEquals(pop, formulas.get("pop"))
+        assertEquals(f, formulas.get("f"))
+
+        val normalized = normalizer.normalize(f)
+
+        assertEquals(
+                (
+                (True EU True)  //EF
+                        and
+                not(True AU not(    //EG
+                        True
+                            EU
+                        (
+                            ((p2 and False) or (not(p2) and not(False)))    //<=>
+                                EU
+                            (True and p1)
+                        )
+                ))
+                )
+                    or
+                not(EX(not(True and p1))),    //AX
+                normalized
+        )
+
+        val optimized = optimizer.optimize(normalized)
+
+        assertEquals(
+                not(
+                    True AU not(True EU (np2 EU p1))
+                        and
+                    EX(not(p1))
+                ),
+                optimized
+        )
+
+    }
+
+}
\ No newline at end of file

From 20a839d5a9642d427f716993d340d893f37b077e Mon Sep 17 00:00:00 2001
From: Samuel Pastva <daemontus@gmail.com>
Date: Thu, 6 Aug 2015 16:23:05 +0200
Subject: [PATCH 30/36] Update README.md

Usage guide
---
 README.md | 62 ++++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 48 insertions(+), 14 deletions(-)

diff --git a/README.md b/README.md
index 9479424..73e4713 100644
--- a/README.md
+++ b/README.md
@@ -1,23 +1,57 @@
-Simple Java CTL Parser.
+Simple parser, normalizer and optimizer for CTL temporal logic formulas written in Kotlin.
 
-###API
+###Features
+
+ - File includes
+ - References
+ - Full range of boolean and temporal operators
+ - Simple formula optimizer
+ - Normalizer into until normal form (EU, AU, EX, &&, ||, !)
+
+###Syntax
+
+Each CTL file contains zero or more include statements and zero or more assignment statements. Each statement is separated by a new line. Multi-line formulas are not supported, use references instead.
+
+Input statement has the following form: ```#include "string"``` where ```string``` is a path to a file (can be absolute or relative) that should be included. For now, escaping quotation marks is not allowed, so make sure your path does not contain any. Each file is included at most once, so you don't have to worry about multiple includes.
+
+Assignment statement has the form of ```identifier = formula```. ```identifier``` consists of numbers and upper/lowercase characters (has to start with a character). Formula can be
+ - identifier (reference to formula defined elsewhere) 
+ - boolean constant (True/False/tt/ff)
+ - float proposition: ```id operator number``` where ```id``` is a name of the model property and operator is one of <, >, <=, >=, !=, ==. Numbers can't use scientific notation (1e10).
+ - direction proposition: ```id:direction facet```(space is not mandatory)  where ```id``` is a name of the model property, direction is either in or our and facet can be positive(+) or negative(-). Example: ```val:in+```
+ - another formula in parentheses
+ - Formula with unary operator applied. Unary operators: !, EX, AX, EF, AF, EG, AG
+ - Two formulas with binary operator applied (infix notation: ```f1 op f2```). Binary operators: &&, ||, =>, <=>, EU, AU
+ 
+Forward declaration, even accross files is supported, so that you can define your formulas in whatever order you choose. For obvious reasons, cyclic references are not allowed.
+
+Operator priority: In general, unary operators have higher priority than binary operators. Binary operators have following priority: && >> || >> => >> <=> >> EU >> AU
 
-- FormulaParser - Parses a file or string into object representing a formula.
-- FormulaNormalizer - Normalizes given formula to the form that can be used for model checking.
+Also note that =>, EU and AU are right associative, so that ```a EU b EU c``` is parsed as ```a EU (b EU c)```, as expected.
+
+Example of usage:
 
-###Input Syntax
 ```
-#define propositionName variableName <= floatValue
-#property A ((True => AF proposotion) U EX False)
+  f = (AG (p1 EU a)) || (EG (p2 AU b))
+  p1 = val > 3.14
+  p2 = val2 < -44
+  p2 = var:in+ && var:in-
+  a = EF (p1 && p2)
+  b = AF foo
+  #include "other/foo.ctl"
 ```
 
-- operators (temporal and boolean) should be separated by whitespace (wrong: AFEX, UEX, !AX)
-- binary operators have to be enclosed in brackets: (f && g), (f => g), E(f U g), A(f U g)
-- all standard boolean and CTL operators are supported except reversed implication (<=): 
-!, &&, ||, =>, <=>, AX, EX, AF, EF, AG, EG, AU, EU
-- all standard float comparison operators are supported: <,>,<=,>=,==,!=
-- boolean literals are accepted as proposition names: True, False
-- variable and proposition names cannot contain digits
+###Normalization and Optimization
+
+Currently you can transform formulas into normal form that supports only operators EX, EU, AU, &&, ||, !. Alternatively, you can provide our own normalization function map that will implement your own normal form (or modify current one). 
+
+You can also automatically perform some simple formula optimizations (proposition negation, double negation removal, boolean propagation and some simplifications). Note that these optimizations expect the formula to be in until normal form. (Other formulas are also supported, but possible optimizations are limited)
+
+###API
+
+There are currently three main classes you can use ```Parser```, ```Normalizer```, ```Optimizer```. ```Parser``` provides methods that will parse a file, string or a single formula string (you don't have to perform an assignment). These methods automatically resolve all includes and references.
+
+For more complex usage example, see [IntegrationTest]{https://github.com/sybila/CTL-Parser/blob/new_parser/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt}
 
 ###Building and using
 

From 307a09309ad53a96b273abbde5cb6a39a8d9f1d6 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <daemontus@gmail.com>
Date: Wed, 2 Sep 2015 18:24:32 +0200
Subject: [PATCH 31/36] Fix direct aliases

---
 src/main/kotlin/cz/muni/fi/ctl/Parser.kt               |  2 +-
 src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
index 202e991..25190ad 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
@@ -58,7 +58,7 @@ public class Parser {
         }
 
         for ((name, formula) in formulas) {
-            references[name] = formula.treeMap(::replace)
+            references[name] = replace(formula)
         }
 
         return references
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
index 0c462bd..0b58ab6 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
@@ -157,4 +157,14 @@ class References {
         assertEquals(not(True), result.get("l"))
     }
 
+    Test fun aliasInString() {
+        val result = parser.parse("""
+            k = True
+            l = k
+        """)
+        assertEquals(2, result.size())
+        assertEquals(True, result.get("k"))
+        assertEquals(True, result.get("l"))
+    }
+
 }
\ No newline at end of file

From 3e4ae4263c23404989637281f59fc77ff0614e08 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Fri, 7 Aug 2015 16:36:07 +0200
Subject: [PATCH 32/36] Replace expected with failsWith

---
 .../kotlin/cz/muni/fi/ctl/FormulasTest.kt     | 15 ++--
 .../cz/muni/fi/ctl/ParserReferencesTest.kt    | 69 ++++++++++---------
 2 files changed, 44 insertions(+), 40 deletions(-)

diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
index a5707eb..375c8a3 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -2,6 +2,7 @@ package cz.muni.fi.ctl
 
 import org.junit.Test
 import kotlin.test.assertEquals
+import kotlin.test.failsWith
 
 class MapTest {
 
@@ -70,14 +71,16 @@ class Misc {
         assertEquals("null([])",FormulaImpl().toString())
     }
 
-    Test(expected = IllegalArgumentException::class)
-    fun notEnoughFormulas() {
-        FormulaImpl(Op.ALL_UNTIL, True)
+    Test fun notEnoughFormulas() {
+        failsWith(javaClass<IllegalStateException>()) {
+            FormulaImpl(Op.ALL_UNTIL, True)
+        }
     }
 
-    Test(expected = IllegalArgumentException::class)
-    fun tooManyFormulas() {
-        FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
+    Test fun tooManyFormulas() {
+        failsWith(javaClass<IllegalStateException>()) {
+            FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
+        }
     }
 
     Test fun get() {
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
index 0b58ab6..a959b4a 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
@@ -3,45 +3,47 @@ package cz.muni.fi.ctl
 import org.junit.Test
 import java.io.File
 import kotlin.test.assertEquals
+import kotlin.test.failsWith
 
 class References {
 
     val parser = Parser()
 
-    Test(expected = IllegalStateException::class)
-    fun cyclicReferenceThroughFiles() {
+    Test fun cyclicReferenceThroughFiles() {
         val file = File.createTempFile("file", ".ctx")
-        try {
 
-            file.bufferedWriter().use {
-                it.write("k = m")
-            }
+        file.bufferedWriter().use {
+            it.write("k = m")
+        }
 
+        failsWith(javaClass<IllegalStateException>()) {
             parser.parse("""
                 m = !k
             """)
-        } finally {
-            file.delete()
         }
+        file.delete()
     }
 
-    Test(expected = IllegalStateException::class)
-    fun transitiveCyclicReference() {
-        parser.parse("""
-            k = EX l
-            l = AX m
-            m = ! k
-        """)
+    Test fun transitiveCyclicReference() {
+        failsWith(javaClass<IllegalStateException>()) {
+            parser.parse("""
+                k = EX l
+                l = AX m
+                m = ! k
+            """)
+        }
     }
 
-    Test(expected = IllegalStateException::class)
-    fun simpleCyclicReference() {
-        parser.parse("k = !k")
+    Test fun simpleCyclicReference() {
+        failsWith(javaClass<IllegalStateException>()) {
+            parser.parse("k = !k")
+        }
     }
 
-    Test(expected = IllegalStateException::class)
-    fun undefinedReference() {
-        parser.parse("k = EF m")
+    Test fun undefinedReference() {
+        failsWith(javaClass<IllegalStateException>()) {
+            parser.parse("k = EF m")
+        }
     }
 
     Test fun declarationOrderIndependence() {
@@ -57,8 +59,7 @@ class References {
 
     }
 
-    Test(expected = IllegalStateException::class)
-    fun duplicateDeclarationInFiles() {
+    Test fun duplicateDeclarationInFiles() {
 
         val i1 = File.createTempFile("include1", ".ctl")
 
@@ -66,24 +67,24 @@ class References {
             it.write("k = True")
         }
 
-        try {
+        failsWith(javaClass<IllegalStateException>()) {
             parser.parse(
                     "#include \"${ i1.getAbsolutePath() }\" \n" +
                             "k = False"
             )
-        } finally {
-            i1.delete()
         }
-    }
 
-    Test(expected = IllegalStateException::class)
-    fun duplicateDeclarationInString() {
+        i1.delete()
+    }
 
-        parser.parse("""
-            k = True
-            l = False
-            k = False
-        """)
+    Test fun duplicateDeclarationInString() {
+        failsWith(javaClass<IllegalStateException>()) {
+            parser.parse("""
+                k = True
+                l = False
+                k = False
+            """)
+        }
     }
 
     Test fun transitiveResolveInFiles() {

From ac9e79d517c5ad1f3774deb98005f9eabeecf4d2 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Sat, 8 Aug 2015 20:45:33 +0200
Subject: [PATCH 33/36] Typo

---
 src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
index 375c8a3..9767bf4 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -72,13 +72,13 @@ class Misc {
     }
 
     Test fun notEnoughFormulas() {
-        failsWith(javaClass<IllegalStateException>()) {
+        failsWith(javaClass<IllegalArgumentException>()) {
             FormulaImpl(Op.ALL_UNTIL, True)
         }
     }
 
     Test fun tooManyFormulas() {
-        failsWith(javaClass<IllegalStateException>()) {
+        failsWith(javaClass<IllegalArgumentException>()) {
             FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
         }
     }

From 4411417664cc82993e1efb64d03ec60bb4488eec Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Mon, 17 Aug 2015 21:54:04 +0200
Subject: [PATCH 34/36] Make atom public as a base for all propositions.

---
 src/main/kotlin/cz/muni/fi/ctl/Formulas.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
index 84f3fdc..b4eb52a 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Formulas.kt
@@ -31,7 +31,7 @@ data class FormulaImpl (
 
 }
 
-open class Atom : Formula {
+public open class Atom : Formula {
     final override val operator = Op.ATOM
     final override val subFormulas = listOf<Formula>()
 }

From 7ae5106db7b5f33f6af864eea6f01301fafff9b6 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Mon, 17 Aug 2015 21:54:35 +0200
Subject: [PATCH 35/36] Upgrade kotlin

---
 build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index f58abdd..af3a04e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,6 +1,6 @@
 //include antlr plugin
 buildscript {
-    ext.kotlin_version = '0.12.1218'
+    ext.kotlin_version = '0.12.1230'
     repositories {
         maven {
             name 'JFrog OSS snapshot repo'

From 6c57f5fe0a5e7eb8fb3e2480b13266df6a8ecd43 Mon Sep 17 00:00:00 2001
From: daemontus <daemontus@gmail.com>
Date: Sat, 19 Sep 2015 12:26:14 +0200
Subject: [PATCH 36/36] Migrate to Kotlin M13

---
 build.gradle                                  |  2 +-
 src/main/kotlin/cz/muni/fi/ctl/Parser.kt      | 23 +++---
 .../kotlin/cz/muni/fi/ctl/FormulasTest.kt     | 28 +++----
 .../kotlin/cz/muni/fi/ctl/IntegrationTest.kt  | 12 +--
 .../kotlin/cz/muni/fi/ctl/NormalizerTest.kt   | 38 +++++-----
 .../kotlin/cz/muni/fi/ctl/OptimizerTest.kt    | 20 ++---
 .../kotlin/cz/muni/fi/ctl/ParserBasicTest.kt  | 12 +--
 .../cz/muni/fi/ctl/ParserComplexTest.kt       | 32 ++++----
 .../cz/muni/fi/ctl/ParserIncludeTest.kt       | 44 +++++------
 .../cz/muni/fi/ctl/ParserReferencesTest.kt    | 74 +++++++++----------
 10 files changed, 142 insertions(+), 143 deletions(-)

diff --git a/build.gradle b/build.gradle
index af3a04e..a1686fd 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,6 +1,6 @@
 //include antlr plugin
 buildscript {
-    ext.kotlin_version = '0.12.1230'
+    ext.kotlin_version = '0.13.1513'
     repositories {
         maven {
             name 'JFrog OSS snapshot repo'
diff --git a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
index 25190ad..c5e4720 100644
--- a/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
+++ b/src/main/kotlin/cz/muni/fi/ctl/Parser.kt
@@ -9,10 +9,7 @@ import org.antlr.v4.runtime.tree.ParseTree
 import org.antlr.v4.runtime.tree.ParseTreeProperty
 import org.antlr.v4.runtime.tree.ParseTreeWalker
 import java.io.File
-import java.util.ArrayList
-import java.util.HashMap
-import java.util.HashSet
-import java.util.Stack
+import java.util.*
 
 /**
  * Workflow:
@@ -49,7 +46,7 @@ public class Parser {
                     throw IllegalStateException("Cyclic reference: ${f.name}")
                 else -> {
                     replaced.push(f.name)
-                    val result = references[f.name].treeMap(::replace)
+                    val result = references[f.name]!!.treeMap(::replace)
                     replaced.pop()
                     result
                 }
@@ -88,7 +85,7 @@ class FileParser {
             processStream(ANTLRInputStream(input.toCharArray(), input.length()), "input string")
 
     private fun processFile(input: File): FileContext =
-            input.inputStream().use { processStream(ANTLRInputStream(it), input.getAbsolutePath()) }
+            input.inputStream().use { processStream(ANTLRInputStream(it), input.absolutePath) }
 
     private fun processStream(input: ANTLRInputStream, location: String): FileContext {
         val root = CTLParser(CommonTokenStream(CTLLexer(input))).root()
@@ -137,22 +134,22 @@ class FileContext(val location: String) : CTLBaseListener() {
     fun toParseContext() = ParserContext(assignments)
 
     override fun exitInclude(ctx: CTLParser.IncludeContext) {
-        val string = ctx.STRING().getText()!!
+        val string = ctx.STRING().text!!
         includes.add(File(string.substring(1, string.length() - 1)))    //remove quotes
     }
 
     override fun exitAssign(ctx: CTLParser.AssignContext) {
         assignments.add(Assignment(
-                ctx.VAR_NAME().getText()!!,
+                ctx.VAR_NAME().text!!,
                 formulas[ctx.formula()]!!,
-                location+":"+ctx.start.getLine()
+                location+":"+ctx.start.line
         ))
     }
 
     /** ------ Formula Parsing ------ **/
 
     override fun exitId(ctx: CTLParser.IdContext) {
-        formulas[ctx] = Reference(ctx.getText()!!)
+        formulas[ctx] = Reference(ctx.text!!)
     }
 
     override fun exitBool(ctx: CTLParser.BoolContext) {
@@ -161,7 +158,7 @@ class FileContext(val location: String) : CTLBaseListener() {
 
     override fun exitDirection(ctx: CTLParser.DirectionContext) {
         formulas[ctx] = DirectionProposition(
-                variable = ctx.VAR_NAME().getText()!!,
+                variable = ctx.VAR_NAME().text!!,
                 direction = if (ctx.IN() != null) Direction.IN else Direction.OUT,
                 facet = if (ctx.PLUS() != null) Facet.POSITIVE else Facet.NEGATIVE
         )
@@ -169,9 +166,9 @@ class FileContext(val location: String) : CTLBaseListener() {
 
     override fun exitProposition(ctx: CTLParser.PropositionContext) {
         formulas[ctx] = FloatProposition(
-                variable = ctx.VAR_NAME().getText()!!,
+                variable = ctx.VAR_NAME().text!!,
                 floatOp = ctx.floatOp().toOperator(),
-                value = ctx.FLOAT_VAL().getText().toDouble()
+                value = ctx.FLOAT_VAL().text.toDouble()
         )
     }
 
diff --git a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
index 9767bf4..a1ea973 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
@@ -2,7 +2,7 @@ package cz.muni.fi.ctl
 
 import org.junit.Test
 import kotlin.test.assertEquals
-import kotlin.test.failsWith
+import kotlin.test.assertFailsWith
 
 class MapTest {
 
@@ -13,13 +13,13 @@ class MapTest {
         )
     )
 
-    Test fun treeMapId() {
+    @Test fun treeMapId() {
 
         assertEquals(formula, formula.treeMap { it })
 
     }
 
-    Test fun treeMapPropositions() {
+    @Test fun treeMapPropositions() {
 
         formula.treeMap {
             if (it.operator.cardinality == 0) throw IllegalStateException("Executing tree map on a leaf")
@@ -27,7 +27,7 @@ class MapTest {
         }
     }
 
-    Test fun treeMapComplex() {
+    @Test fun treeMapComplex() {
 
         fun transform(f: Formula): Formula = when(f.operator) {
             Op.EXISTS_NEXT -> FormulaImpl(Op.ALL_NEXT, f.subFormulas.map(::transform))
@@ -50,40 +50,40 @@ class MapTest {
 
 class Misc {
 
-    Test fun booleanToString() {
+    @Test fun booleanToString() {
         assertEquals("True", True.toString())
         assertEquals("False", False.toString())
     }
 
-    Test fun formulaToString() {
+    @Test fun formulaToString() {
         assertEquals("(True && EX (False EU True))", (True and EX(False EU True)).toString())
     }
 
-    Test fun floatToString() {
+    @Test fun floatToString() {
         assertEquals("prop > 5.3", FloatProposition("prop", FloatOp.GT, 5.3).toString())
     }
 
-    Test fun directionToString() {
+    @Test fun directionToString() {
         assertEquals("prop:in+", DirectionProposition("prop", Direction.IN, Facet.POSITIVE).toString())
     }
 
-    Test fun emptyFormula() {
+    @Test fun emptyFormula() {
         assertEquals("null([])",FormulaImpl().toString())
     }
 
-    Test fun notEnoughFormulas() {
-        failsWith(javaClass<IllegalArgumentException>()) {
+    @Test fun notEnoughFormulas() {
+        assertFailsWith(IllegalArgumentException::class) {
             FormulaImpl(Op.ALL_UNTIL, True)
         }
     }
 
-    Test fun tooManyFormulas() {
-        failsWith(javaClass<IllegalArgumentException>()) {
+    @Test fun tooManyFormulas() {
+        assertFailsWith(IllegalArgumentException::class) {
             FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
         }
     }
 
-    Test fun get() {
+    @Test fun get() {
         val float = FloatProposition("val", FloatOp.GT, 34.12)
         assertEquals("val", float.variable)
         assertEquals(FloatOp.GT, float.floatOp)
diff --git a/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
index 46612bd..ca318e1 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
@@ -9,7 +9,7 @@ import kotlin.test.assertEquals
  */
 class Integration {
 
-    Test fun test() {
+    @Test fun test() {
 
         val f1 = File.createTempFile("file", ".ctl")
 
@@ -23,7 +23,7 @@ class Integration {
         }
 
         val formulas = parser.parse(
-                "#include \"${ f1.getAbsolutePath() }\" \n" +
+                "#include \"${ f1.absolutePath }\" \n" +
         """
             a = True && p1:out+
             f = EF True && EG pop || AX a
@@ -39,10 +39,10 @@ class Integration {
         val f = (EF(True) and EG(pop)) or AX(a)
 
         assertEquals(4, formulas.size())
-        assertEquals(a, formulas.get("a"))
-        assertEquals(c, formulas.get("c"))
-        assertEquals(pop, formulas.get("pop"))
-        assertEquals(f, formulas.get("f"))
+        assertEquals(a, formulas["a"])
+        assertEquals(c, formulas["c"])
+        assertEquals(pop, formulas["pop"])
+        assertEquals(f, formulas["f"])
 
         val normalized = normalizer.normalize(f)
 
diff --git a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
index fb766de..bfddc0c 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
@@ -12,7 +12,7 @@ class UntilNormalFormTest {
 
     val normalizer = Normalizer()
 
-    Test fun complexTest() {
+    @Test fun complexTest() {
 
         val f1 = FloatProposition("var1", FloatOp.NEQ, 14.3)
         val f2 = FloatProposition("var2", FloatOp.LT, -15.3)
@@ -29,7 +29,7 @@ class UntilNormalFormTest {
         )
     }
 
-    Test fun nestingNoPropositions() {
+    @Test fun nestingNoPropositions() {
         val prop = EF( p1 implies AX( EG(p2) EU AG(p1)))
         assertEquals(
                 True EU (not(p1) or not( EX( not( (not( True AU not(p2))) EU (not( True EU not(p1))) )))),
@@ -37,103 +37,103 @@ class UntilNormalFormTest {
         )
     }
 
-    Test fun nestingPreserve() {
+    @Test fun nestingPreserve() {
         val prop = (p1 and EX(not(p2))) EU ( not(p3) AU (p4 or p2))
         assertEquals(prop, normalizer.normalize(prop))
     }
 
     //trivial cases
 
-    Test fun equivChange() {
+    @Test fun equivChange() {
         val prop = p1 equal p2
         val norm = normalizer.normalize(prop)
         assertEquals( (p1 and p2) or (not(p1) and not(p2)), norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun implChange() {
+    @Test fun implChange() {
         val prop = p1 implies p2
         val norm = normalizer.normalize(prop)
         assertEquals(not(p1) or p2, norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun agChange() {
+    @Test fun agChange() {
         val prop = AG(p1)
         val norm = normalizer.normalize(prop)
         assertEquals(not( True EU  not(p1) ), norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun egChange() {
+    @Test fun egChange() {
         val prop = EG(p1)
         val norm = normalizer.normalize(prop)
         assertEquals(not( True AU not(p1) ), norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun afChange() {
+    @Test fun afChange() {
         val prop = AF(p1)
         val norm = normalizer.normalize(prop)
         assertEquals(True AU p1, norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun efChange() {
+    @Test fun efChange() {
         val prop = EF(p1)
         val norm = normalizer.normalize(prop)
         assertEquals(True EU p1, norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun axChange() {
+    @Test fun axChange() {
         val prop = AX(p1)
         val norm = normalizer.normalize(prop)
         assertEquals(not( EX( not(p1) ) ), norm)
         assertEquals(norm, normalizer.normalize(norm))
     }
 
-    Test fun auPreserve() {
+    @Test fun auPreserve() {
         val prop = p1 AU p2
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun euPreserve() {
+    @Test fun euPreserve() {
         val prop = p1 EU p2
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun orPreserve() {
+    @Test fun orPreserve() {
         val prop = p1 or p2
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun andPreserve() {
+    @Test fun andPreserve() {
         val prop = p1 and p2
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun negPreserve() {
+    @Test fun negPreserve() {
         val prop = not(p1)
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun exPreserve() {
+    @Test fun exPreserve() {
         val prop = EX(p1)
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun floatPreserve() {
+    @Test fun floatPreserve() {
         val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2)
         assertEquals(prop, normalizer.normalize(prop))
     }
 
-    Test fun booleanPreserve() {
+    @Test fun booleanPreserve() {
         assertEquals(True, normalizer.normalize(True))
         assertEquals(False, normalizer.normalize(False))
     }
 
-    Test fun directionPreserve() {
+    @Test fun directionPreserve() {
         val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE)
         assertEquals(prop, normalizer.normalize(prop))
     }
diff --git a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
index 3eda50e..2bbd484 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/OptimizerTest.kt
@@ -10,7 +10,7 @@ class OptimizerTest {
 
     val optimizer = Optimizer()
 
-    Test fun complexTest() {
+    @Test fun complexTest() {
         val f1 = FloatProposition("var2", FloatOp.LT_EQ, -15.3)
         val nf1 = FloatProposition("var2", FloatOp.GT, -15.3)
         val d1 = DirectionProposition("var1", Direction.IN, Facet.NEGATIVE)
@@ -22,15 +22,15 @@ class OptimizerTest {
         assertEquals(optimized, optimizer.optimize(optimized))
     }
 
-    Test fun orNegation() {
+    @Test fun orNegation() {
         assertEquals(not(p1 and p2), optimizer.optimize(not(p1) or not(p2)))
     }
 
-    Test fun andNegation() {
+    @Test fun andNegation() {
         assertEquals(not(p1 or p2), optimizer.optimize(not(p1) and not(p2)))
     }
 
-    Test fun floatNegation() {
+    @Test fun floatNegation() {
         assertEquals(
                 FloatProposition("val", FloatOp.NEQ, 13.2),
                 optimizer.optimize(
@@ -45,32 +45,32 @@ class OptimizerTest {
         )
     }
 
-    Test fun doubleNegation() {
+    @Test fun doubleNegation() {
         assertEquals(p1, optimizer.optimize(not(not(p1))))
         assertEquals(not(p2), optimizer.optimize(not(not(not(p2)))))
     }
 
-    Test fun booleanReduction() {
+    @Test fun booleanReduction() {
         val prop = EX( not(False) and ( (True or False) EU (False AU True) ))
         assertEquals(True, optimizer.optimize(prop))
     }
 
-    Test fun preserveUnsupported() {
+    @Test fun preserveUnsupported() {
         val prop = AX(EG(p1 implies p2))
         assertEquals(prop, optimizer.optimize(prop))
     }
 
-    Test fun floatPreserve() {
+    @Test fun floatPreserve() {
         val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2)
         assertEquals(prop, optimizer.optimize(prop))
     }
 
-    Test fun booleanPreserve() {
+    @Test fun booleanPreserve() {
         assertEquals(True, optimizer.optimize(True))
         assertEquals(False, optimizer.optimize(False))
     }
 
-    Test fun directionPreserve() {
+    @Test fun directionPreserve() {
         val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE)
         assertEquals(prop, optimizer.optimize(prop))
     }
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt
index d22251b..8dcb29b 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserBasicTest.kt
@@ -7,14 +7,14 @@ class Basic {
 
     val parser = Parser()
 
-    Test fun parenthesis() {
+    @Test fun parenthesis() {
         assertEquals(
                 True,
                 parser.formula("(True)")
         )
     }
 
-    Test fun binaryOps() {
+    @Test fun binaryOps() {
         assertEquals(
                 True EU False,
                 parser.formula("True EU False")
@@ -41,7 +41,7 @@ class Basic {
         )
     }
 
-    Test fun unaryOps() {
+    @Test fun unaryOps() {
         assertEquals(
                 not(True),
                 parser.formula("!True")
@@ -72,7 +72,7 @@ class Basic {
         )
     }
 
-    Test fun floats() {
+    @Test fun floats() {
         assertEquals(
                 FloatProposition("var", FloatOp.EQ, 0.0),
                 parser.formula("var == 0")
@@ -103,7 +103,7 @@ class Basic {
         )
     }
 
-    Test fun directions() {
+    @Test fun directions() {
         assertEquals(
                 DirectionProposition("var", Direction.IN, Facet.POSITIVE),
                 parser.formula("var:in+")
@@ -122,7 +122,7 @@ class Basic {
         )
     }
 
-    Test fun booleans() {
+    @Test fun booleans() {
         assertEquals(True, parser.formula("true"))
         assertEquals(True, parser.formula("True"))
         assertEquals(True, parser.formula("tt"))
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
index fa5caf5..45be4c4 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserComplexTest.kt
@@ -13,7 +13,7 @@ class Complex {
     val p2 = DirectionProposition("p2", Direction.IN, Facet.NEGATIVE)
     val p3 = FloatProposition("p3", FloatOp.LT, -3.14)
 
-    Test fun complexFiles() {
+    @Test fun complexFiles() {
 
         val f1 = File.createTempFile("file", ".ctl")
         val f2 = File.createTempFile("file2", ".ctl")
@@ -24,14 +24,14 @@ class Complex {
         }
 
         f2.bufferedWriter().use {
-            it.write("#include \"${ f1.getAbsolutePath() }\" \n")
+            it.write("#include \"${ f1.absolutePath }\" \n")
             it.write("b = EX c <=> True \n")
             it.write("d = e => e")
         }
 
         f3.bufferedWriter().use {
             it.write("a = ! p1 == 4 \n")
-            it.write("#include \"${ f2.getAbsolutePath() }\" \n")
+            it.write("#include \"${ f2.absolutePath }\" \n")
             it.write("e = True && c || c && False")
         }
 
@@ -44,11 +44,11 @@ class Complex {
         val d = e implies e
 
         assertEquals(5, result.size())
-        assertEquals(a, result.get("a"))
-        assertEquals(b, result.get("b"))
-        assertEquals(c, result.get("c"))
-        assertEquals(d, result.get("d"))
-        assertEquals(e, result.get("e"))
+        assertEquals(a, result["a"])
+        assertEquals(b, result["b"])
+        assertEquals(c, result["c"])
+        assertEquals(d, result["d"])
+        assertEquals(e, result["e"])
 
         f1.delete()
         f2.delete()
@@ -56,7 +56,7 @@ class Complex {
 
     }
 
-    Test fun complexString() {
+    @Test fun complexString() {
 
         val result = parser.parse("""
             b = EX p3 < -3.14 EU a
@@ -73,15 +73,15 @@ class Complex {
         val e = (c and True) or (False and b)
 
         assertEquals(5, result.size())
-        assertEquals(a, result.get("a"))
-        assertEquals(b, result.get("b"))
-        assertEquals(c, result.get("c"))
-        assertEquals(d, result.get("d"))
-        assertEquals(e, result.get("e"))
+        assertEquals(a, result["a"])
+        assertEquals(b, result["b"])
+        assertEquals(c, result["c"])
+        assertEquals(d, result["d"])
+        assertEquals(e, result["e"])
 
     }
 
-    Test fun operatorAssociativity() {
+    @Test fun operatorAssociativity() {
         //These binary operators are by convention right-associative
         //Other binary operators, such as &&, ||, <=> are associative,
         //so it doesn't matter if we resolve them left to right or right to left
@@ -99,7 +99,7 @@ class Complex {
         )
     }
 
-    Test fun operatorPriority() {
+    @Test fun operatorPriority() {
         //we do not test every combination, since priority should be transitive
         assertEquals(
                 not(False) and not(True),
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt
index 463d119..2ae66c6 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserIncludeTest.kt
@@ -4,46 +4,48 @@ import org.junit.Test
 import java.io.File
 import java.io.FileNotFoundException
 import kotlin.test.assertEquals
+import kotlin.test.assertFailsWith
 
 class Includes {
 
     val parser = Parser()
 
-    Test(expected = FileNotFoundException::class)
-    fun invalidInclude() {
-        parser.parse("#include \"bogus.foo\" ")
+    @Test fun invalidInclude() {
+        assertFailsWith(FileNotFoundException::class) {
+            parser.parse("#include \"bogus.foo\" ")
+        }
     }
 
-    Test fun duplicateInclude() {
+    @Test fun duplicateInclude() {
 
         val i1 = File.createTempFile("include1", ".ctl")
         val i2 = File.createTempFile("include2", ".ctl")
 
         i1.bufferedWriter().use {
             it.write("val = True \n")
-            it.write("#include \"${ i1.getAbsolutePath() }\"")
+            it.write("#include \"${ i1.absolutePath }\"")
         }
         i2.bufferedWriter().use {
-            it.write("#include \"${ i1.getAbsolutePath() }\" \n")
-            it.write("#include \"${ i2.getAbsolutePath() }\" \n")
+            it.write("#include \"${ i1.absolutePath }\" \n")
+            it.write("#include \"${ i2.absolutePath }\" \n")
             it.write("val2 = False")
         }
 
         val result = parser.parse(
-                "#include \"${ i2.getAbsolutePath() }\" \n" +
-                        "#include \"${ i1.getAbsolutePath() }\" "
+                "#include \"${ i2.absolutePath }\" \n" +
+                        "#include \"${ i1.absolutePath }\" "
         )
 
         assertEquals(2, result.size())
-        assertEquals(True, result.get("val"))
-        assertEquals(False, result.get("val2"))
+        assertEquals(True, result["val"])
+        assertEquals(False, result["val2"])
 
         i1.delete()
         i2.delete()
 
     }
 
-    Test fun transitiveInclude() {
+    @Test fun transitiveInclude() {
 
         val i1 = File.createTempFile("include1", ".ctl")
         val i2 = File.createTempFile("include2", ".ctl")
@@ -52,20 +54,20 @@ class Includes {
             it.write("val = True")
         }
         i2.bufferedWriter().use {
-            it.write("#include \"${ i1.getAbsolutePath() }\"")
+            it.write("#include \"${ i1.absolutePath }\"")
         }
 
-        val result = parser.parse("#include \"${ i2.getAbsolutePath() }\"")
+        val result = parser.parse("#include \"${ i2.absolutePath }\"")
 
         assertEquals(1, result.size())
-        assertEquals(True, result.get("val"))
+        assertEquals(True, result["val"])
 
         i1.delete()
         i2.delete()
 
     }
 
-    Test fun simpleIncludeFromFile() {
+    @Test fun simpleIncludeFromFile() {
 
         val include = File.createTempFile("simpleInclude", ".ctl")
 
@@ -75,19 +77,19 @@ class Includes {
 
         val file = File.createTempFile("simpleFile", ".ctl")
         file.bufferedWriter().use {
-            it.write("#include \"${include.getAbsolutePath()}\"")
+            it.write("#include \"${ include.absolutePath }\"")
         }
 
         val result = parser.parse(file)
 
         assertEquals(1, result.size())
-        assertEquals(True, result.get("val"))
+        assertEquals(True, result["val"])
 
         file.delete()
         include.delete()
     }
 
-    Test fun simpleIncludeFromString() {
+    @Test fun simpleIncludeFromString() {
 
         val file = File.createTempFile("simpleInclude", ".ctl")
 
@@ -96,11 +98,11 @@ class Includes {
         }
 
         val result = parser.parse(
-                "#include \"${ file.getAbsolutePath() }\""
+                "#include \"${ file.absolutePath }\""
         )
 
         assertEquals(1, result.size())
-        assertEquals(True, result.get("val"))
+        assertEquals(True, result["val"])
 
         file.delete()
     }
diff --git a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
index a959b4a..cc0f71f 100644
--- a/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
+++ b/src/test/kotlin/cz/muni/fi/ctl/ParserReferencesTest.kt
@@ -3,20 +3,20 @@ package cz.muni.fi.ctl
 import org.junit.Test
 import java.io.File
 import kotlin.test.assertEquals
-import kotlin.test.failsWith
+import kotlin.test.assertFailsWith
 
 class References {
 
     val parser = Parser()
 
-    Test fun cyclicReferenceThroughFiles() {
+    @Test fun cyclicReferenceThroughFiles() {
         val file = File.createTempFile("file", ".ctx")
 
         file.bufferedWriter().use {
             it.write("k = m")
         }
 
-        failsWith(javaClass<IllegalStateException>()) {
+        assertFailsWith(IllegalStateException::class) {
             parser.parse("""
                 m = !k
             """)
@@ -24,8 +24,8 @@ class References {
         file.delete()
     }
 
-    Test fun transitiveCyclicReference() {
-        failsWith(javaClass<IllegalStateException>()) {
+    @Test fun transitiveCyclicReference() {
+        assertFailsWith(IllegalStateException::class) {
             parser.parse("""
                 k = EX l
                 l = AX m
@@ -34,19 +34,19 @@ class References {
         }
     }
 
-    Test fun simpleCyclicReference() {
-        failsWith(javaClass<IllegalStateException>()) {
+    @Test fun simpleCyclicReference() {
+        assertFailsWith(IllegalStateException::class) {
             parser.parse("k = !k")
         }
     }
 
-    Test fun undefinedReference() {
-        failsWith(javaClass<IllegalStateException>()) {
+    @Test fun undefinedReference() {
+        assertFailsWith(IllegalStateException::class) {
             parser.parse("k = EF m")
         }
     }
 
-    Test fun declarationOrderIndependence() {
+    @Test fun declarationOrderIndependence() {
 
         val result = parser.parse("""
             k = ! m
@@ -54,12 +54,12 @@ class References {
         """)
 
         assertEquals(2, result.size())
-        assertEquals(not(True), result.get("k"))
-        assertEquals(True, result.get("m"))
+        assertEquals(not(True), result["k"])
+        assertEquals(True, result["m"])
 
     }
 
-    Test fun duplicateDeclarationInFiles() {
+    @Test fun duplicateDeclarationInFiles() {
 
         val i1 = File.createTempFile("include1", ".ctl")
 
@@ -67,9 +67,9 @@ class References {
             it.write("k = True")
         }
 
-        failsWith(javaClass<IllegalStateException>()) {
+        assertFailsWith(IllegalStateException::class) {
             parser.parse(
-                    "#include \"${ i1.getAbsolutePath() }\" \n" +
+                    "#include \"${ i1.absolutePath }\" \n" +
                             "k = False"
             )
         }
@@ -77,8 +77,8 @@ class References {
         i1.delete()
     }
 
-    Test fun duplicateDeclarationInString() {
-        failsWith(javaClass<IllegalStateException>()) {
+    @Test fun duplicateDeclarationInString() {
+        assertFailsWith(IllegalStateException::class) {
             parser.parse("""
                 k = True
                 l = False
@@ -87,7 +87,7 @@ class References {
         }
     }
 
-    Test fun transitiveResolveInFiles() {
+    @Test fun transitiveResolveInFiles() {
 
         val i1 = File.createTempFile("include1", ".ctl")
         val i2 = File.createTempFile("include2", ".ctl")
@@ -101,18 +101,18 @@ class References {
 
         val result = parser.parse(
                 "m = !l \n" +
-                        "#include \"${ i1.getAbsolutePath() }\" \n" +
-                        "#include \"${ i2.getAbsolutePath() }\" \n"
+                        "#include \"${ i1.absolutePath }\" \n" +
+                        "#include \"${ i2.absolutePath }\" \n"
         )
 
         assertEquals(3, result.size())
-        assertEquals(True, result.get("k"))
-        assertEquals(EF(True), result.get("l"))
-        assertEquals(not(EF(True)), result.get("m"))
+        assertEquals(True, result["k"])
+        assertEquals(EF(True), result["l"])
+        assertEquals(not(EF(True)), result["m"])
 
     }
 
-    Test fun transitiveResolveInString() {
+    @Test fun transitiveResolveInString() {
 
         val result = parser.parse("""
                 k = True
@@ -121,13 +121,13 @@ class References {
         """)
 
         assertEquals(3, result.size())
-        assertEquals(True, result.get("k"))
-        assertEquals(EF(True), result.get("l"))
-        assertEquals(not(EF(True)), result.get("m"))
+        assertEquals(True, result["k"])
+        assertEquals(EF(True), result["l"])
+        assertEquals(not(EF(True)), result["m"])
 
     }
 
-    Test fun simpleResolveInInclude() {
+    @Test fun simpleResolveInInclude() {
 
         val i = File.createTempFile("include", ".ctl")
 
@@ -137,35 +137,35 @@ class References {
 
         val result = parser.parse(
                 "k = !val \n " +
-                        "#include \"${ i.getAbsoluteFile() }\" \n"
+                        "#include \"${ i.absolutePath }\" \n"
         )
 
         assertEquals(2, result.size())
-        assertEquals(False, result.get("val"))
-        assertEquals(not(False), result.get("k"))
+        assertEquals(False, result["val"])
+        assertEquals(not(False), result["k"])
 
         i.delete()
 
     }
 
-    Test fun simpleResolveInString() {
+    @Test fun simpleResolveInString() {
         val result = parser.parse("""
             k = True
             l = !k
         """)
         assertEquals(2, result.size())
-        assertEquals(True, result.get("k"))
-        assertEquals(not(True), result.get("l"))
+        assertEquals(True, result["k"])
+        assertEquals(not(True), result["l"])
     }
 
-    Test fun aliasInString() {
+    @Test fun aliasInString() {
         val result = parser.parse("""
             k = True
             l = k
         """)
         assertEquals(2, result.size())
-        assertEquals(True, result.get("k"))
-        assertEquals(True, result.get("l"))
+        assertEquals(True, result["k"])
+        assertEquals(True, result["l"])
     }
 
 }
\ No newline at end of file