### Profile

 1 ```-- y is true if the property x is true at least n succesive times. ``` ```-- nb_times is a positive integer which increases by 1 each time x is true ``` ```-- and decreases by 1 each time x is false. ``` ```-- the idea was: x is the error output of a sensor and y has been true ``` ```-- if nb_times equals 0 again, perhaps the sensor is fine again ``` ```--@ requires n > 0; ``` ```--@ ensures (not x) => (not y); ``` ```--@ ensures nb_times >= 0; ``` ```--@ ensures not x => ((pre nb_times > nb_times) or (pre nb_times = 0)); ``` ```--@ ensures x => (pre nb_times < nb_times); ``` ```--@ ensures y => nb_times >= n; ``` ```node check_validity (x: bool; n: int) returns (y: bool; nb_times: int); ``` ```var ``` ```compt: int; ``` ```let ``` ``` compt = (if x then 1 else 0) -> if x then pre compt + 1 else 0; ``` ``` y = (compt >= n); ``` ``` nb_times= (if x then 1 else 0) -> ``` ``` if x then pre nb_times + 1 else ``` ``` (if pre nb_times > 0 then pre nb_times - 1 else 0); ``` ```tel ``` ```-- at the beginning, y = x ``` ```-- once x is true, y is true until reset is true ``` ```-- if reset is true, y = x ``` ```--@ ensures reset => y=x; ``` ```--@ ensures x => y; ``` ```--@ ensures pre y and not reset => y; ``` ```node lock (x, reset: bool) returns (y: bool); ``` ```let ``` ```y = x -> if reset then x else x or pre y; ``` ```tel ``` ```-- combination of check_validity and lock ``` ```--@ requires n > 0; ``` ```--@ ensures x => y; ``` ```--@ ensures (pre y and not y) => (not x); ``` ```node check_validity_lock (x: bool; n: int) returns (y: bool); ``` ```var ``` ``` nb_times: int; ``` ``` er: bool; ``` ```let ``` ``` (er, nb_times) = check_validity(x, n); ``` ``` y = x or lock(er, (nb_times = 0)); ``` ```tel ``` ```-- check if the input is not changing too fast ``` ```--@ requires delta > 0.; ``` ```--@ ensures abs_1(v - pre v) <= delta; ``` ```node check_speed (s, delta: real) returns (v: real); ``` ```let ``` ``` v = s -> if s - pre v > delta ``` ``` then ``` ``` pre v + delta ``` ``` else ``` ``` if pre v - s > delta ``` ``` then ``` ``` pre v - delta ``` ``` else s; ``` ```tel ``` ```-- the classic absolute value function ``` ```--@ ensures y >= 0.0; ``` ```--@ ensures (x >= 0.0) => (x = y); ``` ```--@ ensures (x <= 0.0) => (x = -y); ``` ```node abs_1 (x: real) returns (y: real); ``` ```let ``` ``` y= if x>0.0 then x else -x; ``` ```tel ``` ```-- ensures that the ranged_val output is between min and max. ``` ```-- [min , max] is the legal interval where the value must be ``` ```-- [min - delta , max + delta] is the interval the input value is allowed to be ``` ```-- delta can match for instance with the uncertainty of measurement ``` ```-- satmax => value > max ``` ```-- satmin => value < min ``` ```-- "error" occurs if the input value is out of [min - delta, max + delta] ``` ```--@ requires delta > 0.0; ``` ```--@ requires min <= max; ``` ```--@ ensures min <= ranged_val and ranged_val <= max; ``` ```--@ ensures ((min <= value) and (value <= max)) => (ranged_val = value); ``` ```--@ ensures (value < min) => satmin; ``` ```--@ ensures (max < value) => satmax; ``` ```--@ ensures satmin => (value < min); ``` ```--@ ensures satmax => (max <= value); ``` ```--@ ensures value < min => ranged_val = min; ``` ```--@ ensures value > value => ranged_val = max; ``` ```--@ ensures error => satmin or satmax; ``` ```--@ ensures delta + max < value => error; ``` ```--@ ensures value < min - delta => error; ``` ```node ranged_value (value, min, max, delta: real) returns (ranged_val:real; satmin, satmax, error: bool); ``` ```let ``` ``` satmin = value < min; ``` ``` satmax = value > max; ``` ``` error = (value > max + delta) or (value < min - delta); ``` ``` ranged_val = if value > max then max else (if value < min then min else value); ``` ```tel ``` ```-- checks if the node "aberration" has valid outputs ``` ```node obs_aberration(s1,s2,s3,delta: real; ab1,ab2,ab3: bool) ``` ```returns (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool); ``` ```var ``` ``` diff12, diff13, diff23: real; ``` ```let ``` ``` diff12 = abs_1(s1 - s2); ``` ``` diff13 = abs_1(s1 - s3); ``` ``` diff23 = abs_1(s2 - s3); ``` ``` ok_ab1 = (ab1 => (diff12 > delta and diff13 > delta)); ``` ``` ok_ab2 = (ab2 => (diff12 > delta and diff23 > delta)); ``` ``` ok_ab3 = (ab3 => (diff13 > delta and diff23 > delta)); ``` ``` ok_rev1 = ((diff12 > delta and diff13 > delta) => ab1 ); ``` ``` ok_rev2 = ((diff12 > delta and diff23 > delta) => ab2); ``` ``` ok_rev3 = ((diff13 > delta and diff23 > delta) => ab3); ``` ```tel ``` ```-- it checks to make sure that there is no aberrant input value ``` ```-- i.e. here, if there isn't a value which is too remote from the other two. ``` ```-- delta is a safe range ``` ```--@ requires delta > 0.0; ``` ```--@ ensures exists ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool; (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3) = (obs_aberration (s1,s2,s3,delta,ab1,ab2,ab3)); ``` ```node aberration (s1,s2,s3, delta: real) returns (ab1, ab2, ab3: bool); ``` ```var ``` ``` diff12, diff13, diff23: real; ``` ```let ``` ``` diff12 = abs_1(s1 - s2); ``` ``` diff13 = abs_1(s1 - s3); ``` ``` diff23 = abs_1(s2 - s3); ``` ``` ab1 = (diff12 > delta) and (diff13 > delta); ``` ``` ab2 = (diff12 > delta) and (diff23 > delta); ``` ``` ab3 = (diff13 > delta) and (diff23 > delta); ``` ```tel ``` ```--@ ensures (nb_errors = 0) => not (e1 or e2 or e3); ``` ```--@ ensures not (e1 or e2 or e3) => (nb_errors = 0); ``` ```--@ ensures e1 or e2 or e3 => nb_errors >= 1; ``` ```--@ ensures e1 and e2 and e3 => (nb_errors = 3); ``` ```--@ ensures e1 and e2 and not e3 => (nb_errors = 2); ``` ```--@ ensures e1 and not e2 and e3 => (nb_errors = 2); ``` ```--@ ensures not e1 and e2 and e3 => (nb_errors = 2); ``` ```--@ ensures not e1 and not e2 and e3 => (nb_errors = 1); ``` ```--@ ensures not e1 and e2 and not e3 => (nb_errors = 1); ``` ```--@ ensures e1 and not e2 and not e3 => (nb_errors = 1); ``` ```--@ ensures nb_errors = 0 or nb_errors = 1 or nb_errors = 2 or nb_errors =3; ``` ```node nb_err_calc( e1, e2, e3: bool) returns (nb_errors: int); ``` ```let ``` ``` nb_errors = if e1 and e2 and e3 ``` ``` then 3 ``` ``` else if (e1 and e2) or (e2 and e3) or (e1 and e3) ``` ``` then 2 ``` ``` else if e1 or e2 or e3 ``` ``` then 1 ``` ``` else 0; ``` ```tel ``` ```--@ requires nb_err = 0 or nb_err = 1 or nb_err = 2 or nb_err = 3; ``` ```--@ requires nb_err = nb_err_calc(e1, e2, e3); ``` ```--@ ensures nb_err = 2 => (v = s1 or v = s2 or v = s3); ``` ```--@ ensures nb_err = 3 => (v = pre v); ``` ```--@ ensures (nb_err = 1 and e1) => v = (s2 + s3) / 2.0; ``` ```--@ ensures (nb_err = 1 and e2) => v = (s1 + s3) / 2.0; ``` ```--@ ensures (nb_err = 1 and e3) => v = (s1 + s2) / 2.0; ``` ```--@ ensures nb_err = 0 => v = (s1 + s2 + s3) / 3.0; ``` ```node calc_value (nb_err: int; e1, e2, e3: bool; s1, s2, s3: real) returns (v: real); ``` ```var ``` ``` previous_good_value, v1, v2, v3, di: real; ``` ```let ``` ``` previous_good_value = 0.0 -> pre v; ``` ``` di = if nb_err = 0 ``` ``` then 3.0 ``` ``` else ``` ``` if nb_err = 1 ``` ``` then 2.0 ``` ``` else 1.0; ``` ``` ``` ``` v1 = if e1 then 0.0 else s1; ``` ``` v2 = if e2 then 0.0 else s2; ``` ``` v3 = if e3 then 0.0 else s3; ``` ``` v = if nb_err = 3 ``` ``` then previous_good_value ``` ``` else (v1 + v2 + v3) / di; ``` ```tel ``` ```--@ requires min <= max; ``` ```--@ ensures min <= v and v <= max; ``` ```--@ ensures s < min => v = min; ``` ```--@ ensures s > max => v = max; ``` ```--@ ensures (min <= s and s <= max) => v = s; ``` ```node range(s, min, max: real) returns (v: real); ``` ```let ``` ``` v = if s < min then min else if s > max then max else s; ``` ```tel ``` ``` ``` ``` ``` ```--@ requires min <= max; ``` ```--@ requires delta > 0.0; ``` ```--@ ensures min <= value and value <= max; ``` ```--@ ensures 0 <= nb_errors and nb_errors <= 3; ``` ```--@ ensures nb_errors = 3 => value = pre value; ``` ```--@ ensures exists ok_stMin, ok_stMax, ok_revMin, ok_revMax: bool; (ok_stMin, ok_stMax, ok_revMin, ok_revMax) = obs_simple_voter(s1, s2, s3, min, max, delta, value, warning_stMax, warning_stMin); ``` ```node simple_voter (s1, s2, s3, min, max, delta: real) returns (value: real; warning_stMax, warning_stMin: bool; nb_errors:int); ``` ```var ``` ``` sp_s1, sp_s2, sp_s3: real; ``` ```-- sp_er1, sp_er2, sp_er3: bool; ``` ```-- speed_error1, speed_error2, speed_error3: bool; ``` ``` r_s1, r_s2, r_s3: real; ``` ``` stmin1, stmin2, stmin3, stmax1, stmax2, stmax3: bool; ``` ``` errorRange1, errorRange2, errorRange3: bool; ``` ``` error1, error2, error3: bool; ``` ``` ab1, ab2, ab3: bool; ``` ``` error_ab1, error_ab2, error_ab3: bool; ``` ```let ``` ``` sp_s1 = check_speed (s1, delta); ``` ```-- speed_error1 = check_validity_lock(sp_er1, 20); ``` ``` (r_s1, stmin1, stmax1, errorRange1) = ranged_value(sp_s1, min, max, delta); ``` ``` error1 = errorRange1 or check_validity_lock (errorRange1, 12); ``` ``` sp_s2 = check_speed (s2, delta); ``` ```-- speed_error2 = check_validity_lock(sp_er2, 20); ``` ``` (r_s2, stmin2, stmax2, errorRange2) = ranged_value(sp_s2, min, max, delta); ``` ``` error2 = errorRange2 or check_validity_lock (errorRange2, 14); ``` ``` sp_s3 = check_speed (s3, delta); ``` ```-- speed_error3 = check_validity_lock(sp_er3, 20); ``` ``` (r_s3, stmin3, stmax3, errorRange3) = ranged_value(sp_s3, min, max, delta); ``` ``` error3 = errorRange3 or check_validity_lock (errorRange3, 16); ``` ``` warning_stMin = (stmin1 and stmin2) or (stmin1 and stmin3) or (stmin2 and stmin3); ``` ``` warning_stMax = (stmax1 and stmax2) or (stmax1 and stmax3) or (stmax2 and stmax3); ``` ``` (ab1, ab2, ab3) = if error1 or error2 or error3 ``` ``` then ``` ``` (error1, error2, error3) ``` ``` else ``` ``` aberration(r_s1, r_s2, r_s3, delta); ``` ``` error_ab1 = check_validity_lock (ab1, 16); ``` ``` error_ab2 = check_validity_lock (ab2, 18); ``` ``` error_ab3 = check_validity_lock (ab3, 22); ``` ``` nb_errors = nb_err_calc(error_ab1, error_ab2, error_ab3); ``` ``` value = calc_value(nb_errors, error_ab1, error_ab2, error_ab3, r_s1, r_s2, r_s3); ``` ```tel ``` ```-- it checks if the warnings are valid ``` ```node obs_simple_voter(s1, s2, s3, min, max, delta, value: real; warning_stMax, warning_stMin: bool) ``` ```returns (ok_stMin, ok_stMax, ok_revMin, ok_revMax : bool); ``` ```var ``` ``` stmin1, stmin2, stmin3 : bool; ``` ``` stmax1, stmax2, stmax3 : bool; ``` ```let ``` ``` stmin1 = s1 < min - delta; ``` ``` stmin2 = s2 < min - delta; ``` ``` stmin3 = s3 < min - delta; ``` ``` stmax1 = s1 > max + delta; ``` ``` stmax2 = s2 > max + delta; ``` ``` stmax3 = s3 > max + delta; ``` ``` ok_stMin = (warning_stMin => ((stmin1 and stmin2) or (stmin2 and stmin3) or (stmin1 and stmin3))); ``` ``` ok_stMax = (warning_stMax => ((stmax1 and stmax2) or (stmax2 and stmax3) or (stmax1 and stmax3))); ``` ``` ok_revMin = (((stmin1 and stmin2) or (stmin2 and stmin3) or (stmin1 and stmin3)) => warning_stMin); ``` ``` ok_revMax = (((stmax1 and stmax2) or (stmax2 and stmax3) or (stmax1 and stmax3)) => warning_stMax); ``` ```tel ``` ```node voter_temp (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int); ``` ```let ``` ``` (value, warningMin, warningMax, nb_err) = simple_voter (s1, s2, s3, 200.0, 2000.0, 80.0); ``` ```tel ``` ```node voter_alt (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int); ``` ```let ``` ``` (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0); ``` ```tel ``` ```node safety_plane_archi(s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int); ``` ```let ``` ``` (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0); ``` ```tel ```