diff --git a/.idea/compiler.xml b/.idea/compiler.xml index 782b34134..e632420f5 100644 --- a/.idea/compiler.xml +++ b/.idea/compiler.xml @@ -4,7 +4,7 @@ - + diff --git a/.idea/misc.xml b/.idea/misc.xml index 84640d6f3..9c9cdbfc0 100644 --- a/.idea/misc.xml +++ b/.idea/misc.xml @@ -7,7 +7,7 @@ - + - + \ No newline at end of file diff --git a/exec/src/main/kotlin/edu/kit/iti/formal/automation/Kastel.kt b/exec/src/main/kotlin/edu/kit/iti/formal/automation/Kastel.kt index 603d068db..1e4757a8b 100644 --- a/exec/src/main/kotlin/edu/kit/iti/formal/automation/Kastel.kt +++ b/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 diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/monitor.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/monitor.kt index 341bb75c7..262b92ad7 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/monitor.kt +++ b/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", diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/print.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/print.kt index 336e33b08..07b508944 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/print.kt +++ b/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", diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/synthesis.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/synthesis.kt index fed3625cf..1e05edc13 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/apps/synthesis.kt +++ b/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().associateBy { it.name.toLowerCase() }) + .choice(enumValues().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( diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/builder/miter.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/builder/miter.kt index 23df40a0e..53bae9b76 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/builder/miter.kt +++ b/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 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 diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/exception/SpecificationInterfaceMisMatchException.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/exception/SpecificationInterfaceMisMatchException.kt index 54cf5980e..495133ddc 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/exception/SpecificationInterfaceMisMatchException.kt +++ b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/exception/SpecificationInterfaceMisMatchException.kt @@ -68,7 +68,7 @@ class SpecificationInterfaceMisMatchException : GetetaException { var computed: MutableMap = 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).computeIfAbsent(k) { s -> levenshteinDistance(reference, s) } + val k = o1.lowercase(Locale.getDefault()) + return (computed as java.util.Map).computeIfAbsent(k) { s -> + levenshteinDistance( + reference, + s + ) + } } /** diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/io/TblLanguageToSmv.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/io/TblLanguageToSmv.kt index 1080de794..22d9b7b65 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/io/TblLanguageToSmv.kt +++ b/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())) } } diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/model/GeneralizedTestTable.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/model/GeneralizedTestTable.kt index b5f922e1c..22f9ed229 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/model/GeneralizedTestTable.kt +++ b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/model/GeneralizedTestTable.kt @@ -6,7 +6,6 @@ import edu.kit.iti.formal.automation.st.Identifiable import edu.kit.iti.formal.automation.st.LookupList import edu.kit.iti.formal.automation.st.ast.FunctionDeclaration import edu.kit.iti.formal.automation.testtables.GetetaFacade -import edu.kit.iti.formal.automation.testtables.grammar.IteLanguageParser.ExprContext import edu.kit.iti.formal.automation.testtables.grammar.TestTableLanguageParser import edu.kit.iti.formal.automation.testtables.grammar.TestTableLanguageParserBaseVisitor import edu.kit.iti.formal.automation.testtables.model.options.TableOptions @@ -16,6 +15,8 @@ import edu.kit.iti.formal.smv.VariableReplacer import edu.kit.iti.formal.smv.ast.SMVExpr import edu.kit.iti.formal.smv.ast.SVariable import java.util.* +import kotlin.collections.ArrayList +import kotlin.collections.HashMap import kotlin.math.abs import kotlin.math.min @@ -27,10 +28,10 @@ sealed class Variable : Identifiable { abstract var dataType: AnyDt abstract var logicType: SMVType - open fun externalVariable(programRunNames: List, tableName: String): SVariable = - internalVariable(programRunNames).inModule(tableName) as SVariable + open fun externalVariable(programRunNames: List, tableName: String) :SVariable + = internalVariable(programRunNames).inModule(tableName) as SVariable - open fun internalVariable(programRunNames: List): SVariable = SVariable(name, logicType) + open fun internalVariable(programRunNames: List):SVariable = SVariable(name, logicType) } abstract class ColumnVariable(open var category: ColumnCategory = ColumnCategory.ASSUME) : Variable() { @@ -57,8 +58,7 @@ data class ProgramVariable( override var category: ColumnCategory = ColumnCategory.ASSUME, var isState: Boolean = false, var isNext: Boolean = false, - var programRun: Int = 0 -) : ColumnVariable(category) { + var programRun: Int = 0) : ColumnVariable(category) { override val humanCategory: String get() { @@ -88,24 +88,23 @@ data class ProgramVariable( /** * */ - override fun internalVariable(programRunNames: List): SVariable = - SVariable("${programRunNames[programRun]}$realName", logicType) + override fun internalVariable(programRunNames: List): SVariable = SVariable("${programRunNames[programRun]}$realName", logicType) } data class ConstraintVariable( override var name: String, override var dataType: AnyDt, override var logicType: SMVType, - var constraint: TestTableLanguageParser.CellContext? = null -) : Variable() + var constraint: TestTableLanguageParser.CellContext? = null) + : Variable() data class ProjectionVariable( override var name: String, override var dataType: AnyDt, override var logicType: SMVType, override var category: ColumnCategory = ColumnCategory.ASSUME, - var constraint: MutableList = arrayListOf() -) : ColumnVariable(category) { + var constraint: MutableList = arrayListOf()) + : ColumnVariable(category) { val arity: Int get() = constraint.size @@ -145,8 +144,7 @@ class ParseContext( val vars: MutableMap = hashMapOf(), val refs: MutableMap = hashMapOf(), val functions: MutableMap = hashMapOf(), - val fillers: MutableMap = hashMapOf() -) { + val fillers: MutableMap = hashMapOf()) { fun isVariable(v: String) = v in this fun getSMVVariable(v: Variable) = @@ -174,10 +172,8 @@ class ParseContext( val va = if (programRun != null) vars.keys.find { it.name == v && (it as? ProgramVariable)?.programRun == programRun } - ?: throw IllegalArgumentException( - "Could not find a variable for $programRun|>$v in signature. " + - "Signature is ${vars.keys.joinToString { it.name }}" - ) + ?: throw IllegalArgumentException("Could not find a variable for $programRun|>$v in signature. " + + "Signature is ${vars.keys.joinToString { it.name }}") else vars.keys.find { it.name == v } ?: throw IllegalArgumentException("Could not find a variable for $v in signature.") @@ -282,7 +278,7 @@ class GeneralizedTestTable( val maxProgramRun: Int get() = programVariables .filterIsInstance(ProgramVariable::class.java) - .map { it.programRun }.maxByOrNull { it } ?: 0 + .map { it.programRun }.maxBy { it } ?: 0 fun getProgramVariables(name: String, run: Int?): ColumnVariable { val pv = programVariables.find { it.respondTo(name, run) } @@ -307,105 +303,6 @@ class GeneralizedTestTable( fun isConstraintVariable(variable: String): Boolean = constraintVariables.any { it.name == variable } } -class ContractAutomata( - var name: String = "anonym", - val programVariables: MutableList = ArrayList(), - val constraintVariables: MutableList = ArrayList(), - var properties: MutableMap = HashMap(), - var states: MutableList = ArrayList(), - val functions: LookupList = ArrayLookupList(), -// var programRuns: List = arrayListOf() -) { - val options: TableOptions by lazy { - TableOptions(properties) - } - - fun add(v: ColumnVariable) { - programVariables += v - } - - fun add(v: ConstraintVariable) = { - constraintVariables += v - } - - fun addOption(key: String, value: String) { - properties[key] = value - } - - val DEFAULT_CELL_CONTENT = "-" - - fun generateSmvExpression(): ParseContext { - states.forEach { s -> s.contracts.forEach { c -> c.generateSmvExpression(parseContext) } } - return parseContext - } - - val parseContext: ParseContext by lazy { - val vc = ParseContext(options.relational, 1) - constraintVariables.forEach { - vc.getSMVVariable(it) - } - programVariables.forEach { - vc.getSMVVariable(it) - vc.fillers[it] = GetetaFacade.parseCell(DEFAULT_CELL_CONTENT).cell() - } - - functions.forEach { fd -> - vc.functions[fd.name] = GetetaFacade.functionToSmv(fd) - } - - vc - } - val maxProgramRun: Int - get() = programVariables - .filterIsInstance(ProgramVariable::class.java) - .map { it.programRun }.maxByOrNull { it } ?: 0 - - fun getProgramVariables(name: String, run: Int?): ColumnVariable { - val pv = programVariables.find { it.respondTo(name, run) } - return pv ?: throw IllegalStateException("Could not find variable: $run|>$name.") - } - - fun getTableRow(rowId: String) = region.flat().find { it.id == rowId } - fun isProgramVariable(variable: String): Boolean = programVariables.any { it.name == variable } - fun isConstraintVariable(variable: String): Boolean = constraintVariables.any { it.name == variable } -} - -data class ContractAutomataStates( - var id: String, - var contracts: ArrayList = arrayListOf(), - var gotos: MutableList = arrayListOf() -) - -interface ContractAutomataContract { - var id: String - val assume: SMVExpr? - val assert: SMVExpr? - fun generateSmvExpression(ctx: ParseContext) -} - -class AssumeAssertContract( - override var id: String, val rawAssume: ExprContext, val rawAssert: ExprContext -) : ContractAutomataContract { - override var assume: SMVExpr? = null - override var assert: SMVExpr? = null - - override fun generateSmvExpression(ctx: ParseContext) { - TODO("Not yet implemented") - } -} - -class FieldwiseContract(override var id: String) : ContractAutomataContract { - val rawFields: MutableMap = linkedMapOf() - override var assume: SMVExpr? = null - override var assert: SMVExpr? = null - - override fun generateSmvExpression(ctx: ParseContext) { - TODO("Not yet implemented") - } - -} - - operator fun Iterable.get(text: String) = find { it.name == text } operator fun Iterable.contains(text: String) = this[text] != null @@ -449,8 +346,7 @@ sealed class Duration { get() = true } - data class OpenInterval(val lower: Int, override var modifier: DurationModifier = DurationModifier.NONE) : - Duration() { + data class OpenInterval(val lower: Int, override var modifier: DurationModifier = DurationModifier.NONE) : Duration() { override fun contains(cycles: Int): Boolean = lower <= cycles override val isUnbounded: Boolean @@ -463,11 +359,7 @@ sealed class Duration { get() = true } - data class ClosedInterval( - val lower: Int, - val upper: Int, - override var modifier: DurationModifier = DurationModifier.NONE - ) : Duration() { + data class ClosedInterval(val lower: Int, val upper: Int, override var modifier: DurationModifier = DurationModifier.NONE) : Duration() { override fun contains(cycles: Int): Boolean = cycles in lower..upper override val isUnbounded: Boolean @@ -542,10 +434,8 @@ sealed class TableNode(open var id: String, var duration: Duration = Duration.Cl abstract fun visit(visitor: (TableNode) -> Unit) } -data class Region( - override var id: String, - var children: MutableList = arrayListOf() -) : TableNode(id) { +data class Region(override var id: String, + var children: MutableList = arrayListOf()) : TableNode(id) { constructor(id: Int) : this("$id") override fun count(): Int = this.children.sumBy { it.count() } diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cmonitor.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cmonitor.kt index 125ba8b69..c18039856 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cmonitor.kt +++ b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cmonitor.kt @@ -34,8 +34,8 @@ private class CMonitorGeneratorImpl(val gtt: GeneralizedTestTable, val automaton val monitor = Monitor() val stream = StringWriter() val writer = CodeWriter(stream) - val state_t = "state_${gtt.name.toLowerCase()}_t" - val inout_t = "inout_${gtt.name.toLowerCase()}_t" + val state_t = "state_${gtt.name.lowercase(Locale.getDefault())}_t" + val inout_t = "inout_${gtt.name.lowercase(Locale.getDefault())}_t" val userReset = "FORCE_RST" val error = "ERROR" diff --git a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cppmonitor.kt b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cppmonitor.kt index 4266613a3..71c6aff5a 100644 --- a/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cppmonitor.kt +++ b/geteta/src/main/kotlin/edu/kit/iti/formal/automation/testtables/monitor/cppmonitor.kt @@ -19,6 +19,7 @@ import edu.kit.iti.formal.util.CodeWriter import edu.kit.iti.formal.util.error import edu.kit.iti.formal.util.joinInto import edu.kit.iti.formal.util.warn +import java.util.* val EMPTY_COLUMN = SVariable("ERROR", SMVTypes.BOOLEAN) @@ -435,7 +436,7 @@ class CppCombinedMonitorGenerationImpl( } private val Monitor.instanceName: String - get() = "_" + this.name.toLowerCase() + get() = "_" + this.name.lowercase(Locale.getDefault()) } private fun CodeWriter.historyValuesDeclaration(gtt: GeneralizedTestTable) { diff --git a/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/fx.kt b/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/fx.kt index e861ebc86..02e47eb7e 100644 --- a/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/fx.kt +++ b/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/fx.kt @@ -3,11 +3,13 @@ package edu.kit.iti.formal.automation.fx import edu.kit.iti.formal.util.info import javafx.beans.property.SimpleObjectProperty import javafx.collections.FXCollections -import javafx.event.ActionEvent import javafx.event.EventHandler import javafx.geometry.Side import javafx.scene.Node -import javafx.scene.control.* +import javafx.scene.control.Menu +import javafx.scene.control.MenuItem +import javafx.scene.control.Tab +import javafx.scene.control.TabPane import javafx.scene.input.KeyCombination import javafx.scene.paint.Color import javafx.scene.text.FontWeight @@ -18,14 +20,13 @@ import tornadofx.* import java.io.File import java.nio.file.Files import java.nio.file.Paths -import java.util.* fun main(args: Array) { launch(*args) } -class IdeStyle : tornadofx.Stylesheet() { +class IdeStyle : Stylesheet() { companion object { val styleTextArea by cssclass("styled-text-area") val text by cssclass() @@ -215,7 +216,7 @@ class IdeView : View("VERIFAPS IDE") { //if (appData.lastNavigatorPath.value != null) // fileNavigator.rootFile.value = Paths.get(appData.lastNavigatorPath.value) subscribe { publishMessage(it.text, it.graphic) } - open(File("../geteta/examples/NewFile.gtt").absoluteFile) + open(File("geteta/examples/NewFile.gtt").absoluteFile) } fun publishMessage(status: String, graphic: Node? = null) { diff --git a/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/navigator.kt b/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/navigator.kt index 8e39bfff0..7fd118e0f 100644 --- a/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/navigator.kt +++ b/ide/src/main/kotlin/edu/kit/iti/formal/automation/fx/navigator.kt @@ -13,13 +13,14 @@ import org.kordamp.ikonli.javafx.FontIcon import org.kordamp.ikonli.javafx.IkonResolver import tornadofx.View import tornadofx.contextmenu -import tornadofx.item as titem import tornadofx.separator import java.awt.Desktop import java.io.IOException import java.nio.file.Files import java.nio.file.Path import java.nio.file.Paths +import kotlin.io.path.name +import tornadofx.item as titem /** * @@ -166,6 +167,10 @@ fun ContextMenu.item(name: String, key: String? = null, ikon: String? = null, ev } class SimpleFileTreeItem(f: Path) : TreeItem(f) { + private val pathComparator: Comparator> = java.util.Comparator.comparingInt?> { + if (Files.isDirectory(it.value)) 0 else 1 + }.thenComparing { it -> it.value.name } + private var isFirstTimeChildren = true private var isFirstTimeLeaf = true private var isLeaf = false @@ -194,7 +199,7 @@ class SimpleFileTreeItem(f: Path) : TreeItem(f) { Files.list(f).forEach { children.add(SimpleFileTreeItem(it)) } - return children + return children.sorted(pathComparator) } return FXCollections.emptyObservableList() } diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/RewriteEnums.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/RewriteEnums.kt index 1cc7d2b2a..9af38e0c3 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/RewriteEnums.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/RewriteEnums.kt @@ -7,6 +7,7 @@ import edu.kit.iti.formal.automation.st.ast.Expression import edu.kit.iti.formal.automation.st.ast.Literal import edu.kit.iti.formal.automation.st.ast.SymbolicReference import edu.kit.iti.formal.automation.st.util.AstMutableVisitor +import java.util.* object RewriteEnums : AstMutableVisitor() { private var lastScope: Scope? = null @@ -18,7 +19,7 @@ object RewriteEnums : AstMutableVisitor() { override fun visit(literal: Literal): Expression { when (literal) { - is EnumLit -> literal.value = literal.value.toUpperCase() + is EnumLit -> literal.value = literal.value.uppercase(Locale.getDefault()) else -> {} } return literal @@ -30,11 +31,11 @@ object RewriteEnums : AstMutableVisitor() { val value = symbolicReference.identifier if (scope.resolveVariable(symbolicReference) == null) { val enum0 = scope.resolveEnumByValue(value) - if (enum0 != null) return EnumLit(RefTo(enum0), value.toUpperCase()) + if (enum0 != null) return EnumLit(RefTo(enum0), value.uppercase(Locale.getDefault())) val enum1 = scope.resolveEnum(value) if (enum1 != null && symbolicReference.hasSub()) - return EnumLit(RefTo(enum1), symbolicReference.sub!!.identifier.toUpperCase()) + return EnumLit(RefTo(enum1), symbolicReference.sub!!.identifier.uppercase(Locale.getDefault())) } } return symbolicReference diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/checks.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/checks.kt index ce8c7c27b..50bdd508a 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/checks.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/analysis/checks.kt @@ -13,6 +13,8 @@ import edu.kit.iti.formal.automation.st.util.AstVisitorWithScope import edu.kit.iti.formal.util.dlevenshtein import org.antlr.v4.runtime.Token import java.lang.Throwable +import java.util.* +import kotlin.collections.ArrayList import kotlin.math.ceil import kotlin.math.log @@ -23,7 +25,7 @@ fun getCheckers(reporter: Reporter) = listOf(CheckForTypes(reporter), CheckForLi * Percentage of changed characters. */ fun variableSimilarity(expected: String, defined: String): Double = - dlevenshtein(expected.toLowerCase(), defined.toLowerCase()).toDouble() / expected.length + dlevenshtein(expected.lowercase(Locale.getDefault()), defined.lowercase(Locale.getDefault())).toDouble() / expected.length fun Iterable.similarCandidates(reference: String, threshold: Double = .9) = this.map { it to variableSimilarity(reference, it) } diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/dt.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/dt.kt index f5614b2f6..ceb6813ec 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/dt.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/dt.kt @@ -17,7 +17,7 @@ import kotlin.math.ln sealed class AnyDt(override var name: String = "ANY") : Identifiable { constructor() : this("") { - name = javaClass.getSimpleName().toUpperCase() + name = javaClass.getSimpleName().uppercase(Locale.getDefault()) } abstract fun repr(obj: Any): String @@ -66,7 +66,7 @@ open class AnyNum : AnyDt("ANY_NUM") { abstract class AnyReal : AnyNum() { override fun repr(obj: Any): String { val d = obj as BigDecimal - return name.toUpperCase() + "#" + d + return name.uppercase(Locale.getDefault()) + "#" + d } override fun accept(visitor: DataTypeVisitorNN) = visitor.visit(this) @@ -102,7 +102,7 @@ abstract class AnyBit(var bitLength: Int = 0) : AnyDt() { override fun repr(obj: Any): String { if (obj is Bits) if (obj.register > 0) - return (name.toUpperCase() + "#2#" + java.lang.Long.toBinaryString(obj.register)) + return (name.uppercase(Locale.getDefault()) + "#2#" + java.lang.Long.toBinaryString(obj.register)) return "" } @@ -329,7 +329,7 @@ abstract class IECString : AnyDt() { val pattern = Pattern.compile("[\$]([\"'NLRTnlrt]|[0-9]{$bytes})") val m = pattern.matcher(str) while (m.find()) { - val replacement = when (m.group(1).toUpperCase()) { + val replacement = when (m.group(1).uppercase(Locale.getDefault())) { "$" -> "$" "'" -> "'" "\"" -> "\"" @@ -393,8 +393,10 @@ class EnumerateType(name: String = "ENUM", return ceil(ln(allowedValues.size.toDouble())).toInt() } - constructor(name: String, allowedValues: MutableList, - defValue: String = allowedValues[0]) : this(name) { + constructor( + name: String, allowedValues: MutableList, + defValue: String = allowedValues[0] + ) : this(name) { allowedValues.forEachIndexed { index, s -> this.allowedValues[s] = index } this.defValue = defValue } @@ -402,9 +404,9 @@ class EnumerateType(name: String = "ENUM", constructor(etd: EnumerationTypeDeclaration) : this() { name = etd.name etd.allowedValues.zip(etd.values).forEach { (a, b) -> - allowedValues.put(a.text!!.toUpperCase(), b) + allowedValues.put(a.text!!.uppercase(Locale.getDefault()), b) } - defValue = etd.allowedValues[0].text.toUpperCase() + defValue = etd.allowedValues[0].text.uppercase(Locale.getDefault()) } override fun repr(obj: Any): String { @@ -414,7 +416,7 @@ class EnumerateType(name: String = "ENUM", override fun accept(visitor: DataTypeVisitorNN) = visitor.visit(this) fun isAllowedValue(value: String) = this.allowedValues.contains(value) - operator fun contains(textValue: String) = textValue.toUpperCase() in allowedValues + operator fun contains(textValue: String) = textValue.uppercase(Locale.getDefault()) in allowedValues override fun toString(): String = "ENUM $name" @@ -452,7 +454,7 @@ class EnumerateType(name: String = "ENUM", open class AnyInt(var bitLength: kotlin.Int = 0, var isSigned: Boolean = false) : AnyNum() { init { - name = javaClass.getSimpleName().toUpperCase() + name = javaClass.getSimpleName().uppercase(Locale.getDefault()) } open val upperBound: BigInteger @@ -474,7 +476,7 @@ open class AnyInt(var bitLength: kotlin.Int = 0, var isSigned: Boolean = false) override fun repr(obj: Any): String { - return javaClass.getSimpleName().toUpperCase() + "#" + obj + return javaClass.getSimpleName().uppercase(Locale.getDefault()) + "#" + obj } open fun next(): AnyInt? = null diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/values/Value.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/values/Value.kt index 3858493fb..107f41317 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/values/Value.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/datatypes/values/Value.kt @@ -26,6 +26,7 @@ import edu.kit.iti.formal.automation.datatypes.* import edu.kit.iti.formal.automation.st.ast.* import java.math.BigDecimal import java.math.BigInteger +import java.util.* /** * Created by weigl on 11.06.14. @@ -111,7 +112,7 @@ class VTimeOfDay(dt: AnyDate.TIME_OF_DAY, v: TimeofDayData) : Value(dt, v.toUpperCase()) { +class VAnyEnum(dt: EnumerateType, v: String) : Value(dt, v.uppercase(Locale.getDefault())) { override fun assignTo(ref: SymbolicReference) = StatementList(ref assignTo EnumLit(dataType, value)) } diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/experimental/java.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/experimental/java.kt index 491352d71..7be6ef396 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/experimental/java.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/experimental/java.kt @@ -12,6 +12,7 @@ import edu.kit.iti.formal.automation.st.util.AstVisitor import edu.kit.iti.formal.automation.st.util.AstVisitorWithScope import edu.kit.iti.formal.util.CodeWriter import java.io.StringWriter +import java.util.* /** * @@ -159,7 +160,7 @@ class JavaExportVisitor(val packageName: String, val rootClass: String) { override fun visit(enumerationTypeDeclaration: EnumerationTypeDeclaration) { cw.nl().cblock("public enum ${enumerationTypeDeclaration.name} {", "}") { val v = enumerationTypeDeclaration.allowedValues - .joinToString(", ", "", ";") { it.text.toUpperCase() } + .joinToString(", ", "", ";") { it.text.uppercase(Locale.getDefault()) } cw.write(v) } cw.nl() @@ -264,7 +265,7 @@ class JavaExportVisitor(val packageName: String, val rootClass: String) { } override fun visit(enumeration: CaseCondition.Enumeration) { - val n = (enumeration.start).value.toUpperCase() + val n = (enumeration.start).value.uppercase(Locale.getDefault()) cw.nl().write("case $n:") } @@ -390,7 +391,7 @@ class JavaExportVisitor(val packageName: String, val rootClass: String) { a.milliseconds.toString() } is EnumLit -> { - literal.dataType.identifier!! + "." + literal.value.toUpperCase() + literal.dataType.identifier!! + "." + literal.value.uppercase(Locale.getDefault()) } else -> td?.toString() ?: "" } diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/operators/Operators.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/operators/Operators.kt index 33db20b2c..a30664bab 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/operators/Operators.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/operators/Operators.kt @@ -24,6 +24,7 @@ package edu.kit.iti.formal.automation.operators import edu.kit.iti.formal.automation.datatypes.AnyBit import edu.kit.iti.formal.automation.datatypes.AnyNum +import java.util.* /** * Facade. @@ -82,10 +83,10 @@ object Operators { } fun lookup(operator: String): Operator { - if (operator.toUpperCase() !in TABLE) { + if (operator.uppercase(Locale.getDefault()) !in TABLE) { throw IllegalArgumentException("Operator $operator is not defined") } - return TABLE[operator.toUpperCase()]!! + return TABLE[operator.uppercase(Locale.getDefault())]!! } fun register(op: Operator) = register(op.symbol, op) diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/scope/Scope.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/scope/Scope.kt index 24916c683..4da767d51 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/scope/Scope.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/scope/Scope.kt @@ -189,8 +189,11 @@ data class Scope(val variables: VariableScope = VariableScope()) fun resolveFunctionBlock(key: String) = functionBlocks.lookup(key) fun resolveFunction(key: String) = functions.lookup(key) - fun registerProgram(programDeclaration: ProgramDeclaration) = programs.register(programDeclaration.name!!, programDeclaration) - fun registerFunction(functionDeclaration: FunctionDeclaration) = functions.register(functionDeclaration.name, functionDeclaration) + fun registerProgram(programDeclaration: ProgramDeclaration) = + programs.register(programDeclaration.name!!, programDeclaration) + + fun registerFunction(functionDeclaration: FunctionDeclaration) = + functions.register(functionDeclaration.name, functionDeclaration) fun registerFunctionBlock(fblock: FunctionBlockDeclaration) = functionBlocks.register(fblock.name, fblock) @@ -200,8 +203,8 @@ data class Scope(val variables: VariableScope = VariableScope()) if (dt is EnumerationTypeDeclaration) { val edt = dt.getDataType(this) dt.allowedValues - .map { it.text!! } - .forEach { allowedEnumValues[it.toUpperCase()] = edt } + .map { it.text!! } + .forEach { allowedEnumValues[it.uppercase(Locale.getDefault())] = edt } } } @@ -218,8 +221,8 @@ data class Scope(val variables: VariableScope = VariableScope()) //if (a && b || a && c || b && c) { val ambigue = arrayListOf(a, b, c, d) - .map { if (it != null) 1 else 0 } - .sum() > 1 + .map { if (it != null) 1 else 0 } + .sum() > 1 if (ambigue) { System.err.println("Ambiguity in Name Resolution for: $name") @@ -269,11 +272,11 @@ data class Scope(val variables: VariableScope = VariableScope()) fun registerClass(clazz: ClassDeclaration) = - classes.register(clazz.name, clazz) + classes.register(clazz.name, clazz) fun resolveClass(key: String) = classes.lookup(key) fun registerInterface(interfaceDeclaration: InterfaceDeclaration) = - interfaces.register(interfaceDeclaration.name, interfaceDeclaration) + interfaces.register(interfaceDeclaration.name, interfaceDeclaration) fun registerMethod(md: MethodDeclaration) = methods.register(md.name, md) fun resolveInterface(key: String) = interfaces.lookup(key) @@ -338,9 +341,9 @@ data class Scope(val variables: VariableScope = VariableScope()) } fun resolveEnumByValue(value: String): EnumerateType? = - value.toUpperCase().let { - this.allowedEnumValues[it] ?: parent?.resolveEnumByValue(it) - } + value.uppercase(Locale.getDefault()).let { + this.allowedEnumValues[it] ?: parent?.resolveEnumByValue(it) + } /** * Construct a complete map of values to EnumerationType @@ -354,11 +357,11 @@ data class Scope(val variables: VariableScope = VariableScope()) //region call resolver fun resolveInvocation(callee: SymbolicReference): Invoked? { val resolvers = listOf( - this::resolveProgramInvocation, - this::resolveActionInvocation, - this::resolveFunctionBlockInvocation, - this::resolveFunctionInvocation - //, this::resolveMethodInvocation + this::resolveProgramInvocation, + this::resolveActionInvocation, + this::resolveFunctionBlockInvocation, + this::resolveFunctionInvocation + //, this::resolveMethodInvocation ) val resolved = resolvers.map { it(callee) }.filter { it != null } diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/HccPrinter.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/HccPrinter.kt index b49dbdeca..533f1aa20 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/HccPrinter.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/HccPrinter.kt @@ -10,6 +10,7 @@ import edu.kit.iti.formal.automation.st.ast.* import edu.kit.iti.formal.util.CodeWriter import edu.kit.iti.formal.util.joinInto import edu.kit.iti.formal.util.meta +import java.util.* open class HccPrinter(sb: CodeWriter = CodeWriter(), noPreamble: Boolean = false) : StructuredTextPrinter(sb) { init { @@ -169,7 +170,7 @@ open class HccPrinter(sb: CodeWriter = CodeWriter(), noPreamble: Boolean = false val returnType = functionDeclaration.returnType.identifier if (!(returnType == null || returnType.isEmpty())) - sb.printf(returnType.toLowerCase()).printf(" ${functionDeclaration.name}( ") + sb.printf(returnType.lowercase(Locale.getDefault())).printf(" ${functionDeclaration.name}( ") functionDeclaration.scope.variables.filter { it.isInput || it.isInOut }.forEachIndexed { i, it -> if (i != 0) { sb.printf(", ") @@ -245,7 +246,7 @@ open class HccPrinter(sb: CodeWriter = CodeWriter(), noPreamble: Boolean = false } else if (simpleTypeDeclaration.baseType.obj is UINT) { sb.printf("unsigned int") } else { - sb.printf(simpleTypeDeclaration.baseType.identifier!!.toLowerCase()) + sb.printf(simpleTypeDeclaration.baseType.identifier!!.lowercase(Locale.getDefault())) } @@ -274,7 +275,7 @@ open class HccPrinter(sb: CodeWriter = CodeWriter(), noPreamble: Boolean = false } is SpecialCommentMeta.HavocComment -> { sb.nl() - val haveocName = "nondet_${meta.dataType.name.toLowerCase()}();" + val haveocName = "nondet_${meta.dataType.name.lowercase(Locale.getDefault())}();" //sb.printf(" ").printf(haveocName).printf(" = _;").nl() //uninitialised Var sb.printf(meta.variable).printf(" = ").printf(haveocName) } diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/StructuredTextPrinter.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/StructuredTextPrinter.kt index bd6ec8f4c..8bfee2df9 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/StructuredTextPrinter.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/StructuredTextPrinter.kt @@ -227,7 +227,7 @@ open class StructuredTextPrinter(var sb: CodeWriter = CodeWriter()) : AstVisitor val QUOTED_IDENTIFIER = listOf("STEP", "END_STEP", "TRANSITION", "END_TRANSITION", "INITIAL_STEP", "FROM") private fun quoteIdentifier(identifier: String): String { - return if (identifier.toUpperCase() in QUOTED_IDENTIFIER) { + return if (identifier.uppercase(Locale.getDefault()) in QUOTED_IDENTIFIER) { "`$identifier`" } else { identifier @@ -587,37 +587,44 @@ open class StructuredTextPrinter(var sb: CodeWriter = CodeWriter()) : AstVisitor fun print(prefix: Any?, suffix: Any) = (if (prefix != null) "$prefix#" else "") + suffix - sb.printf(when (literal) { - is IntegerLit -> print(literal.dataType.obj?.name, literal.value.abs()) - is RealLit -> print(literal.dataType.obj?.name, literal.value.abs()) - is EnumLit -> print(literal.dataType.obj?.name, literal.value) - is ToDLit -> { - val (h, m, s, ms) = literal.value - print(literal.dataType().name, "$h:$m:$s.$ms") - } - is DateLit -> { - val (y, m, d) = literal.value - print(literal.dataType().name, "$y-$m-$d") - } - is DateAndTimeLit -> { - val (y, mo, d) = literal.value.date - val (h, m, s, ms) = literal.value.tod - print(literal.dataType().name, "$y-$mo-$d-$h:$m:$s.$ms") - } - is StringLit -> { - if (literal.dataType() is IECString.WSTRING) "\"${literal.value}\"" - else "'${literal.value}'" - } - is NullLit -> "null" - is TimeLit -> { - print(literal.dataType().name, "${literal.value.milliseconds}ms") - } - is BooleanLit -> literal.value.toString().toUpperCase() - is BitLit -> { - print(literal.dataType.obj?.name, "2#" + literal.value.toString(2)) - } - is UnindentifiedLit -> literal.value - }) + sb.printf( + when (literal) { + is IntegerLit -> print(literal.dataType.obj?.name, literal.value.abs()) + is RealLit -> print(literal.dataType.obj?.name, literal.value.abs()) + is EnumLit -> print(literal.dataType.obj?.name, literal.value) + is ToDLit -> { + val (h, m, s, ms) = literal.value + print(literal.dataType().name, "$h:$m:$s.$ms") + } + + is DateLit -> { + val (y, m, d) = literal.value + print(literal.dataType().name, "$y-$m-$d") + } + + is DateAndTimeLit -> { + val (y, mo, d) = literal.value.date + val (h, m, s, ms) = literal.value.tod + print(literal.dataType().name, "$y-$mo-$d-$h:$m:$s.$ms") + } + + is StringLit -> { + if (literal.dataType() is IECString.WSTRING) "\"${literal.value}\"" + else "'${literal.value}'" + } + + is NullLit -> "null" + is TimeLit -> { + print(literal.dataType().name, "${literal.value.milliseconds}ms") + } + + is BooleanLit -> literal.value.toString().uppercase(Locale.getDefault()) + is BitLit -> { + print(literal.dataType.obj?.name, "2#" + literal.value.toString(2)) + } + + is UnindentifiedLit -> literal.value + }) } override fun visit(arrayinit: ArrayInitialization) { diff --git a/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/TranslationSfcToStPipeline.kt b/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/TranslationSfcToStPipeline.kt index f2793d8cc..52ab0ed7d 100644 --- a/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/TranslationSfcToStPipeline.kt +++ b/lang/src/main/kotlin/edu/kit/iti/formal/automation/st/TranslationSfcToStPipeline.kt @@ -12,6 +12,7 @@ import edu.kit.iti.formal.automation.st.ast.BooleanLit.Companion.LTRUE import edu.kit.iti.formal.automation.st.ast.SFCActionQualifier.Qualifier.* import edu.kit.iti.formal.automation.st.util.AstMutableVisitor import org.antlr.v4.runtime.CommonToken +import java.util.* import java.util.concurrent.Callable private val SFCStep.onEntry: String? @@ -518,11 +519,13 @@ object Falling : ActionQualifierHandler(FALLING) { } } -data class PipelineData(val network: SFCNetwork, val name: String, val index: Int, val scope: Scope, - val finalScan: Boolean, val sfcFlags: Boolean, val maxNeededTokens: TokenAmount) { +data class PipelineData( + val network: SFCNetwork, val name: String, val index: Int, val scope: Scope, + val finalScan: Boolean, val sfcFlags: Boolean, val maxNeededTokens: TokenAmount +) { val tokenIsBoundedTo1: Boolean = maxNeededTokens is TokenAmount.Bounded && maxNeededTokens.max == 1 val transitions: Map, List> = network.steps.flatMap { it.outgoing }.distinct() - .sortedByDescending { it.priority }.groupBy { it.from } + .sortedByDescending { it.priority }.groupBy { it.from } val actions: MutableMap = mutableMapOf() val specialResetStatements: StatementList = StatementList() @@ -541,20 +544,20 @@ data class PipelineData(val network: SFCNetwork, val name: String, val index: In val stateName = SymbolicReference(if (index <= 0) "_state" else "_${index}_state") val enumName = - (if (index <= 0) "STATES_$name" else "STATES_$name\$${index}").toUpperCase() + (if (index <= 0) "STATES_$name" else "STATES_$name\$${index}").uppercase(Locale.getDefault()) val stateEnumType = - createEnumerationTypeForSfc(enumName, network, this::enumStepName) + createEnumerationTypeForSfc(enumName, network, this::enumStepName) val stateEnumTypeDeclaration by lazy { val enumType = EnumerationTypeDeclaration(enumName) val et = stateEnumType enumType.addValue(CommonToken(IEC61131Lexer.IDENTIFIER, enumStepName(stepName(et.defValue)))) et.allowedValues - .map { it.key } - .filter { it != et.defValue } - .forEach { - enumType.addValue(CommonToken(IEC61131Lexer.IDENTIFIER, enumStepName(stepName(it)))) - } + .map { it.key } + .filter { it != et.defValue } + .forEach { + enumType.addValue(CommonToken(IEC61131Lexer.IDENTIFIER, enumStepName(stepName(it)))) + } //enumType.initialization = IdentifierInitializer(value = enumStepName(network.initialStep!!.name)) //scope.dataTypes.register(enumName, enumType) //specialResetStatements += enumName.assignTo(enumType.initialization!!.value!!) @@ -577,13 +580,13 @@ data class PipelineData(val network: SFCNetwork, val name: String, val index: In fun enumValue(step: SFCStep) = EnumLit(stateEnumType, enumStepName(stepName(step.name))) fun stepName(stepName: String, idx: Int = index, sfcName: String = name): String = - if (idx <= 0) stepName else "_${idx}_$stepName" + if (idx <= 0) stepName else "_${idx}_$stepName" //0 -> "$sfcName$stepName" //else -> "$sfcName${idx}_$stepName" fun enumStepName(stepName: String) = - if (index <= 0) stepName else "_${index}_$stepName" + if (index <= 0) stepName else "_${index}_$stepName" fun addToScope(name: String, dt: AnyDt, type: Int = 0): VariableDeclaration { return if (!scope.variables.contains(name)) { @@ -594,20 +597,30 @@ data class PipelineData(val network: SFCNetwork, val name: String, val index: In fun addToScope(names: List, dt: AnyDt, type: Int = 0) = names.map { addToScope(it, dt, type) } fun moduleTON(name: String, input: Expression, pt: Expression) { - specialResetStatements += InvocationStatement(SymbolicReference(name), mutableListOf(InvocationParameter("IN", - false, LFALSE), InvocationParameter("PT", false, TimeLit(TimeData())))) + specialResetStatements += InvocationStatement( + SymbolicReference(name), mutableListOf( + InvocationParameter( + "IN", + false, LFALSE + ), InvocationParameter("PT", false, TimeLit(TimeData())) + ) + ) moduleFB(name, "TON", listOf(Pair("IN", input), Pair("PT", pt))) } fun moduleRS(name: String, set: Expression, reset1: Expression) { - specialResetStatements += InvocationStatement(SymbolicReference(name), - mutableListOf(InvocationParameter("R", false, LTRUE))) + specialResetStatements += InvocationStatement( + SymbolicReference(name), + mutableListOf(InvocationParameter("R", false, LTRUE)) + ) moduleFB(name, "RS", listOf(Pair("SET", set), Pair("RESET1", reset1))) } fun moduleTRIG(name: String, clk: Expression, type: String = "R_TRIG") { - specialResetStatements += InvocationStatement(SymbolicReference(name), - mutableListOf(InvocationParameter("CLK", false, LFALSE))) + specialResetStatements += InvocationStatement( + SymbolicReference(name), + mutableListOf(InvocationParameter("CLK", false, LFALSE)) + ) moduleFB(name, type, listOf(Pair("CLK", clk))) } diff --git a/smv/src/main/kotlin/edu/kit/iti/formal/smv/types.kt b/smv/src/main/kotlin/edu/kit/iti/formal/smv/types.kt index 4ad8bfdec..d5bbd044b 100644 --- a/smv/src/main/kotlin/edu/kit/iti/formal/smv/types.kt +++ b/smv/src/main/kotlin/edu/kit/iti/formal/smv/types.kt @@ -27,7 +27,7 @@ data class SMVWordType( override fun valueOf(str: String) = SWordLiteral(read(str), this) override fun read(str: String): BigInteger { - val re = Pattern.compile("(?-)?0(?s|u)d(?\\d+)_(?\\d+)") + val re = Pattern.compile("(?-)?0(?[su])d(?\\d+)_(?\\d+)") val m = re.matcher(str) if (m.matches()) { val word = SMVFacade.parseWordLiteral(str) @@ -82,7 +82,7 @@ object SMVTypes { object BOOLEAN : SMVType { override fun valueOf(str: String) = if (str.equals("true", true)) SLiteral.TRUE else SLiteral.FALSE - override fun format(value: Any): String = value.toString().toUpperCase() + override fun format(value: Any): String = value.toString().uppercase(Locale.getDefault()) override fun read(str: String): Any = str.equals("TRUE", true) override fun repr(): String = "boolean" override fun allowedValue(obj: Any): Boolean = obj is Boolean diff --git a/symbex/src/main/kotlin/edu/kit/iti/formal/automation/cpp/translatecpp.kt b/symbex/src/main/kotlin/edu/kit/iti/formal/automation/cpp/translatecpp.kt index 060ba0409..acdc03149 100644 --- a/symbex/src/main/kotlin/edu/kit/iti/formal/automation/cpp/translatecpp.kt +++ b/symbex/src/main/kotlin/edu/kit/iti/formal/automation/cpp/translatecpp.kt @@ -296,7 +296,12 @@ class TranslateToCpp(val out: CodeWriter) : AstVisitor() { override fun visit(programDeclaration: ProgramDeclaration) { visit(programDeclaration as PouExecutable, programDeclaration.actions) val rt = RecordType(programDeclaration.name, programDeclaration.scope.variables) - out.println("struct ${programDeclaration.name}_t ${programDeclaration.name.toUpperCase()} = ${value(DefaultInitValue.getInit(rt))};") + out.println( + "struct ${programDeclaration.name}_t ${programDeclaration.name.uppercase(Locale.getDefault())} = ${ + value( + DefaultInitValue.getInit(rt) + ) + };") } fun visit(pd: PouExecutable, actions: LookupList) { @@ -483,8 +488,8 @@ fun generateRunnableStub(cw: CodeWriter, main: PouElements) { main.elements.forEach { p -> if (p is ProgramDeclaration) { val inputs = p.scope.filterByFlags(VariableDeclaration.INPUT, VariableDeclaration.INOUT) - inputs.forEach { print("havoc(&${p.name.toUpperCase()}.${it.name});").nl() } - print("${p.name}(& ${p.name.toUpperCase()});").nl() + inputs.forEach { print("havoc(&${p.name.uppercase(Locale.getDefault())}.${it.name});").nl() } + print("${p.name}(& ${p.name.uppercase(Locale.getDefault())});").nl() } } } diff --git a/util/src/main/kotlin/edu/kit/iti/formal/util/CodeWriter.kt b/util/src/main/kotlin/edu/kit/iti/formal/util/CodeWriter.kt index 00b5c0c8e..9f2a554c2 100644 --- a/util/src/main/kotlin/edu/kit/iti/formal/util/CodeWriter.kt +++ b/util/src/main/kotlin/edu/kit/iti/formal/util/CodeWriter.kt @@ -2,6 +2,7 @@ package edu.kit.iti.formal.util import java.io.StringWriter import java.io.Writer +import java.util.* /** * CodeWriter class. @@ -39,7 +40,7 @@ open class CodeWriter(var stream: Writer = StringWriter()) } open fun keyword(keyword: String): CodeWriter { - return printf(if (uppercaseKeywords) keyword.toUpperCase() else keyword.toLowerCase()) + return printf(if (uppercaseKeywords) keyword.uppercase(Locale.getDefault()) else keyword.lowercase(Locale.getDefault())) } fun nl(): CodeWriter { diff --git a/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/IECXMLFacade.kt b/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/IECXMLFacade.kt index 167626a9c..fe4f72471 100644 --- a/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/IECXMLFacade.kt +++ b/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/IECXMLFacade.kt @@ -4,6 +4,7 @@ import edu.kit.iti.formal.util.CodeWriter import java.io.* import java.net.URL import java.nio.file.Path +import java.util.* /** * @author Alexander Weigl @@ -33,7 +34,7 @@ object IECXMLFacade { val SFC_KEYWORDS = setOf("step", "end_step", "transition", "end_transition") fun quoteVariable(name: String): String = - if(name.toLowerCase() in SFC_KEYWORDS) "`$name`" else name + if (name.lowercase(Locale.getDefault()) in SFC_KEYWORDS) "`$name`" else name fun quoteStBody(body: String): String { return body.replace("\\b\\w+\\b".toRegex()) { diff --git a/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/fbdtranslator.kt b/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/fbdtranslator.kt index f080b9c53..ab9f66990 100644 --- a/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/fbdtranslator.kt +++ b/xml/src/main/kotlin/edu/kit/iti/formal/automation/plcopenxml/fbdtranslator.kt @@ -7,25 +7,26 @@ import edu.kit.iti.formal.util.CodeWriter import org.jdom2.Element import org.jdom2.filter.Filters import org.jdom2.xpath.XPathFactory +import java.util.* private val xpathFactory = XPathFactory.instance() internal fun getVariables(block: Element, child: String) = - block.getChild(child)?.children?.map { BlockVariable(it) } ?: listOf() + block.getChild(child)?.children?.map { BlockVariable(it) } ?: listOf() internal fun operatorSymbol(name: String) = - when (name.toLowerCase()) { - "eq" -> " = " - "sub" -> " - " - "add" -> " + " - "div" -> " / " - "mult" -> " * " - "and" -> " AND " - "or" -> " OR " - "xor" -> " ^ " - else -> "/*!! UNKNOWN OP: $name !!*/" - } + when (name.lowercase(Locale.getDefault())) { + "eq" -> " = " + "sub" -> " - " + "add" -> " + " + "div" -> " / " + "mult" -> " * " + "and" -> " AND " + "or" -> " OR " + "xor" -> " ^ " + else -> "/*!! UNKNOWN OP: $name !!*/" + } //TODO: Edges could be negated //TODO: Storage modifier (S=, R=) @@ -145,6 +146,7 @@ class FBDTranslator(val fbd: Element, val writer: CodeWriter) { println("Vendor Elements not supported in FBDs.") null } + else -> throw IllegalStateException("Xml element: ${block.name}") } @@ -204,11 +206,11 @@ sealed class FbdNode(val block: Element, val network: FBDTranslator) { class FbdBlock(e: Element, network: FBDTranslator) : FbdNode(e, network) { val type: String by lazy { block.getAttributeValue("typeName") } val instanceName: String by lazy { - block.getAttributeValue("instanceName") ?: this.type.toLowerCase() + block.getAttributeValue("instanceName") ?: this.type.lowercase(Locale.getDefault()) } val callType: FBDCallType by lazy { - when (type.toLowerCase()) { + when (type.lowercase(Locale.getDefault())) { "mux" -> FBDCallType.FUNCTION "add" -> FBDCallType.OPERATOR else -> { @@ -277,6 +279,7 @@ class FbdBlock(e: Element, network: FBDTranslator) : FbdNode(e, network) { FBDCallType.EXECUTE -> { Execute(executeBody ?: "//NO BODY WAS FOUND!") } + FBDCallType.OPERATOR -> Operator(instanceName) FBDCallType.FUNCTION -> Function(instanceName) FBDCallType.UNKNOWN -> FunctionBlock(instanceName)