Skip to content

Commit

Permalink
Migrate to Kotlin M13
Browse files Browse the repository at this point in the history
  • Loading branch information
@daemontus
daemontus committed Sep 19, 2015
1 parent 7ae5106 commit 6c57f5f
Show file tree
Hide file tree
Showing 10 changed files with 142 additions and 143 deletions.
2 changes: 1 addition & 1 deletion build.gradle
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//include antlr plugin
buildscript {
ext.kotlin_version = '0.12.1230'
ext.kotlin_version = '0.13.1513'
repositories {
maven {
name 'JFrog OSS snapshot repo'
Expand Down
23 changes: 10 additions & 13 deletions src/main/kotlin/cz/muni/fi/ctl/Parser.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,7 @@ import org.antlr.v4.runtime.tree.ParseTree
import org.antlr.v4.runtime.tree.ParseTreeProperty
import org.antlr.v4.runtime.tree.ParseTreeWalker
import java.io.File
import java.util.ArrayList
import java.util.HashMap
import java.util.HashSet
import java.util.Stack
import java.util.*

/**
* Workflow:
Expand Down Expand Up @@ -49,7 +46,7 @@ public class Parser {
throw IllegalStateException("Cyclic reference: ${f.name}")
else -> {
replaced.push(f.name)
val result = references[f.name].treeMap(::replace)
val result = references[f.name]!!.treeMap(::replace)
replaced.pop()
result
}
Expand Down Expand Up @@ -88,7 +85,7 @@ class FileParser {
processStream(ANTLRInputStream(input.toCharArray(), input.length()), "input string")

private fun processFile(input: File): FileContext =
input.inputStream().use { processStream(ANTLRInputStream(it), input.getAbsolutePath()) }
input.inputStream().use { processStream(ANTLRInputStream(it), input.absolutePath) }

private fun processStream(input: ANTLRInputStream, location: String): FileContext {
val root = CTLParser(CommonTokenStream(CTLLexer(input))).root()
Expand Down Expand Up @@ -137,22 +134,22 @@ class FileContext(val location: String) : CTLBaseListener() {
fun toParseContext() = ParserContext(assignments)

override fun exitInclude(ctx: CTLParser.IncludeContext) {
val string = ctx.STRING().getText()!!
val string = ctx.STRING().text!!
includes.add(File(string.substring(1, string.length() - 1))) //remove quotes
}

override fun exitAssign(ctx: CTLParser.AssignContext) {
assignments.add(Assignment(
ctx.VAR_NAME().getText()!!,
ctx.VAR_NAME().text!!,
formulas[ctx.formula()]!!,
location+":"+ctx.start.getLine()
location+":"+ctx.start.line
))
}

/** ------ Formula Parsing ------ **/

override fun exitId(ctx: CTLParser.IdContext) {
formulas[ctx] = Reference(ctx.getText()!!)
formulas[ctx] = Reference(ctx.text!!)
}

override fun exitBool(ctx: CTLParser.BoolContext) {
Expand All @@ -161,17 +158,17 @@ class FileContext(val location: String) : CTLBaseListener() {

override fun exitDirection(ctx: CTLParser.DirectionContext) {
formulas[ctx] = DirectionProposition(
variable = ctx.VAR_NAME().getText()!!,
variable = ctx.VAR_NAME().text!!,
direction = if (ctx.IN() != null) Direction.IN else Direction.OUT,
facet = if (ctx.PLUS() != null) Facet.POSITIVE else Facet.NEGATIVE
)
}

override fun exitProposition(ctx: CTLParser.PropositionContext) {
formulas[ctx] = FloatProposition(
variable = ctx.VAR_NAME().getText()!!,
variable = ctx.VAR_NAME().text!!,
floatOp = ctx.floatOp().toOperator(),
value = ctx.FLOAT_VAL().getText().toDouble()
value = ctx.FLOAT_VAL().text.toDouble()
)
}

Expand Down
28 changes: 14 additions & 14 deletions src/test/kotlin/cz/muni/fi/ctl/FormulasTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ package cz.muni.fi.ctl

import org.junit.Test
import kotlin.test.assertEquals
import kotlin.test.failsWith
import kotlin.test.assertFailsWith

class MapTest {

Expand All @@ -13,21 +13,21 @@ class MapTest {
)
)

Test fun treeMapId() {
@Test fun treeMapId() {

assertEquals(formula, formula.treeMap { it })

}

Test fun treeMapPropositions() {
@Test fun treeMapPropositions() {

formula.treeMap {
if (it.operator.cardinality == 0) throw IllegalStateException("Executing tree map on a leaf")
else it
}
}

Test fun treeMapComplex() {
@Test fun treeMapComplex() {

fun transform(f: Formula): Formula = when(f.operator) {
Op.EXISTS_NEXT -> FormulaImpl(Op.ALL_NEXT, f.subFormulas.map(::transform))
Expand All @@ -50,40 +50,40 @@ class MapTest {

class Misc {

Test fun booleanToString() {
@Test fun booleanToString() {
assertEquals("True", True.toString())
assertEquals("False", False.toString())
}

Test fun formulaToString() {
@Test fun formulaToString() {
assertEquals("(True && EX (False EU True))", (True and EX(False EU True)).toString())
}

Test fun floatToString() {
@Test fun floatToString() {
assertEquals("prop > 5.3", FloatProposition("prop", FloatOp.GT, 5.3).toString())
}

Test fun directionToString() {
@Test fun directionToString() {
assertEquals("prop:in+", DirectionProposition("prop", Direction.IN, Facet.POSITIVE).toString())
}

Test fun emptyFormula() {
@Test fun emptyFormula() {
assertEquals("null([])",FormulaImpl().toString())
}

Test fun notEnoughFormulas() {
failsWith(javaClass<IllegalArgumentException>()) {
@Test fun notEnoughFormulas() {
assertFailsWith(IllegalArgumentException::class) {
FormulaImpl(Op.ALL_UNTIL, True)
}
}

Test fun tooManyFormulas() {
failsWith(javaClass<IllegalArgumentException>()) {
@Test fun tooManyFormulas() {
assertFailsWith(IllegalArgumentException::class) {
FormulaImpl(Op.ALL_UNTIL, True, False, Atom())
}
}

Test fun get() {
@Test fun get() {
val float = FloatProposition("val", FloatOp.GT, 34.12)
assertEquals("val", float.variable)
assertEquals(FloatOp.GT, float.floatOp)
Expand Down
12 changes: 6 additions & 6 deletions src/test/kotlin/cz/muni/fi/ctl/IntegrationTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ import kotlin.test.assertEquals
*/
class Integration {

Test fun test() {
@Test fun test() {

val f1 = File.createTempFile("file", ".ctl")

Expand All @@ -23,7 +23,7 @@ class Integration {
}

val formulas = parser.parse(
"#include \"${ f1.getAbsolutePath() }\" \n" +
"#include \"${ f1.absolutePath }\" \n" +
"""
a = True && p1:out+
f = EF True && EG pop || AX a
Expand All @@ -39,10 +39,10 @@ class Integration {
val f = (EF(True) and EG(pop)) or AX(a)

assertEquals(4, formulas.size())
assertEquals(a, formulas.get("a"))
assertEquals(c, formulas.get("c"))
assertEquals(pop, formulas.get("pop"))
assertEquals(f, formulas.get("f"))
assertEquals(a, formulas["a"])
assertEquals(c, formulas["c"])
assertEquals(pop, formulas["pop"])
assertEquals(f, formulas["f"])

val normalized = normalizer.normalize(f)

Expand Down
38 changes: 19 additions & 19 deletions src/test/kotlin/cz/muni/fi/ctl/NormalizerTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ class UntilNormalFormTest {

val normalizer = Normalizer()

Test fun complexTest() {
@Test fun complexTest() {

val f1 = FloatProposition("var1", FloatOp.NEQ, 14.3)
val f2 = FloatProposition("var2", FloatOp.LT, -15.3)
Expand All @@ -29,111 +29,111 @@ class UntilNormalFormTest {
)
}

Test fun nestingNoPropositions() {
@Test fun nestingNoPropositions() {
val prop = EF( p1 implies AX( EG(p2) EU AG(p1)))
assertEquals(
True EU (not(p1) or not( EX( not( (not( True AU not(p2))) EU (not( True EU not(p1))) )))),
normalizer.normalize(prop)
)
}

Test fun nestingPreserve() {
@Test fun nestingPreserve() {
val prop = (p1 and EX(not(p2))) EU ( not(p3) AU (p4 or p2))
assertEquals(prop, normalizer.normalize(prop))
}

//trivial cases

Test fun equivChange() {
@Test fun equivChange() {
val prop = p1 equal p2
val norm = normalizer.normalize(prop)
assertEquals( (p1 and p2) or (not(p1) and not(p2)), norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun implChange() {
@Test fun implChange() {
val prop = p1 implies p2
val norm = normalizer.normalize(prop)
assertEquals(not(p1) or p2, norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun agChange() {
@Test fun agChange() {
val prop = AG(p1)
val norm = normalizer.normalize(prop)
assertEquals(not( True EU not(p1) ), norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun egChange() {
@Test fun egChange() {
val prop = EG(p1)
val norm = normalizer.normalize(prop)
assertEquals(not( True AU not(p1) ), norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun afChange() {
@Test fun afChange() {
val prop = AF(p1)
val norm = normalizer.normalize(prop)
assertEquals(True AU p1, norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun efChange() {
@Test fun efChange() {
val prop = EF(p1)
val norm = normalizer.normalize(prop)
assertEquals(True EU p1, norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun axChange() {
@Test fun axChange() {
val prop = AX(p1)
val norm = normalizer.normalize(prop)
assertEquals(not( EX( not(p1) ) ), norm)
assertEquals(norm, normalizer.normalize(norm))
}

Test fun auPreserve() {
@Test fun auPreserve() {
val prop = p1 AU p2
assertEquals(prop, normalizer.normalize(prop))
}

Test fun euPreserve() {
@Test fun euPreserve() {
val prop = p1 EU p2
assertEquals(prop, normalizer.normalize(prop))
}

Test fun orPreserve() {
@Test fun orPreserve() {
val prop = p1 or p2
assertEquals(prop, normalizer.normalize(prop))
}

Test fun andPreserve() {
@Test fun andPreserve() {
val prop = p1 and p2
assertEquals(prop, normalizer.normalize(prop))
}

Test fun negPreserve() {
@Test fun negPreserve() {
val prop = not(p1)
assertEquals(prop, normalizer.normalize(prop))
}

Test fun exPreserve() {
@Test fun exPreserve() {
val prop = EX(p1)
assertEquals(prop, normalizer.normalize(prop))
}

Test fun floatPreserve() {
@Test fun floatPreserve() {
val prop = FloatProposition("val", FloatOp.GT_EQ, 32.2)
assertEquals(prop, normalizer.normalize(prop))
}

Test fun booleanPreserve() {
@Test fun booleanPreserve() {
assertEquals(True, normalizer.normalize(True))
assertEquals(False, normalizer.normalize(False))
}

Test fun directionPreserve() {
@Test fun directionPreserve() {
val prop = DirectionProposition("var", Direction.IN, Facet.POSITIVE)
assertEquals(prop, normalizer.normalize(prop))
}
Expand Down
Loading

0 comments on commit 6c57f5f

Please sign in to comment.