Door weak bisimulation
Two labeled transition systems connected by an animated weak-bisimulation relation.
specification
visible behavior
implementation
extra internal states
opened
closed
τ
opened
τ
closed
closed
open
closed
opening
open
closing