It was used in my college Discrete Math class (a version specifically aimed at Computer Science students) as an exercise in formally proving the properties of a real-life system. That was a fun lecture :-D