| Maintainer | Guilherme G. Azzi <ggazzi@inf.ufrgs.br> |
|---|---|
| Stability | provisional |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Logic.Model
Contents
Description
- data KripkeStructure a = KripkeStructure {
- states :: [State a]
- transitions :: [Transition a]
- data State a = State Int [a]
- data Transition a = Transition {
- transitionId :: Int
- source :: Int
- target :: Int
- transitionPayload :: [a]
- stateIds :: KripkeStructure a -> [Int]
- lookupState :: Int -> KripkeStructure a -> Maybe (State a)
- getState :: Int -> KripkeStructure a -> State a
- transitionIds :: KripkeStructure a -> [Int]
- lookupTransition :: Int -> KripkeStructure a -> Maybe (Transition a)
- getTransition :: Int -> KripkeStructure a -> Transition a
- nextStates :: KripkeStructure a -> Int -> [Int]
- precedes :: KripkeStructure a -> Int -> Int -> Bool
- prevStates :: KripkeStructure a -> Int -> [Int]
- follows :: KripkeStructure a -> Int -> Int -> Bool
- class Element e where
- findById :: Element a => Int -> [a] -> Maybe a
Kripke structures
data KripkeStructure a Source #
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.
Constructors
| KripkeStructure | |
Fields
| |
Instances
| Eq a => Eq (KripkeStructure a) Source # | |
| Read a => Read (KripkeStructure a) Source # | |
| Show a => Show (KripkeStructure a) Source # | |
A state contains its unique identifier and a list of atomic propositions that hold in it.
data Transition a Source #
A transition contains the identifiers of the source and target states.
Constructors
| Transition | |
Fields
| |
Instances
| Eq a => Eq (Transition a) Source # | |
| Read a => Read (Transition a) Source # | |
| Show a => Show (Transition a) Source # | |
| Element (Transition a) Source # | |
| type Payload (Transition a) Source # | |
Looking up states
stateIds :: KripkeStructure a -> [Int] Source #
List of all state IDs from a given Kripke structure
lookupState :: Int -> KripkeStructure a -> Maybe (State a) Source #
Finds the state with given ID in the given Kripke structure
getState :: Int -> KripkeStructure a -> State a Source #
Gets the state with given ID in the given Kripke structure, fails if there is none.
Looking up transitions
transitionIds :: KripkeStructure a -> [Int] Source #
List of all transition IDs on a given Kripke structure
lookupTransition :: Int -> KripkeStructure a -> Maybe (Transition a) Source #
Finds the transition with given ID in the given Kripke structure.
getTransition :: Int -> KripkeStructure a -> Transition a Source #
Gets the transition with given ID in the given Kripke structure, fails if there is none.
Lookup by adjacency
nextStates :: KripkeStructure a -> Int -> [Int] Source #
Obtains the IDs of the states that are reachable by a single transition from the state with given ID.
precedes :: KripkeStructure a -> Int -> Int -> Bool Source #
Tests if the second given state is reachable from the first by a single transition
prevStates :: KripkeStructure a -> Int -> [Int] Source #
Obtains the IDs of the states from which the given state is reachable by a single transition.
follows :: KripkeStructure a -> Int -> Int -> Bool Source #
Tests if the first given state is reachable from the second by a single transition