\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ボタン制御 : 「ボタン制御」;
  private iライン制御 : 「ライン監視制御」;

operations
  public 「制御マシン」 : () ==> 「制御マシン」
  「制御マシン」() ==
  (
    i走行状態 := <停止中>;
    
    i駆動制御 := new 「駆動制御」();
    iボタン制御 := new 「ボタン制御」();
    iライン制御 := new 「ライン監視制御」();
    
    return self;
  );
  
  public 停止する : () ==> ()
  停止する() ==
  (
    i駆動制御.停止する();
    i走行状態 := <停止中>;
  )
    post i走行状態 = <停止中>;

  public 走行する : () ==> ()
  走行する() ==
  (
    cases iライン制御.ライン状態を判定する():
      <黒> -> 右ターンする(),
      <白> -> 左ターンする(),
      others -> skip
    end;
    
    i走行状態 := <走行中>;
  )
    pre iボタン制御.ボタン状態を得る() = <ON>
    post i走行状態 = <走行中>;

  public 右ターンする : () ==> ()
  右ターンする() ==
    i駆動制御.右ターンする()
    pre iライン制御.ライン状態を判定する() = <黒>
    post i駆動制御.駆動状態を得る() = <右ターン中>;

  public 左ターンする : () ==> ()
  左ターンする() ==
    i駆動制御.左ターンする()
    pre iライン制御.ライン状態を判定する() = <白>
    post i駆動制御.駆動状態を得る() = <左ターン中>;


  -- テスト用操作
  public 走行状態を得る : () ==> 「走行状態」
  走行状態を得る() ==
    return i走行状態;
  
  public 進行方向を得る : () ==> 「駆動制御」`「駆動状態」
  進行方向を得る() ==
    return i駆動制御.駆動状態を得る();
  
  public 黒線レベルを値をセットする : 「光センサー」`「黒線レベル値」 ==> ()
  黒線レベルを値をセットする(a黒線レベル値) ==
    iライン制御.黒線レベルを値をセットする(a黒線レベル値);
  
  public 電源ボタンを押す : () ==> ()
  電源ボタンを押す() ==
    iボタン制御.電源ボタンを押す();
  
end 「制御マシン」
\end{vdm_al}

\begin{rtinfo}
  [「制御マシン」]{vdm.tc}[「制御マシン」]
\end{rtinfo}