コンポーネント
コンポーネントは、Lilo のシステムを階層的な構成要素として組織化するための仕組みです。
次のように構成された Vehicle システムを考えてみましょう:
VehicleはPowerUnitとBatteryをコンポーネントとして持ちます。- バッテリーは2つの
BatteryCellから構成されます。 PowerUnit、Battery、BatteryCell、Vehicleの各システムは、それぞれ独自のシグナル、パラメータ、仕様を持ちます。
BatteryCell と PowerUnit はコンポーネントを持たないため、次のように単純に宣言できます:
// BatteryCell.lilo
system BatteryCell
pub signal voltage: Float
pub signal temperature: Float
pub param nominal_voltage: Float
pub def over_voltage: Bool = voltage > nominal_voltage * 1.15
spec voltage_range = voltage >= 2.5 && voltage <= 4.5
// PowerUnit.lilo
system PowerUnit
pub signal temperature: Float
pub signal output: Float
pub param max_output: Float
pub def is_overheating: Bool = temperature > 85.0
spec output_bounded = output <= max_output
ここで pub キーワードは、これらの signal、param、def が、これらのシステムをコンポーネントとしてインスタンス化する他のシステムからアクセス可能であることを示します。spec で宣言された仕様は常に公開されます。
コンポーネントのインスタンス化
Battery システムは BatteryCell コンポーネントを使用します。これは component キーワードを使って宣言できます:
// Battery.lilo
system Battery
pub signal level: Float
pub signal voltage: Float
pub param capacity: Float
component cell1: BatteryCell
// ...
リフトされるシグナル・パラメータとマップされるシグナル・パラメータ
あるシステムが別のシステムのコンポーネントとしてインスタンス化されると、そのパラメータとシグナルは親システムへリフトされます。したがって、Battery のスキーマには level、voltage、capacity に加えて、cell1::voltage、cell1::temperature、cell1::nominal_voltage が含まれます。
コンポーネントのシグナルやパラメータの一部はマップされることがあります。これは、それらが入力スキーマの一部ではなく、その値が(親システムの)他のシグナルやパラメータによって決定されることを意味します。例えば次の例では、Battery のスキーマには依然として cell1::voltage、cell1::temperature、cell1::nominal_voltage、および cell2::temperature が現れますが、cell2::nominal_voltage や cell2::voltage は現れません。cell2::nominal_voltage の値は 3.7 に固定され、cell2::voltage の値は Battery の voltage シグナルから導出されます:
// Unmapped component - all signals and params will be lifted
component cell1: BatteryCell
// Partially mapped component - voltage is mapped, temperature is lifted
component cell2: BatteryCell {
param nominal_voltage = 3.7
signal voltage = voltage / 2.0 // Derived from battery voltage
}
コンポーネントのシグナルとパラメータへのアクセス
システム内の Lilo 式では、:: 演算子を使ってコンポーネントのシグナルやパラメータを参照できます:
// Use cell component signals
pub def any_cell_over_voltage: Bool = cell1::over_voltage || cell2::over_voltage
spec level_valid = level >= 0.0 && level <= 100.0
// Reference cell component specs
spec cells_safe = cell1::voltage_range && cell2::voltage_range
システムは、そのコンポーネントが持つコンポーネントのシグナルやパラメータも参照できます。例えば、Battery コンポーネントと PowerUnit コンポーネントの両方を持つ Vehicle システムを考えます。Vehicle システムでは、次のように仕様を記述できます:
// Vehicle.lilo
// ...
// Two-level signal references
def low_battery: Bool = battery::level < 20.0
def power_hot: Bool = power::temperature > 80.0
def bat_cell1_voltage: Float = battery::cell1::voltage
def at_meihan: Bool = 34.63 < gps.lat < 34.65 && 135.99 < gps.lon < 136.01
// Three-level signal references (Vehicle -> Battery -> BatteryCell)
def cell1_overheated: Bool = battery::cell1::temperature > 65.0
def cell2_voltage_ok: Bool = battery::cell2::voltage > 3.0
// Two-level def references
def battery_or_power_issue: Bool = battery::is_low || power::is_overheating
// Three-level def references (Vehicle -> Battery -> BatteryCell)
def any_cell_overvoltage: Bool = battery::cell1::over_voltage || battery::cell2::over_voltage
// Combined two-level and three-level
def critical_state: Bool = battery::is_low && battery::any_cell_over_voltage
// ...
システムスキーマ
システムのスキーマとは、そのシステムの入力を構成するシグナルとパラメータの集合を指します。モニタリングを行う際、ユーザーはスキーマの各要素に対して値を与えます。Vehicle システムに対応するスキーマを下図に示します:
システムのスキーマは、SpecForge CLI の schema コマンドで確認できます。マップされたシグナルやパラメータは、その値が別のシグナルやパラメータから導出されるため、スキーマには現れないことに注意してください:
$ schema --project /Users/agnishom/code/reqeng/api/examples/projects/vehicle -s Vehicle flat
Signals:
ambient_temp Float
battery::cell1::temperature Float
battery::cell1::voltage Float
battery::cell2::temperature Float
battery::level Float
battery::voltage Float
gps_lat Float
gps_lon Float
power::output Float
speed Float
Params:
battery::capacity Float
battery::cell1::nominal_voltage Float
temp_threshold Float (default: 75.0)
schema コマンドは --diff オプションを付けて実行することで、Lilo システムのスキーマをパラメータファイルやデータファイルと比較できます。このコマンドは、ファイル内で不足しているシグナル・パラメータや余分なシグナル・パラメータ、および型の不一致を報告します:
$ specforge schema --system Vehicle --only signals --diff --datafile vehicle_data.json
Signal Diff Summary:
2 missing, 1 mismatched, 1 expected-scalars, 2 extra
Missing Fields:
battery::voltage
battery::cell2::temperature
Mismatched Types:
speed expected Float but got String
Expected Scalars but Found Records Instead:
ambient_temp
Extra Fields:
ambient_temp.value
battery.cell2.temperture (did you mean battery::cell2::temperature?)
モニタリング時にスキーマへ値を与える際の形式の詳細については、データファイルのドキュメントを参照してください。