-- -- THIS FILE IS AUTOMATICALLY GENERATED!! -- -- Generated at 10-Nov-08 by the UML-VDM++ Link -- class 「制御マシン」 types public 「走行状態」 = <走行中> | <停止中>; instance variables private i走行状態 : 「走行状態」; private i駆動制御 : 「駆動制御」; private iボタン制御 : 「ボタン制御」; private iライン制御 : 「ライン監視制御」; -- テスト用にインスタンスだけ private i光センサー : 「光センサー」; private i右モーター : 「モーター」; private i左モーター : 「モーター」; private i電源ボタン : 「電源ボタン」; operations public 停止する : () ==> () 停止する() == is not yet specified post i走行状態 = <停止中>; public 走行する : () ==> () 走行する() == is not yet specified pre iボタン制御.ボタン状態を得る() = post i走行状態 = <走行中>; public 右ターンする : () ==> () 右ターンする() == is not yet specified pre iライン制御.ライン状態を判定する() = <黒> post i駆動制御.駆動状態を得る() = <右ターン中>; public 左ターンする : () ==> () 左ターンする() == is not yet specified pre iライン制御.ライン状態を判定する() = <白> post i駆動制御.駆動状態を得る() = <左ターン中>; end 「制御マシン」