module context sig Style { replaces, parents: set Style } fact ReplacesProps { -- fun ReplacesProps () { Equivalence (Style$replaces) Acyclic (Style$parents) all x: Style { x.replaces.parents.replaces = x.parents all y,z: x.parents | y in z.replaces } } sig State { context: set Style, ancestors: Style -> Style } fact DefineAncestors { all s: State, x: Style | s.ancestors [x] = x.*parents & s.context } fun show () { some s: State | some x, y: Style { x in y.replaces x in s.context y !in s.context -- some x.parents } } run show for 3 fun forest (s: State) { all x: s.context | some root: s.ancestors[x] { no root.parents all y: s.ancestors[x] - root | one y.parents & s.context } all x: Style | sole x.replaces & s.context } fun increment (s, s': State, style: Style) { all x: style.^parents | some x.replaces & s.context s'.context = s.context - style.replaces + style } run increment for 3 assert PreserveForest { all s,s': State, z: Style | forest (s) && increment (s,s',z) => forest (s') } check PreserveForest for 4 fun forest' (s: State) { some root: s.context { no root.parents all y: s.context - root | one y.parents & s.context } all x: Style | sole x.replaces & s.context } assert Same {all s: State | forest(s) iff forest'(s)} check Same for 3 fun Equivalence [t] (r: t -> t) { iden[t->t] in r -- reflexive r.r in r -- transitive ~r = r -- symmetric } fun Acyclic [t] (r: t -> t) {no x: t | x in x.^r}