Safe Haskell | None |
---|---|
Language | Haskell2010 |
Definition of the CTL language
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
CTrue | |
CFalse | Basic bools. |
RArrow (CTL a) (CTL a) | Basic imply. |
DArrow (CTL a) (CTL a) | Basic double imply. |
Atom a | It defines an atomic statement. E.g.: |
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) |
|
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 (getInitialStateAutomata
) (checkCTLCTL
Automata
AutomataInfo
)
modelsCTL :: Eq a => CTL a -> Automata -> AutomataInfo (CTL a) -> Bool Source #
This function returns the result of \(automata \models formula \).
checkFormulas :: Eq a => Automata -> AutomataInfo (CTL a) -> [CTL a] -> [Bool] -> [Bool] Source #
This function loops over multiple formulas and tells you if the automata models each formula.