diff --git a/build.gradle b/build.gradle index 5fd29a8..0dc54c6 100644 --- a/build.gradle +++ b/build.gradle @@ -6,7 +6,7 @@ apply plugin: 'jacoco' apply plugin: "com.madvay.tools.build.gitbuildinfo" buildscript { - ext.kotlin_version = '1.0.5' + ext.kotlin_version = '1.0.5-2' repositories { jcenter() @@ -21,18 +21,17 @@ buildscript { } sourceCompatibility = 1.7 -group = "com.github.sybila" +group = "com.github.sybila.ctl" archivesBaseName = "ctl-parser" -version = '2.0.0' +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,6 +43,7 @@ sourceSets.main.java.srcDirs += new File('src/main/gen') repositories { mavenCentral() + maven { url 'https://jitpack.io' } } dependencies { @@ -51,33 +51,15 @@ dependencies { 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" + } } \ No newline at end of file diff --git a/gradlew b/gradlew index 9aa616c..f7881b6 100755 --- a/gradlew +++ b/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 diff --git a/src/main/antlr/CTL.g4 b/src/main/antlr/com/github/sybila/ctl/antlr/CTL.g4 old mode 100644 new mode 100755 similarity index 98% rename from src/main/antlr/CTL.g4 rename to src/main/antlr/com/github/sybila/ctl/antlr/CTL.g4 index ac5aa0e..2ee892b --- a/src/main/antlr/CTL.g4 +++ b/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)*; diff --git a/src/main/antlr/com/github/sybila/huctl/antlr/HUCTL.g4 b/src/main/antlr/com/github/sybila/huctl/antlr/HUCTL.g4 new file mode 100644 index 0000000..161f084 --- /dev/null +++ b/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 + | formula IMPL formula #implies + | formula EQIV formula #equal + | formula dirModifierL? E_U dirModifierR? formula #existUntil + | 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 + | 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) ; \ No newline at end of file diff --git a/src/main/kotlin/com/github/sybila/ctl/CTLParser.kt b/src/main/kotlin/com/github/sybila/ctl/CTLParser.kt old mode 100644 new mode 100755 index bc119b9..2a10e99 --- a/src/main/kotlin/com/github/sybila/ctl/CTLParser.kt +++ b/src/main/kotlin/com/github/sybila/ctl/CTLParser.kt @@ -6,6 +6,7 @@ import com.github.sybila.ctl.antlr.CTLParser import org.antlr.v4.runtime.* import org.antlr.v4.runtime.atn.ATNConfigSet import org.antlr.v4.runtime.dfa.DFA +import org.antlr.v4.runtime.tree.ErrorNode import org.antlr.v4.runtime.tree.ParseTree import org.antlr.v4.runtime.tree.ParseTreeProperty import org.antlr.v4.runtime.tree.ParseTreeWalker @@ -48,12 +49,12 @@ class CTLParser() { return result } - fun resolveAlias(a: Assignment): Assignment = + fun resolveAlias(a: Assignment<*>): Assignment<*> = when { - a !is AliasAssignment -> a + a.item !is String -> a a.name in replaced -> throw IllegalStateException("Cyclic reference ${a.name} in ${a.location}") - a.alias !in references -> ExpressionAssignment(a.name, a.alias.asVariable(), a.location, a.flagged) - else -> stacked(a.name) { resolveAlias(references[a.alias]!!) } + a.item !in references -> a.copy(item = a.item.asVariable()) + else -> stacked(a.name) { resolveAlias(references[a.item]!!) } } fun resolveExpression(e: Expression): Expression = e.mapLeafs({it}) { e -> @@ -62,7 +63,7 @@ class CTLParser() { in replaced -> throw IllegalStateException("Cyclic reference: $name") in references -> stacked(name) { val assignment = references[name]!! - if (assignment is ExpressionAssignment) resolveExpression(assignment.expression) + if (assignment.item is Expression) resolveExpression(assignment.item) else throw IllegalStateException("$name is a formula. Expression needed.") } else -> e //This is a valid variable, not a reference @@ -78,7 +79,7 @@ class CTLParser() { !in references -> throw IllegalStateException("Undefined reference: $name") else -> stacked(name) { val assignment = references[name]!! - if (assignment is FormulaAssignment) resolveFormula(assignment.formula) + if (assignment.item is Formula) resolveFormula(assignment.item) else throw IllegalStateException("$name is an expression. Formula needed.") } } @@ -98,16 +99,14 @@ class CTLParser() { } for ((name, assignment) in references) { //resolve expressions - this way we catch errors also for unused expressions - if (assignment is ExpressionAssignment) - references[name] = ExpressionAssignment( - name, resolveExpression(assignment.expression), assignment.location, assignment.flagged - ) + if (assignment.item is Expression) + references[name] = assignment.copy(item = resolveExpression(assignment.item)) } val results = HashMap() for ((name, assignment) in references) { - if (assignment is FormulaAssignment && (!onlyFlagged || assignment.flagged)) - results[name] = resolveFormula(assignment.formula) + if (assignment.item is Formula && (!onlyFlagged || assignment.flagged)) + results[name] = resolveFormula(assignment.item) } return results @@ -164,7 +163,7 @@ private class FileParser { } private data class ParserContext( - private val assignments: List + private val assignments: List> ) { fun toMap() = assignments.associateBy({ it.name }, { it }) @@ -192,9 +191,9 @@ private data class ParserContext( private class FileContext(val location: String) : CTLBaseListener() { val includes = ArrayList() - val formulas = ArrayList() - val expressions = ArrayList() - val aliases = ArrayList() + val formulas = ArrayList>() + val expressions = ArrayList>() + val aliases = ArrayList>() private val formulaTree = ParseTreeProperty() private val expressionTree = ParseTreeProperty() @@ -207,7 +206,7 @@ private class FileContext(val location: String) : CTLBaseListener() { } override fun exitAssignFormula(ctx: CTLParser.AssignFormulaContext) { - formulas.add(FormulaAssignment( + formulas.add(Assignment( ctx.VAR_NAME().text, formulaTree[ctx.formula()], location + ":" + ctx.start.line, @@ -216,7 +215,7 @@ private class FileContext(val location: String) : CTLBaseListener() { } override fun exitAssignExpression(ctx: CTLParser.AssignExpressionContext) { - expressions.add(ExpressionAssignment( + expressions.add(Assignment( ctx.VAR_NAME().text, expressionTree[ctx.expression()], location + ":" + ctx.start.line, @@ -225,7 +224,7 @@ private class FileContext(val location: String) : CTLBaseListener() { } override fun exitAssignAlias(ctx: CTLParser.AssignAliasContext) { - aliases.add(AliasAssignment( + aliases.add(Assignment( ctx.VAR_NAME(0).text!!, ctx.VAR_NAME(1).text!!, location + ":" + ctx.start.line, @@ -233,6 +232,10 @@ private class FileContext(val location: String) : CTLBaseListener() { )) } + override fun visitErrorNode(node: ErrorNode) { + throw IllegalStateException("Syntax error at '${node.text}' in $location:${node.symbol.line}") + } + /* ------ Expression Parsing ----- */ override fun exitIdExpression(ctx: CTLParser.IdExpressionContext) { @@ -325,21 +328,12 @@ private class FileContext(val location: String) : CTLBaseListener() { } } -private interface Assignment { - val name: String - val location: String - val flagged: Boolean -} - -private data class FormulaAssignment( - override val name: String, val formula: Formula, override val location: String, override val flagged: Boolean -) : Assignment -private data class ExpressionAssignment( - override val name: String, val expression: Expression, override val location: String, override val flagged: Boolean -) : Assignment -private data class AliasAssignment( - override val name: String, val alias: String, override val location: String, override val flagged: Boolean -) : Assignment +private data class Assignment ( + val name: String, + val item: T, + val location: String, + val flagged: Boolean +) //convenience methods diff --git a/src/main/kotlin/com/github/sybila/ctl/Extensions.kt b/src/main/kotlin/com/github/sybila/ctl/Extensions.kt old mode 100644 new mode 100755 diff --git a/src/main/kotlin/com/github/sybila/ctl/Formula.kt b/src/main/kotlin/com/github/sybila/ctl/Formula.kt old mode 100644 new mode 100755 diff --git a/src/main/kotlin/com/github/sybila/ctl/Normalizer.kt b/src/main/kotlin/com/github/sybila/ctl/Normalizer.kt old mode 100644 new mode 100755 diff --git a/src/main/kotlin/com/github/sybila/ctl/Optimizer.kt b/src/main/kotlin/com/github/sybila/ctl/Optimizer.kt old mode 100644 new mode 100755 diff --git a/src/main/kotlin/com/github/sybila/ctl/Proposition.kt b/src/main/kotlin/com/github/sybila/ctl/Proposition.kt old mode 100644 new mode 100755 diff --git a/src/main/kotlin/com/github/sybila/huctl/DirectionFormula.kt b/src/main/kotlin/com/github/sybila/huctl/DirectionFormula.kt new file mode 100644 index 0000000..822760a --- /dev/null +++ b/src/main/kotlin/com/github/sybila/huctl/DirectionFormula.kt @@ -0,0 +1,86 @@ +package com.github.sybila.huctl + + +sealed class DirectionFormula { + + interface Unary where T : DirectionFormula, T : Unary { + val inner: DirectionFormula + fun copy(inner: DirectionFormula = this.inner): T + } + + interface Binary where T : DirectionFormula, T : Binary { + val left: DirectionFormula + val right: DirectionFormula + fun copy(left: DirectionFormula = this.left, right: DirectionFormula = this.right): T + } + + sealed class Atom : DirectionFormula() { + + object True : Atom() { + override fun toString(): String = "true" + } + object False : Atom() { + override fun toString(): String = "false" + } + + class Proposition(val name: String, val facet: Facet) : Atom() { + override fun equals(other: Any?): Boolean + = other is Proposition && other.name == this.name && other.facet == this.facet + + override fun hashCode(): Int + = (31 * name.hashCode() + facet.hashCode()) + + override fun toString(): String + = "$name$facet" + } + + internal class Reference(val name: String) : Atom() { + override fun equals(other: Any?): Boolean = other is Reference && other.name == this.name + + override fun hashCode(): Int = name.hashCode() + + override fun toString(): String = name + } + + } + + + class Not(override val inner: DirectionFormula) : DirectionFormula(), Unary { + + override fun copy(inner: DirectionFormula): Not = Not(inner) + + override fun equals(other: Any?): Boolean = other is Not && this.inner == other.inner + + override fun hashCode(): Int = inner.hashCode() + + override fun toString(): String = "!$inner" + } + + sealed class Bool>( + override val left: DirectionFormula, override val right: DirectionFormula, + private val op: String + ) : DirectionFormula(), Binary { + + override fun equals(other: Any?): Boolean + = other is Bool<*> && this.javaClass == other.javaClass && + this.right == other.right && this.left == other.left + + override fun hashCode(): Int = 31 * (31 * left.hashCode() + right.hashCode()) + op.hashCode() + + override fun toString(): String = "($left $op $right)" + + class And(left: DirectionFormula, right: DirectionFormula) : Bool(left, right, "&&") { + override fun copy(left: DirectionFormula, right: DirectionFormula): And = And(left, right) + } + class Or(left: DirectionFormula, right: DirectionFormula) : Bool(left, right, "||") { + override fun copy(left: DirectionFormula, right: DirectionFormula): Or = Or(left, right) + } + class Implies(left: DirectionFormula, right: DirectionFormula) : Bool(left, right, "->") { + override fun copy(left: DirectionFormula, right: DirectionFormula): Implies = Implies(left, right) + } + class Equals(left: DirectionFormula, right: DirectionFormula) : Bool(left, right, "<->") { + override fun copy(left: DirectionFormula, right: DirectionFormula): Equals = Equals(left, right) + } + } + +} \ No newline at end of file diff --git a/src/main/kotlin/com/github/sybila/huctl/Expression.kt b/src/main/kotlin/com/github/sybila/huctl/Expression.kt new file mode 100644 index 0000000..2da610d --- /dev/null +++ b/src/main/kotlin/com/github/sybila/huctl/Expression.kt @@ -0,0 +1,45 @@ +package com.github.sybila.huctl + +sealed class Expression { + class Variable(val name: String) : Expression() { + override fun equals(other: Any?): Boolean = other is Variable && other.name == this.name + override fun hashCode(): Int = this.name.hashCode() + override fun toString(): String = this.name + } + class Constant(val value: Double) : Expression() { + override fun equals(other: Any?): Boolean = other is Constant && other.value == this.value + override fun hashCode(): Int = this.value.hashCode() + override fun toString(): String = String.format("%.4f", this.value) //no scientific notation + } + sealed class Arithmetic>( + val left: Expression, + val right: Expression, + private val clazz: Class, + private val op: String + ) : Expression() { + override fun equals(other: Any?): Boolean + = clazz.isInstance(other) && clazz.cast(other).let { that -> + this.left == that.left && this.right == that.right + } + override fun hashCode(): Int = 31 * (31 * clazz.hashCode() + left.hashCode()) + right.hashCode() + override fun toString(): String = "($left $op $right)" + + abstract fun copy(left: Expression = this.left, right: Expression = this.right): Arithmetic + + class Add(left: Expression, right: Expression) : Arithmetic(left, right, Add::class.java, "+") { + override fun copy(left: Expression, right: Expression): Arithmetic = Add(left, right) + } + + class Sub(left: Expression, right: Expression) : Arithmetic(left, right, Sub::class.java, "-") { + override fun copy(left: Expression, right: Expression): Arithmetic = Sub(left, right) + } + + class Mul(left: Expression, right: Expression) : Arithmetic(left, right, Mul::class.java, "*") { + override fun copy(left: Expression, right: Expression): Arithmetic = Mul(left, right) + } + + class Div(left: Expression, right: Expression) : Arithmetic
(left, right, Div::class.java, "/") { + override fun copy(left: Expression, right: Expression): Arithmetic
= Div(left, right) + } + } +} \ No newline at end of file diff --git a/src/main/kotlin/com/github/sybila/huctl/Extensions.kt b/src/main/kotlin/com/github/sybila/huctl/Extensions.kt new file mode 100644 index 0000000..104147a --- /dev/null +++ b/src/main/kotlin/com/github/sybila/huctl/Extensions.kt @@ -0,0 +1,182 @@ +package com.github.sybila.huctl + +import com.github.sybila.huctl.Formula.* +import com.github.sybila.huctl.Formula.Bool.* +import com.github.sybila.huctl.Formula.Simple.* +import com.github.sybila.huctl.PathQuantifier.* + +// -- Catamorphism -- + +fun Expression.fold( + constant: Expression.Constant.() -> R, + variable: Expression.Variable.() -> R, + arithmetic: Expression.Arithmetic<*>.(R, R) -> R): R { + return when (this) { + is Expression.Constant -> constant(this) + is Expression.Variable -> variable(this) + is Expression.Arithmetic<*> -> arithmetic(this, + this.left.fold(constant, variable, arithmetic), + this.right.fold(constant, variable, arithmetic) + ) + } +} + +fun Expression.mapLeafs( + constant: (Expression.Constant) -> Expression, + variable: (Expression.Variable) -> Expression +): Expression { + return this.fold(constant, variable, Expression.Arithmetic<*>::copy) +} + +fun DirectionFormula.fold( + atom: DirectionFormula.Atom.() -> R, + unary: DirectionFormula.Unary<*>.(R) -> R, + binary: DirectionFormula.Binary<*>.(R, R) -> R +) : R { + return when (this) { + is DirectionFormula.Atom -> atom(this) + is DirectionFormula.Unary<*> -> unary(this, this.inner.fold(atom, unary, binary)) + is DirectionFormula.Binary<*> -> binary(this, + this.left.fold(atom, unary, binary), + this.right.fold(atom, unary, binary) + ) + else -> throw IllegalStateException("Cannot fold over formula $this") + } +} + +fun DirectionFormula.mapLeafs( + atom: (DirectionFormula.Atom) -> DirectionFormula +): DirectionFormula { + return this.fold(atom, DirectionFormula.Unary<*>::copy, DirectionFormula.Binary<*>::copy) +} + +fun Formula.fold( + atom: Atom.() -> R, + unary: Unary<*>.(R) -> R, + binary: Binary<*>.(R, R) -> R +): R { + return when (this) { + is Atom -> atom(this) + is Unary<*> -> unary(this, this.inner.fold(atom, unary, binary)) + is Binary<*> -> binary(this, + this.left.fold(atom, unary, binary), + this.right.fold(atom, unary, binary) + ) + else -> throw IllegalStateException("Cannot fold over formula $this") + } +} + +fun Formula.mapLeafs( + atom: (Atom) -> Formula +): Formula { + return this.fold(atom, Unary<*>::copy, Binary<*>::copy) +} + +// -- Construction Utils -- + +// Expressions + +fun String.asVariable(): Expression.Variable = Expression.Variable(this) +fun Double.asConstant(): Expression.Constant = Expression.Constant(this) + +infix operator fun Expression.plus(other: Expression) = Expression.Arithmetic.Add(this, other) +infix operator fun Expression.minus(other: Expression) = Expression.Arithmetic.Sub(this, other) +infix operator fun Expression.times(other: Expression) = Expression.Arithmetic.Mul(this, other) +infix operator fun Expression.div(other: Expression) = Expression.Arithmetic.Div(this, other) + +infix fun Expression.gt(other: Expression): Atom.Float = Atom.Float(this, CompareOp.GT, other) +infix fun Expression.ge(other: Expression): Atom.Float = Atom.Float(this, CompareOp.GE, other) +infix fun Expression.eq(other: Expression): Atom.Float = Atom.Float(this, CompareOp.EQ, other) +infix fun Expression.neq(other: Expression): Atom.Float = Atom.Float(this, CompareOp.NEQ, other) +infix fun Expression.le(other: Expression): Atom.Float = Atom.Float(this, CompareOp.LE, other) +infix fun Expression.lt(other: Expression): Atom.Float = Atom.Float(this, CompareOp.LT, other) + +// Propositions + +val True = Atom.True +val False = Atom.False + +fun String.positiveIn() = Atom.Transition(this, Direction.IN, Facet.POSITIVE) +fun String.positiveOut() = Atom.Transition(this, Direction.OUT, Facet.POSITIVE) +fun String.negativeIn() = Atom.Transition(this, Direction.IN, Facet.NEGATIVE) +fun String.negativeOut() = Atom.Transition(this, Direction.OUT, Facet.NEGATIVE) + +// Direction propositions + +fun String.increase(): DirectionFormula = DirectionFormula.Atom.Proposition(this, Facet.POSITIVE) +fun String.decrease(): DirectionFormula = DirectionFormula.Atom.Proposition(this, Facet.NEGATIVE) + +// Direction formulas + +fun not(inner: DirectionFormula): DirectionFormula = DirectionFormula.Not(inner) + +infix fun DirectionFormula.and(right: DirectionFormula): DirectionFormula = DirectionFormula.Bool.And(this, right) +infix fun DirectionFormula.or(right: DirectionFormula): DirectionFormula = DirectionFormula.Bool.Or(this, right) +infix fun DirectionFormula.implies(right: DirectionFormula): DirectionFormula = DirectionFormula.Bool.Implies(this, right) +infix fun DirectionFormula.equal(right: DirectionFormula): DirectionFormula = DirectionFormula.Bool.Equals(this, right) + + +// Formulas + +fun not(inner: Formula): Formula = Not(inner) + +//Future +fun EF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Future(E, inner, dir) +fun pastEF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Future(pE, inner, dir) +fun AF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Future(A, inner, dir) +fun pastAF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Future(pA, inner, dir) + +//WeakFuture +fun weakEF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakFuture(E, inner, dir) +fun weakAF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakFuture(A, inner, dir) +fun pastWeakEF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakFuture(pE, inner, dir) +fun pastWeakAF(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakFuture(pA, inner, dir) + +//Next +fun EX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Next(E, inner, dir) +fun pastEX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Next(pE, inner, dir) +fun AX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Next(A, inner, dir) +fun pastAX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Next(pA, inner, dir) + +//WeakNext +fun weakEX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakNext(E, inner, dir) +fun pastWeakEX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakNext(pE, inner, dir) +fun weakAX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakNext(A, inner, dir) +fun pastWeakAX(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = WeakNext(pA, inner, dir) + +//Globally +fun EG(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Globally(E, inner, dir) +fun pastEG(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Globally(pE, inner, dir) +fun AG(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Globally(A, inner, dir) +fun pastAG(inner: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula = Globally(pA, inner, dir) + +//Until +infix fun Formula.EU(reach: Formula): Formula + = Until(E, this, reach, DirectionFormula.Atom.True) +fun Formula.EU(reach: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula + = Until(E, this, reach, dir) +infix fun Formula.AU(reach: Formula): Formula + = Until(A, this, reach, DirectionFormula.Atom.True) +fun Formula.AU(reach: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula + = Until(A, this, reach, dir) +infix fun Formula.pastEU(reach: Formula): Formula + = Until(pE, this, reach, DirectionFormula.Atom.True) +fun Formula.pastEU(reach: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula + = Until(pE, this, reach, dir) +infix fun Formula.pastAU(reach: Formula): Formula + = Until(pA, this, reach, DirectionFormula.Atom.True) +fun Formula.pastAU(reach: Formula, dir: DirectionFormula = DirectionFormula.Atom.True): Formula + = Until(pA, this, reach, dir) + +//Hybrid and first order + +fun at(name: String, inner: Formula) : Formula = Formula.Hybrid.At(name, inner) +fun bind(name: String, inner: Formula) : Formula = Formula.Hybrid.Bind(name, inner) +fun forall(name: String, bound: Formula, inner: Formula) : Formula = Formula.FirstOrder.ForAll(name, bound, inner) +fun exists(name: String, bound: Formula, inner: Formula) : Formula = Formula.FirstOrder.Exists(name, bound, inner) + +//Bool +infix fun Formula.and(other: Formula): Formula = And(this, other) +infix fun Formula.or(other: Formula): Formula = Or(this, other) +infix fun Formula.implies(other: Formula): Formula = Implies(this, other) +infix fun Formula.equal(other: Formula): Formula = Equals(this, other) \ No newline at end of file diff --git a/src/main/kotlin/com/github/sybila/huctl/Formula.kt b/src/main/kotlin/com/github/sybila/huctl/Formula.kt new file mode 100644 index 0000000..df308b7 --- /dev/null +++ b/src/main/kotlin/com/github/sybila/huctl/Formula.kt @@ -0,0 +1,315 @@ +package com.github.sybila.huctl + +/** + * Algebraic data type representing a HUCTL formula: + * + * With Kotlin 1.1, we will be able to rewrite this in a more concise manner. + * + * Meanwhile, here is a simple overview: + * class Formula { + * interface Unary + * interface Binary + * class Atom : Formula { + * class True + * class False + * class Float + * class Transition + * internal class Reference + * } + * class FirstOrder : Formula { + * class ForAll : FirstOrder, Binary + * class Exists : FirstOrder, Binary + * } + * class Hybrid : Formula { + * class Bind : Hybrid, Unary + * class At : Hybrid, Unary + * } + * class Not : Formula + * class Bool : Formula, Binary { + * class And : Bool + * class Or : Bool + * class Implies : Bool + * class Equals : Bool + * } + * class Temporal : Formula { + * class Basic : Unary { + * class Next : Basic + * class Future : Basic + * class Globally : Basic + * class WeakNext : Basic + * class WeakFuture : Basic + * } + * class Until : Binary + * } + * } + */ +sealed class Formula { + + abstract fun asDirectionFormula(): DirectionFormula? + + interface Unary where T : Formula, T : Unary { + val inner: Formula + fun copy(inner: Formula = this.inner): T + } + + interface Binary where T : Formula, T : Binary { + val left: Formula + val right: Formula + fun copy(left: Formula = this.left, right: Formula = this.right): T + } + + interface Temporal { + val quantifier: PathQuantifier + val direction: DirectionFormula + } + + sealed class Atom : Formula() { + object True : Atom() { + override fun toString(): String = "true" + override fun asDirectionFormula(): DirectionFormula? = DirectionFormula.Atom.True + } + object False : Atom() { + override fun toString(): String = "false" + override fun asDirectionFormula(): DirectionFormula? = DirectionFormula.Atom.False + } + class Float(val left: Expression, val cmp: CompareOp, val right: Expression) : Atom() { + override fun equals(other: Any?): Boolean + = other is Float && other.left == this.left && other.right == this.right && other.cmp == this.cmp + override fun hashCode(): Int + = (31 * (31 * left.hashCode() + cmp.hashCode()) + right.hashCode()) + override fun toString(): String + = "($left $cmp $right)" + + fun copy(left: Expression = this.left, cmp: CompareOp = this.cmp, right: Expression = this.right): Float + = Float(left, cmp, right) + + override fun asDirectionFormula(): DirectionFormula? = null + } + class Transition(val name: String, val direction: Direction, val facet: Facet) : Atom() { + override fun equals(other: Any?): Boolean + = other is Transition && other.name == this.name && other.direction == this.direction && other.facet == this.facet + override fun hashCode(): Int = 31 * name.hashCode() + direction.hashCode() + override fun toString(): String = "$name:$direction$facet" + override fun asDirectionFormula(): DirectionFormula? = null + } + internal class Reference(val name: String) : Atom() { + override fun equals(other: Any?): Boolean = other is Reference && other.name == this.name + override fun hashCode(): Int = name.hashCode() + override fun toString(): String = name + override fun asDirectionFormula(): DirectionFormula? = DirectionFormula.Atom.Reference(this.name) + } + } + + sealed class FirstOrder>( + val name: String, val bound: Formula, val target: Formula, private val op: String + ) : Formula(), Binary { + + override fun toString(): String + = "($op $name in $bound : $target)" + + override fun equals(other: Any?): Boolean + = other is FirstOrder<*> && other.javaClass == this.javaClass && + other.name == this.name && other.target == this.target && other.bound == this.bound + + override fun hashCode(): Int + = 31 * (31 * (31 * name.hashCode() + bound.hashCode()) + target.hashCode()) + op.hashCode() + + override val left: Formula = bound + override val right: Formula = target + abstract fun copy(name: String = this.name, bound: Formula = this.bound, target: Formula = this.target): T + override fun copy(left: Formula, right: Formula): T = copy(bound = left, target = right) + override fun asDirectionFormula(): DirectionFormula? = null + + class ForAll(name: String, bound: Formula, target: Formula) : FirstOrder(name, bound, target, "forall") { + override fun copy(name: String, bound: Formula, target: Formula) = ForAll(name, bound, target) + } + class Exists(name: String, bound: Formula, target: Formula) : FirstOrder(name, bound, target, "exists") { + override fun copy(name: String, bound: Formula, target: Formula): Exists = Exists(name, bound, target) + } + } + + sealed class Hybrid>(val name: String, val target: Formula, private val op: String) : Formula(), Unary { + + override fun equals(other: Any?): Boolean + = other is Hybrid<*> && this.javaClass == other.javaClass && + other.name == this.name && other.target == this.target + + override fun hashCode(): Int + = 31 * (31 * name.hashCode() + target.hashCode()) + op.hashCode() + + override fun toString(): String + = "($op $name : $target)" + + abstract fun copy(name: String = this.name, target: Formula = this.target): T + + override val inner: Formula = target + override fun copy(inner: Formula): T = copy(target = inner) + override fun asDirectionFormula(): DirectionFormula? = null + + class Bind(name: String, target: Formula) : Hybrid(name, target, "bind") { + override fun copy(name: String, target: Formula): Bind = Bind(name, target) + } + + class At(name: String, target: Formula) : Hybrid(name, target, "at") { + override fun copy(name: String, target: Formula): At = At(name, target) + } + } + + sealed class Simple>(override val quantifier: PathQuantifier, + override val inner: Formula, override val direction: DirectionFormula, + private val op: String + ) : Formula(), Temporal, Unary { + + override fun equals(other: Any?): Boolean + = other is Simple<*> && + other.javaClass == this.javaClass && + this.quantifier == other.quantifier && + this.inner == other.inner && + this.direction == other.direction + + override fun hashCode(): Int + = 31 * (31 * (31 * inner.hashCode() + direction.hashCode()) + quantifier.hashCode()) + op.hashCode() + + override fun toString(): String + = "{$direction}$quantifier$op $inner" + + abstract fun copy(quantifier: PathQuantifier = this.quantifier, + inner: Formula = this.inner, + direction: DirectionFormula = this.direction + ) : T + + override fun copy(inner: Formula): T = copy(this.quantifier, inner, this.direction) + override fun asDirectionFormula(): DirectionFormula? = null + + class Next(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula) : Simple(quantifier, inner, direction, "X") { + override fun copy(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula): Next = Next(quantifier, inner, direction) + } + class Future(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula) : Simple(quantifier, inner, direction,"F") { + override fun copy(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula): Future = Future(quantifier, inner, direction) + } + class Globally(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula) : Simple(quantifier, inner, direction,"G") { + override fun copy(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula): Globally = Globally(quantifier, inner, direction) + } + class WeakNext(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula) : Simple(quantifier, inner, direction, "wX") { + override fun copy(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula): WeakNext = WeakNext(quantifier, inner, direction) + } + class WeakFuture(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula) : Simple(quantifier, inner, direction,"wF") { + override fun copy(quantifier: PathQuantifier, inner: Formula, direction: DirectionFormula): WeakFuture = WeakFuture(quantifier, inner, direction) + } + } + + class Until( + override val quantifier: PathQuantifier, + val path: Formula, + val reach: Formula, + override val direction: DirectionFormula + ) : Formula(), Temporal, Binary { + override fun equals(other: Any?): Boolean + = other is Until && + other.quantifier == this.quantifier && + other.path == this.path && + other.reach == this.reach && + other.direction == this.direction + override fun hashCode(): Int + = (31 * (31 * (31 * path.hashCode() + reach.hashCode()) + direction.hashCode()) + quantifier.hashCode()) + override fun toString(): String + = "($path {$direction}${quantifier}U $reach)" + + override val left: Formula = path + override val right: Formula = reach + override fun copy(left: Formula, right: Formula): Until = copy(path = left, reach = right) + override fun asDirectionFormula(): DirectionFormula? = null + + fun copy( + quantifier: PathQuantifier = this.quantifier, + path: Formula = this.path, + reach: Formula = this.path, + direction: DirectionFormula = this.direction + ) = Until(quantifier, path, reach, direction) + + } + + + class Not(override val inner: Formula) : Formula(), Unary { + override fun equals(other: Any?): Boolean + = other is Not && this.inner == other.inner + override fun hashCode(): Int + = inner.hashCode() + override fun toString(): String + = "!$inner" + override fun copy(inner: Formula) + = Not(inner) + override fun asDirectionFormula(): DirectionFormula? + = inner.asDirectionFormula()?.let { DirectionFormula.Not(it) } + } + + sealed class Bool>( + override val left: Formula, override val right: Formula, + private val op: String + ) : Formula(), Binary { + + override fun equals(other: Any?): Boolean + = other is Bool<*> && other.javaClass == this.javaClass && + this.left == other.left && this.right == other.right + + override fun hashCode(): Int + = 31 * (left.hashCode() + 31 * right.hashCode()) + op.hashCode() + + override fun toString(): String + = "($left $op $right)" + + class And(left: Formula, right: Formula) : Bool(left, right, "&&") { + override fun copy(left: Formula, right: Formula): And = And(left, right) + override fun asDirectionFormula(): DirectionFormula? + = left.asDirectionFormula()?.let { l -> + right.asDirectionFormula()?.let { r -> + DirectionFormula.Bool.And(l, r) + }} + } + class Or(left: Formula, right: Formula) : Bool(left, right, "||") { + override fun copy(left: Formula, right: Formula): Or = Or(left, right) + override fun asDirectionFormula(): DirectionFormula? + = left.asDirectionFormula()?.let { l -> + right.asDirectionFormula()?.let { r -> + DirectionFormula.Bool.Or(l, r) + }} + } + class Implies(left: Formula, right: Formula) : Bool(left, right, "->") { + override fun copy(left: Formula, right: Formula): Implies = Implies(left, right) + override fun asDirectionFormula(): DirectionFormula? + = left.asDirectionFormula()?.let { l -> + right.asDirectionFormula()?.let { r -> + DirectionFormula.Bool.Implies(l, r) + }} + } + class Equals(left: Formula, right: Formula) : Bool(left, right, "<->") { + override fun copy(left: Formula, right: Formula): Equals = Equals(left, right) + override fun asDirectionFormula(): DirectionFormula? + = left.asDirectionFormula()?.let { l -> + right.asDirectionFormula()?.let { r -> + DirectionFormula.Bool.Equals(l, r) + }} + } + } + +} + +enum class PathQuantifier { + A, E, pA, pE; +} + +enum class CompareOp(private val str: String) { + GT(">"), GE(">="), EQ("=="), NEQ("!="), LE("<="), LT("<"); + + override fun toString(): String = str +} + +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 +} \ No newline at end of file diff --git a/src/main/kotlin/com/github/sybila/huctl/HUCTLParser.kt b/src/main/kotlin/com/github/sybila/huctl/HUCTLParser.kt new file mode 100644 index 0000000..ed0753a --- /dev/null +++ b/src/main/kotlin/com/github/sybila/huctl/HUCTLParser.kt @@ -0,0 +1,490 @@ +package com.github.sybila.huctl + +import com.github.sybila.huctl.antlr.HUCTLBaseListener +import com.github.sybila.huctl.antlr.HUCTLLexer +import com.github.sybila.huctl.antlr.HUCTLParser +import org.antlr.v4.runtime.* +import org.antlr.v4.runtime.atn.ATNConfigSet +import org.antlr.v4.runtime.dfa.DFA +import org.antlr.v4.runtime.tree.ErrorNode +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.* + +/* + * 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, cyclic and invalid type references) + * and returns a final map of valid formula assignments + */ + +class HUCTLParser() { + + fun formula(input: String): Formula = parse("val = $input")["val"]!! + + fun parse(input: String, onlyFlagged: Boolean = false): Map + = process(FileParser().process(input), onlyFlagged) + + fun parse(input: File, onlyFlagged: Boolean = false): Map + = process(FileParser().process(input), onlyFlagged) + + private fun process(ctx: ParserContext, onlyFlagged: Boolean): Map { + + //Resolve references and finalize type checking. + //However, some formulas are also valid as direction formulas. (Bool only) + //In such cases, default to normal formulas and if needed, perform typecast. + // + //First resolve all aliases - this will assign some definite types to them. + //(with Formulas being possibly later up-casted to DirectionFormulas) + + val references = HashMap(ctx.toMap()) //mutable copy + val replaced = Stack() //processing stack for cycle detection + + fun String.stacked(action: () -> R): R { + replaced.push(this) + val result = action() + replaced.pop() + return result + } + + //resolve a string alias to a specific type (Formula|DirectionFormula|Expression) + fun resolveAlias(name: String): Any = + if (name in replaced) { + throw IllegalStateException("Cyclic reference: $name") + } else name.stacked { + references[name]?.run { + if (this.item is String) resolveAlias(this.item) + else this.item + } ?: Expression.Variable(name) //a = k and k is not defined, it defaults to variable name + } + + //resolve references in an expression + fun resolveExpression(e: Expression): Expression = e.mapLeafs({it}) { e -> + val name = e.name + if (name in replaced) { + throw IllegalStateException("Cyclic reference: $name") + } else name.stacked { + references[name]?.run { + if (this.item is Expression) resolveExpression(this.item) + else throw IllegalStateException( + "Expected type of $name is an Expression." + ) + } ?: e //e is just a model variable + } + } + + //resolve references in a direction formula + fun resolveDirectionFormula(f: DirectionFormula): DirectionFormula = f.mapLeafs { + if (it is DirectionFormula.Atom.Reference) { + val name = it.name + if (name in replaced) { + throw IllegalStateException("Cyclic reference: $name") + } else name.stacked { + references[name]?.run { + if (this.item is DirectionFormula) resolveDirectionFormula(this.item) + else if (this.item is Formula) //try up-casting + this.item.asDirectionFormula()?.let(::resolveDirectionFormula) + ?: throw IllegalStateException("$name cannot be cast to direction formula.") + else throw IllegalStateException( + "Expected type of $name is a direction formula." + ) + } ?: throw IllegalStateException("Undefined reference $name") + } + } else it //True, False, Proposition + } + + //Resolve references in a formula. + fun resolveFormula(f: Formula): Formula = f.fold({ + when (this) { + is Formula.Atom.Reference -> { + val name = this.name + if (name in replaced) { + throw IllegalStateException("Cyclic reference: $name") + } else name.stacked { + references[name]?.run { + if (this.item is Formula) resolveFormula(this.item) + else throw IllegalStateException("Expected type of $name is a formula.") + } ?: throw IllegalStateException("Undefined reference $name") + } + } + //dive into the expressions + is Formula.Atom.Float -> this.copy( + left = resolveExpression(this.left), + right = resolveExpression(this.right) + ) + //True, False, Transition + else -> this + } + }, { inner -> + when (this) { //resolve direction + is Formula.Simple -> this.copy( + inner = inner, direction = resolveDirectionFormula(this.direction) + ) + else -> this.copy(inner) + } + }, { left, right -> + when (this) { //resolve direction + is Formula.Until -> this.copy( + path = left, reach = right, direction = resolveDirectionFormula(this.direction) + ) + else -> this.copy(left, right) + } + }) + + //aliases need to go first, because all other resolve procedures need can depend on them + for ((name, assignment) in references) { + if (assignment.item is String) { + references[name] = assignment.copy(item = resolveAlias(assignment.item)) + } + } + + //the rest can run "in parallel" + for ((name, assignment) in references) { + references[name] = when (assignment.item) { + is Expression -> assignment.copy(item = resolveExpression(assignment.item)) + is DirectionFormula -> assignment.copy(item = resolveDirectionFormula(assignment.item)) + is Formula -> assignment.copy(item = resolveFormula(assignment.item)) + else -> throw IllegalStateException("WTF?!") + } + } + + val results = HashMap() + for ((name, assignment) in references) { + if (assignment.item is Formula && (!onlyFlagged || assignment.flagged)) + results[name] = resolveFormula(assignment.item) + } + + return results + } + +} + +private class FileParser { + + private val processed = HashSet() + + 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.absolutePath) } + + private fun processStream(input: ANTLRInputStream, location: String): FileContext { + val lexer = HUCTLLexer(input) + val parser = HUCTLParser(CommonTokenStream(lexer)) + lexer.removeErrorListeners() + lexer.addErrorListener(errorListener) + parser.removeErrorListeners() + lexer.addErrorListener(errorListener) + val root = parser.root() + val context = FileContext(location) + ParseTreeWalker().walk(context, root) + return context + } + + private val errorListener = object : ANTLRErrorListener { + override fun reportAttemptingFullContext(p0: Parser?, p1: DFA?, p2: Int, p3: Int, p4: BitSet?, p5: ATNConfigSet?) { } + override fun syntaxError(p0: Recognizer<*, *>?, p1: Any?, line: Int, char: Int, msg: String?, p5: RecognitionException?) { + throw IllegalArgumentException("Syntax error at $line:$char: $msg") + } + override fun reportAmbiguity(p0: Parser?, p1: DFA?, p2: Int, p3: Int, p4: Boolean, p5: BitSet?, p6: ATNConfigSet?) { } + override fun reportContextSensitivity(p0: Parser?, p1: DFA?, p2: Int, p3: Int, p4: Int, p5: ATNConfigSet?) { } + } + +} + +private data class ParserContext( + private val assignments: List> +) { + + fun toMap() = assignments.associateBy({ it.name }, { it }) + + /* + * Checks for duplicate assignments received from parser + */ + init { + assignments + .map { one -> assignments.filter { two -> one.name == two.name }.toSet().toList() } + .filter { it.size > 1 } + .any { + throw IllegalStateException( + "Duplicate assignment for ${it[0].name} defined in ${it[0].location} and ${it[1].location}" + ) + } + } + + operator fun plus(ctx: ParserContext): ParserContext { + return ParserContext(assignments + ctx.assignments) + } + +} + +private class FileContext(val location: String) : HUCTLBaseListener() { + + val includes = ArrayList() + val formulas = ArrayList>() + val dirFormulas = ArrayList>() + val expressions = ArrayList>() + val aliases = ArrayList>() + + private val formulaTree = ParseTreeProperty() + private val expressionTree = ParseTreeProperty() + private val dirFormulaTree = ParseTreeProperty() + + fun toParseContext() = ParserContext(formulas + expressions + aliases + dirFormulas) + + /* ----- Basic control flow ------ */ + + override fun exitIncludeStatement(ctx: HUCTLParser.IncludeStatementContext) { + val string = ctx.STRING().text + includes.add(File(string.substring(1, string.length - 1))) //remove quotes + } + + override fun exitAssignStatement(ctx: HUCTLParser.AssignStatementContext) { + fun put(data: MutableList>, item: T) { + data.add(Assignment(ctx.VAR_NAME(0).text, item, "$location:${ctx.start.line}", ctx.FLAG() != null)) + } + when { + ctx.formula() != null -> put(formulas, formulaTree[ctx.formula()]) + ctx.dirFormula() != null -> put(dirFormulas, dirFormulaTree[ctx.dirFormula()]) + ctx.expression() != null -> put(expressions, expressionTree[ctx.expression()]) + else -> put(aliases, ctx.VAR_NAME(1).text) + } + } + + override fun visitErrorNode(node: ErrorNode) { + throw IllegalStateException("Syntax error at '${node.text}' in $location:${node.symbol.line}") + } + + /* ------ Formula Parsing ------ */ + + override fun exitId(ctx: HUCTLParser.IdContext) { + formulaTree[ctx] = Formula.Atom.Reference(ctx.text) + } + + override fun exitBool(ctx: HUCTLParser.BoolContext) { + formulaTree[ctx] = if (ctx.TRUE() != null) True else False + } + + override fun exitTransition(ctx: HUCTLParser.TransitionContext) { + formulaTree[ctx] = Formula.Atom.Transition( + name = ctx.VAR_NAME().text, + direction = if (ctx.IN() != null) Direction.IN else Direction.OUT, + facet = if (ctx.PLUS() != null) Facet.POSITIVE else Facet.NEGATIVE + ) + } + + override fun exitProposition(ctx: HUCTLParser.PropositionContext) { + val left = expressionTree[ctx.expression(0)] + val right = expressionTree[ctx.expression(1)] + val cmp = ctx.compare() + formulaTree[ctx] = when { + cmp.EQ() != null -> left eq right + cmp.NEQ() != null -> left neq right + cmp.LT() != null -> left lt right + cmp.LTEQ() != null -> left le right + cmp.GT() != null -> left gt right + else -> left ge right + } + } + + override fun exitParenthesis(ctx: HUCTLParser.ParenthesisContext) { + formulaTree[ctx] = formulaTree[ctx.formula()] + } + + override fun exitNegation(ctx: HUCTLParser.NegationContext) { + formulaTree[ctx] = not(formulaTree[ctx.formula()]) + } + + private fun splitOperator(operator: String): Pair { + return if (operator.startsWith("p")) { + PathQuantifier.valueOf(operator.take(2)) to operator.drop(2) + } else (PathQuantifier.valueOf(operator.take(1)) to operator.drop(1)) + } + + override fun exitUnaryTemporal(ctx: HUCTLParser.UnaryTemporalContext) { + val (path, state) = splitOperator(ctx.TEMPORAL_UNARY().text) + val dir = ctx.dirModifier()?.let { dirFormulaTree[it.dirFormula()] } ?: DirectionFormula.Atom.True + fun put(constructor: (PathQuantifier, Formula, DirectionFormula) -> Formula) { + formulaTree[ctx] = constructor(path, formulaTree[ctx.formula()], dir) + } + put(unaryTemporalConstructors[state]!!) + } + + override fun exitOr(ctx: HUCTLParser.OrContext) { + formulaTree[ctx] = formulaTree[ctx.formula(0)] or formulaTree[ctx.formula(1)] + } + + override fun exitAnd(ctx: HUCTLParser.AndContext) { + formulaTree[ctx] = formulaTree[ctx.formula(0)] and formulaTree[ctx.formula(1)] + } + + override fun exitImplies(ctx: HUCTLParser.ImpliesContext) { + formulaTree[ctx] = formulaTree[ctx.formula(0)] implies formulaTree[ctx.formula(1)] + } + + override fun exitEqual(ctx: HUCTLParser.EqualContext) { + formulaTree[ctx] = formulaTree[ctx.formula(0)] equal formulaTree[ctx.formula(1)] + } + + override fun exitAllUntil(ctx: HUCTLParser.AllUntilContext) { + ctx.makeUntil(ctx.A_U().text, ctx.formula(0), ctx.formula(1), + ctx.dirModifierL()?.dirModifier()?.dirFormula(), + ctx.dirModifierR()?.dirModifier()?.dirFormula() + ) + } + + override fun exitExistUntil(ctx: HUCTLParser.ExistUntilContext) { + ctx.makeUntil(ctx.E_U().text, ctx.formula(0), ctx.formula(1), + ctx.dirModifierL()?.dirModifier()?.dirFormula(), + ctx.dirModifierR()?.dirModifier()?.dirFormula() + ) + } + + private fun HUCTLParser.FormulaContext.makeUntil(op: String, + pathC: HUCTLParser.FormulaContext, + reachC: HUCTLParser.FormulaContext, + dirLC: HUCTLParser.DirFormulaContext?, + dirRC: HUCTLParser.DirFormulaContext? + ) { + val (path, state) = splitOperator(op) + assert(state == "U") + val left = formulaTree[pathC] + val right = formulaTree[reachC] + val dirL = dirFormulaTree[dirLC] ?: DirectionFormula.Atom.True + val dirR = dirFormulaTree[dirRC] ?: DirectionFormula.Atom.True + if (dirR != DirectionFormula.Atom.True) { + //rewrite using U X + val next = Formula.Simple.Next(path, right, dirR) + formulaTree[this] = Formula.Until(path, left, next, dirL) + } else { + formulaTree[this] = Formula.Until(path, left, right, dirL) + } + } + + override fun exitFirstOrder(ctx: HUCTLParser.FirstOrderContext) { + val bound = ctx.setBound()?.formula()?.let { formulaTree[it] } ?: True + val name = ctx.VAR_NAME().text + val inner = formulaTree[ctx.formula()] + formulaTree[ctx] = + if (ctx.FORALL() != null) Formula.FirstOrder.ForAll(name, bound, inner) + else Formula.FirstOrder.Exists(name, bound, inner) + } + + override fun exitHybrid(ctx: HUCTLParser.HybridContext) { + val name = ctx.VAR_NAME().text + val inner = formulaTree[ctx.formula()] + formulaTree[ctx] = + if (ctx.BIND() != null) Formula.Hybrid.Bind(name, inner) + else Formula.Hybrid.At(name, inner) + } + + /* ------ Direction formula parsing ------ */ + + override fun exitDirId(ctx: HUCTLParser.DirIdContext) { + dirFormulaTree[ctx] = DirectionFormula.Atom.Reference(ctx.text) + } + + override fun exitDirBool(ctx: HUCTLParser.DirBoolContext) { + dirFormulaTree[ctx] = if (ctx.TRUE() != null) DirectionFormula.Atom.True else DirectionFormula.Atom.False + } + + override fun exitDirProposition(ctx: HUCTLParser.DirPropositionContext) { + dirFormulaTree[ctx] = DirectionFormula.Atom.Proposition( + ctx.VAR_NAME().text, if (ctx.PLUS() != null) Facet.POSITIVE else Facet.NEGATIVE + ) + } + + override fun exitDirParenthesis(ctx: HUCTLParser.DirParenthesisContext) { + dirFormulaTree[ctx] = dirFormulaTree[ctx.dirFormula()] + } + + override fun exitDirNegation(ctx: HUCTLParser.DirNegationContext) { + dirFormulaTree[ctx] = not(dirFormulaTree[ctx.dirFormula()]) + } + + override fun exitDirAnd(ctx: HUCTLParser.DirAndContext) { + dirFormulaTree[ctx] = dirFormulaTree[ctx.dirFormula(0)] and dirFormulaTree[ctx.dirFormula(1)] + } + + override fun exitDirOr(ctx: HUCTLParser.DirOrContext) { + dirFormulaTree[ctx] = dirFormulaTree[ctx.dirFormula(0)] or dirFormulaTree[ctx.dirFormula(1)] + } + + override fun exitDirImplies(ctx: HUCTLParser.DirImpliesContext) { + dirFormulaTree[ctx] = dirFormulaTree[ctx.dirFormula(0)] implies dirFormulaTree[ctx.dirFormula(1)] + } + + override fun exitDirEqual(ctx: HUCTLParser.DirEqualContext) { + dirFormulaTree[ctx] = dirFormulaTree[ctx.dirFormula(0)] equal dirFormulaTree[ctx.dirFormula(1)] + } + + + /* ------ Expression Parsing ----- */ + + override fun exitExpId(ctx: HUCTLParser.ExpIdContext) { + expressionTree[ctx] = ctx.text.asVariable() + } + + override fun exitExpValue(ctx: HUCTLParser.ExpValueContext) { + expressionTree[ctx] = Expression.Constant(ctx.FLOAT_VAL().text.toDouble()) + } + + override fun exitExpParenthesis(ctx: HUCTLParser.ExpParenthesisContext) { + expressionTree[ctx] = expressionTree[ctx.expression()] + } + + override fun exitExpMultiply(ctx: HUCTLParser.ExpMultiplyContext) { + expressionTree[ctx] = expressionTree[ctx.expression(0)] times expressionTree[ctx.expression(1)] + } + + override fun exitExpDivide(ctx: HUCTLParser.ExpDivideContext) { + expressionTree[ctx] = expressionTree[ctx.expression(0)] div expressionTree[ctx.expression(1)] + } + + override fun exitExpAdd(ctx: HUCTLParser.ExpAddContext) { + expressionTree[ctx] = expressionTree[ctx.expression(0)] plus expressionTree[ctx.expression(1)] + } + + override fun exitExpSubtract(ctx: HUCTLParser.ExpSubtractContext) { + expressionTree[ctx] = expressionTree[ctx.expression(0)] minus expressionTree[ctx.expression(1)] + } + +} + +private val unaryTemporalConstructors = mapOf Formula>( + "X" to { a,b,c -> Formula.Simple.Next(a, b, c) }, + "wX" to { a,b,c -> Formula.Simple.WeakNext(a, b, c) }, + "F" to { a,b,c -> Formula.Simple.Future(a, b, c) }, + "wF" to { a,b,c -> Formula.Simple.WeakFuture(a, b, c) }, + "G" to { a,b,c -> Formula.Simple.Globally(a, b, c) } +) + +private data class Assignment( + val name: String, + val item: T, + val location: String, + val flagged: Boolean +) + +operator fun ParseTreeProperty.set(k: ParseTree, v: T) = this.put(k, v) +//operator fun ParseTreeProperty.get(k: ParseTree): T = this.get(k) diff --git a/src/test/kotlin/com/github/sybila/ctl/FormulasTest.kt b/src/test/kotlin/com/github/sybila/ctl/FormulasTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/ctl/IntegrationTest.kt b/src/test/kotlin/com/github/sybila/ctl/IntegrationTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/ctl/NormalizerTest.kt b/src/test/kotlin/com/github/sybila/ctl/NormalizerTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/ctl/OptimizerTest.kt b/src/test/kotlin/com/github/sybila/ctl/OptimizerTest.kt old mode 100644 new mode 100755 index 24935df..cd575a6 --- a/src/test/kotlin/com/github/sybila/ctl/OptimizerTest.kt +++ b/src/test/kotlin/com/github/sybila/ctl/OptimizerTest.kt @@ -85,4 +85,12 @@ class OptimizerTest { assertEquals(prop, prop.optimize()) } + @Test + fun cannotOptimize() { + val p = "val".negativeIn() + val q = "var".positiveIn() + val prop = (p and q) or (p and not(q)) + assertEquals(prop, prop.optimize()) + } + } \ No newline at end of file diff --git a/src/test/kotlin/com/github/sybila/ctl/ParserBasicTest.kt b/src/test/kotlin/com/github/sybila/ctl/ParserBasicTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/ctl/ParserComplexTest.kt b/src/test/kotlin/com/github/sybila/ctl/ParserComplexTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/ctl/ParserIncludeTest.kt b/src/test/kotlin/com/github/sybila/ctl/ParserIncludeTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/ctl/ParserReferencesTest.kt b/src/test/kotlin/com/github/sybila/ctl/ParserReferencesTest.kt old mode 100644 new mode 100755 diff --git a/src/test/kotlin/com/github/sybila/huctl/FormulasTest.kt b/src/test/kotlin/com/github/sybila/huctl/FormulasTest.kt new file mode 100644 index 0000000..c1ea720 --- /dev/null +++ b/src/test/kotlin/com/github/sybila/huctl/FormulasTest.kt @@ -0,0 +1,188 @@ +package com.github.sybila.huctl + +import org.junit.Test +import kotlin.test.assertEquals +import kotlin.test.assertNotEquals +import kotlin.test.assertNull + +class FoldTest { + + val formula = EX((True EU ( + "var".asVariable() eq 13.3.asConstant() + or + "val".negativeIn())) + , dir = "x".increase() + ) + + + @Test + fun foldIdentity() { + assertEquals(formula, formula.fold({this}, Formula.Unary<*>::copy, Formula.Binary<*>::copy)) + } + + @Test + fun foldLeafs() { + assertEquals( + EX(False EU ( + "var".positiveOut() + or + ("val".asVariable() neq 10.3.asConstant()) + ), dir = "x".increase() + ), formula.mapLeafs { + when (it) { + is Formula.Atom.True -> False + is Formula.Atom.Float -> "var".positiveOut() + is Formula.Atom.Transition -> ("val".asVariable() neq 10.3.asConstant()) + else -> it + } + } + ) + } + + @Test + fun foldOperators() { + assertEquals( + AX(True AU ( + "var".asVariable() eq 13.3.asConstant() + and + "val".negativeIn() + ), dir = "y".decrease() + ), formula.fold({this}, { + if (this is Formula.Simple.Next) { + AX(it, dir = "y".decrease()) + } else this.copy(it) + }, { l,r -> + if (this is Formula.Until) { + l AU r + } else if (this is Formula.Bool.Or) { + l and r + } else this.copy(l, r) + }) + ) + } + + @Test + fun foldHeight() { + assertEquals(4, formula.fold({1}, { it + 1 }, { l, r -> Math.max(l,r) + 1 } )) + } + +} + +class Misc { + + @Test + fun booleanToString() { + assertEquals("true", True.toString()) + assertEquals("false", False.toString()) + } + + @Test + fun variableToString() { + assertEquals("test", "test".asVariable().toString()) + } + + @Test + fun constantToString() { + assertEquals("3.1400", 3.14.asConstant().toString()) + } + + @Test + fun expressionToString() { + assertEquals("((a + 12.0000) / ((3.0000 * 4.0000) - Var))", + ( + ("a".asVariable() plus 12.0.asConstant()) + div + ((3.0.asConstant() times 4.0.asConstant()) minus "Var".asVariable()) + ).toString()) + } + + @Test + fun ctlFormulaToString() { + assertEquals("(!true && {true}pEwX (false {true}EU true))", (not(True) and pastWeakEX(False EU True)).toString()) + } + + @Test + fun hybridFormulaToString() { + assertEquals("(at x : (bind y : true))", at("x", bind("y", True)).toString()) + } + + @Test + fun firstOrderFormulaToString() { + assertEquals( + "(forall x in false : (exists y in true : false))", + forall("x", False, exists("y", True, False)).toString() + ) + } + + @Test + fun floatPropositionToString() { + val prop = ("prop".asVariable() gt 5.3.asConstant()) + assertEquals("(prop > 5.3000)", prop.toString()) + } + + @Test + fun directionToString() { + assertEquals("prop:in+", "prop".positiveIn().toString()) + } + + @Test + fun basicProperties() { + val v1 = "v1".asVariable() + val v2 = "v2".asVariable() + assertNotEquals(v1.hashCode(), v2.hashCode()) + assertNotEquals(v1, v2) + + val prop1 = ("prop1".asVariable() gt 5.3.asConstant()) + val prop2 = ("prop2".asVariable() gt (54.3.asConstant() plus 3.2.asConstant())) + assertNotEquals(prop1.hashCode(), prop2.hashCode()) + assertNotEquals(prop1, prop2) + + val dir1 = "v1".positiveIn() + val dir2 = "v1".negativeOut() + assertNotEquals(dir1.hashCode(), dir2.hashCode()) + assertNotEquals(dir1, dir2) + assertEquals("v1", dir1.name) + assertEquals(Facet.POSITIVE, dir1.facet) + assertEquals(Direction.IN, dir1.direction) + + val u = (prop1 EU prop2) as Formula.Until + assertEquals(prop1, u.path) + assertEquals(prop2, u.reach) + } + + @Test + fun directionCast() { + val tt = Formula.Atom.True + val ff = Formula.Atom.False + val dTT = DirectionFormula.Atom.True + val dFF = DirectionFormula.Atom.False + + //simple invalid + assertNull(("a".asVariable() gt "b".asVariable()).asDirectionFormula()) + assertNull("a".positiveIn().asDirectionFormula()) + assertNull(EX(tt).asDirectionFormula()) + assertNull((tt EU ff).asDirectionFormula()) + assertNull(forall("x", tt, tt).asDirectionFormula()) + assertNull(bind("x", tt).asDirectionFormula()) + + //simple valid + assertEquals(dTT, tt.asDirectionFormula()) + assertEquals(dFF, ff.asDirectionFormula()) + assertEquals(not(dTT), not(tt).asDirectionFormula()) + assertEquals(dTT and dFF, (tt and ff).asDirectionFormula()) + assertEquals(dTT or dFF, (tt or ff).asDirectionFormula()) + assertEquals(dTT implies dFF, (tt implies ff).asDirectionFormula()) + assertEquals(dTT equal dFF, (tt equal ff).asDirectionFormula()) + + //complex invalid + assertNull((tt and "a".positiveIn()).asDirectionFormula()) + assertNull(("a".positiveIn() and ff).asDirectionFormula()) + assertNull((tt or "a".positiveIn()).asDirectionFormula()) + assertNull(("a".positiveIn() or ff).asDirectionFormula()) + assertNull((tt implies "a".positiveIn()).asDirectionFormula()) + assertNull(("a".positiveIn() implies ff).asDirectionFormula()) + assertNull((tt equal "a".positiveIn()).asDirectionFormula()) + assertNull(("a".positiveIn() equal ff).asDirectionFormula()) + } + +} \ No newline at end of file diff --git a/src/test/kotlin/com/github/sybila/huctl/IntegrationTest.kt b/src/test/kotlin/com/github/sybila/huctl/IntegrationTest.kt new file mode 100644 index 0000000..d5e0672 --- /dev/null +++ b/src/test/kotlin/com/github/sybila/huctl/IntegrationTest.kt @@ -0,0 +1,50 @@ +package com.github.sybila.huctl + +import org.junit.Test +import java.io.File +import kotlin.test.assertEquals + +/** + * Consider this an example of usage + */ +class Integration { + + @Test fun test() { + + val f1 = File.createTempFile("file", ".ctl") + + val parser = HUCTLParser() + + f1.bufferedWriter().use { + it.write(":? c = p2 > 3.14 <-> False \n") + it.write("pop = True EU c EU a \n") + } + + val input = ":include \"${ f1.absolutePath }\" \n" + + """ + a = True && p1:out+ + :? f = EF True && EG pop || AX a + """ + val formulas = parser.parse(input) + val flagged = parser.parse(input, onlyFlagged = true) + + val p1 = "p1".positiveOut() + val p2 = ("p2".asVariable() gt 3.14.asConstant()) + val np2 =("p2".asVariable() le 3.14.asConstant()) + + 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["a"]) + assertEquals(c, formulas["c"]) + assertEquals(pop, formulas["pop"]) + assertEquals(f, formulas["f"]) + assertEquals(2, flagged.size) + assertEquals(f, flagged["f"]) + assertEquals(c, flagged["c"]) + } + +} \ No newline at end of file diff --git a/src/test/kotlin/com/github/sybila/huctl/ParserBasicTest.kt b/src/test/kotlin/com/github/sybila/huctl/ParserBasicTest.kt new file mode 100644 index 0000000..6dc2cbf --- /dev/null +++ b/src/test/kotlin/com/github/sybila/huctl/ParserBasicTest.kt @@ -0,0 +1,396 @@ +package com.github.sybila.huctl + +import org.junit.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class Basic { + + val parser = HUCTLParser() + + @Test + fun parenthesis() { + assertEquals( + True, + parser.formula("(True)") + ) + } + + @Test + fun boolOps() { + assertEquals( + not(True), + parser.formula("!True") + ) + 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 untilOps() { + //basic + assertEquals( + True EU False, + parser.formula("True EU False") + ) + assertEquals( + True AU False, + parser.formula("True AU False") + ) + //path direction + assertEquals( + True.pastEU(False, True.asDirectionFormula()!!), + parser.formula("True {True}pEU False") + ) + assertEquals( + True.pastAU(False, True.asDirectionFormula()!!), + parser.formula("True {True}pAU False") + ) + //reach direction + assertEquals( + True EU (EX(False, False.asDirectionFormula()!!)), + parser.formula("True EU{False} False") + ) + assertEquals( + True pastEU (pastEX(False, False.asDirectionFormula()!!)), + parser.formula("True pEU{False} False") + ) + assertEquals( + True AU (AX(False, False.asDirectionFormula()!!)), + parser.formula("True AU{False} False") + ) + assertEquals( + True pastAU (pastAX(False, False.asDirectionFormula()!!)), + parser.formula("True pAU{False} False") + ) + //both + assertEquals( + True.pastEU(pastEX(False, False.asDirectionFormula()!!), True.asDirectionFormula()!!), + parser.formula("True {True}pEU{False} False") + ) + assertEquals( + True.EU(EX(False, False.asDirectionFormula()!!), True.asDirectionFormula()!!), + parser.formula("True {True}EU{False} False") + ) + assertEquals( + True.pastAU(pastAX(False, False.asDirectionFormula()!!), True.asDirectionFormula()!!), + parser.formula("True {True}pAU{False} False") + ) + assertEquals( + True.AU(AX(False, False.asDirectionFormula()!!), True.asDirectionFormula()!!), + parser.formula("True {True}AU{False} False") + ) + } + + @Test + fun unaryOps() { + //basic + 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") + ) + assertEquals( + weakEX(True), + parser.formula("EwX True") + ) + assertEquals( + weakAX(True), + parser.formula("AwX True") + ) + assertEquals( + weakEF(True), + parser.formula("EwF True") + ) + assertEquals( + weakAF(True), + parser.formula("AwF True") + ) + //past + assertEquals( + pastEX(True), + parser.formula("pEX True") + ) + assertEquals( + pastAX(True), + parser.formula("pAX True") + ) + assertEquals( + pastEF(True), + parser.formula("pEF True") + ) + assertEquals( + pastAF(True), + parser.formula("pAF True") + ) + assertEquals( + pastEG(True), + parser.formula("pEG True") + ) + assertEquals( + pastAG(True), + parser.formula("pAG True") + ) + assertEquals( + pastWeakEX(True), + parser.formula("pEwX True") + ) + assertEquals( + pastWeakAX(True), + parser.formula("pAwX True") + ) + assertEquals( + pastWeakEF(True), + parser.formula("pEwF True") + ) + assertEquals( + pastWeakAF(True), + parser.formula("pAwF True") + ) + //transitions + assertEquals( + pastWeakAF(True, False.asDirectionFormula()!!), + parser.formula("{False}pAwF True") + ) + } + + @Test + fun floats() { + val v = "var".asVariable() + assertEquals( + (v eq 0.0.asConstant()), + parser.formula("var == 0") + ) + assertEquals( + (v eq 1.0.asConstant()), + parser.formula("var == 1") + ) + assertEquals( + (v neq (-1.0).asConstant()), + parser.formula("var != -1") + ) + assertEquals( + (v gt 0.158.asConstant()), + parser.formula("var > 0.158") + ) + assertEquals( + (v ge (-0.9995).asConstant()), + parser.formula("var >= -0.9995") + ) + assertEquals( + (v lt 1040.58.asConstant()), + parser.formula("var < 1040.58") + ) + assertEquals( + (v le (-586.44).asConstant()), + parser.formula("var <= -586.44") + ) + } + + @Test + fun firstOrder() { + assertEquals( + forall("x", True, False), parser.formula("forall x: False") + ) + assertEquals( + forall("x", False, False), parser.formula("forall x in False: False") + ) + assertEquals( + exists("x", True, False), parser.formula("exists x: False") + ) + assertEquals( + exists("x", False, False), parser.formula("exists x in False: False") + ) + } + + @Test + fun hybrid() { + assertEquals( + at("x", True), parser.formula("at x: True") + ) + assertEquals( + bind("x", True), parser.formula("bind x: True") + ) + } + + @Test + fun directionProposition() { + assertEquals(EX(True, "x".increase()), parser.formula("{x+}EX True")) + assertEquals(EX(True, "x".decrease()), parser.formula("{x-}EX True")) + assertEquals(EX(True, True.asDirectionFormula()!!), parser.formula("{True}EX True")) + assertEquals(EX(True, False.asDirectionFormula()!!), parser.formula("{False}EX True")) + } + + @Test + fun directionBool() { + assertEquals(EX(True, not("x".increase())), parser.formula("{!x+}EX True")) + assertEquals(EX(True, "x".increase() and "y".decrease()), parser.formula("{x+ && y-}EX True")) + assertEquals(EX(True, "x".increase() or "y".decrease()), parser.formula("{x+ || y-}EX True")) + assertEquals(EX(True, "x".increase() implies "y".decrease()), parser.formula("{x+ -> y-}EX True")) + assertEquals(EX(True, "x".increase() equal "y".decrease()), parser.formula("{x+ <-> y-}EX True")) + } + + @Test + fun transitions() { + assertEquals( + "var".positiveIn(), + parser.formula("var:in+") + ) + assertEquals( + "var".positiveOut(), + parser.formula("var:out+") + ) + assertEquals( + "var".negativeIn(), + parser.formula("var:in-") + ) + assertEquals( + "var".negativeOut(), + parser.formula("var:out-") + ) + } + + @Test + fun floatOps() { + val v = "var1".asVariable() + val w = "var2".asVariable() + val zero = 0.0.asConstant() + assertEquals( + ((v plus w) eq zero), + parser.formula("var1 + var2 == 0") + ) + assertEquals( + ((v minus w) eq zero), + parser.formula("var1 - var2 == 0") + ) + assertEquals( + ((v times w) eq zero), + parser.formula("var1 * var2 == 0") + ) + assertEquals( + ((v div w) eq zero), + parser.formula("var1 / var2 == 0") + ) + } + + @Test + fun comments() { + var result = parser.parse(""" + //f = False + k = True + //l = False + """) + assertEquals(1, result.size) + assertEquals(True, result["k"]) + + result = parser.parse(""" + /* Some redundant text + f = False + */ + k = True + //l = False + """) + assertEquals(1, result.size) + assertEquals(True, result["k"]) + + result = parser.parse(""" + k = True + # Python style comment + f = False + """) + assertEquals(2, result.size) + assertEquals(True, result["k"]) + assertEquals(False, result["f"]) + + result = parser.parse(""" + /* Comment f = False + /* With nesting */ + */ + k = True + //l = False + """) + assertEquals(1, result.size) + assertEquals(True, result["k"]) + + result = parser.parse(""" + k = True + //comment at the end of file""") + assertEquals(1, result.size) + assertEquals(True, result["k"]) + } + + @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")) + } + + @Test + fun invalidInput() { + assertFailsWith { + parser.parse(""" + l = True && False + k = tr&ue && False + """) + } + } + + @Test + fun flaggedFormulasParseAll() { + val result = parser.parse(""" + foo = True + :? goo = False + """, onlyFlagged = false) + assertEquals(2, result.size) + assertEquals(True, result["foo"]) + assertEquals(False, result["goo"]) + } + + @Test + fun flaggedFormulas() { + val result = parser.parse(""" + foo = True + :? goo = False + """, onlyFlagged = true) + assertEquals(1, result.size) + assertEquals(False, result["goo"]) + } + +} \ No newline at end of file diff --git a/src/test/kotlin/com/github/sybila/huctl/ParserComplexTest.kt b/src/test/kotlin/com/github/sybila/huctl/ParserComplexTest.kt new file mode 100644 index 0000000..ab9b0c3 --- /dev/null +++ b/src/test/kotlin/com/github/sybila/huctl/ParserComplexTest.kt @@ -0,0 +1,248 @@ +package com.github.sybila.huctl + +import org.junit.Test +import java.io.File +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class Complex { + + val parser = HUCTLParser() + + + val p1 = ("p1".asVariable() eq 4.0.asConstant()) + val p2 = "p2".negativeIn() + val p3 = (("p3".asVariable() div 1.3.asConstant()) plus 2.0.asConstant() lt + (((-3.14).asConstant() plus (12.0.asConstant() minus "f".asVariable())) times 2.0.asConstant()) + ) + + @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 z + 2 < x*2 EU a") + } + + f2.bufferedWriter().use { + it.write(":include \"${ f1.absolutePath }\" \n") + it.write("b = EX c <-> True \n") + it.write("d = e -> e \n") + it.write("q = 12 - f \n") + it.write("x = -3.14 + q \n") + } + + f3.bufferedWriter().use { + it.write("a = ! p1 == 4 \n") + it.write("z = p3 / 1.3 \n") + it.write(":include \"${ f2.absolutePath }\" \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["a"]) + assertEquals(b, result["b"]) + assertEquals(c, result["c"]) + assertEquals(d, result["d"]) + assertEquals(e, result["e"]) + + f1.delete() + f2.delete() + f3.delete() + + } + + @Test + fun complexString() { + + val result = parser.parse(""" + dir = true || x+ + z = p3 + x = 12 - f + b = EX z/1.3 + 2 < (-3.14 + x) * 2 EU a + a = (p1 == 4) && p2:in- + d = {(y-) -> dir}AG {dir}AX c + c = b <-> b + e = c && (forall x: True) || (exists y in d: False) && b + """) + + val dir = DirectionFormula.Atom.True or "x".increase() + val a = p1 and p2 + val b = EX(p3) EU a + val c = b equal b + val d = AG(AX(c, dir), "y".decrease() implies dir) + val e = (c and forall("x", True, True)) or (exists("y", d, False) and b) + + assertEquals(5, result.size) + assertEquals(a, result["a"]) + assertEquals(b, result["b"]) + assertEquals(c, result["c"]) + assertEquals(d, result["d"]) + assertEquals(e, result["e"]) + + } + + @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 + // +, -, *, / are also associative + 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 directionOperatorAssociativity() { + //Implication is right associative! + assertEquals( + EX(True, ("z".increase() implies ("x".increase() implies "y".decrease()))), + parser.formula("{z+ -> x+ -> y-}EX 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") + ) + 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") + ) + assertEquals( + forall("x", False, (True or False) AU (True and exists("y", True, False))), + parser.formula("forall x in False: True || False AU True && exists y in True: False") + ) + } + + @Test + fun directionOperatorPriority() { + //we do not test every combination, since priority should be transitive + val xp = "x".increase() + val yd = "y".decrease() + assertEquals( + EX(True, not(xp) and not(yd)), + parser.formula("{!x+ && !y-} EX true") + ) + assertEquals( + EX(True, (xp and yd) or (yd and xp)), + parser.formula("{x+ && y- || y- && x+} EX True") + ) + assertEquals( + EX(True, (xp or yd) implies (yd or xp)), + parser.formula("{x+ || y- -> y- || x+} EX True") + ) + assertEquals( + EX(True, (xp implies yd) equal (yd implies xp)), + parser.formula("{x+ -> y- <-> y- -> x+} EX True") + ) + } + + @Test + fun expressionOperatorPriority() { + //We don't care about priority of * vs. / and + vs. - + val three = 3.0.asConstant() + assertEquals(((three times three) plus three eq 0.0.asConstant()), + parser.formula("3 * 3 + 3 == 0")) + assertEquals(((three times three) minus three eq 0.0.asConstant()), + parser.formula("3 * 3 - 3 == 0")) + assertEquals(((three div three) plus three eq 0.0.asConstant()), + parser.formula("3 / 3 + 3 == 0")) + assertEquals(((three div three) minus three eq 0.0.asConstant()), + parser.formula("3 / 3 - 3 == 0")) + } + + @Test + fun ambiguousFormulas() { + val r = parser.parse(""" + k = True && False + l = {k}EX True + m = k || False + """) + assertEquals(3, r.size) + assertEquals(True and False, r["k"]) + assertEquals(EX(True, True.asDirectionFormula()!! and False.asDirectionFormula()!!), r["l"]) + assertEquals((True and False) or False, r["m"]) + } + + @Test + fun formulaCastError() { + //direction to formula + assertFailsWith { + parser.parse(""" + k = x+ || y- + l = EX k + """) + } + //formula to direction + assertFailsWith { + parser.parse(""" + k = EX True + l = {k}EF False + """) + } + //expression to direction formula + assertFailsWith { + parser.parse(""" + k = 1 + 2 + l = {k} EX False + """) + } + //expression to formula + assertFailsWith { + parser.parse(""" + k = a + b + l = EX k + """) + } + //formula to expression + assertFailsWith { + parser.parse(""" + k = EX True + a = k + 2 + """) + } + } + +} + diff --git a/src/test/kotlin/com/github/sybila/huctl/ParserIncludeTest.kt b/src/test/kotlin/com/github/sybila/huctl/ParserIncludeTest.kt new file mode 100644 index 0000000..da41bf1 --- /dev/null +++ b/src/test/kotlin/com/github/sybila/huctl/ParserIncludeTest.kt @@ -0,0 +1,113 @@ +package com.github.sybila.huctl + +import com.github.sybila.huctl.HUCTLParser +import com.github.sybila.huctl.False +import com.github.sybila.huctl.True +import org.junit.Test +import java.io.File +import java.io.FileNotFoundException +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class Includes { + + val parser = HUCTLParser() + + @Test fun invalidInclude() { + assertFailsWith(FileNotFoundException::class) { + 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.absolutePath }\"") + } + i2.bufferedWriter().use { + it.write(":include \"${ i1.absolutePath }\" \n") + it.write(":include \"${ i2.absolutePath }\" \n") + it.write("val2 = False") + } + + val result = parser.parse( + ":include \"${ i2.absolutePath }\" \n" + + ":include \"${ i1.absolutePath }\" " + ) + + assertEquals(2, result.size) + assertEquals(True, result["val"]) + assertEquals(False, result["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.absolutePath }\"") + } + + val result = parser.parse(":include \"${ i2.absolutePath }\"") + + assertEquals(1, result.size) + assertEquals(True, result["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.absolutePath }\"") + } + + val result = parser.parse(file) + + assertEquals(1, result.size) + assertEquals(True, result["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.absolutePath }\"" + ) + + assertEquals(1, result.size) + assertEquals(True, result["val"]) + + file.delete() + } + +} diff --git a/src/test/kotlin/com/github/sybila/huctl/ParserReferencesTest.kt b/src/test/kotlin/com/github/sybila/huctl/ParserReferencesTest.kt new file mode 100644 index 0000000..1adf344 --- /dev/null +++ b/src/test/kotlin/com/github/sybila/huctl/ParserReferencesTest.kt @@ -0,0 +1,230 @@ +package com.github.sybila.huctl + +import org.junit.Test +import java.io.File +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith + +class References { + + val parser = HUCTLParser() + + @Test fun cyclicReferenceThroughFiles() { + val file = File.createTempFile("file", ".ctx") + + file.bufferedWriter().use { + it.write("k = m") + } + + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + m = !k + """) + } + file.delete() + } + + @Test fun transitiveCyclicReference() { + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + k = EX l + l = AX m + m = ! k + """) + } + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + e = a + 2 + a = b - 2 + b = 2 * e + """) + } + } + + @Test fun simpleCyclicReference() { + //formula + assertFailsWith { + parser.parse("k = !k") + } + //expression + assertFailsWith { + parser.parse("a = a + a") + } + //direction formula + assertFailsWith { + parser.parse("a = b+ || a") + } + //alias + assertFailsWith { + parser.parse("a = a") + } + } + + @Test fun undefinedReference() { + assertFailsWith(IllegalStateException::class) { + parser.parse("k = EF m") + } + } + + @Test fun declarationOrderIndependence() { + + val result = parser.parse(""" + k = ! m + m = True + """) + + assertEquals(2, result.size) + assertEquals(not(True), result["k"]) + assertEquals(True, result["m"]) + + } + + @Test fun duplicateDeclarationInFiles() { + + val i1 = File.createTempFile("include1", ".ctl") + + i1.bufferedWriter().use { + it.write("k = True") + } + + assertFailsWith(IllegalStateException::class) { + parser.parse( + ":include \"${ i1.absolutePath }\" \n" + + "k = False" + ) + } + + i1.delete() + } + + @Test fun duplicateDeclarationInString() { + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + k = True + l = False + k = False + """) + } + } + + @Test fun duplicateDeclarationExpression() { + assertFailsWith(IllegalStateException::class) { + parser.parse(""" + k = 1 + l = 2 + k = 1.5 + """) + } + } + + @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.absolutePath }\" \n" + + ":include \"${ i2.absolutePath }\" \n" + ) + + assertEquals(3, result.size) + assertEquals(True, result["k"]) + assertEquals(EF(True), result["l"]) + assertEquals(not(EF(True)), result["m"]) + + } + + @Test fun transitiveResolveInString() { + + val result = parser.parse(""" + j = True + k = j + l = EF k + m = !l + """) + + assertEquals(4, result.size) + assertEquals(True, result["j"]) + assertEquals(True, result["k"]) + assertEquals(EF(True), result["l"]) + assertEquals(not(EF(True)), result["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.absolutePath }\" \n" + ) + + assertEquals(2, result.size) + assertEquals(False, result["val"]) + assertEquals(not(False), result["k"]) + + i.delete() + + } + + @Test fun simpleResolveInString() { + val result = parser.parse(""" + k = True + l = !k + """) + assertEquals(2, result.size) + assertEquals(True, result["k"]) + assertEquals(not(True), result["l"]) + } + + @Test fun simpleResolveExpression() { + val result = parser.parse(""" + k = a + b + l = k / 2 == 0 + """) + assertEquals(1, result.size) + assertEquals((("a".asVariable() plus "b".asVariable()) div 2.0.asConstant() eq 0.0.asConstant()), + result["l"]) + } + + @Test fun aliasInString() { + try { + val result = parser.parse(""" + k = True + l = k + m = l + n = m + """) + assertEquals(4, result.size) + assertEquals(True, result["k"]) + assertEquals(True, result["l"]) + assertEquals(True, result["m"]) + assertEquals(True, result["n"]) + } catch (e: IllegalStateException) { e.printStackTrace() } + } + + @Test fun expressionAlias() { + val result = parser.parse(""" + k = name + l = k + m = l + n = m > 0 + """) + assertEquals(1, result.size) + assertEquals(("name".asVariable() gt 0.0.asConstant()), result["n"]) + } + +} \ No newline at end of file