ࡱ> gibch}( SL/ 0DArialew Ro<7LP40Wo 0"DTahomaew Ro<7LP40Wo 0" DTimes New RomanP40Wo 00DWingdingsRomanP40Wo 0@DTimes New Roman MT Extra BoldWo 0PDSymbolew Roman MT Extra BoldWo 0 a.  @n?" dd@  @@`` la)FL FG   ) '&-"&: %( 0"B$, #(%)+!(,&$+ 0e0e A@A5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?0 @89 : { m ʚ;D7ʚ;g4LdLd0ppp@ <4!d!d 0L<5<4dddd 0L<5<4BdBd 0L<5? %O =o>:CTL Model-checking for Systems with Unspecified Components;;(Gaoyan Xie and Zhe Dang School of Electrical Engineering and Computer Science, Washington State University, Pullman, WA 99164, USA < k A Motivation (TChallenges to the quality assurance of component-based systems: Externally obtained components may be new sources of system failures Safely upgrading a deployed component is extremely difficult Example: The Ariane 5 disaster was caused by reusing certain software module from Ariane 4 without sufficiently testing it in the new environmentT@ZZ ZZ@ 9B(Two Dimensions of The Possible Solutions))(Methodologies Compositional approachesconventional, used most often Bottom-up, from components to systems Decompositional approachesnot many can be automated Top-down, from systems to components Techniques Software Testing A trial and error technique Integration/system testing is often needed at the system level Model-checking: A formal and usually complete technique The assume-guarantee paradigm is often used for system-level verificationFZ7Z&Z5Z%Z ZZ[ZZuZ&$     [/5kH? Testing a Component in Isolation!!(TBefore it is released By component developers By third-party labscomponent certification Difficulty: A component may target a wide scope of deployment environments, which may not be tried out When it is integrated into a system By system developers Expensive: A component is usually built with multiple sets of functionalities Infeasible: The state space of a component s interface may be too large to be thoroughly tested ZQZ[Z$Z!ZCZ ZUZ+ [$  !C U@&Testing A Component-based System (CBS)''(iIntegration/system testing Difficulties: Components within a CBS may run concurrently Even inside a component may have multi-threads running concurrently, and Concurrency is notoriously difficult to test Locating the source of a bug is not easy! Feasibility: A component may be used for dynamic upgrading a running system, which may not be stopped for testing e  0          J Model-checking(Checks whether a finite-state system is a model of a given temporal formula Requires a complete and formal specification of the finite-state system Not always possible: design details or source codes of components in a CBS are generally unavailable The assume-guarantee paradigm is often used for system-level verification A compositional approach Requires an assumption for the environment of a moduleZeZJZPZe5PCThe Research Problem(JA different perspective How to ensure that a component functions correctly in a specific deployment environment (which is called a host system) A model-checking problem Given a host system M with an unspecified component X and a CTL formula f, check whether f is a model of (M, X): (M, X)= f ZxZZqZ ZV               D Basic Ideas (Goal Seek a definite answer (no approximation) to the model-checking problem, i.e., (M, X)= f Solution Automatically deduce a sufficient and necessary condition over the unspecified component Check the condition through testing the unspecified component[ A hEThe System Model(A system Sys= (M, X) consists of a host system M and an unspecified component X The host system M is a well-specified finite state transition system The unspecified component X can be viewed as a deterministic Mealy machine Internal detail of X is unknown Interface (input/output symbols) and an upper bound for the number of states in X are known An implementation of X is available for testing M and X run concurrently and communicate with each other by synchronizing over X s input/output symbolsPZZZhZ N0  Hq) An ExampleCheck: starting from state s0, is state s3 reachable? (M, Comm), s0= E[true U s3]6ZZ      :p("An Examplecontd.$ Check: starting from state s0, is state s3 reachable? M, s0= E[true U s3]6      V"An Examplecontd.$ ^Check: starting from state s0, is state s3 reachable? M, s0= E[true U s3] Search the graph to see whether there is a path between s0 and s3 s0s1s4s3 is such a witness path6ZZBZ#Z      8        W"An Examplecontd.$ rCheck: starting from state s0, is state s3 reachable? (M, Comm), s0= E[true U s3] Search the graph to see whether there is a path between s0 and s3 Is s0s1s4s3 still a witness path?6ZZBZ%Z      8      :|Y"An Examplecontd.$ Infinite number of paths could be witness path: s0s1s2s1s4s3, s0s1s2s3, s0s1s2s1s2& s3,& Infinite number of communication traces need to be tested:  send/yes send/no ack/yes ,  send/yes ack/yes ,  send/yes send/yes& ack/yes , & 0Z5Z;ZOZ0                ;O Z"An Examplecontd.$ 4Use an annotated directed graph Gh (called witness graph) to represent all those communication traces The original model-checking problem is: True, if one of the communication traces in Gh is a successful test case for Comm False, if none of the communication traces in Gh is a successful test case for CommZZ   W      ]"An Examplecontd.$ How to handle communication traces with infinite length? A result from traditional black-box testing: An equivalent internal structure of a black-box can be recovered through testing if only an upper bound for its number of states is known This result implies that Only communication traces with bounded length need to be tested The bound can be calculated from the number of states in M and the upper bound for the number of states in Comm9Z-ZZZ@ZpZ9-91[ Our AlgorithmThe original CTL model-checking algorithm for checking M= f: Goes through a series of stages. A subformula h of f is processed at each stage: h is added to the labels of a state s if h is true at s Returns true if s0 is labeled with f, or false otherwise Our algorithm adapts the original algorithm to handle systems with unspecified components. It follows a similar structure, except that during each stage for subformula h, the labeling of a state s is far more complicated>ZRZ8Z:ZZ7/#             \(Our Algorithm contd.A state s could be labeled with 1 if h is true at s and the truth has nothing to do with communications A witness graph if h is an CTL operator and the truth of h at s depends on communication traces in the graph A logical combination of witness graphs if h is a logic combination of other formulas and the truth of h at s depends on communication traces in the graph For each CTL operator in h, a witness graph is constructed and associated with an ID (which begins from 2) A state is labeled with an ID expression (constructed from IDs and logic connectives , ) A labeling function Lh is returned upon the completion of processing h ZVZ Z 5%.(;.82 - .P1^(Our Algorithm contd.The algorithm outline: _ Another ExampleHCheck: starting from the initial state s0, whenever the system reaches state s2, it would eventually reach s3; i.e., check (M, X), s0= AG(s2 AF s3 ) to be true,{Z*Z' $        `!JCheck (M, X), s0=E[true U(s2EGs3)]&$$$$$$ $$$$$$$$$$$ $$iStep 1. Atomic subformula s2 is processed by ProcessCTL, which returns a labeling function L1 = {(s2, 1)}j $  m%JCheck (M, X), s0=E[true U(s2EGs3)]&$$$$$$ $$$$$$ $$$$$$$iStep 1. Atomic subformula s2 is processed by ProcessCTL, which returns a labeling function L1 = {(s2, 1)}j  $  n&JCheck (M, X), s0=E[true U(s2EGs3)]&$$$$$$ $$$$$$ $$$$$$$iStep 1. Atomic subformula s2 is processed by ProcessCTL, which returns a labeling function L1 = {(s2, 1)}j $a"JCheck (M, X), s0=E[true U(s2EGs3)]&$$$$$$ $$$$$$ $$$$$$$fStep 4. Subformula EG s3 is processed by ProcessEG, which constructs a witness graph G1 = <N, E, L3> with an ID 2 and returns a labeling function L4 = {(s0, 2), (s1, 2), (s2, 2)}x  #   !    o'JCheck (M, X), s0=E[true U(s2EGs3)](&$$$$$$ $$$$$$$$$$$$$fStep 4. Subformula EG s3 is processed by ProcessEG, which constructs a witness graph G1 = <N, E, L3> with an ID 2 and returns a labeling function L4 = {(s0, 2), (s1, 2), (s2, 2)}v  #   !    b#JCheck (M, X), s0=E[true U(s2EGs3)]8&$$$$$$ $$$$$$$$$$$$$Step 6. The formula E[true U (s2 EG s3)] is processed by procedure ProcessEU, which constructs a witness graph G2 = <N, E, Ltrue, L5> with an ID 3 and returns a labeling function Lf = {(s0, 3), (s1, 3), (s2, 3), (s3, 3), (s4, 3)}vZ #    !      c$Evaluate ID Expression Lf (s0)NnEvaluating Lf (s0) is a testing process with test-cases generated from the two witness graphs (details can be seen in the paper) Essentially, we are testing whether some communication trace (of bounded length) with m consecutive symbol pairs  send yes is a successful test-case for the unspecified component X.8Z   ]USummaryA decompositional approach Reduces a system verification problem to a testing problem over the unspecified component A hybrid approach Combines model-checking with software testing techniques Advantages Stronger confidence about the reliability of the system Customization of testing over a component with respect to particular system requirement Reuse of intermediate verification results Automatic carrying out of the whole process Complete and sound algorithm with an appropriate boundZ9 Z9   Q Related WorkfSpecification-based testing [Heitmeyer et. al. 1999], generate test-cases from counter-examples produced by a model-checker Black-box checking [Peled et. al. 1999], test a single black-box against a given LTL formula Automatic assume-guarantee [Giannakopoulou et. al. 2004], automatic generation of assumptions of a component, uses a less expressive formalism (LTS) for properties Automatic deduction of model-checking conditions [Fisler et. al. 2001], has false negative [Xie & Dang 2004] LTL algorithms for systems with only one, finite-state unspecified component (FATES 04) An automata-theoretic and decompositional approach to testing a system of concurrent black-boxes (submitted) ZZbL0,% , kG  Ongoing WorkDecompositional LTL model-checking Less-restricted system model Asynchronous communications Multiple unspecified components Unspecified components with infinite state space Case studies CORBA applicationsT@ZnZ ZZ@n /TfghijkP ` 33PP` 3333` ___MMM` 13` 333fpKNāvI` j@v۩ῑ΂H` Q_{>?" dd@,?n<d@ `7 `2@`7``2 n?" dd@   @@``PR    @ ` ` p>>      (    <n"J @   THqd"J @   <tt")U_T @   Tvd")>&T @   Ny"P @   <|"r @   C x?d?"U @   6, "  T Click to edit Master title style! !$  0T "P `  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  6܊ "@  >   6$ "@`   HSAVCBS 04     6 "`  D*B  s *޽h ? 3333  Blends      @! (  T +  "+bb P@ # "Dwoh  s *"PP  Bd" P@bb P 0  # "Nyh  s *"P    Bd"P 0 z   <" a*h   s *"    f?d?"+)   <` ?"pP  T Click to edit Master title style! !   0 " `    W#Click to edit Master subtitle style$ $  6 "`p   HOctober 29, 2004d  6 "`p   |SAVCBS 04 Presented by: Gaoyan Xie??;B  s *޽h ? 3333 0 `:(    0 P    \*   0%     ^* d  c $ ?    0)  @  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  6- `P   \*   6/ `   ^* H  0޽h ? ̙33 H(    0, P    B*   0     D*   6 `P   B*   6 `   D* H  0޽h ? ̙33 l 0t$(  tr t S Թ @pP  r t S d 0 @  H t 0޽h ? 3333  ` p*(  x  c $    r  S  y  H  0޽h ? 3333  p *(  x  c $    r  S  0`  H  0޽h ? 3333  P x*(  xx x c $L    r x S H `  H x 0޽h ? 3333  0l |*(  |x | c $8m    r | S \L   H | 0޽h ? 3333    *(  x  c $    r  S č 0  H  0޽h ? 3333    *(  x  c $    r  S    H  0޽h ? 3333   *(  x  c $|I    r  S $J    H  0޽h ? 3333   *(  x  c $N    r  S HO `  H  0޽h ? 3333R  P #%\z(  \~ \ s *k    2 \ # lm ?? 0P  Fs0(   2 \ # lc ?? @  Fs1(   2 \ # lf ??  0  Fs2(   2 \ # l ??0P0 Fs4(   B \  fDg ??p P p B  \  `D??p @ p B  \  fDg ??P B  \  `D?? B  \@  fDg ?? P@B  \@  `D?? @ | \ S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `   \  ` ?? >q  8msg?  \  `4 ??   <send/yes    \  ` ??  ;ack/yes  \  `R ??` P  ;send/no  \  `@? ??  ;ack/yes  \  `A ??` P  8msg?  \  ` ?? l  8msg? F  3 p  \  UM \  ``??P   8CommB \  `D??  B \  `D?? p p B \  `D?? p B \  `D??p pp  \  fd ?? 3   8data  \  fTh ?? S   7ack  \  fk ??3   7yes  \  fo ??S   6no B !\  `D??   "\ To ??Lp  Q Host system M( 2  #\ <p  `<$D 0  2 $\ # lXt ?? @0,$ 0 Fs3(   2 %\  fx?? @0,$D 0 Fs3(   H \ 0޽h ? 3333  pl IAT(  Tx T c $ w  2 T 3 r ?? 0P  Fs0(   2 T 3 rԑ ?? @  Fs1(   2 T 3 r\ ??  0  Fs2(   2 T 3 r ??0P0 Fs4(   2  T # l?? @0 Fs3(   B  T # lDg ??p P p B  T  fD??p @ p B  T # lDg ??P B  T  fD?? B T@ # lDg ?? P@B T@  fD?? @ | T S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `  B T  `D??   T T8 ??Lp  WTransition system M( 2 T s D0e0e     H T 0޽h ? 3333  p G?  (  r  S  `   2  3 r  ?? 0P  Fs0(   2  3 ra ?? @  Fs1(   2  3 r ??  0  Fs2(   2  3 r ??0P0 Fs4(   2  # lti?? @0 Fs3(   B   # lDo??p P p B    fD??p @ p B   # lDo??P B    fD?? B  @ # lDo?? P@B @  fD?? @ |  S T0e0e BCDEFA@ A5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `  B   `D??    T ??Lp  WTransition system M( 2  s 0e0e     H  0޽h ? 3333T  Pl 0#,p(  2  3 r ?? 0P  Fs0(   2  3 r ?? @  Fs1(   2  3 rC ??  0  Fs2(   2  3 rl ??0P0 Fs4(   2   # lT?? @0 Fs3(   B   # lDo??p P p B    fD??p @ p B   # lDo??P B    fD?? B @ # lDo?? P@B @  fD?? @ |  S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `     ` ?? >q  8msg?    ` ??   <send/yes      ` ??  ;ack/yes    ` ??` P  ;send/no    ` ??  ;ack/yes    `P ??` P  8msg?    ` ?? l  8msg? 8  3 p  % UM   `0??P   8CommB   `D??  B   `D?? p p B   `D?? p B   `D??p pp     f ?? 3   8send  !  f  ?? S   7ack  "  fH# ??3   7yes  #  fp  ??S   6no  $ T) ??N ` P ,$D  0 4Test Comm to see whether the communication trace along the path can be accepted by Comm: Will  send/no, ack/yes be a successful test case for Comm?  2J2,S+B &  `D??   ' T4 ??Lp  Q Host system M( 2  * <6  `    , s 70e0e     H  0޽h ? 33334  l @"%\(  2  # lI ?? 0P  Fs0(   2  # l{ ?? @  Fs1(   2  # lQ ??  0  Fs2(   2  # lU ??0P0 Fs4(   2   f0Z?? @0 Fs3(   B   fDg ??p P p B    `D??p @ p B    fDg ??P B    `D?? B  @  fDg ?? P@B  @  `D?? @ |  S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `     `@ ?? >q  8msg?    `8> ??   <send/yes      `_ ??  ;ack/yes    ` ??` P  ;send/no    `x ??  ;ack/yes    ` ??` P  8msg?    `T ?? l  8msg?   <    F  3 p    UM   `L??P   8CommB   `D??  B   `D?? p p B   `D?? p B   `D??p pp    f ?? 3   8send    f ?? S   7ack    ft ??3   7yes     f ??S   6no B "  `D??   # TX ??Lp  Q Host system M( 2  % s d0e0e     H  0޽h ? 3333}    l   P'9(  2  # llf ?? 0P  Fs0(   2  # lا ?? @  Fs1(   2  # l ??  0  Fs2(   2  # l ??0P0 Fs4(   2   f?? @0 Fs3(   B   fDg ??p P p B    `D??p @ p B    fDg ??P B    `D?? B  @  fDg ?? P@B  @  `D?? @ |  S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `     ` ?? >q  8msg?    `$ ??   <send/yes      ` ??  ;ack/yes    `x ??` P  ;send/no    ` ??  ;ack/yes    ` ??` P  8msg?    ` ?? l  8msg?   <$  w  2 " # l ??   Fs1(   2 # # l ?? p  Fs2(   2 $ # lXH ?? 0 Fs4(   2 %  f0??0 Fs3(   B '  `D??p pp B (  fDg ?? B )  `D?? B *@  fDg ?? @B +@  `D??  .  ` ??   <send/yes    /  `  ?? K  ;ack/yes  0  ` ??` |  ;send/no  1  `0 ?? @ ;ack/yes B 4  `D??  B 5  `D??   6 T$ ??Lp  Q Host system M( 2  7 T! ??L  dWitness graph Gh8 2  9 s $0e0e     H  0޽h ? 3333  l `*(  x  c $    r  S  0  H  0޽h ? 3333   p*(  x  c $U    r  S V 0  H  0޽h ? 3333  s *(  x  c $@G    r  S lN ``  H  0޽h ? 3333  P SK(  x  c $o      S E 0`  (yCc  0o  ,$D  0 JProcessCTL is the lableling process, it recursively handles the five cases of f: , , EX, EU, and EG by calling the procedures Negation, Union, ProcessEX, ProcessEU, and ProcessEG respectively4 n< D !    Z  v     T$x ??CP T Procedure CheckCTL(M, X, s0, f) Lf := ProcessCTL(M, f); If s0 is labeled by Lf Then If Lf (s0) = 1 Then Return true; Else Return TestWG(X, reset, s0, Lf (s0)); Endif Else Return false; Endif End Procedurer0n<Z               b  ~$    0Й  `,$D  0 |The maximal length of communication traces to be tested is bounded by O(knm2), where k is the number of CTL operators in the formula f, m is the upper bound for the number of states in the unspecified component X, and n is the number of states in the host system M6  n<F##  /J,H  0޽h ? 3333f  l #$(  x  c $    r  S ( 0  2  # l ?? @`  Fs0(   2  # lT ?? 0P  Fs1(   2  # lT ?? @  Fs2(   2  # l ??@`0 Fs4(   2   f ??0P0 Fs3(   B    fDg ??p `0p B    `D??p P p B    fDg ??`0B    `D?? B  @  fDg ?? 0`@B @  `D?? P |  S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `     ` ?? Nq  8msg?    `L ??   <send/yes      ` ??   ;ack/yes    `0 ??` `,  ;send/no    `  ??  ;ack/yes    `P ??` `  8msg?    ` ?? l  8msg? F  3 p    UM   `h??P   8CommB   `D??  B   `D?? p p B   `D?? p B   `D??p pp    f ?? 3   8send    f ?? S   7ack    f ??3   7yes     fp ??S   6no B !  `D??   " T ??Lp  Q Host system M( 2  $ 0 0 ,$D 0 Taking a negation of the original problem, it s equivalent to checking (M, X), s0= E[true U (s2 EG s3 )] to be falsez0n<ZP    H  0޽h ? 3333D  PXl "' l(   x   c $        S  `<$ 0  2   # lxA ?? @` ,$D 0 Fs0(   2   # lt  ?? 0P ,$D  0 Fs1(   2   # l$ ?? @  Fs2(   2   # l` ??@`0 Fs4(   2    f ??0P0 Fs3(   B    fDg ??p `0p B    `D??p P p B    fDg ??`0B    `D?? B  @  fDg ?? 0`@B  @  `D?? P |   S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `      ` ?? Nq  8msg?     `lB ??   <send/yes       `\F ??   ;ack/yes     `I ??` `,  ;send/no     `XL ??  ;ack/yes     `O ??` `  8msg?     `xS ?? l  8msg? F  3 p     UM    `V??P   8CommB    `D??  B    `D?? p p B    `D?? p B    `D??p pp     fZ ?? 3   8send     f<^ ?? S   7ack     f,a ??3   7yes     fd ??S   6no B !   `D??   "  Th ??Lp  Q Host system M( 2 H   0޽h ? 3333  PXl wo#(H(  H H c $ `<$ 0  2 H # l\ ?? @` ,$D 0 Fs0(   2 H # l ?? 0P ,$D  0 Fs1(   2 H # lܺ ?? @  Fs2(   2 H # l| ??@`0 Fs4(   2 H  f ??0P0 Fs3(   B  H  fDg ??p `0p B  H  `D??p P p B  H  fDg ??`0B  H  `D?? B  H@  fDg ?? 0`@B H@  `D?? P | H S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `   H  `0 ?? Nq  8msg?  H  `n ??   <send/yes    H  `  ??   ;ack/yes  H  ` ??` `,  ;send/no  H  `0 ??  ;ack/yes  H  `D ??` `  8msg?  H  ` ?? l  8msg? F  3 p  H  UM H  `(??P   8CommB H  `D??  B H  `D?? p p B H  `D?? p B H  `D??p pp  H  fX ?? 3   8send  H  f ?? S   7ack  H  f ??3   7yes   H  ft ??S   6no B !H  `D??   "H T ??Lp  Q Host system M( 2 ' #H 0 ,$D 0 iStep 2. Atomic subformula s3 is processed by ProcessCTL, which returns a labeling function L2 = {(s3, 1)}j n< $  ,  3 (H s 0e0e     H H 0޽h ? 3333"  PXl !!$*L;!(  L L c $  `<$  0  2 L # l ?? @` ,$D 0 Fs0(   2 L # l( ?? 0P ,$D  0 Fs1(   2 L # l\ ?? @  Fs2(   2 L # l ??@`0 Fs4(   2 L  f( ??0P0 Fs3(   B  L  fDg ??p `0p B  L  `D??p P p B  L  fDg ??`0B  L  `D?? B  L@  fDg ?? 0`@B L@  `D?? P | L S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `   L  ` ?? Nq  8msg?  L  ` ??   <send/yes    L  `$ ??   ;ack/yes  L  ` ??` `,  ;send/no  L  ` ??  ;ack/yes  L  `̐ ??` `  8msg?  L  `$ ?? l  8msg? F  3 p  L  UM L  `??P   8CommB L  `D??  B L  `D?? p p B L  `D?? p B L  `D??p pp  L  fx ?? 3   8send  L  f ?? S   7ack  L  f ??3   7yes   L  f ??S   6no B !L  `D??   "L T ??Lp  Q Host system M( 2  #L 0p ,$D 0 iStep 2. Atomic subformula s3 is processed by ProcessCTL, which returns a labeling function L2 = {(s3, 1)}j n<  $  ,  34 $L 0\> ` ,$D 0 Step 3. Subformula s3 is processed by Negation, which returns a labeling function L3 = {(s0, 1), (s1, 1), (s2, 1), (s4, 1)}T} n<$      k *L s 00e0e     H L 0޽h ? 33333  l !/[(    S T) 0<$D 0  2  # l* ?? @`  Fs0(   2  # l{ ?? 0P  Fs1(   2  # l- ?? @  Fs2(   2  # lx: ??@`0 Fs4(   2   fa ??0P0 Fs3(   B    fDg ??p `0p B    `D??p P p B    fDg ??`0B    `D?? B  @  fDg ?? 0`@B @  `D?? P |  S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@  `     `f ?? Nq  8msg?    `j ??   <send/yes      `(n ??   ;ack/yes    `o ??` `,  ;send/no    `Ds ??  ;ack/yes    `v ??` `  8msg?    ` z ?? l  8msg? B !  `D??   " Tt} ??Lp  UThe host system M( 22 # # l ??0 P  Fs0(   2 $ # l\ ??0 P  Fs1(   2 % # l@ ??0 P  Fs2(   B &  fDg ??  B '  `D??  | ( S T0e0e BCDEF@ 5%8c8c     ?1d0u0@Ty2 NP'p<'p@A)BCD|E?<8@   P@0  )  `m ??/ `P  <send/yes   B *  `D??p ` ` 0  + T  ?? p Witness graph G1 with ID 2 ` 2  / s 0e0e     H  0޽h ? 3333_"