diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,3 @@ +# Changelog for interval-algebra + +## Unreleased changes diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright NoviSci, Inc (c) 2020 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Author name here nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,30 @@ +# interval-algebra + +The `interval-algebra` package implements [Allen's interval algebra](https://www.ics.uci.edu/~alspaugh/cls/shr/allen.html) in [Haskell](https://www.haskell.org). The main module provides data types and related classes for the interval-based temporal logic described in [Allen (1983)](https://doi.org/10.1145/182.358434) and axiomatized in [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x). + +A good primer on Allen's algebra can be [found here](https://thomasalspaugh.org/pub/fnd/allen.html). + +# Design + +The module is built around three typeclasses designed to separate concerns of +constructing, relating, and combining `Interval`s: + +1. `Intervallic` provides an interface to the data structure of an `Interval`, defining how an `Interval a` (simply a pair `(a, a)`) is constructed. +2. `IntervalAlgebraic` provides an interface to the `IntervalRelation`s, the workhorse of Allen's temporal logic. +3. `IntervalCombinable` provides an interface to methods of combining multiple `Interval`s. + +An advantage of nested typeclass design is that developers can define an +`Interval` of type `a` with just the amount of structure that they need. + +## Total Ordering of `Interval`s + +The modules makes the (opinionated) choice of a total ordering for `Intervallic` `Interval`s. Namely, the ordering is based on first ordering the `begin`s +then the `end`s. + +# Axiom tests + +The package [includes tests](test/IntervalAlgebraSpec.hs) that the functions of the `IntervalAlgebraic` typeclass meets the axioms for _intervals_ (not points) as laid out in [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x). + +# Development + +This module is under development and the API may change in the future. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/interval-algebra.cabal b/interval-algebra.cabal new file mode 100644 --- /dev/null +++ b/interval-algebra.cabal @@ -0,0 +1,57 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.33.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: afab50a57b38d45082f7b71f75ba5ec1cb8188302aa601326ba694aaa856a8be + +name: interval-algebra +version: 0.1.2 +synopsis: An implementation of Allen's interval algebra for temporal logic +description: Please see the README on GitHub at +category: Algebra,Time +homepage: https://github.com/novisci/interval-algebra#readme +bug-reports: https://github.com/novisci/interval-algebra/issues +author: Bradley Saul +maintainer: bsaul@novisci.com +copyright: 2020 NoviSci +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + ChangeLog.md + +source-repository head + type: git + location: https://github.com/novisci/interval-algebra + +library + exposed-modules: + IntervalAlgebra + IntervalAlgebra.IntervalFilter + other-modules: + Paths_interval_algebra + hs-source-dirs: + src + build-depends: + base >=4.7 && <5 + , time >=1.8 && <2 + default-language: Haskell2010 + +test-suite interval-algebra-test + type: exitcode-stdio-1.0 + main-is: IntervalAlgebraSpec.hs + other-modules: + Paths_interval_algebra + hs-source-dirs: + test + ghc-options: -threaded -rtsopts -with-rtsopts=-N + build-depends: + QuickCheck + , base >=4.7 && <5 + , hspec + , interval-algebra + , time >=1.8 && <2 + default-language: Haskell2010 diff --git a/src/IntervalAlgebra.hs b/src/IntervalAlgebra.hs new file mode 100644 --- /dev/null +++ b/src/IntervalAlgebra.hs @@ -0,0 +1,311 @@ +{-| +Module : Interval Algebra +Description : Implementation of Allen's interval algebra +Copyright : (c) NoviSci, Inc 2020 +License : BSD3 +Maintainer : bsaul@novisci.com +Stability : experimental + +The @IntervalAlgebra@ module provides data types and related classes for the +interval-based temporal logic described in [Allen (1983)](https://doi.org/10.1145/182.358434) +and axiomatized in [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x). + +A good primer on Allen's algebra can be [found here](https://thomasalspaugh.org/pub/fnd/allen.html). + += Design + +The module is built around three typeclasses designed to separate concerns of +constructing, relating, and combining @'Interval'@s: + +1. @'Intervallic'@ provides an interface to the data structure of an @'Interval'@, + defining how an @'Interval' a@ is constructed. +2. @'IntervalAlgebraic'@ provides an interface to the @'IntervalRelation's@, + the workhorse of Allen's temporal logic. +3. @'IntervalCombinable'@ provides an interface to methods of combining multiple + @'Interval's@. + +An advantage of nested typeclass design is that developers can define an +@'Interval'@ of type @a@ with just the amount of structure that they need. + +== Total Ordering of @Interval@s + +The modules makes the (opinionated) choice of a total ordering for @'Intervallic'@ +@'Interval'@s. Namely, the ordering is based on first ordering the 'begin's +then the 'end's. + += Development + +This module is under development and the API may change in the future. +-} + +module IntervalAlgebra( + + -- * Classes + Intervallic(..) + , IntervalAlgebraic(..) + , IntervalCombinable(..) + + -- * Data Types + , Interval(..) + , IntervalRelation + , ComparativePredicateOf + +) where + +import Data.Time as DT + +{- | An @'Interval' a@ is a pair of @a@s \( (x, y) \text{ where } x < y\). The +@'Intervallic'@ class provides a safe @'parseInterval'@ function that returns a +@'Left'@ error if \(y < x\) and 'unsafeInterval' as constructor for creating an +interval that may not be valid. +-} +newtype Interval a = Interval (a, a) deriving (Eq) + +{- | + +The 'IntervalRelation' type enumerates the thirteen possible ways that two +@'Interval' a@ objects can relate according to the interval algebra. + +=== Meets, Metby + +> x `meets` y +> y `metBy` x + +@ +x: |-----| +y: |-----| +@ + +=== Before, After + +> x `before` y +> y `after` x + +@ +x: |-----| +y: |-----| +@ + + +=== Overlaps, OverlappedBy + +> x `overlaps` y +> y `overlappedBy` x + +@ +x: |-----| +y: |-----| +@ + +=== Starts, StartedBy + +> x `starts` y +> y `startedBy` x + +@ +x: |---| +y: |-----| +@ + +=== Finishes, FinishedBy + +> x `finishes` y +> y `finishedBy` x + +@ +x: |---| +y: |-----| +@ + +=== During, Contains + +> x `during` y +> y `contains` x + +@ +x: |-| +y: |-----| +@ + +=== Equal + +> x `equal` y +> y `equal` x + +@ +x: |-----| +y: |-----| +@ + +-} +data IntervalRelation = + Meets + | MetBy + | Before + | After + | Overlaps + | OverlappedBy + | Starts + | StartedBy + | Finishes + | FinishedBy + | During + | Contains + | Equals + deriving (Show, Read) + +{- | +The @'Intervallic'@ typeclass specifies how an @'Interval' a@s is constructed. +It also includes functions for getting the @'begin'@ and @'end'@ of an @'Interval' a@. +-} +class (Ord a, Show a) => Intervallic a where + + -- | Safely parse a pair of @a@s to create an @'Interval' a@. + parseInterval :: a -> a -> Either String (Interval a) + parseInterval x y + -- TODO: create more general framework for error handling + | y < x = Left $ show y ++ "<" ++ show x + | otherwise = Right $ Interval (x, y) + + {- | Create a new @'Interval' a@. This function is __not__ safe as it does + not enforce that \(x < y\). Use with caution. It is meant to be helper + function in early prototyping of this package. This function may be + deprecated in future releases. + -} + unsafeInterval :: a -> a -> Interval a + unsafeInterval x y = Interval (x, y) + + -- | Access the ends of an @'Interval' a@ . + begin, end :: Interval a -> a + begin (Interval x) = fst x -- \( \text{begin}(x, y) = x \) + end (Interval x) = snd x -- \( \text{end}(x, y) = y \) + +{- | +The @'IntervalAlgebraic'@ typeclass specifies the functions and relational +operators for interval-based temporal logic. The typeclass defines the +relational operators for intervals, plus other useful utilities such as +@'disjoint'@, @'in''@, and @'composeRelations'@. +-} +class (Eq a, Intervallic a) => IntervalAlgebraic a where + + -- | Compare two intervals to determine their 'IntervalRelation'. + relate :: Interval a -> Interval a -> IntervalRelation + relate x y + | x `before` y = Before + | x `after` y = After + | x `meets` y = Meets + | x `metBy` y = MetBy + | x `overlaps` y = Overlaps + | x `overlappedBy` y = OverlappedBy + | x `starts` y = Starts + | x `startedBy` y = StartedBy + | x `finishes` y = Finishes + | x `finishedBy` y = FinishedBy + | x `during` y = During + | x `contains` y = Contains + | otherwise = Equals + + -- | Does x equal y? + equals :: ComparativePredicateOf (Interval a) + equals x y = x == y + + -- | Does x meet y? Is y metBy x? + meets, metBy :: ComparativePredicateOf (Interval a) + meets x y = end x == begin y + metBy = flip meets + + -- | Is x before y? Is x after y? + before, after :: ComparativePredicateOf (Interval a) + before x y = end x < begin y + after = flip before + + -- | Does x overlap y? Is x overlapped by y? + overlaps, overlappedBy :: ComparativePredicateOf (Interval a) + overlaps x y = begin x < begin y && end x < end y && end x > begin y + overlappedBy = flip overlaps + + -- | Does x start y? Is x started by y? + starts, startedBy :: ComparativePredicateOf (Interval a) + starts x y = begin x == begin y && (end x < end y) + startedBy = flip starts + + -- | Does x finish y? Is x finished by y? + finishes, finishedBy :: ComparativePredicateOf (Interval a) + finishes x y = begin x > begin y && end x == end y + finishedBy = flip finishes + + -- | Is x during y? Does x contain y? + during, contains :: ComparativePredicateOf (Interval a) + during x y = begin x > begin y && end x < end y + contains = flip during + + -- ** Interval Algebra utilities + + -- | Compose a list of interval relations with _or_ to create a new + -- @'ComparativePredicateOf' 'Interval' a@.For example, + -- @composeRelations [before, meets]@ creates a predicate function determining + -- if one interval is either before or meets another interval. + composeRelations :: [ComparativePredicateOf (Interval a)] -> + ComparativePredicateOf (Interval a) + composeRelations fs x y = any (\ f -> f x y) fs + + -- | Are x and y disjoint ('before', 'after', 'meets', or 'metBy')? + disjoint :: ComparativePredicateOf (Interval a) + disjoint = composeRelations [before, after, meets, metBy] + + -- | Is x contained in y in any sense ('during', 'starts', 'finishes' + -- or 'equals'? + in' :: ComparativePredicateOf (Interval a) + in' = composeRelations [during, starts, finishes, equals] + + +{- | +The @'IntervalCombinable'@ typeclass provides methods combining multiple @'Interval's@. +-} +class (IntervalAlgebraic a) => IntervalCombinable a where + + -- | Maybe form a new @'Interval'@ by the union of two @'Interval'@s that 'meet'. + (.+.) :: Interval a -> Interval a -> Maybe (Interval a) + (.+.) x y + | x `meets` y = Just $ Interval (begin x, end y) + | otherwise = Nothing + +{- +Instances +-} + +-- | Imposes a total ordering on @'Interval' a@ based on first ordering the +-- 'begin's then the 'end's. +instance (Intervallic a) => Ord (Interval a) where + (<=) x y + | begin x < begin y = True + | begin x == begin y = end x <= end y + | otherwise = False + (<) x y + | begin x < begin y = True + | begin x == begin y = end x < end y + | otherwise = False + +instance (Intervallic a, Show a) => Show (Interval a) where + show x = "(" ++ show (begin x) ++ ", " ++ show (end x) ++ ")" + +instance Intervallic Int +instance IntervalAlgebraic Int +instance IntervalCombinable Int + +instance Intervallic Integer +instance IntervalAlgebraic Integer +instance IntervalCombinable Integer + +instance Intervallic DT.Day +instance IntervalAlgebraic DT.Day +instance IntervalCombinable DT.Day + +{- +Misc Utilities +-} + +-- | Defines a predicate of two objects of type @a@. +type ComparativePredicateOf a = (a -> a -> Bool) + + diff --git a/src/IntervalAlgebra/IntervalFilter.hs b/src/IntervalAlgebra/IntervalFilter.hs new file mode 100644 --- /dev/null +++ b/src/IntervalAlgebra/IntervalFilter.hs @@ -0,0 +1,64 @@ +{-| +Module : Interval Algebra Filtrations +Description : Offers functions for filtering list of intervals based on a + reference interval. +Copyright : (c) NoviSci, Inc 2020 +License : BSD3 +Maintainer : bsaul@novisci.com +Stability : experimental +-} + +module IntervalAlgebra.IntervalFilter ( + -- * Classes + IntervalFilterable(..) +) where + +import IntervalAlgebra + +{- | +The @'IntervalFilterable'@ class provides functions for filtering 'List's of +@'Interval'@s based on @'IntervalAlgebraic'@ relations. +-} +class (IntervalAlgebraic a) => IntervalFilterable a where + +-- TODO: generalize the class to handle generalized "filterable" containers (not +-- just lists). + + -- |Creates a function for filtering a list of Interval as based on a predicate + filterMaker :: ComparativePredicateOf (Interval a) + -> Interval a + -> ([Interval a] + -> [Interval a]) + filterMaker f p = filter (`f` p) + + -- | Filter a list of Interval as to those overlapping the Interval a p + filterOverlaps :: Interval a -> ([Interval a] -> [Interval a]) + filterOverlaps = filterMaker overlaps + + -- | Filter a list of Interval as to those overlapped by the Interval a p + filterOverlappedBy :: Interval a -> ([Interval a] -> [Interval a]) + filterOverlappedBy = filterMaker overlappedBy + + -- | Filter a list of Interval as to those before the Interval a p + filterBefore :: Interval a -> ([Interval a] -> [Interval a]) + filterBefore = filterMaker before + + -- | Filter a list of Interval as to those before the Interval a p + filterAfter :: Interval a -> ([Interval a] -> [Interval a]) + filterAfter = filterMaker after + + -- | Filter a list of Interval as to those meeting the Interval a p + filterMeets :: Interval a -> ([Interval a] -> [Interval a]) + filterMeets = filterMaker meets + + -- | Filter a list of Interval as to those meeting the Interval a p + filterMetBy :: Interval a -> ([Interval a] -> [Interval a]) + filterMetBy = filterMaker metBy + + -- | Filter a list of Interval as to those during the Interval a p + filterDuring :: Interval a -> ([Interval a] -> [Interval a]) + filterDuring = filterMaker during + + -- | Filter a list of Interval as to those containing the Interval a p + filterContains :: Interval a -> ([Interval a] -> [Interval a]) + filterContains = filterMaker contains diff --git a/test/IntervalAlgebraSpec.hs b/test/IntervalAlgebraSpec.hs new file mode 100644 --- /dev/null +++ b/test/IntervalAlgebraSpec.hs @@ -0,0 +1,378 @@ +{-# LANGUAGE FlexibleInstances #-} +import Test.Hspec +import Test.Hspec.QuickCheck +import Test.QuickCheck +import IntervalAlgebra as IA +import Data.Maybe +import Control.Monad + +xor :: Bool -> Bool -> Bool +xor a b = a /= b + +instance Arbitrary IntervalInt where + arbitrary = liftM2 safeInterval' arbitrary arbitrary + +type IntervalInt = Interval Int + +makePos :: Int -> Int +makePos x + | x == 0 = x + 1 + | x < 0 = negate x + | otherwise = x + +-- | A function for creating intervals when you think you know what you're doing. +safeInterval :: Int -> Int -> IntervalInt +safeInterval x y = unsafeInterval (min x y) (max x y) + +-- | Safely create a valid 'IntervalInt' from two Ints by adding 'makepos' @dur@ +-- to @start@ to set the duration of the interval. +safeInterval' :: Int -> Int -> IntervalInt +safeInterval' start dur = safeInterval start (start + makePos dur) + +-- | Create a 'Maybe IntervalInt' from two Ints. +safeInterval'' :: Int -> Int -> Maybe IntervalInt +safeInterval'' a b + | b <= a = Nothing + | otherwise = Just $ safeInterval a b + + +-- | A set used for testing M1 defined so that the M1 condition is true. +data M1set = M1set { + m11 :: IntervalInt + , m12 :: IntervalInt + , m13 :: IntervalInt + , m14 :: IntervalInt } + deriving (Show) + +instance Arbitrary M1set where + arbitrary = do + x <- arbitrary + a <- arbitrary + b <- arbitrary + c <- arbitrary + return $ m1set x a b c + +-- | Smart constructor of 'M1set'. +m1set :: IntervalInt -> Int -> Int -> Int -> M1set +m1set x a b c = M1set p1 p2 p3 p4 + where p1 = x -- interval i in prop_IAaxiomM1 + p2 = safeInterval' (end x) a -- interval j in prop_IAaxiomM1 + p3 = safeInterval' (end x) b -- interval k in prop_IAaxiomM1 + p4 = safeInterval (begin p2 - (makePos c)) (begin p2) + +{- + + ** 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 i,j,k,l s.t. (i:j & i:k & l:j) \implies l:k + \] +-} +prop_IAaxiomM1 :: M1set -> Property +prop_IAaxiomM1 x = + (i `meets` j && i `meets` k && l `meets` j) ==> (l `meets` k) + where i = m11 x + j = m12 x + k = m13 x + l = m14 x + +-- | A set used for testing M2 defined so that the M2 condition is true. +data M2set = M2set { + m21 :: IntervalInt + , m22 :: IntervalInt + , m23 :: IntervalInt + , m24 :: IntervalInt } + deriving (Show) + +instance Arbitrary M2set where + arbitrary = do + x <- arbitrary + a <- arbitrary + b <- arbitrary + c <- arbitrary + return $ m2set x a b c + +-- | Smart constructor of 'M2set'. +m2set :: IntervalInt -> IntervalInt -> Int -> Int -> M2set +m2set x y a b = M2set p1 p2 p3 p4 + where p1 = x -- interval i in prop_IAaxiomM2 + p2 = safeInterval' (end x) a -- interval j in prop_IAaxiomM2 + p3 = y -- interval k in prop_IAaxiomM2 + p4 = safeInterval' (end y) b -- interval l in prop_IAaxiomM2 + +{- + +** 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 & k:l) \implies + i:l \oplus + (\exists m s.t. i:m:l) \oplus + (\exists m s.t. k:m:j) + \] +-} + +prop_IAaxiomM2 :: M2set -> Property +prop_IAaxiomM2 x = + (i `meets` j && k `meets` l) ==> + (i `meets` l) `xor` + (not $ isNothing m) `xor` + (not $ isNothing n) + where i = m21 x + j = m22 x + k = m23 x + l = m24 x + m = safeInterval'' (end $ i) (begin $ l) + n = safeInterval'' (end $ k) (begin $ j) + +{- + + ** Axiom ML1 + + An interval cannot meet itself. + + \[ + \forall i \lnot i:i + \] +-} + +prop_IAaxiomML1 :: IntervalInt -> Property +prop_IAaxiomML1 x = not (x `meets` x) === True + +{- + +** Axiom ML2 + +If i meets j then j does not meet i. + +\[ + \forall i,j i:j \implies \lnot j:i +\] +-} + +prop_IAaxiomML2 :: M2set -> Property +prop_IAaxiomML2 x = + (i `meets` j) ==> not (j `meets` i) + where i = m21 x + j = m22 x + + +{- + +** Axiom M3 + +Time does not start or stop: + +\[ + \forall i \exists j,k s.t. j:i:k +\] +-} + +prop_IAaxiomM3 :: IntervalInt -> Property +prop_IAaxiomM3 i = + (j `meets` i && i `meets` k) === True + where j = safeInterval (begin i - 1) (begin i) + k = safeInterval (end i) (end i + 1) + +{- + +** 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 & m:k:n) +\] +-} + +prop_IAaxiomM4 :: M2set -> Property +prop_IAaxiomM4 x = + ((m `meets` i && i `meets` j && j `meets` n) && + (m `meets` k && k `meets` n)) === True + where i = m21 x + j = m22 x + m = safeInterval (begin i - 1) (begin i) + n = safeInterval (end j) (end j + 1) + k = safeInterval (end m) (begin n) + + +{- + +** Axiom M5 + +If two meets are separated by intervals, then this sequence is a longer interval. + +\[ + \forall i,j,k,l (i:j:l & i:k:l) \seteq j = k +\] +-} + +-- | A set used for testing M5. +data M5set = M5set { + m51 :: IntervalInt + , m52 :: IntervalInt } + deriving (Show) + +instance Arbitrary M5set where + arbitrary = do + x <- arbitrary + a <- arbitrary + b <- arbitrary + return $ m5set x a b + +-- | Smart constructor of 'M5set'. +m5set :: IntervalInt -> Int -> Int -> M5set +m5set x a b = M5set p1 p2 + where p1 = x -- interval i in prop_IAaxiomM5 + p2 = safeInterval' ps a -- interval l in prop_IAaxiomM5 + ps = (makePos b) + (end x) -- creating l by shifting and expanding i + + +prop_IAaxiomM5 :: M5set -> Property +prop_IAaxiomM5 x = + ((i `meets` j && j `meets` l) && + (i `meets` k && k `meets` l)) === (j == k) + where i = m51 x + j = safeInterval (end i) (begin l) + k = safeInterval (end i) (begin l) + l = m52 x + +{- + +** Axiom M4.1 + +Ordered unions: + +\[ + \forall i,j i:j \implies (\exists m,n s.t. m:i:j:n & m:(i+j):n) +\] +-} + +prop_IAaxiomM4_1 :: M2set -> Property +prop_IAaxiomM4_1 x = + ((m `meets` i && i `meets` j && j `meets` n) && + (m `meets` ij && ij `meets` n)) === True + where i = m21 x + j = m22 x + m = safeInterval (begin i - 1) (begin i) + n = safeInterval (end j) (end j + 1) + ij = fromJust $ i .+. j + + +{- +* Interval Relation property testing +-} + +prop_IAbefore :: IntervalInt -> IntervalInt -> Property +prop_IAbefore i j = + IA.before i j ==> (i `meets` k) && (k `meets` j) + where k = safeInterval (end i) (begin j) + + +prop_IAstarts:: IntervalInt -> IntervalInt -> Property +prop_IAstarts i j + | ((IA.starts i j) == True) = + let k = safeInterval (end i) (end j) + in + (j == (fromJust $ i .+. k)) === True + | otherwise = IA.starts i j === False + + +prop_IAfinishes:: IntervalInt -> IntervalInt -> Property +prop_IAfinishes i j + | ((IA.finishes i j) == True) = + let k = safeInterval (begin j) (begin i) + in + (j == (fromJust $ k .+. i)) === True + | otherwise = IA.finishes i j === False + +prop_IAoverlaps:: IntervalInt -> IntervalInt -> Property +prop_IAoverlaps i j + | ((IA.overlaps i j) == True) = + let k = safeInterval (begin i) (begin j) + l = safeInterval (begin j) (end i) + m = safeInterval (end i) (end j) + in + ((i == (fromJust $ k .+. l )) && + (j == (fromJust $ l .+. m ))) === True + | otherwise = IA.overlaps i j === False + +prop_IAduring:: IntervalInt -> IntervalInt -> Property +prop_IAduring i j + | ((IA.during i j) == True) = + let k = safeInterval (begin j) (begin i) + l = safeInterval (end i) (end j) + in + (j == (fromJust $ (fromJust $ k .+. i) .+. l)) === True + | otherwise = IA.during i j === False + +{- +For any two pair of intervals exactly one 'IntervalRelation' should hold. +-} + +allIArelations:: [(ComparativePredicateOf (IntervalInt))] +allIArelations = [ IA.equals + , IA.meets + , IA.metBy + , IA.before + , IA.after + , IA.starts + , IA.startedBy + , IA.finishes + , IA.finishedBy + , IA.overlaps + , IA.overlappedBy + , IA.during + , IA.contains ] + +prop_exclusiveRelations:: IntervalInt -> IntervalInt -> Property +prop_exclusiveRelations x y = + ( 1 == length (filter id $ map (\r -> r x y) allIArelations)) === True + +main :: IO () +main = hspec $ do + describe "Interval Algebra Axioms for meets property" $ + --modifyMaxDiscardRatio (* 10) $ + do + it "M1" $ property prop_IAaxiomM1 + it "M2" $ property prop_IAaxiomM2 + it "ML1" $ property prop_IAaxiomML1 + it "ML2" $ property prop_IAaxiomML2 + {- + 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. + -} + --it "ML3" $ property prop_IAaxiomML3 + it "M3" $ property prop_IAaxiomM3 + it "M4" $ property prop_IAaxiomM4 + it "M5" $ property prop_IAaxiomM5 + it "M4.1" $ property prop_IAaxiomM4_1 + + + describe "Interval Algebra relation properties" $ + modifyMaxSuccess (*10) $ + do + it "before" $ property prop_IAbefore + it "starts" $ property prop_IAstarts + it "finishes" $ property prop_IAfinishes + it "overlaps" $ property prop_IAoverlaps + it "during" $ property prop_IAduring + + describe "Interval Algebra relation uniqueness" $ + modifyMaxSuccess (*100) $ + do + it "exactly one relation must be true" $ property prop_exclusiveRelations +