Reformatted code (#204)

Co-authored-by: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com>
ftsrg · Sep 10, 2023 · d1f33e6 · d1f33e6
1 parent df97782
commit d1f33e6
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 7 deletions.
diff --git a/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt b/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt
@@ -198,7 +198,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
                 if (stack.size >= 2) {
                     val lastButOne = stack[stack.size - 2]
                     val mutexNeverReleased =
-                        last.mutexLocks.containsKey("") && (last.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains(
+                        last.mutexLocks.containsKey(
+                            "") && (last.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains(
                             ""
                         )
                     if (last.node.explored.isEmpty() || mutexNeverReleased) {
@@ -413,10 +414,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
         private fun notdep(start: Int, action: A): List<A> {
             val e = stack[start].action
             return stack.slice(start + 1 until stack.size).filterIndexed { index, item ->
-                    item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent(
-                        e, item.action
-                    )
-                }.map { it.action }.toMutableList().apply { add(action) }
+                item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent(
+                    e, item.action
+                )
+            }.map { it.action }.toMutableList().apply { add(action) }
         }
 
         /**

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt
@@ -306,7 +306,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass {
     private fun isNotLocal(edge: XcfaEdge): Boolean {
         return !edge.getFlatLabels().all { label ->
             !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) &&
-                    !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr)
+                !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr)
         }
     }
 }
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt
@@ -40,6 +40,7 @@ import java.util.*
 class LoopUnrollPass : ProcedurePass {
 
     companion object {
+
         var UNROLL_LIMIT = 50
 
         private val solver: Solver = SolverManager.resolveSolverFactory("Z3").createSolver()
@@ -48,8 +49,11 @@ class LoopUnrollPass : ProcedurePass {
     private val testedLoops = mutableSetOf<Loop>()
 
     private data class Loop(
-        val loopVar: VarDecl<*>, val loopVarModifiers: List<XcfaEdge>, val loopVarInit: XcfaEdge, val loopCondEdge: XcfaEdge, val exitCondEdge: XcfaEdge, val loopStart: XcfaLocation, val loopLocs: List<XcfaLocation>, val loopEdges: List<XcfaEdge>
+        val loopVar: VarDecl<*>, val loopVarModifiers: List<XcfaEdge>, val loopVarInit: XcfaEdge,
+        val loopCondEdge: XcfaEdge, val exitCondEdge: XcfaEdge, val loopStart: XcfaLocation,
+        val loopLocs: List<XcfaLocation>, val loopEdges: List<XcfaEdge>
     ) {
+
         private class BasicStmtAction(private val stmt: Stmt) : StmtAction() {
             constructor(edge: XcfaEdge) : this(edge.label.toStmt())
             constructor(edges: List<XcfaEdge>) : this(SequenceLabel(edges.map { it.label }).toStmt())