New chp-spec library released

I recently published a multi-part guide on how to provide a mirror implementation of (most of the API of) CHP that spits out a CSP specification of the program rather than execute it. You can go back and read:

• part 1: representing a specification and modelling parallelism,
• part 2: pretty-printing the CSP specification, and calculating parallel alphabets,
• part 3: modelling choice and lifted IO actions,
• part 4: modelling communication, and tracking communicated values, and
• part 5: modelling iteration — processes that repeat their behaviour.

This is the final post I plan to make on the matter (at least for a while)! This post is to announce the release of the work in the above guide as a new chp-spec-1.0.0 library. If you aren’t interested in formal specification, and just want to use CHP, you can ignore the chp-spec library. (And if you don’t use CHP, you can definitely ignore it!) It’s only useful if you want to try to generate a CSP model of your CHP program — and even then, the technique comes with a lot of caveats. But I’d rather release it than leave it sitting on my hard drive.

Instructions

To use the chp-spec library in place of chp, you must do the following:

• Change the library dependency from chp to chp-spec when you want to generate a specification. You may be able, in cabal, to have both dependencies listed all the time. Currently there is no chp-spec-plus; if you want this, let me know.
• Change the imports in all your modules from Control.Concurrent.CHP* to Control.Concurrent.CHPSpec* when you want to generate a specification; this can be automated somewhat using preprocessor macros if you want to switch between the two regularly.
• Make sure that all uses of the forever function in your process are changed to CHP’s foreverP (this is included in CHP 2.2.0 onwards so you can make this change permanent, even when using plain chp).
• Add the process annotation to all directly recursive processes (again, this is included in CHP 2.2.0 onwards, so you can make this change permanent, even when using plain CHP).
• When you want to generate a specification, change the top-level function from runCHP to specify.

Specify

The specify function mentioned in the last point is the top-level call that generates and post-processes the CSP specification. The generation has been mostly covered in previous posts; the generation part of specify is trivial; it annotates the top-level process to be called main, then runs the state transformer to get the altered state with all the processes recorded in it (among other things), which it passes to specify', the function that does all the post-processing:

specify :: Bool -> CHP () -> IO String
specify showIO main
  = specify' showIO <$> execStateT (finSpecT $ process "main" main) emptyCHPState

That showIO parameter will be explained later in the post. The code for specify' is long-winded but not very exciting. It can be split into two aspects:

specify' :: Bool -> CHPState -> String
specify' showIO st = render specs ++ declMain
  where ...

We’ll start with the first part of that concatenation. The render call uses the pretty-printing to print the specifications. The specs item is generated from the recorded process by two steps: first, it pulls up any Repeated processes to be top-level recursive processes — modern CSP has no iteration operator — and second, it transforms all the process-ids and communications into strings by uniquely numbering the processes and channel values.

The second part of the concatenation, declMain, declares a main process, named “main”. We know, because it’s the first process that is encountered, that our top-level process will end up named “main_1″, so at the most basic we end up with a line “main = main_1″, which wraps up all the numbering in a simpler name. But it can have different behaviour depending on that mysterious “unhideIO” parameter.

CSP’s semantics revolve around traces, which are records of the visible actions that a process takes. That visible qualifier is significant: CSP allows for hiding of events. This is particularly relevant in case of our dummy IO events. If we leave them as-is, they will show up in the trace of the process even though they are not really a part of its behaviour — but this does allow us to read traces produced by the FDR tool more easily, as we can see which IO events occurred. So the setting is useful for “debugging” any deadlocks, but these extra events can ruin refinement checks because the process appears to be taking extra events. If you’re doing a deadlock check, pass True to keep the IO events visible, otherwise pass False to hide them. That is done by the following code for declMain in the where clause of specify’:

declMain :: String
declMain = "\nmain = main_1 " ++ (if showIO then "" else
  "\\ {" ++ intercalate "," (map getName $ Set.toList $ chpIOEvents st) ++ "}"
  ) ++ "\n"
  where
    getName = fromJust . flip Map.lookup events

If showIO is False, the main process will hide (backslash is the hide operator in CSP) all the IO events, to stop them being visible to the outside, and in traces of the main process.

About these ads