Feature/javafx

exec/src/main/kotlin/edu/kit/iti/formal/automation/Kastel.kt

@@ -111,7 +111,7 @@ object KastelDemonstrator {
 object AssignmentDScratch : STCodeTransformation, AstMutableVisitor() {
     override fun transform(stBody: StatementList): StatementList = stBody.accept(this) as StatementList
     override fun visit(assignmentStatement: AssignmentStatement): Statement {
-        if ((assignmentStatement.location as SymbolicReference).identifier == "dScratch") {
+        if (assignmentStatement.location.identifier == "dScratch") {
             return StatementList()
         }
         return assignmentStatement
@@ -322,7 +322,7 @@ object SeqParamsActiveStep : CodeTransformation, AstMutableVisitor() {
                 if (sub.identifier == "Sequence" && sub.sub?.identifier == "iActStep") {
                     return SymbolicReference("ActStep", symbolicReference.sub)
                 }
-            } catch (e: ClassCastException) {
+            } catch (_: ClassCastException) {
 
             }
         }
@@ -361,7 +361,7 @@ object RemoveVSObj : STCodeTransformation, AstMutableVisitor() {
     override fun transform(stBody: StatementList) = stBody.accept(this) as StatementList
 
     override fun visit(assignmentStatement: AssignmentStatement): Statement {
-        val ident = (assignmentStatement.location as SymbolicReference).identifier
+        val ident = assignmentStatement.location.identifier
         return if (ident == "VSObj_McFaultDescription")
             return StatementList()
         else assignmentStatement

geteta/src/main/antlr/TestTableLanguageLexer.g4

@@ -17,6 +17,8 @@ public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
 public boolean relational = false;
 }
 
+CONTRACT: 'contract';
+AUTOMATON: 'automaton';
 TCONST: 'timeconst';
 INHERIT_FROM:'\\inherit_from';
 DOT:'.';

geteta/src/main/antlr/TestTableLanguageParser.g4

@@ -21,7 +21,8 @@ public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
 }
 
 //structure level
-file  : table* EOF;
+file  : (ca | table)* EOF;
+
 table : tableHeader LBRACE
             (inheritance_signature)*
             (signature | freeVariable | column | decl_time_const)*
@@ -31,6 +32,41 @@ table : tableHeader LBRACE
          RBRACE
 ;
 
+ca: CONTRACT AUTOMATON name=IDENTIFIER
+    LBRACE
+    (inheritance_signature)*
+    (signature | freeVariable | column | decl_time_const)*
+    opts?
+    contract*
+    state*
+    function*
+    RBRACE
+;
+
+state:
+  STATE LBRACE contract* RBRACE
+;
+
+contract: CONTRACT
+  ( name=intOrId
+  | LBRACE
+    ( ASSUME (EQUALS|COLON) valuesOrFormula
+    | ASSERT (EQUALS|COLON) valuesOrFormula
+    )
+    goto_*
+    RBRACE
+  )
+;
+
+valuesOrFormula:
+    expr
+  | LBRACE
+    (kc osem)*
+    RBRACE
+;
+
+
+
 tableHeader:
                {relational=false;} TABLE name=IDENTIFIER                     #tableHeaderFunctional
   | RELATIONAL {relational=true; } TABLE name=IDENTIFIER LPAREN

geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/monitor.kt

@@ -10,6 +10,7 @@ import edu.kit.iti.formal.automation.testtables.model.ConstraintVariable
 import edu.kit.iti.formal.automation.testtables.monitor.*
 import edu.kit.iti.formal.util.info
 import java.io.File
+import java.util.*
 
 /**
  *
@@ -39,7 +40,7 @@ class MonitorApp : CliktCommand(name = "ttmonitor",
 
     val format by option("--format", "-f", help = "code format, possible values: " +
             CodeOutput.entries.joinToString(",") { it.name })
-            .convert { CodeOutput.valueOf(it.toUpperCase()) }
+            .convert { CodeOutput.valueOf(it.uppercase(Locale.getDefault())) }
             .default(CodeOutput.CPP)
 
     val disableCombinedMonitor by option("--disable-combined",

geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/print.kt

@@ -14,6 +14,7 @@ import edu.kit.iti.formal.automation.testtables.print.LatexTablePrinter
 import edu.kit.iti.formal.automation.testtables.print.TextTablePrinter
 import edu.kit.iti.formal.util.CodeWriter
 import java.io.OutputStreamWriter
+import java.util.*
 
 /**
  *
@@ -29,7 +30,7 @@ class PrinterApp : CliktCommand(name="ttprint", help = "generate print files for
     enum class Format { HTML, LATEX, TEXT }
 
     val format by option("-f", "--format")
-            .convert { Format.valueOf(it.toUpperCase()) }
+            .convert { Format.valueOf(it.uppercase(Locale.getDefault())) }
             .default(Format.LATEX)
 
     val output by option("--output",

geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/synthesis.kt

@@ -29,6 +29,8 @@ import org.antlr.v4.runtime.CharStreams
 import org.antlr.v4.runtime.CommonTokenStream
 import java.io.File
 import java.nio.file.Paths
+import java.util.*
+import kotlin.collections.HashMap
 import kotlin.math.max
 
 /**
@@ -65,7 +67,7 @@ class SynthesisApp : CliktCommand(
 
     private val outputFunctionStrategy by option("--row-selection-strategy",
             help = "Strategy for choosing output function when multiple rows are active")
-            .choice(enumValues<OutputFunctionStrategy>().associateBy { it.name.toLowerCase() })
+            .choice(enumValues<OutputFunctionStrategy>().associateBy { it.name.lowercase(Locale.getDefault()) })
             .default(OutputFunctionStrategy.ASSUME_ORTHOGONAL)
 
     override fun run() {
@@ -881,11 +883,11 @@ class ExpressionSynthesizer(private val pythonExecutable: String = "python") {
                 "${ctx.identifier().accept(this)} = ${ctx.expr().accept(this)}"
 
         override fun visitExpr(ctx: IteLanguageParser.ExprContext): String =
-                ctx.iteExpr()?.accept(this)
-                        ?: ctx.expr()?.let { "(not ${it.accept(this)})" }
-                        ?: ctx.identifier()?.accept(this)
-                        ?: ctx.BOOLEAN()?.text?.toLowerCase()
-                        ?: ctx.INTEGER()!!.text
+            ctx.iteExpr()?.accept(this)
+                ?: ctx.expr()?.let { "(not ${it.accept(this)})" }
+                ?: ctx.identifier()?.accept(this)
+                ?: ctx.BOOLEAN()?.text?.lowercase(Locale.getDefault())
+                ?: ctx.INTEGER()!!.text
 
         override fun visitIteExpr(ctx: IteLanguageParser.IteExprContext): String =
                 iteExprCache.getOrPut(

geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/builder/miter.kt

@@ -31,6 +31,9 @@ import edu.kit.iti.formal.util.CodeWriter
 import edu.kit.iti.formal.util.meta
 import java.io.File
 import java.io.PrintWriter
+import java.util.*
+import kotlin.collections.ArrayList
+import kotlin.collections.HashMap
 import kotlin.math.abs
 
 data class ReactiveProgram(
@@ -52,7 +55,7 @@ private fun createNext(t: Transition): SMVExpr {
     } else {
 
         val inputExpr = (t.from as RowState).row.inputExpr.values.conjunction(SLiteral.TRUE)
-        val outputExpr = (t.from as RowState).row.outputExpr.values.conjunction(SLiteral.TRUE)
+        val outputExpr = t.from.row.outputExpr.values.conjunction(SLiteral.TRUE)
 
         when (t.type) {
             TransitionType.ACCEPT ->
@@ -152,7 +155,7 @@ class GttMiterConstruction(val gtt: GeneralizedTestTable,
                 .or(SVariable(err.name, SMVTypes.BOOLEAN).not())
         target.body.add("__INV__" assignTo invAssign.translateToSt())
         val assert = SpecialCommentFactory
-                .createAssert(SymbolicReference("__INV__"));
+                .createAssert(SymbolicReference("__INV__"))
         target.body.add(assert)
     }
 
@@ -255,19 +258,20 @@ class ProgMiterConstruction(val exec: PouExecutable) {
                 is EnumerationTypeDeclaration -> {
                     td.allowedValues.forEachIndexed { i, value ->
                         val vd = VariableDeclaration(
-                                "${td.name}__${value.text.toUpperCase()}",
+                            "${td.name}__${value.text.uppercase()}",
                                 VariableDeclaration.CONSTANT,
                                 SimpleTypeDeclaration(INT, IntegerLit(i)))
                         target.scope.topLevel.add(vd)
                     }
 
-                    val fdecl = FunctionDeclaration("nondet_${td.name.toLowerCase()}",
+                    val fdecl = FunctionDeclaration(
+                        "nondet_${td.name.lowercase()}",
                             returnType = RefTo(INT))
                     fdecl.scope.add(VariableDeclaration("x", VariableDeclaration.LOCAL, INT))
                     fdecl.stBody = StatementList().also {
                         val x = SymbolicReference("x")
-                        val assume = td.values.map {
-                            x eq IntegerLit(INT, it.toBigInteger())
+                        val assume = td.values.map { int ->
+                            x eq IntegerLit(INT, int.toBigInteger())
                         }.disjunction()
                         it.add(SpecialCommentFactory.createHavoc("x", INT))
                         it.add(SpecialCommentFactory.createAssume(assume))
@@ -307,8 +311,8 @@ class ExpressionConversion(val enumValues: EnumValueTable) : SMVAstVisitor<Expre
             is SMVTypes.BOOLEAN -> BooleanLit(l.value == true)
             is SMVWordType -> IntegerLit(INT, l.value.toString().toBigInteger())
             is EnumType -> {
-                val et = enumValues[l.value.toString().toUpperCase()]
-                        ?: error("No enum defined which contains ${l.value}. Defined values: ${enumValues.keys}")
+                val et = enumValues[l.value.toString().uppercase(Locale.getDefault())]
+                    ?: error("No enum defined which contains ${l.value}. Defined values: ${enumValues.keys}")
                 EnumLit(et, l.value.toString())
             }
             else -> error("Literals of type '${l.javaClass} are not supported")
@@ -391,7 +395,11 @@ class InvocationBasedProductProgramBuilder(name: String = "main") {
     }
 
     private fun createInstance(p: ReactiveProgram, fbd: FunctionBlockDeclaration): VariableDeclaration {
-        val vd = VariableDeclaration(p.name.toLowerCase(), VariableDeclaration.LOCAL, FunctionBlockDataType(fbd))
+        val vd = VariableDeclaration(
+            p.name.lowercase(Locale.getDefault()),
+            VariableDeclaration.LOCAL,
+            FunctionBlockDataType(fbd)
+        )
         target.scope.add(vd)
         return vd
 

geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/exception/SpecificationInterfaceMisMatchException.kt

@@ -68,7 +68,7 @@ class SpecificationInterfaceMisMatchException : GetetaException {
             var computed: MutableMap<String, Int> = HashMap()
 
             init {
-                this.reference = name.toLowerCase()
+                this.reference = name.lowercase(Locale.getDefault())
             }
 
 
@@ -79,8 +79,13 @@ class SpecificationInterfaceMisMatchException : GetetaException {
             }
 
             private fun getLevenstheinToRef(o1: String): Int {
-                val k = o1.toLowerCase()
-                return (computed as java.util.Map<String, Int>).computeIfAbsent(k) { s -> levenshteinDistance(reference, s) }
+                val k = o1.lowercase(Locale.getDefault())
+                return (computed as java.util.Map<String, Int>).computeIfAbsent(k) { s ->
+                    levenshteinDistance(
+                        reference,
+                        s
+                    )
+                }
             }
 
             /**

geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/io/TblLanguageToSmv.kt

@@ -194,7 +194,7 @@ class TblLanguageToSmv(private val columnVariable: SVariable,
             if (isReference)
                 throw IllegalExpressionException("You referenced a variable $varText, " +
                         "but it is not found as a defined program variable.")
-            SEnumLiteral(varText.toUpperCase())
+            SEnumLiteral(varText.uppercase(Locale.getDefault()))
         }
     }