// A weaker version of InterleavedResponse
property InterleavedResponseWeak
  // vertex names: w = got writer; W = used writer; similarly for s, S
  message "Incompatible methods for putting data into a response were used."
  prefix "javax.servlet.ServletResponse"
  nondet (start)
  start -> start: *
  start -> w: W = getWriter(R)
  start -> s: S = getOutputStream(R)
  w -> sw: S = getOutputStream(r)
  s -> sw: W = getWriter(r)
  w -> W: *(w)
  sw -> sW: *(w)
  s -> S: *(s)
  sw -> Sw: *(s)
  W -> sW: S = getOutputStream(r)
  S -> Sw: W = getWriter(r)
  sW -> error: *(s)
  Sw -> error: *(w)