From 0be641cbfdd8694b7d999f75b86fbe0e66a524b2 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 28 Nov 2024 16:06:50 +0100
Subject: [PATCH] Added SBEPass with test

---
 .../hu/bme/mit/theta/xcfa/passes/SBEPass.kt   | 44 +++++++++++++++++++
 .../hu/bme/mit/theta/xcfa/passes/PassTests.kt | 14 ++++++
 2 files changed, 58 insertions(+)
 create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SBEPass.kt

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SBEPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SBEPass.kt
new file mode 100644
index 0000000000..46c717198c
--- /dev/null
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SBEPass.kt
@@ -0,0 +1,44 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.passes
+
+import hu.bme.mit.theta.xcfa.model.*
+
+/**
+ * Transforms all sequence labels to consequtive edges. Requires the ProcedureBuilder be
+ * `deterministic`.
+ */
+class SBEPass() : ProcedurePass {
+
+  override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
+    checkNotNull(builder.metaData["deterministic"])
+    for (edge in ArrayList(builder.getEdges())) {
+      val edges = edge.splitIf(this::predicate)
+      if (
+        edges.size > 1 ||
+          (edges.size == 1 && predicate((edges[0].label as SequenceLabel).labels[0]))
+      ) {
+        builder.removeEdge(edge)
+        edges.forEach { builder.addEdge(it) }
+      }
+    }
+    return builder
+  }
+
+  private fun predicate(it: XcfaLabel): Boolean {
+    return true
+  }
+}
diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt
index f7604eb9dd..b570289418 100644
--- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt
+++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt
@@ -365,6 +365,20 @@ class PassTests {
           input = { ("L1" to "L1") { assume("1 == 1") } },
           output = null,
         ),
+        PassTestData(
+          global = {},
+          passes = listOf(NormalizePass(), DeterministicPass(), SBEPass()),
+          input = {
+            ("L1" to "L2") {
+              assume("1 == 1")
+              assume("2 == 2")
+            }
+          },
+          output = {
+            ("L1" to "loc3") { assume("1 == 1") }
+            ("loc3" to "L2") { assume("2 == 2") }
+          },
+        ),
       )
   }