エレベータの仕様

やっと「エレベータ」の仕様をVDMで記述できました。
とりかかる前は、「たかがエレベータだろ？」と甘く見ていたのだけれど、やってみて、コレがとんでもなく難しく、奥が深いのに気づきました。さすが「形式手法の先生がた」が出しただけのことはあります。誰でも知っているにもかかわらず、難解＆奥が深い「題材」です。
（偶然にも最近ニュースで事件になってて、身近な重要インフラなのに気づかされます）