{-# LANGUAGE DeriveGeneric #-}
module Data.LTS
( LTSState (..)
, Transition (..)
, LTS
, checkTrans
, getFromIds
, getToIds
, sortById
, sortByToSt
, sortByFromSt
, collectTrans
, getStartSt
, getFinalSt
, depth
, Alphabet
, findTransIndex
, transExists
)
where
import Data.Nat
import GHC.Generics
import Data.List (sortBy)
import Data.Ord (comparing)
data LTSState a =
LTSState {stateId::Int
, out::a
}
deriving (Read, Show, Eq, Generic)
instance (Eq a) => Ord (LTSState a) where
compare = comparing stateId
data Transition a b =
Transition { transitionFrom::LTSState a
, transitionGuard::b
, transitionTo::LTSState a
}
deriving (Read, Show, Eq, Generic)
instance (Eq a, Eq b) => Ord (Transition a b) where
compare = comparing transitionFrom
type Alphabet b = [b]
type LTS a b = [Transition a b]
transExists :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> Bool
transExists st x (t:ts) =
(transitionFrom t == st && transitionGuard t == x) || transExists st x ts
findTransIndex :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> Int
findTransIndex st x (t:ts) =
if transExists st x (t:ts)
then index
else error "doesn't exist"
where index = if transitionFrom t == st && transitionGuard t == x
then 0
else 1+ findTransIndex st x ts
nextStateSymbol :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> LTSState a
nextStateSymbol s x ts =
if transExists s x ts
then transitionTo (ts !! findTransIndex s x ts)
else s
nextStateAlphabet :: (Eq a, Eq b) => LTSState a -> Alphabet b -> LTS a b -> LTSState a
nextStateAlphabet s (x:xs) ts =
nextStateAlphabet (nextStateSymbol s x ts) xs ts
checkTrans :: (Eq a, Eq b) => LTSState a -> LTS a b -> Bool
checkTrans st (t:ts) =
stateId st == stateId (transitionFrom t) && checkTrans st ts
getFromIds:: (Eq a, Eq b) => LTS a b -> [Int]
getFromIds = map (stateId . transitionFrom)
getToIds :: (Eq a, Eq b) => LTS a b -> [Int]
getToIds = map (stateId . transitionTo)
sortById :: (Eq a) => [LTSState a] -> [LTSState a]
sortById = sortBy (comparing stateId)
sortByFromSt :: (Eq a, Eq b) => LTS a b -> LTS a b
sortByFromSt = sortBy (comparing transitionFrom)
sortByToSt :: (Eq a, Eq b) => LTS a b -> LTS a b
sortByToSt = sortBy (comparing transitionTo)
collectTrans:: (Eq a, Eq b) => LTSState a -> LTS a b -> Bool -> LTS a b
collectTrans st (t:ts) b =
let op = if stateId st == stateId (transitionFrom t)
then t:collectTrans st ts b
else collectTrans st ts b
in if b then sortByToSt op else op
getStartSt :: (Eq a, Eq b) => LTS a b -> LTSState a
getStartSt ts = transitionFrom (head (sortByToSt (sortByFromSt ts)))
getFinalSt :: (Eq a, Eq b) => LTS a b -> LTSState a
getFinalSt ts = transitionTo (head (sortByToSt (sortByFromSt ts)))
depth :: (Eq a, Eq b) => LTS a b -> LTSState a -> Nat
depth [] _ = 0
depth (t:ts) st
| transitionFrom t == st && (transitionFrom t /= transitionTo t) =
1 + depth ts (transitionTo t)
| otherwise = depth ts st