module stylesheet1

sig Para, Style {}
abstract sig Property {values: set Value}

abstract sig Value {}
static sig Same extends Value {}
sig Real extends Value {}

sig Doc {
  paras: set Para,
  styles: set Style,
  based: styles ->? styles,
  declared, actual: (styles -> Property) ->? Value,
  style: paras ->? styles
  } {
  all s: styles, p: Property |
    s.actual [p] = 
      if s.declared [p] in Same then s.based.actual [p] else s.declared [p]
  }

pred DocDetails (d: Doc) {
  -- all these in response to invariant checking
  all s: d.styles | no s.(d.based) => s.(d.declared) [Property] in Real
  acyclic (d.based)
  all p: d.paras | some p.(d.style)
  all s: d.styles, p: Property | some s.(d.declared)[p]
  }

pred RealProps (d: Doc) {
  -- all paragraph properties have real values
  all x: Property, p: d.paras | some d.actual[d.style[p]][x] & Real
--  all x: Property, p: d.paras | some d::Actual (p, x) & Real
  }

-- assert DocOK {all d: Doc | DocDetails (d) => RealProps (d)}
-- check DocOK for 3 but 1 Doc

pred delete1 (d, d': Doc, s: Style) {
  d'.paras = d.paras
  d'.styles = d.styles - s
  d'.based = d.based - s->Style - Style->s
  d'.declared = d.declared - s->Property->Value
  d'.style = d.style - Para->s
  }

pred delete2 (d, d': Doc, s: Style) {
  d'.paras = d.paras
  d'.styles = d.styles - s
  d'.based = d.based - s->Style - Style->s
  d'.declared = (d.declared - s->Property->Value) ++
    {t: s.~(d.based), x: Property, v: Value |
        v = if d.declared [t][x] in Same then d.actual [t][x] else d.declared [t][x]}
  d'.style = d.style - Para->s
  }

assert deleteOK {
  all d, d': Doc, s: Style |
    RealProps (d) and DocDetails (d) and delete2 (d, d', s) => RealProps (d')
  }
check deleteOK for 3 but 2 Doc

pred delete2sim (d, d': Doc, s: Style) {
  delete2 (d, d', s)
  s in d.styles
  some Property
  some d.based
  DocDetails (d)
  }

run delete2sim for 3 but 2 Doc
pred acyclic (r: Style -> Style) {no iden & ^r}
--pred acyclic (r: univ -> univ) {no iden & ^r}

/*
history
check inv; fails; say can't have same if not based on
check inv; fails because of cycle; add acyclic
check inv; fails because of para without style; add this
may need to reorder because of nondet etc
check delete1 preserves inv; fails because of same; make delete2
check delete2 preserves inv; fails because can delete a root
*/


fun Doc::Actual (p: Para, x: Property) : Value {
  this.actual [this.style[p]][x]
  }

fun Doc::Declared (s: Style, x: Property) : Value {
  this.declared [s][x]
  }

fun Doc::ActualP (s: Style, x: Property) : Value {
  this.declared [s][x]
  }