Merge remote-tracking branch 'origin/master'

# Conflicts:
#	README.md

README.md

@@ -22,7 +22,7 @@ Using this class you can parse strings, files or inlined formulas
 Additional operations such as normalization and optimization are provided as 
 extension (static) functions. 
 
-Project also defines a convenient syntax for writing formulas directly in code.
+Project also defines a convenient syntax for writing formulas directly in code (See Extensions.kt file).
 
 For more complex usage example, see the
  [IntegrationTest](src/test/kotlin/com/github/sybila/ctl/IntegrationTest.kt)
@@ -72,8 +72,9 @@ Expression can be
  - two expressions joined by +,-,*,/
 
 Finally, you can use special flag  ```:?``` in front of an assignment to indicate formulas that
- are in some way interesting/important. The exact semantics of this flag depend on what you
- plan to use the input for.
+are in some way interesting/important. You can then configure the parser to only include
+these formulas in the result. The exact semantics of this flag depend on what you
+plan to use the input for. 
 
 Forward declaration, even across files is supported, so that you can define your formulas in 
 whatever order you choose. For obvious reasons, cyclic references are not allowed.

build.gradle

@@ -21,18 +21,17 @@ buildscript {
 }
 
 sourceCompatibility = 1.7
-group = "com.github.sybila"
+group = "com.github.sybila.ctl"
 archivesBaseName = "ctl-parser"
 version = '2.1.0'
 
 //antlr config
 generateGrammarSource {
     arguments += [
             "-no-visitor",
-            "-listener",
-            "-package", "com.github.sybila.ctl.antlr"
+            "-listener"
     ]
-    outputDirectory = new File('src/main/gen/com/github/sybila/ctl/antlr')
+    outputDirectory = new File('src/main/gen/')
 }
 
 // make the Java compile task depend on the antlr4 task
@@ -44,40 +43,23 @@ sourceSets.main.java.srcDirs += new File('src/main/gen')
 
 repositories {
     mavenCentral()
+    maven { url 'https://jitpack.io' }
 }
 
 dependencies {
     testCompile group: 'junit', name: 'junit', version: '4.11'
     testCompile "org.jetbrains.kotlin:kotlin-test:$kotlin_version"
     compile "org.jetbrains.kotlin:kotlin-stdlib:$kotlin_version"
     compile 'com.intellij:annotations:5.1'
+    compile 'com.github.daemontus:kotlin-option-result:1.0.0'
     antlr "org.antlr:antlr4:4.5.1-1"
 }
 
-//create a single Jar with all dependencies
-task fullJar(type: Jar) {
-    manifest {
-        attributes 'Implementation-Title': 'CTL Parser',
-                'Implementation-Version': version
-    }
-    baseName = project.name + '-all'
-    from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
-    with jar
-}
-
 sourceSets {
     main.java.srcDirs += 'src/main/kotlin'
     test.java.srcDirs += 'src/test/kotlin'
 }
 
-/* For some esoteric reason, javadoc is broken with git build info in this repository
-You can try to enable this later - hopefully it's a bug in javadoc
-task javadocJar(type: Jar) {
-    classifier = 'javadoc'
-    from javadoc
-}
-*/
-
 task sourcesJar(type: Jar) {
     classifier = 'sources'
     from sourceSets.main.allSource
@@ -88,10 +70,6 @@ artifacts {
     archives sourcesJar
 }
 
-jacoco {
-    toolVersion = "0.7.5.201505241946"
-}
-
 jacocoTestReport {
     reports {
         xml.enabled = true
@@ -103,8 +81,14 @@ check.dependsOn jacocoTestReport
 
 buildStamp {
     // The git commit SHA will be appended to this url to generate the final url.
-    repoBaseUrl "https://github.com/sybila/ctl-parser/tree/"
+    repoBaseUrl "https://github.com/sybila/ctl-parser"
     // BuildInfo.java will be added under this package, in a
     // generated build/ directory.
     packageName "com.github.sybila.ctl"
+}
+
+test {
+    testLogging {
+        events "skipped", "failed", "standardOut", "standardError"
+    }
 }

gradlew

@@ -111,8 +111,8 @@ fi
 
 # For Cygwin, switch paths to Windows format before running java
 if $cygwin ; then
-    APP_HOME=`cygpath --path --mixed "$APP_HOME"`
-    CLASSPATH=`cygpath --path --mixed "$CLASSPATH"`
+    APP_HOME=`cygpath --quantifier --mixed "$APP_HOME"`
+    CLASSPATH=`cygpath --quantifier --mixed "$CLASSPATH"`
     JAVACMD=`cygpath --unix "$JAVACMD"`
 
     # We build the pattern for arguments to be converted via cygpath
@@ -134,7 +134,7 @@ if $cygwin ; then
         CHECK2=`echo "$arg"|egrep -c "^-"`                                 ### Determine if an option
 
         if [ $CHECK -ne 0 ] && [ $CHECK2 -eq 0 ] ; then                    ### Added a condition
-            eval `echo args$i`=`cygpath --path --ignore --mixed "$arg"`
+            eval `echo args$i`=`cygpath --quantifier --ignore --mixed "$arg"`
         else
             eval `echo args$i`="\"$arg\""
         fi

src/main/antlr/CTL.g4 → src/main/antlr/com/github/sybila/ctl/antlr/CTL.g4

@@ -1,6 +1,9 @@
-
 grammar CTL;
 
+@header {
+package com.github.sybila.ctl.antlr;
+}
+
 /* Main format structure */
 
 root : fullStop? (statement fullStop)*;

src/main/antlr/com/github/sybila/huctl/antlr/HUCTL.g4

@@ -0,0 +1,150 @@
+grammar HUCTL;
+
+@header {
+package com.github.sybila.huctl.antlr;
+}
+
+/* Main format structure */
+
+root : fullStop? (statement fullStop)*;
+
+statement : ':include' STRING                                                           #includeStatement
+          //aliases are ambiguous - we can't decide whether they are formulas or expressions until they are resolved
+          | FLAG? VAR_NAME '=' (VAR_NAME | formula | dirFormula | expression)           #assignStatement
+          ;
+
+fullStop : NEWLINE+ | EOF | ';';
+
+/* Formula and propositions */
+
+formula : VAR_NAME                                                                      #id
+        | (TRUE | FALSE)                                                                #bool
+        | VAR_NAME ':' (IN | OUT) (PLUS | MINUS)                                        #transition
+        | expression compare expression                                                 #proposition
+        | '(' formula ')'                                                               #parenthesis
+        | NEG formula                                                                   #negation
+        | dirModifier? TEMPORAL_UNARY formula                                           #unaryTemporal
+        //we list operators explicitly, becuase writing them as a subrule broke operator priority
+        | formula CON formula                                                           #and
+        | formula DIS formula                                                           #or
+        |<assoc=right> formula IMPL formula                                             #implies
+        | formula EQIV formula                                                          #equal
+        |<assoc=right> formula dirModifierL? E_U dirModifierR? formula                  #existUntil
+        |<assoc=right> formula dirModifierL? A_U dirModifierR? formula                  #allUntil
+        | (FORALL | EXISTS) VAR_NAME setBound? ':' formula                              #firstOrder
+        | (AT | BIND) VAR_NAME ':' formula                                              #hybrid
+        ;
+
+setBound : 'in' formula;
+
+dirModifier : '{' dirFormula '}';
+dirModifierL : dirModifier;
+dirModifierR : dirModifier;
+
+/* Direction formula - used as an optional parameter for temporal operators */
+
+dirFormula : VAR_NAME                                       #dirId
+           | (TRUE | FALSE)                                 #dirBool
+           | VAR_NAME (PLUS | MINUS)                        #dirProposition
+           | '(' dirFormula ')'                             #dirParenthesis
+           | NEG dirFormula                                 #dirNegation
+           | dirFormula CON dirFormula                      #dirAnd
+           | dirFormula DIS dirFormula                      #dirOr
+           | <assoc=right> dirFormula IMPL dirFormula       #dirImplies
+           | dirFormula EQIV dirFormula                     #dirEqual
+           ;
+
+/* Numeric proposition */
+
+compare : EQ | NEQ | | GT | LT | GTEQ | LTEQ;
+
+expression : VAR_NAME                                       #expId
+        | FLOAT_VAL                                         #expValue
+        | '(' expression ')'                                #expParenthesis
+        //we list operators explicitly, becuase writing them as a subrule broke operator priority
+        | expression MUL expression                         #expMultiply
+        | expression DIV expression                         #expDivide
+        | expression PLUS expression                        #expAdd
+        | expression MINUS expression                       #expSubtract
+        ;
+
+/** Terminals **/
+
+TRUE : ([tT]'rue' | 'tt');
+FALSE : ([fF]'alse' | 'ff');
+
+IN : 'in';
+OUT : 'out';
+
+PLUS : '+';
+MINUS : '-';
+
+FLAG : ':?';
+
+/** Path quantifiers **/
+
+A : 'A';
+E : 'E';
+PA : 'pA';
+PE : 'pE';
+
+PATH : (A|E|PA|PE);
+
+/** Temporal operators **/
+
+X : 'X';
+F : 'F';
+G : 'G';
+U : 'U';
+WF : 'wF';
+WX : 'wX';
+
+TEMPORAL_UNARY : PATH (X|G|F|WF|WX);
+E_U : (E|PE) U;
+A_U : (A|PA) U;
+
+/** Logical operators **/
+
+NEG : '!';
+CON : '&&';
+DIS : '||';
+IMPL : '->';
+EQIV : '<->';
+
+/** first order operators **/
+
+FORALL : 'forall';
+EXISTS : 'exists';
+
+/** Hybrid operators **/
+
+BIND : 'bind';
+AT : 'at';
+
+/** Compare operators **/
+
+EQ : '==';
+NEQ : '!=';
+GT : '>';
+LT : '<';
+GTEQ : '>=';
+LTEQ : '<=';
+
+/** Arithmetics **/
+
+MUL : '*';
+DIV : '/';
+
+/* 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
+C_Line_comment : '//' .*? ('\n' | EOF) -> channel(HIDDEN) ;
+Python_Line_comment : '#' .*? ('\n' | EOF) -> channel(HIDDEN) ;