IntervalAlgebra.Axioms

This module exports utilities for property-based tests for the axioms in section 1 of Allen and Hayes (1987). The notation below is that of the original paper.

This module is useful if creating a new instance of interval types that you want to test.

Documentation

xor :: Bool -> Bool -> Bool

makePos :: (Ord b, Num b) => b -> b

Internal function for converting a number to a strictly positive value.

data M1set a

A set used for testing M1 defined so that the M1 condition is true.

Constructors

M1set

Fields

• m11 :: Interval a
• m12 :: Interval a
• m13 :: Interval a
• m14 :: Interval a

Instances

(Show a, Ord a) => Show (M1set a)

Defined in IntervalAlgebra.Axioms

Methods

showsPrec :: Int -> M1set a -> ShowS

show :: M1set a -> String

showList :: [M1set a] -> ShowS

Arbitrary (M1set Int)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M1set Int)

shrink :: M1set Int -> [M1set Int]

Arbitrary (M1set UTCTime)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M1set UTCTime)

shrink :: M1set UTCTime -> [M1set UTCTime]

Arbitrary (M1set Day)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M1set Day)

shrink :: M1set Day -> [M1set Day]

data M2set a

A set used for testing M2 defined so that the M2 condition is true.

Constructors

M2set

Fields

• m21 :: Interval a
• m22 :: Interval a
• m23 :: Interval a
• m24 :: Interval a

Instances

(Show a, Ord a) => Show (M2set a)

Defined in IntervalAlgebra.Axioms

Methods

showsPrec :: Int -> M2set a -> ShowS

show :: M2set a -> String

showList :: [M2set a] -> ShowS

Arbitrary (M2set Int)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M2set Int)

shrink :: M2set Int -> [M2set Int]

Arbitrary (M2set UTCTime)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M2set UTCTime)

shrink :: M2set UTCTime -> [M2set UTCTime]

Arbitrary (M2set Day)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M2set Day)

shrink :: M2set Day -> [M2set Day]

data M5set a

A set used for testing M5.

Constructors

M5set

Fields

• m51 :: Interval a
• m52 :: Interval a

Instances

(Show a, Ord a) => Show (M5set a)

Defined in IntervalAlgebra.Axioms

Methods

showsPrec :: Int -> M5set a -> ShowS

show :: M5set a -> String

showList :: [M5set a] -> ShowS

Arbitrary (M5set Int)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M5set Int)

shrink :: M5set Int -> [M5set Int]

Arbitrary (M5set UTCTime)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M5set UTCTime)

shrink :: M5set UTCTime -> [M5set UTCTime]

Arbitrary (M5set Day)

Defined in IntervalAlgebra.Axioms

Methods

arbitrary :: Gen (M5set Day)

shrink :: M5set Day -> [M5set Day]

m1set :: (SizedIv (Interval a), b ~ Moment (Interval a), Ord b, Num b) => Interval a -> b -> b -> b -> M1set a

Smart constructor of M1set.

prop_IAaxiomM1 :: (Iv (Interval a), SizedIv (Interval a)) => M1set a -> Property

Axiom M1

The first axiom of Allen and Hayes (1987) states that if "two periods both meet a third, thn any period met by one must also be met by the other." That is:

\[ \forall \text{ i,j,k,l } s.t. (i:j \text{ & } i:k \text{ & } l:j) \implies l:k \]

m2set :: SizedIv (Interval a) => Interval a -> Interval a -> Moment (Interval a) -> Moment (Interval a) -> M2set a

Smart constructor of M2set.

prop_IAaxiomM2 :: (SizedIv (Interval a), Show a, Ord a) => M2set a -> Property

Axiom M2

If period i meets period j and period k meets l, then exactly one of the following holds:

1) i meets l; 2) there is an m such that i meets m and m meets l; 3) there is an n such that k meets n and n meets j.

That is,

\[ \forall i,j,k,l s.t. (i:j \text { & } k:l) \implies i:l \oplus (\exists m s.t. i:m:l) \oplus (\exists m s.t. k:m:j) \]

prop_IAaxiomML1 :: (Iv (Interval a), SizedIv (Interval a)) => Interval a -> Property

Axiom ML1

An interval cannot meet itself.

\[ \forall i \lnot i:i \]

prop_IAaxiomML2 :: (Iv (Interval a), SizedIv (Interval a)) => M2set a -> Property

Axiom ML2

If i meets j then j does not meet i.

\[ \forall i,j i:j \implies \lnot j:i \]

prop_IAaxiomM3 :: (Iv (Interval a), SizedIv (Interval a)) => Moment (Interval a) -> Interval a -> Property

Axiom M3

Time does not start or stop:

\[ \forall i \exists j,k s.t. j:i:k \]

prop_IAaxiomM4 :: forall a. (Iv (Interval a), SizedIv (Interval a), Ord (Moment (Interval a))) => Moment (Interval a) -> M2set a -> Property

ML3 says that For all i, there does not exist m such that i meets m and m meet i. Not testing that this axiom holds, as I'm not sure how I would test the lack of existence easily.

Axiom M4

If two meets are separated by intervals, then this sequence is a longer interval.

\[ \forall i,j i:j \implies (\exists k,m,n s.t m:i:j:n \text { & } m:k:n) \]

m5set :: (SizedIv (Interval a), Eq a, Ord (Moment (Interval a)), Num (Moment (Interval a))) => Interval a -> Moment (Interval a) -> Moment (Interval a) -> M5set a

Smart constructor of M5set.

prop_IAaxiomM5 :: forall a. (SizedIv (Interval a), Ord a, Ord (Moment (Interval a))) => M5set a -> Property

Axiom M5

There is only one time period between any two meeting places.

\[ \forall i,j,k,l (i:j:l \text{ & } i:k:l) \equiv j = k \]

prop_IAaxiomM4_1 :: (SizedIv (Interval a), Ord a, Ord (Moment (Interval a))) => Moment (Interval a) -> M2set a -> Property

Axiom M4.1

Ordered unions:

\[ \forall i,j i:j \implies (\exists m,n s.t. m:i:j:n \text{ & } m:(i+j):n) \]