heater_control.lus 3.42 KB
 Erwan Jahier committed Jun 24, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ``````-- -- A fault-tolerant heater controller with 3 sensors. -- -- To guess the temperature (T), -- -- (1) It compares the value of the 3 sensors 2 by 2 to determine -- which ones seem are broken -- we consider then broken if they -- differ too much. -- -- (2) then, it performs a vote: -- o If the tree sensors are broken, it does not heat; -- o If the temperature is bigger than TMAX, it does not heat; -- o If the temperature is smaller than TMIN, it heats; -- o Otherwise, it keeps its previous state. `````` Erwan Jahier committed May 16, 2012 17 ``````const FAILURE = -999.0; -- a fake temperature given when all sensors are broken `````` Erwan Jahier committed Jun 24, 2011 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 ``````const TMIN = 6.0; const TMAX = 9.0; const DELTA = 0.5; -- const DELTA : real; ----------------------------------------------------------------------- ----------------------------------------------------------------------- node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool); -- T is supposed to be the real temperature and is not -- used in the controller; we add it here in oder to test the -- controller to be able to write a sensible oracle. var V12, V13, V23 : bool; Tguess : real; let V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid? V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid? V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid? Tguess = if noneoftree(V12, V13, V23) then FAILURE else if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else if alloftree(V12, V13, V23) then Median(T1, T2, T3) else -- 2 among V1, V2, V3 are false if V12 then Average(T1, T2) else if V13 then Average(T1, T3) else -- V23 is necessarily true, hence T1 is wrong Average(T2, T3) ; `````` Erwan Jahier committed Mar 07, 2012 52 `````` Heat_on = false -> `````` Erwan Jahier committed Jun 24, 2011 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 `````` if Tguess = FAILURE then false else if Tguess < TMIN then true else if Tguess > TMAX then false else pre Heat_on; tel ----------------------------------------------------------------------- ----------------------------------------------------------------------- node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool;LT1, LT2, LT3 : real); let LT1 = T1; LT2 = T2; LT3 = T3; ok = true -> pre T < TMAX + 1.0 ; tel node not_a_sauna2(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool); let ok = true -> pre T < TMAX - 6.0 ; tel ----------------------------------------------------------------------- ----------------------------------------------------------------------- -- returns the absolute value of 2 reals node abs (v : real) returns (a : real) ; let a = if v >= 0.0 then v else -v ; tel -- returns the average values of 2 reals node Average(a, b: real) returns (z : real); let z = (a+b)/2.0 ; tel -- returns the median values of 3 reals node Median(a, b, c : real) returns (z : real); let z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ; tel -- returns the maximum values of 2 reals node max2 (one, two : real) returns (m : real) ; let m = if one > two then one else two ; tel -- returns the minimum values of 2 reals node min2 (one, two : real) returns (m : real) ; let m = if one < two then one else two ; tel node noneoftree (f1, f2, f3 : bool) returns (r : bool) let r = not f1 and not f2 and not f3 ; tel node alloftree (f1, f2, f3 : bool) returns (r : bool) let r = f1 and f2 and f3 ; tel node oneoftree (f1, f2, f3 : bool) returns (r : bool) let r = f1 and not f2 and not f3 or f2 and not f1 and not f3 or f3 and not f1 and not f2 ; tel``````