From adbcd3f917e9c8a345f1acc5da1e508b8de2c0fc Mon Sep 17 00:00:00 2001
From: AdamZsofi <adamzsofi.mail@gmail.com>
Date: Sun, 16 Feb 2025 20:37:50 +0100
Subject: [PATCH] added cycles and cycle heads to yml witness

---
 .../theta/xcfa/cli/witnesses/YamlWitness.kt   | 30 ++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
index 7b1a8d3968..6d438821b0 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/YamlWitness.kt
@@ -156,14 +156,33 @@ enum class Language {
  *   a mapping that describes one invariant.
  */
 @Serializable
-data class ContentItem(val segment: Segment? = null, val invariant: Invariant? = null) {
+data class ContentItem(
+  val segment: Segment? = null,
+  val invariant: Invariant? = null,
+  val cycle: Cycle? = null,
+) {
   constructor(wpContent: WaypointContent) : this(listOf(Waypoint(wpContent)))
+
+  constructor(
+    cycleHeadContent: CycleHeadContent,
+    segments: List<WaypointContent>,
+  ) : this(
+    cycle =
+      listOf(CycleItem(CycleHead(cycleHeadContent))) +
+        segments.map { CycleItem(segment = listOf(Waypoint(it))) }
+  )
 }
 
 typealias Segment = List<Waypoint>
 
+typealias Cycle = List<CycleItem>
+
+@Serializable data class CycleItem(val cycleHead: CycleHead? = null, val segment: Segment? = null)
+
 @Serializable data class Waypoint(val waypoint: WaypointContent)
 
+@Serializable data class CycleHead(val chContent: CycleHeadContent)
+
 /**
  * The `waypoint` elements are the basic building block of violation witnesses. They have the form
  * of simple restrictions on program executions. Technically, a waypoint is a mapping with four
@@ -234,6 +253,15 @@ data class WaypointContent(
   val action: Action,
 )
 
+@Serializable
+data class CycleHeadContent(
+  val location: Location,
+  val value: String,
+  val format: String,
+  val invariant: Boolean = false,
+  val inductive: Boolean = false,
+)
+
 @Serializable
 enum class WaypointType {
   @SerialName("assumption") ASSUMPTION,