Safe Haskell	None
Language	Haskell2010

FSM.Logic

Contents

Definition of the CTL language
Implementation of the model checking algorithm for CTL

Synopsis

data CTL a
- = Atom a
- | Not (CTL a)
- | And (CTL a) (CTL a)
- | Or (CTL a) (CTL a)
- | EX (CTL a)
- | EF (CTL a)
- | EG (CTL a)
- | AX (CTL a)
- | AF (CTL a)
- | AG (CTL a)
- | EU (CTL a) (CTL a)
- | AU (CTL a) (CTL a)
checkCTL :: Eq a => CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool

Definition of the CTL language

data CTL a Source #

This is the definition of the CTL language. More info about this language can be found here. You can find the details of the constructors in the definition of the CTL data.

Here you can find a visual explanation of the constructors defined below. CTL examples

Source: A SAFE COTS-BASED DESIGN FLOW OF EMBEDDED SYSTEMS by Salam Hajjar

Constructors

Atom a	It defines an atomic statement. E.g.: `Atom` `"The plants look great."`
Not (CTL a)
And (CTL a) (CTL a)
Or (CTL a) (CTL a)
EX (CTL a)	`EX` means that the `CTL` formula holds in at least one of the inmediate successors states.
EF (CTL a)	`EF` means that the `CTL` formula holds in at least one of the future states.
EG (CTL a)	`EG` means that the `CTL` formula holds always from one of the future states.
AX (CTL a)	`AX` means that the `CTL` formula holds in every one of the inmediate successors states.
AF (CTL a)	`AF` means that the `CTL` formula holds in at least one state of every possible path.
AG (CTL a)	`AG` means that the `CTL` formula holds in the current states and all the successors in all paths. (It is true globally)
EU (CTL a) (CTL a)	`EU` means that exists a path from the current state that satisfies the first `CTL` formula until it reaches a state in that path that satisfies the second `CTL` formula.
AU (CTL a) (CTL a)	`AU` means that every path from the current state satisfies the first `CTL` formula until it reaches a state that satisfies the second `CTL` formula.

Instances

Instances details

Eq a => Eq (CTL a) Source #
Instance details Defined in FSM.Logic Methods (==) :: CTL a -> CTL a -> Bool # (/=) :: CTL a -> CTL a -> Bool #
Ord a => Ord (CTL a) Source #
Instance details Defined in FSM.Logic Methods compare :: CTL a -> CTL a -> Ordering # (<) :: CTL a -> CTL a -> Bool # (<=) :: CTL a -> CTL a -> Bool # (>) :: CTL a -> CTL a -> Bool # (>=) :: CTL a -> CTL a -> Bool # max :: CTL a -> CTL a -> CTL a # min :: CTL a -> CTL a -> CTL a #
Show a => Show (CTL a) Source #
Instance details Defined in FSM.Logic Methods showsPrec :: Int -> CTL a -> ShowS # show :: CTL a -> String # showList :: [CTL a] -> ShowS #

Implementation of the model checking algorithm for CTL

checkCTL :: Eq a => CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool Source #

This is the function that implements the model checking algorithm for CTL as defined by Queille, Sifakis, Clarke, Emerson and Sistla here and that was later improved.

This function takes as an argument a CTL formula, an Automata and information about the states as defined in FSM.Automata and FSM.States respectively and checks whether the Automata implies the CTL formula. Once the algorithm has finished, you just need to look at the value in the initial state of the automata to know if it does, for example with:

Map.lookup (getInitialState Automata) (checkCTL CTL Automata AutomataInfo)