interval-algebra (empty) → 0.1.2
raw patch · 8 files changed
+875/−0 lines, 8 filesdep +QuickCheckdep +basedep +hspecsetup-changed
Dependencies added: QuickCheck, base, hspec, interval-algebra, time
Files
- ChangeLog.md +3/−0
- LICENSE +30/−0
- README.md +30/−0
- Setup.hs +2/−0
- interval-algebra.cabal +57/−0
- src/IntervalAlgebra.hs +311/−0
- src/IntervalAlgebra/IntervalFilter.hs +64/−0
- test/IntervalAlgebraSpec.hs +378/−0
+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for interval-algebra++## Unreleased changes
+ LICENSE view
@@ -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.
+ README.md view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ interval-algebra.cabal view
@@ -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 <https://github.com/novisci/interval-algebra>+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
+ src/IntervalAlgebra.hs view
@@ -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) ++
+ src/IntervalAlgebra/IntervalFilter.hs view
@@ -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
+ test/IntervalAlgebraSpec.hs view
@@ -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+