module styles_1

sig Para, Style {}
abstract sig Property {}

abstract sig Value {}

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

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

pred show () {}
run show for 3 but 1 Doc, 2 Property

pred WellFormed (d: Doc) {
  acyclic (d.based)
  all s: Style | no s.(d.based) => s.(d.given) [Property] in Real
  }

run WellFormed for 3 but 1 Doc, exactly 2 Property

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

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

pred acyclic (r: Style -> Style) {no iden & ^r}