module stylesheet2

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

-- abstract 
sig Value {}
-- fact {Value in Same + Real}
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,
  override, final: paras -> Property ->? Value
  } {
  all s: styles, p: Property |
    s.actual [p] = 
      if s.declared [p] in Same then s.based.actual [p] else s.declared [p]
   all p: paras | p.final = p.style.actual ++ p.override
  }

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]

  all p: d.paras, x: Property | d.override[p][x] in Real
  }

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

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

pred delete3 (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'.override = d.override
  d'.override = d.override ++
    {p: d.paras, x: Property, v: Value | 
        v = if no d'.style[p] and no d.override[p][x] then d.actual[s][x] else d.override[p][x]}
  d'.style = d.style - Para->s
  }

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

assert deleteChangesNothing {
  all d, d': Doc, s: Style, p: Para |
    RealProps (d) and DocDetails (d) and delete3 (d, d', s) =>
       all x: Property | d'.final [p][x] = d.final [p][x]
  }
check deleteChangesNothing for 3 but 2 Doc

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

run delete3sim 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]
  }