FSM.Logic

Definition of the CTL language

data CTL a

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.

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

Eq a => Eq (CTL a)

Defined in FSM.Logic

Methods

(==) :: CTL a -> CTL a -> Bool

(/=) :: CTL a -> CTL a -> Bool

Ord a => Ord (CTL a)

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)

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

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)