One of my big interests in computer science is the notion of programs that treat
other programs as data. This includes compilers, interpreters, and programs
that prove properties of other programs. Since this is the first real post to
this blog, I thought I'd make it a good one: model checking.
This post is a literate haskell program (in "Bird style"). A plain text version is
available at:
http://aaron.13th-floor.org/src/model-checking/ctl-checker.lhs
You should be able to compile it directly using GHC.
Today's problem is the following: Suppose we have a program that looks vaguely
like:
do{
cmd <- waitForInput;
resp <- executeCommand cmd;
if resp == Failure
errorflag <- true;
exit;
else
print "Success"
}while(true)
And we would like to prove that whenever we get to the top of the loop, there is
some way for the program to eventually output "Success"
This is a toy example so we can tell by looking that if (and only if)
executeCommand returns something other than Failure then the program will
eventually print "Success" (most of you probably arrived at this using an
informal mental process similar to proving Hoare triples using Djikstra's
Weakest Precondition; that's not what we're doing today..maybe later). Our
approach will be different, instead of looking at the program as a sentence in
some axiomatic system (a la Hoare, Djikstra et al) we will look at it as a
non-deterministic state machine and we will verify our property by showing that
there exist runs of the machine which by waiting for input, and eventually
transition to writing output. In short, we will be writing a model checker.
Specifically we will write an explicit state Computation Tree Logic (CTL) model
checker.
Before we begin, we need to import a number of packages for manipulating basic
data types.
> import Array
> import List
> import Maybe
We'll also be using Parsec to build parsers for state transition systems, and
CTL propositions so we need a number of packages for that:
> import System.Environment
> import Text.ParserCombinators.Parsec.Language
> import Text.ParserCombinators.Parsec
> import Text.ParserCombinators.Parsec.Expr
> import qualified Text.ParserCombinators.Parsec.Token as P
We also need a couple of list manipulation functions that aren't part of the
List package. We'll get them out of the way here
> difference :: Eq a => [a] -> [a] -> [a]
> difference xs ys = [x | x <- xs, not (any (\y -> x == y) ys)]
>
> elemOf :: Eq a => [a] -> a -> Bool
> elemOf [] _ = False
> elemOf (y:ys) x = if x == y then True else elemOf ys x
Explicit state model checking roughly involves verifying properties of state
transition systems by searching the state space to show that the property holds
for all reachable states in the system.
To do this we'll need three key elements:
- A representation of state transition systems
- A logic for specifying the properties we wish to check
- Routines which can verify that a system does (or doesn't) exhibit a
particular property.
Specifically the state transition systems we wish to model are known as ;Kripke
structures and are defined by a finite set of states (including a distinguished
initial state), a set of atomic propositions (i.e., facts that may be true or
false) a function which given a state returns the set of propositions that are
true in the state, a transition function which given the current state of the system
returns the set of states to which the system may transition.
A Kripke structure could be defined by two enumerated data types (one for
states, and one for propositions), an element of the state type defined to be
the initial state, a function from states to lists of propositions, and a
transition function mapping states to lists of states.
> data ExampleState = Waiting | Executing | Success | Failure
> data ExampleProposition = AcceptingInput | OutputReady | ErrorFlag
> exampleInitialState = Waiting
> examplePropsForState :: ExampleState -> [ExampleProposition]
> examplePropsForState Waiting = [AcceptingInput]
> examplePropsForState Executing = []
> examplePropsForState Success = [OutputReady]
> examplePropsForState Failure = [ErrorFlag]
> exampleTransitions :: ExampleState -> [ExampleState]
> exampleTransitions Waiting = [Waiting, Executing]
> exampleTransitions Executing = [Success, Failure]
> exampleTransitions Success = [Waiting]
> exampleTransitions Failure = [Failure]
This would work well if our goal was to actually execute the system. We could
write functions like:
> exampleStatesAfterNSteps :: Int -> [ExampleState]
> exampleStatesAfterNSteps n = statesAfterNStepsFrom n exampleInitialState
> where statesAfterNStepsFrom n state = if n == 0
> then [state]
> else (concatMap
> (statesAfterNStepsFrom (n - 1))
> (exampleTransitions state))
But that's not really what we're after here. Our goal is to be able to verify
more interesting properties about transition systems. For example, we may want
to know that it is always the case that the system will eventually accept more
input, or raise the error flag. For this we'll need to represent Kripke
structures as first class objects (types aren't first class objects, so neither
is our above definition; we can't pass it as an argument to a function!).
Kripke structures can be thought of as directed graphs where each node
corresponds to a state and is labeled by the atomic propositions that are true
in that state, and edge between two states indicates that the system may
transition from the source state to the destination.
We'll enhance this just a little and allow the user to provide descriptive names
for the states. Both state names and atomic propositions will be represented as
strings, so we'll add some type aliases to help keep things straight.
> type StateIdx = Int
> type StateName = String
> type AtomicProp = String
We'll represent kripke structures as an array of nodes and an adjacency matrix
describing the edges of the graph. (sidenote: from here on out I'll tend to use
the terms Graph and Node rather than Kripke Structure and State; for the
purposes of this discussion the terms are synonymous).
> type Matrix b = Array StateIdx (Array StateIdx b)
> data Kripke = K {ss :: Array StateIdx (StateName,[AtomicProp]),
> es :: Matrix Bool}
Many times we want to talk about states in isolation (rather than whole
systems), but in order to get the state's successors, predecessors, etc we need
to haul the graph around, and know the state's index in the node array. To ease
this burden, we'll introduce a new type for states.
> data State = S {idx :: StateIdx,
> name :: StateName,
> props :: [AtomicProp],
> sys :: Kripke
> }
Hopefully this all makes sense and seems fairly natural thus far. Before we
move on to CTL, we'll introduce some basic functions for playing with kripke
structures and states
Get a particular state
> state :: StateIdx -> Kripke -> State
> state i g = S i (fst s) (snd s) g
> where s = (ss g)!i
Get a list of all the states:
> states :: Kripke -> [State]
> states g = map (\x -> state x g) (indices.ss $ g)
Impose an ordering on states (we'll just assume they belong to the same system)
> instance Ord State where
> compare a b = compare (idx a) (idx b)
Equality on states (again assuming same system)
> instance Eq State where
> a == b = (idx a) == (idx b)
And we'd like to print out states (this should really be done using shows to
avoid the non-tail recursive appending, but meh).
> instance Show State where
> show n = "{"++(name n)++"}"
Get all the successors of a given state (i.e., the states to which the system may
transition from the given state)
> successors :: State -> [State]
> successors s = [s' | s' <- (states.sys $ s), (es.sys $ s)!(idx s)!(idx s')]
And actually making a kripke structure from a list of pairs describing atomic propositions
and adjacencies
> mk_kripke :: [((StateName, [AtomicProp]), [StateIdx])] -> Kripke
> mk_kripke xs = (K
> (listArray (0,(length xs)-1) (map fst xs))
> (listArray (0,(length xs)-1)
> (map (\x -> (array (0,(length xs)-1)
> [(i,any (\z -> z == i) (snd $ x))
> | i <- [0..(length xs)-1]]))
> xs)))
>
Now we can model the example Kripke structure above using this representation
> exampleKripke = mk_kripke [(("Waiting", ["AcceptingInput"]), [1]),
> (("Executing", []), [2, 3]),
> (("Success", ["OutputReady"]), [0]),
> (("Failure", ["ErrorFlag"]), [3])]
And we can write a generic version of the statesAfterNSteps function:
> statesAfterNSteps :: Kripke -> Int -> [StateName]
> statesAfterNSteps g n = map name (statesAfterNStepsFrom n (state 0 g))
> where statesAfterNStepsFrom n s = if n == 0
> then [s]
> else (concatMap
> (statesAfterNStepsFrom (n - 1))
> (successors s))
Great, that's all we need as far as Kripke/Graph manipulation functions. Now's
probably a good time to grab a beer or something. We're moving into deeper
waters pretty soon.
It's time to start thinking about CTL.
CTL is like propositional logic, except that instead of expressions being
evaluated with respect to a state (a mapping of truth-values to atomic
propositions), the expressions are evaluated with respect to a Kripke structure
in some state
CTL includes all the standard operators of propositional logic like /\ (and), \/ (or),
and ~ (not). But adds a notion of time.
Specifically CTL uses a branching notion of time (hence Tree logic). The idea
is that the current state is the root of a tree, all of the successors of the
current states are the children of the root, and their successors are the
grand-children of the root (arranged properly). One can think of this as an
unrolling the graph of the Kripke structure into an infinite height tree by
inserting fresh copies of each node everytime it appears. In the example kripke
system above, the first few levels of the tree might look like:
> data ExampleStateTree = ExTree (ExampleState, [ExampleStateTree])
> exampleTree :: ExampleStateTree
> exampleTree = ExTree (Waiting,
> [ExTree (Executing,
> [ExTree (Success,
> [ExTree (Waiting,
> [ExTree (Executing,
> [ExTree (Success, []),
> ExTree (Failure, [])])])]),
> ExTree (Failure,
> [ExTree (Failure,
> [ExTree (Failure,
> [ExTree (Failure, [])])])])])])
To handle the branching time concept, CTL includes two operators for quantifying
over paths: forall paths (written A), and there exists a path (written E). In
CTL all temporal operators must be quantified using one of these two operators
(this is not true for CTL*).
The primitive temporal operators of CTL are: next, always, and until. Combining
these operators with modalities and propositional phrases allows statements such
as:
AX(y)
meaning:
"on all paths (from the current state) the proposition 'y' is true in the
next state"
and:
E (x U y)
meaning:
"there exists a path (from the current state) the proposition 'x' is true
until the proposition 'y' is true (and 'y' is eventually true)."
Other common operators in CTL finally (F), release (R), and the weak until which
can be derived as:
AF x = A(true U x)
A(x R y) = A(~ (~ x U ~ y) )
A(x W y) = A(y R (y \/ x))
Note: the same derivations hold for quantification using E instead of A.
The release operator may not be immediately obvious, the intuition is that x R y
states that y must be true until both y and x are true at the same time,
i.e. that x releases the obligation of holding y true. Weak until is like the
normal until but without the obligation that the second propisition ever become
true (in CTL* we could write x W y as ((x U y) \/ G x), but this would not be
valid CTL because the two temporal operators would be grouped under the same
path quantifier which is invalid).
This isn't a very rigorous discussion of CTL, but it should get the gist of it
across. And it is detailed enough that we can express the property we wish to
prove as a CTL proposition:
(AcceptingInput /\ EF OutputReady)
As we move through the model checker you will see the exact semantics of each
operator of CTL and later the complete syntax for the language (since we'll be
writing a parser).
The important question now is: how should we represent CTL expressions? An
obvious choice might be to represent propositions as:
> type Prop_ex1 = State -> Bool
One attractive feature of this is we might be able to write our checker very
easily as:
> check_ex1 :: Prop_ex1 -> Kripke -> Bool
> check_ex1 p g = p (state 0 g)
The problem is that while we can write some of the basic CTL operators very
easily with this representation as in:
> andp_ex1 :: Prop_ex1 -> Prop_ex1 -> Prop_ex1
> andp_ex1 p1 p2 = (\n -> if (p1 n) then (p2 n) else False)
> orp_ex1 :: Prop_ex1 -> Prop_ex1 -> Prop_ex1
> orp_ex1 p1 p2 = (\n -> if (p1 n) then True else (p2 n))
These aren't too bad, but we'll see later on that writing the temporal operators
out in this way would be quite bothersome. Instead of using a checker like
check_ex1, our approach will be to determine the set of all states which satisfy
the CTL proposition, then checking to see if the initial state is in that set.
This suggests the following type for propositions:
> type Prop = [State] -> [State]
This has the nice properties that Propositions are composable, and don't require
a special evaluator function. We can now easily write the basic operators from
propositional logic:
> satisfies :: AtomicProp -> Prop
> satisfies a ss = [s | s <- ss, any (\b -> b==a) (props s)]
>
> notp :: Prop -> Prop
> notp p ss = difference ss (p ss)
>
> orp :: Prop -> Prop -> Prop
> orp p1 p2 ss = union (p1 ss) (p2 ss)
>
> andp :: Prop -> Prop -> Prop
> andp p1 p2 ss = p2.p1 $ ss
Note how elegant the definition of /\ becomes; because propositions act like
filters composition acts like conjunction. Very sexy.
The most basic temporal operator in CTL is next. Since we know that temporal
operators are always paired with path quantifiers, we will write two
propositions for next: one quantified by exists, the other by forall.
> exists_next :: Prop -> Prop
> exists_next p ss = [s | s <- ss, (p.successors $ s) /= []]
>
> forall_next :: Prop -> Prop
> forall_next p ss = [s | s <- ss, (difference (successors s)
> (p.successors $ s)) == []]
Next is fairly simple because it only needs to consider a predefined set of
states: the successors of the currents state. But how can we represent the more
forward looking operators like Always or Until? There's no way to know how far
into the future we need to look to verify these.
This is where we begin to really motivate the choice of representation for Prop.
The approach we take relies on two key observations:
1) A Kripke structure contains a finite number of states
2) The remaining CTL temporal operators can be expressed as greatest or
least fixed points of monotonic functions on the lattice of sets of states
of the Kripke structure.
The first point is hopefully obvious, the second requires a bit of explaining.
A lattice is just a collection of elements with a partial ordering and the
property that any two elements have a greatest lower bound and a least upper
bound (and consequently any finite, nonempty set of elements which is the real
definition). In this case the elements are sets of states, and the ordering is
the subset relation.
For example if
> set1_ex1 = [Waiting, Executing]
> set2_ex1 = [Executing, Failure]
> set3_ex1 = [Waiting, Executing, Failure]
> set4_ex1 = [Executing]
Then both set3_ex1 is the least upper bound of set1_ex1 and set2_ex1, that is
set3_ex1 is the smallest set that contains both set1_ex1 and set2_ex1 as
subsets. And set4_ex1 is the greatest lower bound of set1_ex1, and set2_ex1.
An important sidenote is that the least upper bound may also be called the LUB,
the join, or the supremum and the greatest lower bound may be called the GLUB,
the meet, or the infimum).
All finite lattices have a top element that is greater than all other elements
and a bottom element that is less than all other elements. In the case of a
lattice where the elements are the subsets of some other set, the top is the
original set and the bottom is the empty set.
In our case this would be:
> top_ex1 = [Waiting, Executing, Success, Failure]
> bottom_ex1 = []
A monotonic function (f) on a lattice is one for which either
x <= (f x) for all x or (f x) >= x
Which is to say that the function either always moves up the lattice, or always
moves down the lattice. An important theorem of lattice theory states that a
montonic function on a finite lattice has a unique least and greatest fixed
points (this is actually a corrolary to the stronger Knaster Tarski theorem
which states that any order preserving function on a complete lattice has a
complete lattice of fixed points, but that is irrelevent). The effect of this
is both obvious and profound at the same time; if you keep moving up
(respectively down) a finite lattice, you eventually stop.
To write our functions for the other temporal operators of CTL, we need to
understand the sense in which these operators are fixpoints of recursive
functions on the lattice of sets of states.
Let's start with AG (forall always)
The key observation is to see that a state satisfies (AG p) if and only if the
state satisfies p, and all of its successors also satisfy (AG p).
This suggests a strategy for defining forall_always: start by considering all
states satisfying p as candidates, then recursively eliminate candidates which
don't satisfy (forall_next p) setting p <- (forall_next p) at each recursion.
> forall_always_ex1 p xs = helper p (p xs)
> where helper p' candidates = let candidates' = (intersect candidates
> (p' candidates)) in
> if candidates' == candidates
> then candidates
> else (helper (forall_next
> (intersect candidates))
> candidates')
The key here is that at each recursive call to helper, candidates' must be a
subset of candidates so eventually it must either reach the empty list (the
bottom of the lattice), or the two will be equal. This is what is meant by a
greatest fixed point. We start at the top of the lattice (the set of all
states) and at each recursion we move step down the lattice (to some subset of
the previous candidate set) until we get stuck. This is guaranteed to work
because the lattice is finite (size = 2 ^ number of states), and the candidate
set shrinks at every stage.
In fact we can generalize the structure of the helper function above into a
greatest fixed point operator
> gfp :: Prop -> Prop
> gfp f ss = let ss' = intersect ss $ f ss in
> if ss' == ss then ss else gfp f ss'
No we can define forall_always easily as:
> forall_always :: Prop -> Prop
> forall_always p g = gfp (\ss -> forall_next (intersect ss) ss) (p g)
exists_always, forall_release, and exists_release are all greatest fixed points
and can be defined simarly
> exists_always :: Prop -> Prop
> exists_always p g = gfp (\ss -> exists_next (intersect ss) ss) (p g)
>
> forall_release :: Prop -> Prop -> Prop
> forall_release p1 p2 g = gfp (\ss -> (orp p1
> (andp (forall_next (intersect ss)) p2)
> ss)) (p2 g)
>
> exists_release :: Prop -> Prop -> Prop
> exists_release p1 p2 g = gfp (\ss -> (orp p1
> (andp (exists_next (intersect ss)) p2)
> ss)) (p2 g)
The other operators (forall/exists_eventually and forall/exists_until) are least
fixed point operators. With these we begin by assuming that no states satisfy
the proposition and add nodes from a candidate set until we either run out of
states to add.
We'll start by defining forall_eventually analogously to how we defined
forall_always_ex1 above. Clearly any state in (p x) should also be in
(forall_eventually p x), as should any state satisfying (forall_next p x), and
(forall_next (forall_next p x)), and so on.
> forall_eventually_ex1 :: Prop -> Prop
> forall_eventually_ex1 p xs = helper p (p xs) (difference xs (p xs))
> where helper p sats cs = let newsats = p cs in
> if newsats == [] then sats
> else let sats' = union sats newsats in
> (helper (forall_next (intersect sats')) sats'
> (difference cs newsats))
Note that in the least fixpoint case we have to track two different sets of
state: those states which definitely satisfy the proposition (called sats) and
those which we have yet to consider (called cs for candidates). At each step we
find the elements in cs for which all successors are known to satisfy the
previous proposition and move them to sats. We then recur with the new set of
satisfying nodes and candidates.
Like the greatest fixed point function, we can generalize the structure of
forall_eventually_ex1 into a least fixed point function:
> lfp :: ([State] -> Prop) -> [State] -> Prop
> lfp f ss c = let ss' = union ss $ f ss candidates in
> if ss' == ss then ss else lfp f ss' candidates
> where candidates = difference c ss
Then define forall_eventually in terms of lfp:
> forall_eventually :: Prop -> Prop
> forall_eventually _ [] = []
> forall_eventually p (s:ss) = intersect (s:ss) fp
> where fp = lfp (\ss -> forall_next (intersect ss)) (p allss) allss
> allss = states.sys $ s
This is a bit peculiar we would really prefer the definition to just be the
fp = ...
part as it is for the greatest fixed point operators. But that doesn't actually
work in this case. To see why consider the following proposition:
AcceptingInput /\ (EF OutputReady)
If we define exists_eventually the way we'd like to as:
> exists_eventually_ex1 :: Prop -> Prop
> exists_eventually_ex1 p ss = lfp (\ss -> exists_next (intersect ss)) (p ss) ss
then we could evaluate this proposition on our example system using
> evaluate_ex1 = andp (satisfies "AcceptingInput")
> (exists_eventually_ex1 (satisfies "OutputReady"))
> (states exampleKripke)
By inspection we can see that the Waiting state does satisfy this property:
AcceptingInput is true,
and OutputReady is true in the Success state which is reachable via the path
Waiting -> Executing -> Success.
But evaluate_ex1 is []. What happened? If we unfold the andp from the
expression above we see the problem:
exists_eventually_ex1 (satisfies "Success")
(satisfies "AcceptingInput" (states exampleKripke))
The proposition (satisfies "AcceptingInput" ...) will return only the node
Waiting so when the exists_eventually_ex1 is unfolded we'll get
lfp (\ns -> exists_next (intersect ns)) (satisfies "Success" Waiting)
(satisfies "Success" Waiting)
But Waiting doesn't satisfy Success, so the initial candidate set will be empty
and thus no states will ever be added. Instead we need to start the candidate
set as all states in the system, and intersect with the true candidate set at
the end.
> exists_eventually :: Prop -> Prop
> exists_eventually _ [] = []
> exists_eventually p (s:ss) = intersect (s:ss) fp
> where fp = lfp (\ss -> exists_next (intersect ss)) (p allss) allss
> allss = states.sys $ s
> forall_until :: Prop -> Prop -> Prop
> forall_until _ _ [] = []
> forall_until p1 p2 (s:ss) = intersect (s:ss) fp
> where fp = lfp (\ss -> andp (forall_next (intersect ss)) p1) (p2 allss) allss
> allss = states.sys $ s
> exists_until :: Prop -> Prop -> Prop
> exists_until _ _ [] = []
> exists_until p1 p2 (s:ss) = intersect (s:ss) fp
> where fp = lfp (\ss -> andp (exists_next (intersect ss)) p1) (p2 allss) allss
> allss = states.sys $ s
That's the end of the actual program logic. Now all we need is a parser for CTL
formulas, a parser for Kripke structures, and a main function that ties
everything together.
Parsec provides some great machinery for writing top down recursive descent
parsers. The basic idea is that we must write functions which recognize each
terminal in our target grammar, and then build functions for recognizing
non-terminals through composition of recognizers as specified by the grammar
rules. Parsec can be a little daunting at first because it uses a lot of rather
peculiar looking types, don't worry; it's easier than it looks. For full
information See the Parsec web page:
;http://legacy.cs.uu.nl/daan/parsec.html;
We'll begin with the Kripke parser.
We'll use a pretty simple format for kripke structure specification, we just
want to read things like:
state "waiting": props: [accepting_input] goes_to: ["executing"]
state "executing": props: [] goes_to: ["success", "failure"]
state "success": props: [output_ready] goes_to: ["waiting"]
state "failure": props: [error_flag] goes_to: ["failure"]
The grammar for this simple Kripke structure language looks like:
kripke ::= <statedef> <statedeflist>
stateDef ::= state <statename>: props: [<proplist>] goes_to: [<statenamelist>]
stateName ::= string_literal
prop ::= <propstart> <propchars>
propStart ::= <lowercase>
|= _
propChars ::= <propchar><propchars>
|=
propChar ::= <propstart>
|= <digit>
stateDefList ::= <satedef> <statedeflist>
|=
propList ::= <prop>, <proplist>
|=
stateNameList ::= <statename>, <statenamelist>
|=
This grammar is completely unambiguous which makes the parser fairly easy to
write. The parser is a function which given a String produces either an error,
or a Graph (as defined earlier) thus, it will have the type:
> parse_kripke :: String -> Either ParseError Kripke
The definition of mk_kripke depends on how we choose to represent parsed state
definitions. In order to use the mkgraph function to build a graph from a list
of nodes we would like the state parsing function to return triples like;
((name, propositions), destinations)
Unfortunately, that won't work. The transitions are described by state names in
the input file but mkgraph expects them to be node indices. What we need is a
lookup function that given a state name and a list of (index, name) pairs will
return the correct index:
> state_lookup :: String -> [(Int, String)] -> Maybe Int
> state_lookup _ [] = Nothing
> state_lookup s ((idx,name):xs) = if s == name then Just idx else state_lookup s xs
This would do the trick, except that the language has to allow for forward
references to states (i.e., a state can transition to a state that hasn't been
defined yet, and thus doesn't have an index). So we can't simply call
state_lookup while parsing each state because we don't yet know the complete
mapping between states and indexes. To get around this, we use the power of
first order functions to give the state parser the type:
> k_state :: Parser ((StateName, [AtomicProp]), [[(Int, String)] -> Maybe StateIdx])
Similarly parsing a state_list returns a list of these beasts
> k_state_list :: Parser [((StateName, [AtomicProp]), [[(StateIdx, String)] -> Maybe StateIdx])]
This makes parse_kripke a bit more complicated because it is now responsible for
generating the (index, state) mapping, and then evaluating the last component of
each parsed state to generate the appropriate argument to pass to mkgraph.
> parse_kripke s = case parse (do{p <- k_state_list ; eof ; return p}) "" s of
> Left err -> Left err
> Right ns -> Right $ mk_kripke.map (\n -> resolve n) $ ns
> where resolve (x,ts) = (x,mapMaybe (\t -> t idxes) ts)
> idxes = gen_index 0 (map (fst.fst) ns)
> gen_index _ [] = []
> gen_index i (x:xs) = (i,x):(gen_index (i+1) xs)
From here on out, Parsec does the heavy lifting for us. We just define Parsers
for each of the non-terminals in the Kripke grammar and string them together as
needed.
As such, the commentary becomes rather sparse bordering on non-existant. After
all, this isn't really meant to be a Parsec tutorial. If you're really curious
about what's going on read this in parallel with the Parsec documentation,
otherwise I'd recommend just taking it on faith that this is a parser.
> k_atomic_prop :: Parser String
> k_state_name :: Parser String
> k_prop_list :: Parser [String]
> k_trans_list :: Parser [String]
> kripke_lexer = P.makeTokenParser (emptyDef {reservedNames = ["state", "props",
> "goes_to"],
> identStart = lower <|> char '_',
> identLetter = alphaNum <|> char '_'
> })
> whiteSpace = P.whiteSpace
> k_atomic_prop = P.identifier ctl_lexer
> k_state_name = P.stringLiteral kripke_lexer
> k_reserved = P.reserved kripke_lexer
> k_squares = P.squares kripke_lexer
> k_sep = P.commaSep kripke_lexer
> k_colon = P.colon kripke_lexer
> k_prop_list = do k_reserved "props" ;
> k_colon ;
> x <- k_squares (k_sep k_atomic_prop) ;
> return x
> k_trans_list = do k_reserved "goes_to";
> k_colon ;
> x <- k_squares (k_sep k_state_name) ;
> return x
> k_state = do k_reserved "state" ;
> n <- k_state_name ;
> k_colon ;
> ps <- k_prop_list ;
> trans <- k_trans_list ;
> return ((n, ps),
> if trans /= []
> then map state_lookup trans
> else [state_lookup n])
> k_state_list = do whiteSpace kripke_lexer ;
> many1 k_state
We're going to be reading Kripke structures from a file, so we might as well
encapsulate that a helper function
> load_kripke :: String -> IO (Either ParseError Kripke)
> load_kripke f = do s <- readFile f
> return $ parse_kripke s
That's it. We're done with the kripke parser! Now on to CTL.
The grammar for CTL propositions looks like this:
prop ::= atomic
|= (prop)
|= ~ prop
|= prop /\ prop
|= prop \/ prop
|= AX prop
|= AX prop
|= AG prop
|= AF prop
|= EG prop
|= EF prop
|= A prop U prop
|= A prop R prop
|= E prop U prop
|= E prop R prop
atomic ::= lowercase [alphaNum_]+
> prop :: GenParser Char () Prop
> prop = buildExpressionParser table basic
> "proposition"
> ctl_lexer = P.makeTokenParser (emptyDef {identStart = lower <|> char '_',
> identLetter = alphaNum <|> char '_',
> reservedOpNames = ["AG", "EG",
> "AX", "EX",
> "AF", "EF",
> "A", "E",
> "U", "R",
> "\\/", "\\/", "~"] })
> ctl_reserved = P.reservedOp ctl_lexer
> ctl_parens = P.parens ctl_lexer
> ctl_atomic_prop = P.identifier ctl_lexer
>
>
> data PropCompletion = Until Prop | Release Prop
>
> make_forall p1 (Until p2) = forall_until p1 p2
> make_forall p1 (Release p2) = forall_release p1 p2
> make_exists p1 (Until p2) = exists_until p1 p2
> make_exists p1 (Release p2) = exists_release p1 p2
>
> partial :: Parser (PropCompletion -> Prop)
> partial = do { ctl_reserved "E" ; p <- prop ; return $ make_exists p}
> <|> do { ctl_reserved "A" ; p <- prop ; return $ make_forall p}
>
> completion :: Parser PropCompletion
> completion = do { ctl_reserved "U" ; p <- prop ; return $ Until p }
> <|> do { ctl_reserved "R" ; p <- prop ; return $ Release p }
>
> basic = ctl_parens prop
> <|> do {p <- ctl_atomic_prop ; return $ satisfies p}
> <|> do {p1 <- partial ; p2 <- completion ; return $ p1 p2 }
>
> table :: OperatorTable Char () Prop
> table = [[pfx "~" notp],
> [pfx "AG" forall_always, pfx "EG" exists_always,
> pfx "AX" forall_next, pfx "EX" exists_next,
> pfx "EF" exists_eventually, pfx "AF" forall_eventually],
> [op "/\\" andp AssocLeft, op "\\/" orp AssocLeft]]
> where
> pfx s f = Prefix (do {ctl_reserved s ; return f})
> op s f assoc = Infix (do {ctl_reserved s ; return f}) assoc
>
>
Ok we made it through the parsers all we have left is to wire stuff
together. Everything's pretty simple except that we have to deal with IO and the
potential for errors and so forth. Nothing really exciting.
>
> check :: Kripke -> String -> IO ([State])
> check g s =
> case parse (do{ whiteSpace ctl_lexer ;
> p <- prop ;
> whiteSpace ctl_lexer ;
> eof ;
> return p}
> ) "" s of
> Left err -> do { putStr "parse error at " ; print err ; return []}
> Right x -> return $ sort.x.states $ g
>
> main =
> do prog <- getProgName ;
> args <- getArgs ;
> case args of
> [] -> putStr $ "Usage "++prog++" <kripke_file> [props...]\n"
> (kf:ps) -> do mk <- load_kripke kf ;
> case mk of
> Left e -> do { putStr $ "parse error at " ;
> print e ;
> return () }
> Right k -> foldl (\a -> \p ->
> do{ ks <- check k p ;
> if elemOf ks (state 0 k)
> then putStr $ "Prop \""++p++"\" holds.\n"
> else putStr $ "Prop \""++p++"\" does not hold.\n"
> })
> (return ()) ps
Saturday, January 24, 2009
CTL Model Checking
Metapost
I'm starting this blog to share the various pieces of code I find particularly interesting. Unlike this first post, all subsequent posts will be heavily commented (often "literate") code. My main areas of interest are security, operating systems, programming language theory/implementation, and formal methods; so most of the posts will be related to one of these themes. Most of the posts will be my original code, but some will be pearls taken from elsewhere (always credited) with added commentary.
Subscribe to:
Posts (Atom)