fmod PROPOSITION is sort Proposition . endfm fmod BASIC-FORMULA is including PROPOSITION . sort Formula . subsort Proposition < Formula . ops true false : -> Formula . op _/\_ : Formula Formula -> Formula [assoc prec 20] . op _\/_ : Formula Formula -> Formula [assoc prec 30] . op _->_ : Formula Formula -> Formula [prec 40] . op _<->_ : Formula Formula -> Formula [prec 40] . op !_ : Formula -> Formula [prec 10] . endfm fmod LTL-BOX-SYNTAX is including BASIC-FORMULA . ops <>_ `[`]_ : Formula -> Formula [prec 7] . endfm fmod INTERVAL is sort Interval . endfm fmod ALLEN-SYNTAX is including BASIC-FORMULA . including INTERVAL . ops Equals Before After Overlaps Overlapped-by Meets Met-by Contains During Starts Started-by Ends Ended-by : Interval Interval -> Formula . ops Holds Occurs : Proposition Interval -> Formula . vars I J : Interval . eq After(I,J) = Before(J,I) . eq Met-by(I,J) = Meets(J,I) . eq Overlapped-by(I,J) = Overlaps(J,I) . eq During(I,J) = Contains(J,I) . eq Started-by(I,J) = Starts(J,I) . eq Ended-by(I,J) = Ends(J,I) . endfm fmod INTERVAL-SET is including INTERVAL . sort IntervalSet . subsort Interval < IntervalSet . op empty : -> IntervalSet . op _,_ : IntervalSet IntervalSet -> IntervalSet [assoc comm id: empty] . var I : Interval . eq I,I = I . endfm fmod INTERVALS-OF is including ALLEN-SYNTAX . including INTERVAL-SET . op intervalsOf : Formula -> IntervalSet . vars I J : Interval . vars F F' : Formula . var P : Proposition . eq intervalsOf(Equals(I,J)) = I,J . eq intervalsOf(Before(I,J)) = I,J . eq intervalsOf(Overlaps(I,J)) = I,J . eq intervalsOf(Meets(I,J)) = I,J . eq intervalsOf(Contains(I,J)) = I,J . eq intervalsOf(Starts(I,J)) = I,J . eq intervalsOf(Ends(I,J)) = I,J . eq intervalsOf(Holds(P,I)) = I . eq intervalsOf(Occurs(P,I)) = I . eq intervalsOf(true) = empty . eq intervalsOf(false) = empty . eq intervalsOf(F /\ F') = intervalsOf(F), intervalsOf(F') . eq intervalsOf(F \/ F') = intervalsOf(F), intervalsOf(F') . eq intervalsOf(F -> F') = intervalsOf(F), intervalsOf(F') . eq intervalsOf(! F) = intervalsOf(F) . endfm fmod ALLEN2LTL is including LTL-BOX-SYNTAX . including INTERVALS-OF . op in : Interval -> Proposition . op psi : IntervalSet -> Formula . vars I J : Interval . var Is : IntervalSet . eq psi(I) = <> in(I) /\ ! <>(in(I) /\ <>(! in(I) /\ <> in(I))) . eq psi(I,J,Is) = psi(I) /\ psi(J,Is) . ops `[_`] `{_`} : Formula -> Formula . var P : Proposition . vars F F' : Formula . eq [Equals(I,J)] = [](in(I) <-> in(J)) . eq [Before(I,J)] = <>(in(I) /\ <>(! in(I) /\ ! in(J) /\ <> in(J))) . eq [Meets(I,J)] = <>(in(I) /\ <> in(J) /\ ! <>(in(I) /\ in(J)) /\ ! <>(! in(I) /\ ! in(J) /\ <> in(J))) . eq [Overlaps(I,J)] = <>(in(I) /\ ! in(J) /\ <>(in(I) /\ in(J) /\ <>(! in(I) /\ in(J)))) . eq [Contains(I,J)] = <>(in(I) /\ ! in(J) /\ <>(in(I) /\ in(J) /\ <>(in(I) /\ ! in(J)))) . eq [Starts(I,J)] = [](in(I) -> in(J)) /\ ! <>(in(J) /\ ! in(I) /\ <> in(I)) /\ <>(in(J) /\ ! in(I)) . eq [Ends(I,J)] = [](in(I) -> in(J)) /\ <>(in(J) /\ ! in(I)) /\ ! <>(in(J) /\ in(I) /\ <>(in(J) /\ ! in(I))) . eq [Holds(P,I)] = [](in(I) -> P) . eq [Occurs(P,I)] = <>(in(I) /\ P) . eq [true] = true . eq [false] = false . eq [F /\ F'] = [F] /\ [F'] . eq [F \/ F'] = [F] \/ [F'] . eq [! F] = ! [F] . eq {F} = [F] /\ psi(intervalsOf(F)) . endfm fmod TEST is including ALLEN2LTL . ops a b c d x y z : -> Proposition . ops i j k : -> Interval . op hungry : -> Proposition . ops Nhb Gb Hb @tree H @x Gx2tree L C CD : -> Interval . ops formula1 formula2 formula3 formula4 : -> Formula . eq formula1 = Meets(Nhb,Gb) /\ Meets(Gb,Hb) /\ During(Gb,@tree) /\ During(Gb,H) . eq formula2 = Meets(@x,Gx2tree) /\ Meets(Gx2tree,@tree) /\ During(Gx2tree,L) . eq formula3 = Meets(L,C) /\ Meets(C,H) /\ Meets(H,CD) /\ Meets(CD,L) /\ During(C,@tree) . eq formula4 = Occurs(hungry,Nhb) /\ Holds(hungry,Gb) /\ Holds(hungry,Hb) . endfm red {formula1 /\ formula2 /\ formula3 /\ formula4} .