\begin{vdm_al}
--
-- 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左モーター : 「モーター」;

operations
  public 「駆動制御」 : () ==> 「駆動制御」
  「駆動制御」() ==
  (
    i右モーター := new 「モーター」();
    i左モーター := new 「モーター」();
  );
  
  public 停止する : () ==> ()
  停止する() ==
  (
    i右モーター.停止する();
    i左モーター.停止する();
    i駆動状態 := <停止中>;
  );

  public 右ターンする : () ==> ()
  右ターンする() ==
  (
    i右モーター.停止する();
    i左モーター.回転する(mk_token(10));
    i駆動状態 := <右ターン中>;
  );

  public 左ターンする : () ==> ()
  左ターンする() ==
  (
    i右モーター.回転する(mk_token(10));
    i左モーター.停止する();
    i駆動状態 := <左ターン中>;
  );
  
  public 駆動状態を得る : () ==> 「駆動状態」
  駆動状態を得る() ==
    return i駆動状態;

end 「駆動制御」
\end{vdm_al}

\begin{rtinfo}
  [「駆動制御」]{vdm.tc}[「駆動制御」]
\end{rtinfo}