Safe Haskell	Safe-Inferred
Language	Haskell2010

Copilot.Verifier.Examples.ShouldPass.WCV

Description

This example shows an implementation of the Well-Clear Violation algorithm, it follows the implementation described in 'Analysis of Well-Clear Bounday Models for the Integration of UAS in the NAS', https://ntrs.nasa.gov/citations/20140010078.

Synopsis

dthr :: Stream Double
tthr :: Stream Double
zthr :: Stream Double
tcoathr :: Stream Double
type Vect2 = (Stream Double, Stream Double)
(|*|) :: Vect2 -> Vect2 -> Stream Double
sq :: Vect2 -> Stream Double
norm :: Vect2 -> Stream Double
det :: Vect2 -> Vect2 -> Stream Double
(~=) :: Stream Double -> Stream Double -> Stream Bool
neg :: Vect2 -> Vect2
tau :: Vect2 -> Vect2 -> Stream Double
tcpa :: Vect2 -> Vect2 -> Stream Double
taumod :: Vect2 -> Vect2 -> Stream Double
tep :: Vect2 -> Vect2 -> Stream Double
delta :: Vect2 -> Vect2 -> Stream Double -> Stream Double
theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double
tcoa :: Stream Double -> Stream Double -> Stream Double
dcpa :: Vect2 -> Vect2 -> Stream Double
wcv :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Stream Double -> Vect2 -> Stream Double -> Stream Bool
verticalWCV :: Stream Double -> Stream Double -> Stream Bool
horizontalWCV :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Vect2 -> Stream Bool
spec :: Spec
verifySpec :: Verbosity -> IO ()

Documentation

dthr :: Stream Double Source #

dthr is the horizontal distance threshold.

tthr :: Stream Double Source #

tthr is the horizontal time threshold.

zthr :: Stream Double Source #

zthr is the vertical distance / altitude threshold.

tcoathr :: Stream Double Source #

tcoathr is the vertical time threshold.

type Vect2 = (Stream Double, Stream Double) Source #

(|*|) :: Vect2 -> Vect2 -> Stream Double Source #

Multiply two Vectors.

sq :: Vect2 -> Stream Double Source #

Calculate the square of a vector.

norm :: Vect2 -> Stream Double Source #

Calculate the length of a vector.

det :: Vect2 -> Vect2 -> Stream Double Source #

Calculate the determinant of two vectors.

(~=) :: Stream Double -> Stream Double -> Stream Bool Source #

Compare two vectors, taking into account the small error that is introduced by the usage of Types.

neg :: Vect2 -> Vect2 Source #

Negate a vector.

tau :: Vect2 -> Vect2 -> Stream Double Source #

tcpa :: Vect2 -> Vect2 -> Stream Double Source #

taumod :: Vect2 -> Vect2 -> Stream Double Source #

tep :: Vect2 -> Vect2 -> Stream Double Source #

delta :: Vect2 -> Vect2 -> Stream Double -> Stream Double Source #

theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double Source #

tcoa :: Stream Double -> Stream Double -> Stream Double Source #

dcpa :: Vect2 -> Vect2 -> Stream Double Source #

wcv :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Stream Double -> Vect2 -> Stream Double -> Stream Bool Source #

Determines if the well clear property is violated or not.

verticalWCV :: Stream Double -> Stream Double -> Stream Bool Source #

horizontalWCV :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Vect2 -> Stream Bool Source #

spec :: Spec Source #

verifySpec :: Verbosity -> IO () Source #