[clash] update Voter.hs to avoid list
This commit is contained in:
parent
0b1d4a05e9
commit
1c606f0326
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue