anchor.diff:              { Name = "unlock"
                 Contents =
                     Map.ofList
  -                      [ ("unlock_V0",
  +                      [ ("unlock_V000",
                            (Mandatory <|
                             Multiset.singleton
                                     (gfunc BTrue "holdLock" [] ),
                             Set.singleton
  -                              { Name = "unlock_C0"
  -                                Dest = "unlock_V1"
  +                              { Name = "unlock_C000"
  +                                Dest = "unlock_V001"
                                   Command =
                                       [ command "!I++" 
                                              [ Int "serving" ]
                                              [ Typed.Int (siBefore "serving") ]] },
                             Set.empty,
                             Entry))
  -                        ("unlock_V1",
  +                        ("unlock_V001",
                            (Mandatory <| Multiset.empty,
                             Set.empty,
                             Set.singleton
  -                              { Name = "unlock_C0"
  -                                Src = "unlock_V0"
  +                              { Name = "unlock_C000"
  +                                Src = "unlock_V000"
                                   Command =
                                       [ command "!I++"
                                              [ Int "serving" ]
  
positive.code:         ///     Test cases for checking edge addition.
          /// </summary>
          static member Adds =
              [ TestCaseData(("unlock_N0", "unlock_V1", "unlock_V0"))
                  .Returns(
                    Some <|
                    Map.ofList
                        [ ("unlock_V0",
                           (Mandatory <|
                            Multiset.singleton
                                (Studies.gHoldLock BTrue),
                            Set.singleton
                                { Name = "unlock_C0"
                                  Dest = "unlock_V1"
                                  Command =
                                      [ command "!I++"
                                             [ Int "serving" ]
                                             [ SMExpr.Int (siBefore "serving") ]] },
                            Set.singleton
                                { Name = "unlock_N0"
                                  Src = "unlock_V1"
                                  Command = [] },
                            Entry ))
                          ("unlock_V1",
                           (Mandatory <| Multiset.empty,
                            Set.singleton
                                { Name = "unlock_N0"
                                  Dest = "unlock_V0"
                                  Command = [] },
                            Set.singleton
                                { Name = "unlock_C0"
                                  Src = "unlock_V0"
                                  Command =
                                      [ command "!I++"
                                             [ Int "serving" ]
  
negative.code:         let ticketLockLockSubgraph : Subgraph =
              { Nodes =
                    Map.ofList
                        [ ("lock_V000",
                               (Mandatory <| Multiset.empty, Entry))
                          ("lock_V001", (Mandatory <| Multiset.singleton (gHoldTick BTrue), Normal))
                          ("lock_V002", (Mandatory <| Multiset.singleton (gHoldLock BTrue), Exit))
                          ("lock_V003", (Mandatory <| Multiset.singleton (gHoldTick BTrue), Normal))
                          ("lock_V004",
                               (Mandatory <|
                                Multiset.ofFlatList
                                   [ gHoldLock (iEq (siVar "s") (siVar "t"))
                                     gHoldTick (BNot (iEq (siVar "s") (siVar "t"))) ], Normal)) ]
                Edges =
                    Map.ofList
                        [ ("lock_C000",
                               edge "lock_V000"
                                    [ command "!ILoad++"
                                           [ Int "t"; Int "ticket" ]
                                           [ Typed.Int (siBefore "t")
                                             Typed.Int (siBefore "ticket") ]]
                                    "lock_V001")
                          ("lock_C001",
                               edge "lock_V003"
                                    [ command "!ILoad"
                                           [ Int "s" ]
                                           [ Typed.Int (siBefore "serving") ]]
                                    "lock_V004")
                          ("lock_C002",
                               edge "lock_V004"
                                    [ command "Assume"
                                           []
                                           [ Typed.Bool
                                                 (BNot (iEq (siBefore "s")
                                                            (siBefore "t"))) ]]
                                    "lock_V003")
                          ("lock_C003",
                               edge "lock_V004"
                                    [ command "Assume"
                                           []
                                           [ Typed.Bool
                                                 (iEq (siBefore "s")
                                                      (siBefore "t")) ]]
                                    "lock_V002")
                          ("lock_C004",
                               edge "lock_V001"
                                    []
                                    "lock_V003") ] }
  
          /// The partial CFG for the ticket lock unlock method.
          let ticketLockUnlockSubgraph : Subgraph =
              { Nodes =
                    Map.ofList
                        [ ("unlock_V000",
                               (Mandatory <|
                                Multiset.singleton
                                   (svgfunc BTrue "holdLock" [] ), Entry))
                          ("unlock_V001", (Mandatory <| Multiset.empty, Exit)) ]
                Edges =
                     Map.ofList
                        [ ("unlock_C000",
                               edge "unlock_V000"
                                    [ command "!I++"
                                           [ Int "serving" ] 
                                           [ Typed.Int (siBefore "serving") ]]
                                    "unlock_V001" ) ] }
  
  
      /// <summary>
  