module paper/house

sig House {
   b : option Base,
   w : set Wall,
   r : option Roof
}
{ 
   (some w => one b)
   (some r => #(w & CompleteWall) = 4)
}

fact {
   House$b = ~ Base$h
   House$w = ~ Wall$h
   House$r = ~ Roof$h
}
sig Base { h : House}
sig Roof { h : House}
sig Wall {
   h : House,
   f : option Frame,
   c : option Cladding
}
{  some c => one f}
fact {
   Wall$f = ~ Frame$w
   Wall$c = ~ Cladding$w
}

sig Frame { w : Wall}
sig Cladding { w : Wall}

sig CompleteWall extends Wall {}
fact { CompleteWall = { w : Wall | some w.c} }
sig CompleteHouse extends House {}
fact { CompleteHouse = { h : House | some h.r} }

fun showHouse() { some CompleteHouse}
fun showSome() { some House }
fun showPartial() { some s : House | some w :s.w | some w.f && no w.c }

run showSome for 4
run showHouse for 4
run showPartial for 4