26 lines
591 B
Text
26 lines
591 B
Text
|
|
|||
|
|
trait SensorStatus = {
|
|||
|
|
name : [ Char ] ;
|
|||
|
|
online_since : TimePoint ;
|
|||
|
|
battery_charge : Energy ;
|
|||
|
|
battery_capacity : Energy ;
|
|||
|
|
min_sampling_period : Duration ;
|
|||
|
|
cur_sampling_period : Duration ;
|
|||
|
|
max_chunk_size : ℤ ;
|
|||
|
|
cur_chunk_size : ℤ ;
|
|||
|
|
n_chunk_capacity : ℤ ;
|
|||
|
|
n_full_data_chunks : ℤ ;
|
|||
|
|
n_empty_data_chunks : ℤ ;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
trait DataChunk = {
|
|||
|
|
begin : TimePoint ;
|
|||
|
|
data : [ Temperature ] ;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
trait Sensor = {
|
|||
|
|
get_status : {} -> SensorStatus ;
|
|||
|
|
set_sampling_period : Duration -> (Ok | OutOfRange);
|
|||
|
|
pop_data_chunk : {} -> DataChunk ;
|
|||
|
|
}
|