diff --git a/haskell/Voter.hs b/haskell/Voter.hs index d59831a..d86376d 100644 --- a/haskell/Voter.hs +++ b/haskell/Voter.hs @@ -1,5 +1,9 @@ module Voter where +-- Can't produce verilog/vhdl: Blackbox error +-- https://groups.google.com/g/clash-language/c/fqzkxyY5eAw?pli=1 +-- Probably because of `list' usage. Got to try vector. ✓ + {- Formal Modeling and Analysis of an Avionics Triplex Sensor Voter - Samar Dajani-Brown, Darren Cofer, Gary Hartmann & Steve Pratt @@ -24,6 +28,10 @@ data State | VNone deriving (Generic, NFDataX) +countValidSens :: Vec 3 Sensor -> Int +countValidSens sens = foldr (\s n -> if valid s then n+1 else n) 0 sens + + tooMuch :: Int -> Int -> Int -> Bool tooMuch limit a b = let val = abs $ a - b in @@ -47,12 +55,14 @@ validSensors sens = nextState :: State -> Vec 3 Sensor -> State nextState VAll sens = - let vsens = validSensors sens in - if L.length vsens < 3 then + if countValidSens sens < 3 then -- 1 sensor newly invalidated. -- 2 valid sensors available. No miscompare. -- (Assumption: No simultaneous failures) - V2NoMis (vsens L.!! 1) (vsens L.!! 0) + let s12 = if (valid $ sens !! 0) && (valid $ sens !! 1) then (0, 1) + else if (valid $ sens !! 0) && (valid $ sens !! 2) then (0, 2) + else (1, 2) in + V2NoMis (fst s12) (snd s12) else -- No new invalid sensor case isMiscomp3 sens of @@ -63,11 +73,13 @@ nextState VAll sens = 2 -> V2NoMis 1 2 nextState (V2NoMis sid1 sid2) sens = - let vsens = validSensors sens in - if L.length vsens < 2 then + if countValidSens sens < 2 then -- 1 sensor newly invalidated. -- 1 valid sensor available - V1 (vsens L.!! 0) + let sid = if (valid $ sens !! 0) then 0 + else if (valid $ sens !! 1) then 1 + else 2 in + V1 sid else -- No new invalid sensor case tooMuch 0 (out $ sens !! sid1) (out $ sens !! sid2) of @@ -77,9 +89,11 @@ nextState (V2NoMis sid1 sid2) sens = True -> V2Mis sid1 sid2 nextState (V2Mis sid1 sid2) sens = - let vsens = validSensors sens in - if L.length vsens < 2 then - V1 (vsens L.!! 0) + if countValidSens sens < 2 then + let sid = if (valid $ sens !! 0) then 0 + else if (valid $ sens !! 1) then 1 + else 2 in + V1 sid else case tooMuch 0 (out $ sens !! sid1) (out $ sens !! sid2) of -- Miscompare over! @@ -88,8 +102,7 @@ nextState (V2Mis sid1 sid2) sens = True -> V2Mis sid1 sid2 nextState (V1 sid) sens = - let vsens = validSensors sens in - if vsens == [] then VNone + if countValidSens sens < 1 then VNone else V1 sid nextState VNone sens = VNone