\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光センサー : 「光センサー」;

operations
  public 「ライン監視制御」 : () ==> 「ライン監視制御」
  「ライン監視制御」() ==
    i光センサー := new 「光センサー」();
  
  public ライン状態を判定する : () ==> 「ライン状態」
  ライン状態を判定する() ==
    cases i光センサー.黒線レベル値を読み取る():
      <黒閾値以下> -> return <黒>,
      <白閾値以上> -> return <白>,
      others -> return <不明>
    end
  pre
    i光センサー.黒線レベル値を読み取る() <> nil
  post
    cases mk_(i光センサー.黒線レベル値を読み取る(), RESULT):
      mk_(<黒閾値以下>, <黒>) -> true,
      mk_(<白閾値以上>, <白>) -> true,
      mk_(-, <不明>) -> true,
      others -> false
    end;

  -- テスト用操作
  public 黒線レベルを値をセットする : 「光センサー」`「黒線レベル値」 ==> ()
  黒線レベルを値をセットする(a黒線レベル値) == i光センサー.黒線レベルを値をセットする(a黒線レベル値);

end 「ライン監視制御」
\end{vdm_al}

\begin{rtinfo}
  [「ライン監視制御」]{vdm.tc}[「ライン監視制御」]
\end{rtinfo}