anchor.diff:  
       ctx.Dispose
   
  +let demoCommand line =
  +    match run parseCommand line with
  +        | Success(result, _, _)   -> printfn "Success: %A" result
  +        | Failure(errorMsg, _, _) -> printfn "Failure: %s" errorMsg
  +
   let main =
       Console.WriteLine("Hello, world!")
  -    match run parseCommand "<a := b> || <c := d>* + (<foo>; <bar>)" with
  -        | Success(result, _, _)   -> printfn "Success: %A" result
  -        | Failure(errorMsg, _, _) -> printfn "Failure: %s" errorMsg
  +    demoCommand "<a := b> || <c := d>* + (<foo>; <bar>)"
  +    demoCommand "{emp} <a := b> {fooBar()} || <c := d>* + (<foo>; <bar>)"
  +    demoCommand """
  +    {emp}
  +        <a := b>
  +    {holdTickIf(true, t)};
  +        (
  +            {holdTickIf(true, t)}
  +            <s = serving;>
  +            {holdTickIf(s != t) * holdLockIf(s = t) * termIf(s = t)}
  +        )*
  +    {holdLockIf(true)}
  +    """
       match run parseViewLine pv2 with
           | Success(result, _, _)   -> printfn "Success: %A" result
           | Failure(errorMsg, _, _) -> printfn "Failure: %s" errorMsg
  
positive.code: open FParsec
  open Microsoft.Z3
  
  type Command =
      | Atomic of string
      | Skip
      | Seq of Command * Command
      | Choice of Command * Command
      | Par of Command * Command
      | Star of Command
  
  type View =
      | Apply of View * args: string list
      | NamedView of string
      | Unit
      | Join of View * View
  
  type Method =
      | End of postcondition: View
      | Step of precondition: View * cmd: Command
  
  let wsc = anyOf " \t"
  let ws = manyChars wsc
  let ws1 = many1Chars wsc
  
  
negative.code: do parseViewRef :=
      chainl1 parseSimpleView (pstring "*" .>> ws >>% fun x y -> Join(x, y))
  
  let cas =
      Choice(Atomic("foo"), Skip)
  
  