Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

システム

最終的に、Liloはシステムを指定するために使用されます。システムは、時系列入力シグナル、(非時系列の)パラメータ、および仕様の宣言をまとめたものです。システムには補助的な定義も含まれます。

システムファイルは、システム宣言で始まる必要があります。例:

system Engine

システムの名前はファイル名と一致する必要があります。

型宣言

新しい型はtypeキーワードで宣言されます。例えば、新しいレコード型Pointを定義するには以下のように記述します:

type Point = { x: Float, y: Float }

その後、ファイル内の他の場所でPointを型として使用できます。

シグナル

システムの時間変化する値はシグナルと呼ばれます。これらはsignalキーワードで宣言されます。例:

signal x: Float
signal y: Float
signal speed: Float
signal rain_sensor: Bool
signal wipers_on: Bool

システムの定義と仕様は、システムのシグナルを自由に参照できます。

シグナルは、関数型を含んでいない任意の型、つまりプリミティブ型とレコードの組み合わせにすることができます。

システムパラメータ

時間的に定数であるシステムの変数はシステムパラメータと呼ばれ、paramキーワードで宣言されます。例:

param temp_threshold: Float
param max_errors: Int

システムの定義と仕様は、システムのパラメータを自由に参照できます。システムパラメータは、監視 (monitoring) を開始する前に事前に提供する必要があることに注意してください。一方で、例示 (exemplification) に際してはシステムパラメータの値は省略できます。つまり、指定された場合、例はそれらに準拠して作成され、指定されなかった場合、例示のプロセスはそのシステムパラメータとして有効な値を見つけようとします。

定義

定義はdefキーワードで宣言されます:

def foo: Int = 42

定義はパラメータに依存することができます:

def foo(x: Float) = x + 42

定義の戻り値の型を指定することもできます:

def foo(x: Float): Float = x + 42

パラメータの型アノテーションと戻り値の型は両方とも省略可能で、指定されなかった場合は推論されます。ただし、これらの型註釈はある種のドキュメントとして常に書いておくことをお勧めします。

定義のパラメータもレコード型にすることができます。例:

type S = { x: Float, y: Float }

def foo(s: S) = eventually [0,1] s.x > s.y

定義は他の定義で使用できます。例:

type S = { x: Float, y: Float }

def more_x_than_y(s: S) = s.x > s.y

def foo(s: S) = eventually [0,1] more_x_than_y(s)

定義は、循環依存を作成しない限り、任意の順序で指定できます。

定義は、パラメータとして宣言することなく、システムの任意のシグナルを自由に使用できます。

仕様

仕様は、システムについて真であるべきことを記述したもので、システムのすべてのsignaldefを参照でき、specキーワードを使用して宣言されます。defによく似ていますが、次の点が異なります:

  • 戻り値の型は常にBoolです(指定する必要はありません)
  • パラメータを持つことはできません。

例:

signal speed: Float

def above_min = 0 <= speed

def below_max = speed <= 100

spec valid_speed =
  always (above_min && below_max)