Skip to content

Commit

Permalink
added cycles and cycle heads to yml witness
Browse files Browse the repository at this point in the history
  • Loading branch information
AdamZsofi committed Feb 16, 2025
1 parent 7936e18 commit adbcd3f
Showing 1 changed file with 29 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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,
Expand Down

0 comments on commit adbcd3f

Please sign in to comment.