システム

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

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

system Engine

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

シグナル

システムの時間変化する値はシグナルと呼ばれます。これらは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)

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

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

仕様

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

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

例：

signal speed: Float

def above_min = 0 <= speed

def below_max = speed <= 100

spec valid_speed =
  always (above_min && below_max)

仮定

assumptionは、システムを解析する際に所与のものとして扱われるプロパティを宣言します。構文的にはspecと同様で、パラメータを持たず戻り値の型は常にBoolですが、ツールによる扱いが異なります：仮定は検証対象ではなく、例示や充足可能性チェックの際に制約として自動的に含まれます。

signal temperature: Float
signal heater_on: Bool

assumption physics = always (heater_on => next temperature >= temperature)

spec eventually_warm = eventually (temperature > 30.0)

この例では、SpecForgeがトレース例を生成する際、または仕様の充足可能性をチェックする際に、physicsは必ず成り立たなければなりません。仮定と解析の相互作用の詳細については、例示と充足可能性を参照してください。

Keyboard shortcuts

SpecForge ユーザーガイド

システム

型宣言

シグナル

システムパラメータ

定義

仕様

仮定