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 のシステムを階層的な構成要素として組織化するための仕組みです。

次のように構成された Vehicle システムを考えてみましょう:

  • VehiclePowerUnitBattery をコンポーネントとして持ちます。
  • バッテリーは2つの BatteryCell から構成されます。
  • PowerUnitBatteryBatteryCellVehicle の各システムは、それぞれ独自のシグナル、パラメータ、仕様を持ちます。

Vehicleシステムの階層

BatteryCellPowerUnit はコンポーネントを持たないため、次のように単純に宣言できます:

// 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 キーワードは、これらの signalparamdef が、これらのシステムをコンポーネントとしてインスタンス化する他のシステムからアクセス可能であることを示します。spec で宣言された仕様は常に公開されます。

コンポーネントのインスタンス化

Battery システムは BatteryCell コンポーネントを使用します。これは component キーワードを使って宣言できます:

// Battery.lilo

system Battery

pub signal level: Float
pub signal voltage: Float
pub param capacity: Float

component cell1: BatteryCell

// ...

リフトされるシグナル・パラメータとマップされるシグナル・パラメータ

あるシステムが別のシステムのコンポーネントとしてインスタンス化されると、そのパラメータとシグナルは親システムへリフトされます。したがって、Battery のスキーマには levelvoltagecapacity に加えて、cell1::voltagecell1::temperaturecell1::nominal_voltage が含まれます。

コンポーネントのシグナルやパラメータの一部はマップされることがあります。これは、それらが入力スキーマの一部ではなく、その値が(親システムの)他のシグナルやパラメータによって決定されることを意味します。例えば次の例では、Battery のスキーマには依然として cell1::voltagecell1::temperaturecell1::nominal_voltage、および cell2::temperature が現れますが、cell2::nominal_voltagecell2::voltage は現れません。cell2::nominal_voltage の値は 3.7 に固定され、cell2::voltage の値は Batteryvoltage シグナルから導出されます:

// 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 システムに対応するスキーマを下図に示します:

Vehicleシステムのスキーマ

システムのスキーマは、SpecForge CLIschema コマンドで確認できます。マップされたシグナルやパラメータは、その値が別のシグナルやパラメータから導出されるため、スキーマには現れないことに注意してください:

$ 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?)

モニタリング時にスキーマへ値を与える際の形式の詳細については、データファイルのドキュメントを参照してください。