118 lines
3.1 KiB
Haskell
118 lines
3.1 KiB
Haskell
module Voter where
|
|
|
|
{-
|
|
Formal Modeling and Analysis of an Avionics Triplex Sensor Voter
|
|
- Samar Dajani-Brown, Darren Cofer, Gary Hartmann & Steve Pratt
|
|
- 2003
|
|
|
|
https://link.springer.com/chapter/10.1007/3-540-44829-2_3
|
|
-}
|
|
|
|
import Clash.Prelude
|
|
import qualified Data.List as L
|
|
|
|
data Sensor = Sensor {
|
|
out :: Int -- ^ Output value
|
|
, valid :: Bool -- ^ Output validity
|
|
}
|
|
|
|
data State
|
|
= VAll
|
|
| V2NoMis Int Int -- ^ valid sensor ids
|
|
| V2Mis Int Int -- ^ valid sensor ids
|
|
| V1 Int -- ^ valid sensor id
|
|
| VNone
|
|
deriving (Generic, NFDataX)
|
|
|
|
tooMuch :: Int -> Int -> Int -> Bool
|
|
tooMuch limit a b =
|
|
let val = abs $ a - b in
|
|
val > limit
|
|
|
|
isMiscomp3 :: Vec 3 Sensor -> Maybe Int
|
|
isMiscomp3 sens =
|
|
let v01 = tooMuch 0 (out $ sens !! 0) (out $ sens !! 1) in
|
|
let v02 = tooMuch 0 (out $ sens !! 0) (out $ sens !! 2) in
|
|
let v12 = tooMuch 0 (out $ sens !! 1) (out $ sens !! 2) in
|
|
if v01 && v02 then Just 0
|
|
else if v01 && v12 then Just 1
|
|
else if v02 && v12 then Just 2
|
|
else Nothing
|
|
|
|
validSensors :: Vec 3 Sensor -> [Int]
|
|
validSensors sens =
|
|
fst $ foldr (\s (res, curidx) ->
|
|
(if valid s then curidx:res else res, curidx+1))
|
|
([], 0) sens
|
|
|
|
nextState :: State -> Vec 3 Sensor -> State
|
|
nextState VAll sens =
|
|
let vsens = validSensors sens in
|
|
if L.length vsens < 3 then
|
|
-- 1 sensor newly invalidated.
|
|
-- 2 valid sensors available. No miscompare.
|
|
-- (Assumption: No simultaneous failures)
|
|
V2NoMis (vsens L.!! 1) (vsens L.!! 0)
|
|
else
|
|
-- No new invalid sensor
|
|
case isMiscomp3 sens of
|
|
Nothing -> VAll -- No miscompare
|
|
Just sid -> case sid of -- Miscompare. Cut off odd one.
|
|
0 -> V2NoMis 1 2
|
|
1 -> V2NoMis 0 2
|
|
2 -> V2NoMis 1 2
|
|
|
|
nextState (V2NoMis sid1 sid2) sens =
|
|
let vsens = validSensors sens in
|
|
if L.length vsens < 2 then
|
|
-- 1 sensor newly invalidated.
|
|
-- 1 valid sensor available
|
|
V1 (vsens L.!! 0)
|
|
else
|
|
-- No new invalid sensor
|
|
case tooMuch 0 (out $ sens !! sid1) (out $ sens !! sid2) of
|
|
-- No miscompare
|
|
False -> V2NoMis sid1 sid2
|
|
-- Miscompare
|
|
True -> V2Mis sid1 sid2
|
|
|
|
nextState (V2Mis sid1 sid2) sens =
|
|
let vsens = validSensors sens in
|
|
if L.length vsens < 2 then
|
|
V1 (vsens L.!! 0)
|
|
else
|
|
case tooMuch 0 (out $ sens !! sid1) (out $ sens !! sid2) of
|
|
-- Miscompare over!
|
|
False -> V2NoMis sid1 sid2
|
|
-- Still miscomparing..
|
|
True -> V2Mis sid1 sid2
|
|
|
|
nextState (V1 sid) sens =
|
|
let vsens = validSensors sens in
|
|
if vsens == [] then VNone
|
|
else V1 sid
|
|
|
|
nextState VNone sens = VNone
|
|
|
|
nextOut :: State -> Vec 3 Sensor -> Sensor
|
|
nextOut st sens = case st of
|
|
VAll -> sens !! 0
|
|
V2NoMis sid1 _ -> sens !! sid1
|
|
V2Mis sid1 _ -> Sensor (out $ sens !! sid1) False
|
|
V1 sid -> sens !! sid
|
|
VNone -> Sensor (out $ sens !! 0) False
|
|
|
|
topFn :: State -> Vec 3 Sensor -> (State, Sensor)
|
|
topFn st sens =
|
|
let nst = nextState st sens in
|
|
let nout = nextOut nst sens in
|
|
(nst, nout)
|
|
|
|
topEntity
|
|
:: Clock System
|
|
-> Reset System
|
|
-> Enable System
|
|
-> Signal System (Vec 3 Sensor)
|
|
-> Signal System Sensor
|
|
topEntity = exposeClockResetEnable $ mealy topFn VAll
|