add initial ldmc variant for random-sensor
This commit is contained in:
parent
cbee09be85
commit
76e3369844
5 changed files with 345 additions and 0 deletions
random-sensor-ldmc
30
random-sensor-ldmc/sensor-internal.lt
Normal file
30
random-sensor-ldmc/sensor-internal.lt
Normal file
|
@ -0,0 +1,30 @@
|
|||
include "../sensor.lt";
|
||||
|
||||
type native.SensorStatus = SensorStatus ~ {
|
||||
online_since : TimePoint ~ <TimeSince UnixEpoch> ~ Milliseconds ~ ℤ ~ native.UInt64 ;
|
||||
battery_charge : Energy ~ mAh ~ native.UInt32 ;
|
||||
battery_capacity : Energy ~ mAh ~ native.UInt32 ;
|
||||
min_sampling_period : Duration ~ Milliseconds ~ native.UInt32 ;
|
||||
cur_sampling_period : Duration ~ Milliseconds ~ native.UInt32 ;
|
||||
max_chunk_size : ℤ ~ native.UInt32 ;
|
||||
cur_chunk_size : ℤ ~ native.UInt32 ;
|
||||
n_chunk_capacity : ℤ ~ native.UInt32 ;
|
||||
n_full_data_chunks : ℤ ~ native.UInt32 ;
|
||||
n_empty_data_chunks : ℤ ~ native.UInt32 ;
|
||||
} ;
|
||||
|
||||
type native.DataChunk = DataChunk ~ {
|
||||
begin : TimePoint ~ <TimeSince UnixEpoch> ~ Milliseconds ~ native.UInt64 ;
|
||||
data : [~<LengthPrefix x86.UInt32>
|
||||
Temperature
|
||||
~ Celsius
|
||||
~ ℝ
|
||||
~ native.Float64
|
||||
] ;
|
||||
} ;
|
||||
|
||||
type native.Sensor = Sensor ~ {
|
||||
get_status : {} -> InternSensorStatus ;
|
||||
set_sampling_period : Duration~Milliseconds~UInt32 -> (Ok | OutOfRange)~Byte ;
|
||||
pop_data_chunk : {} -> InternDataChunk ;
|
||||
} ;
|
Loading…
Add table
Add a link
Reference in a new issue