src/library/Logic/Model.hs
{-|
Description : Data structures that represent models of temporal logic.
Maintainer : Guilherme G. Azzi <ggazzi@inf.ufrgs.br>
Stability : provisional
-}
{-# LANGUAGE TypeFamilies #-}
module Logic.Model
(
-- * Kripke structures
KripkeStructure(..)
, State(..)
, Transition(..)
-- ** Looking up states
, stateIds
, lookupState
, getState
-- ** Looking up transitions
, transitionIds
, lookupTransition
, getTransition
-- ** Lookup by adjacency
, nextStates
, precedes
, prevStates
, follows
-- * Utilities for labeled elements
, Element(..)
, findById
) where
import Data.Maybe
-- | A Kripke structure is composed of a list of states and a list of
-- transitions between such states. States are labeled with the atomic
-- propositions that hold in it.
--
-- This particular kind of labeled transition system may be used as a model
-- for temporal logics. In particular, it may be used for model checking.
--
-- This structure is polymorphic on the type of atomic propositions.
data KripkeStructure a = KripkeStructure
{ states :: [State a] -- ^ List of labeled states of the Kripke structure
, transitions :: [Transition a] -- ^ List of transitions of the Kripke structure
}
deriving (Show, Read, Eq)
-- | A state contains its unique identifier and a list of atomic
-- propositions that hold in it.
data State a
= State Int [a]
deriving (Show, Read, Eq)
-- | A transition contains the identifiers of the source and target states.
data Transition a = Transition
{ transitionId :: Int
, source :: Int
, target :: Int
, transitionPayload :: [a]
}
deriving (Show, Read, Eq)
-- | List of all state IDs from a given Kripke structure
stateIds :: KripkeStructure a -> [Int]
stateIds =
map elementId . states
-- | Finds the state with given ID in the given Kripke structure
lookupState :: Int -> KripkeStructure a -> Maybe (State a)
lookupState i =
findById i . states
-- | Gets the state with given ID in the given Kripke structure, __fails if there is none__.
getState :: Int -> KripkeStructure a -> State a
getState i =
fromJust . lookupState i
-- | List of all transition IDs on a given Kripke structure
transitionIds :: KripkeStructure a -> [Int]
transitionIds =
map elementId . transitions
-- | Finds the transition with given ID in the given Kripke structure.
lookupTransition :: Int -> KripkeStructure a -> Maybe (Transition a)
lookupTransition i =
findById i . transitions
-- | Gets the transition with given ID in the given Kripke structure, __fails if there is none__.
getTransition :: Int -> KripkeStructure a -> Transition a
getTransition i =
fromJust . lookupTransition i
-- | Obtains the IDs of the states that are reachable by a single transition
-- from the state with given ID.
nextStates :: KripkeStructure a -> Int -> [Int]
nextStates (KripkeStructure _ transitions) state =
map target $ filter (\t -> source t == state) transitions
-- | Tests if the first given state is reachable from the second by a single transition
follows :: KripkeStructure a -> Int -> Int -> Bool
follows ts s1 s2 =
s1 `elem` nextStates ts s2
-- | Obtains the IDs of the states from which the given state is reachable by a single transition.
prevStates :: KripkeStructure a -> Int -> [Int]
prevStates (KripkeStructure _ transitions) state =
map source $ filter (\t -> target t == state) transitions
-- | Tests if the second given state is reachable from the first by a single transition
precedes :: KripkeStructure a -> Int -> Int -> Bool
precedes ts s1 s2 =
s1 `elem` prevStates ts s2
-- | Type class for elements that have a numeric identifier and a list of associated values.
class Element e where
-- | Type of associated values.
type Payload e :: *
-- | Obtain the numeric identifier of an element.
elementId :: e -> Int
-- | Obtain the associated values of an element.
values :: e -> [Payload e]
instance Element (State a) where
type Payload (State a) = a
elementId (State i _) = i
values (State _ v) = v
instance Element (Transition a) where
type Payload (Transition a) = a
elementId = transitionId
values = transitionPayload
-- | Given a list of elements, find the element with the given identifier.
findById :: Element a => Int -> [a] -> Maybe a
findById i elems =
listToMaybe $ filter (\e -> elementId e == i) elems