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