26 lines
623 B
Text
26 lines
623 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 ;
|
||
sampling_period: Duration ;
|
||
data : [ Temperature ] ;
|
||
}
|
||
|
||
trait Sensor = {
|
||
get_status : {} -> SensorStatus ;
|
||
set_sampling_period : Duration -> (Ok | OutOfRange);
|
||
pop_data_chunk : {} -> DataChunk ;
|
||
}
|