Automatic Model Generation, part 2: Pretty-Printing the Model

In the first part of this guide, I explained part of a technique for generating CSP models from a CHP program — including the introduction of the specification type. In this second part of the guide I take a slight diversion to explain how to pretty-print the specifications. We will see in this part how parallel composition is rendered, which has particular importance in CSP.

After we’ve created the model of our program, we need to print it out to a file, ready to be fed to the proof-checker or other tool. I wanted the model to be as comprehensible as possible after printing, so that users (and I!) can read it. To that end, I used a pretty-printing library: pretty from Hackage, which is imported as PP throughout the code in this post. (After I wrote this code, Marc Fontaine uploaded a library to Hackage produced that supports CSP notation in an AST, but it’s easier for me to keep my original code rather than switch over.)

Sequence

CSP has two forms of sequencing. A semi-colon sequences two processes, whereas an arrow prefixes a process (right-hand side) with an event (left-hand side). My code for printing out a sequence of processes uses the arrow wherever possible, and a semi-colon otherwise:

type ProcEvents = Map.Map String (Set.Set String)

pprintCSP_Seq :: ProcEvents -> Spec' String String -> PP.Doc
pprintCSP_Seq m = PP.parens . PP.sep . p
  where
    p [] = [PP.text "SKIP"]
    p (Sync c : xs) = [name c, PP.text "->"] ++ p xs
    p [x] = [pprintCSP m x]
    p (x:xs) = [pprintCSP m x, PP.text ";"] ++ p xs

The SKIP process does nothing, so it is used for blank lists and at the end of the list. Note that the singleton list [Sync x] will turn into x -> SKIP, whereas [Par xs] will not turn into xs ; SKIP (it will be merely xs). The ProcEvents parameter is used later on for printing out parallel composition and so must be passed around in case there are any nested parallel compositions.

Choice

External choice is handled by the first case of pprintCSP:

pprintCSP :: ProcEvents -> SpecItem' String String -> PP.Doc
pprintCSP m (Alt s) = zeroOneMore m "STOP" (withOp m "[]") s

The helper functions are used to treat differently the case where the list is empty (in which case it uses the second parameter), has one item (in which case it is printed using pprintCSP_Seq), or has multiple items (in which case it is processed using the third parameter, which above joins the items with the external choice operator []):

withOp :: ProcEvents -> String -> [Spec' String String] -> PP.Doc
withOp m op
  = PP.parens . PP.sep . intersperse (PP.text op) . map (pprintCSP_Seq m)

zeroOneMore :: ProcEvents -> String ->
  ([Spec' String String] -> PP.Doc) -> [Spec' String String] -> PP.Doc
zeroOneMore _ z _ [] = PP.text z
zeroOneMore m _ _ [x] = pprintCSP_Seq m x
zeroOneMore _ _ f xs = f xs

Parallel

When you compose two CSP processes in parallel, you must specify the events on which they synchronise. The process (a -> SKIP) [| {|a|} |] (a -> SKIP) will perform the event “a” once, with both sides of the parallel synchronising on event “a” together — that item in the middle is an infix parallel composition operator, parameterised by the singleton set containing “a”. In contrast, the process a -> SKIP [| {| |} |] a -> SKIP (which can be written more simply as: a -> SKIP ||| a -> SKIP) will perform the event “a” twice, with each side of the parallel doing it in turn — this is known as interleaving on an event.

In CHP, there is no support for interleaving; all events are synchronising. However, we cannot just put all events in the synchronising set. The process (a -> SKIP) [| {|a,b|} |] (b -> SKIP) will deadlock — each side tries to synchronise with the other on their respective events, which never happens. The solution is of course to use the intersection of the events that each side engages in:

pprintCSP m (Par xs) = zeroOneMore m "SKIP" joinPar xs
  where
    joinPar :: [Spec' String String] -> PP.Doc
    joinPar [a] = pprintCSP_Seq m a
    joinPar (a:bs) = PP.parens $ PP.sep $ 
      [ pprintCSP_Seq m a
      , pprintParOp (findAllComms eventName m a `Set.intersection`
                       unionAll (map (findAllComms eventName m) bs))
      , joinPar bs
      ]
pprintCSP _ (Call p) = name p
pprintCSP _ x = error $ "pprintCSP: " ++ show x

pprintParOp :: Set.Set String -> PP.Doc
pprintParOp s
  | Set.null s = PP.text "|||"
  | otherwise = surround "[|{|" "|}|]" $ intersperse PP.comma $
      map name (Set.toList s)
  where
    surround a b x = PP.sep $ [PP.text a] ++ x ++ [PP.text b]

The findAllComms does as its name suggests: it forms a set of all the communications performed anywhere in the process, using the supplied Map that we have been passing around to find out what communications are performed by named processes that are called. Note that as we compose parallel items together, we compose the head of the list using the intersection of all communications performed in the head, and all communications performed in the rest of the list (which will be the right-hand side of the parallel composition). So if you have three processes: [a -> b -> SKIP, b -> c -> SKIP, a -> c -> SKIP], they will get composed as:

(((a -> b -> SKIP)
    [|{| a , b |}|]
    ((b -> c -> SKIP) [|{| c |}|] (a -> c -> SKIP))))

The first process synchronises on “a” and “b” with the others, as both feature somewhere later in the list. The second and third process only synchronise together on “c”; the events “a” and “b” are not shared, and thus occur separately, but synchronised with the first process.

Parallel Composition Omission

Basing the synchronisation sets on those events that are potentially performed has a problem. If a process is given a channel-end or barrier, but never uses it at all, the event will not show up in the model for that process, and thus will not be used in the synchronisation set. Let’s say you have a barrier, “b” with two processes enrolled, but one does not use it. Given those two processes, say “a ->SKIP” and “SKIP” they will be composed as “a ->SKIP ||| SKIP“, which will run fine — even though the original program would have deadlocked! The solution to this is to introduce extra code for tracking how many processes are involved in an event, and add dummy processes that have the events in their synchronisation set but never use them, thus reflecting the deadlock in the model. I haven’t yet implemented this just yet, though.

Summary

We have now seen how parallel composition is implemented, including determination of the synchronisation sets. In future parts of the guide, we will examine the remaining parts of CHP: channel communications, choice, and iteration, as well as how all these are put together.

About these ads