package veh.cluster
import veh.common.Speed
import veh.common.Temperature
import veh.common.MAX_SPEED
import veh.common.GearPosition
import veh.common.WarningFlags
// --- vocabulary local to this contract (typl declarations, package level) ---
struct DoorPayload {
sensorId : integer [0..15]
isOpen : boolean
}
struct DiagFilter {
severity : integer [0..5]
category : Label?
}
struct FaultEvent {
code : integer [0..65535]
message : Message
timestamp : Timestamp
}
error enum DiagError { // failure vocabulary — typl §10.1
FILTER_INVALID = 0
STORAGE_BUSY = 1
ACCESS_DENIED = 2
}
struct FaultPage {
faults : [FaultEvent; 0..64]
}
// --- the contract ---
/**
* Main vehicle status interface.
* @labels SIL_B, CAL_2, PRIVATE
*/
interface VehicleStatus {
/// Current vehicle speed — isochronous, drives rmdl clocks downstream
signal currentSpeed : Speed @10ms
/// Engine temperature — change-driven, 100ms freshness SLO
signal engineTemp : Temperature @[20ms..100ms]
/// Active warnings — last-value delivered on subscribe (§4.4)
signal warnings : WarningFlags @[50ms..1s]
/// Raised on every door state change; stale after 500ms
event doorOpened : DoorPayload @[50ms..500ms]
/// Request a gear change — outcome observed via currentGear, not returned
command setGear(position: GearPosition) [
require position != GearPosition.PARK || currentSpeed == 0.0
]
reserved resetCounters // retired ordinal — never reused
/// Sliding-window average
query getAverageSpeed(window: Duration): Speed [
require window > 0ms
ensure result >= 0.0
]
/// Fault history as a finite stream
query streamFaults(filter: DiagFilter): <FaultEvent>
/// Paged fault snapshot — fallible query via inline `T | E` (§10.1)
query getFaultPage(filter: DiagFilter): FaultPage | DiagError
fixed softwareVersion : Version
fixed capabilities : [Label; 0..32]
}