UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Protocol test sequence generation and analysis using AI techniques Ko, Kai-Chung 1990

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata


831-UBC_1990_A6_7 K62.pdf [ 3.68MB ]
JSON: 831-1.0051978.json
JSON-LD: 831-1.0051978-ld.json
RDF/XML (Pretty): 831-1.0051978-rdf.xml
RDF/JSON: 831-1.0051978-rdf.json
Turtle: 831-1.0051978-turtle.txt
N-Triples: 831-1.0051978-rdf-ntriples.txt
Original Record: 831-1.0051978-source.json
Full Text

Full Text

Protocol Test Sequence Generation and Analysis Using A l Techniques By KAI-CHUNG KO B . A . S c , University of British Columbia, Vancouver, Canada, 1987 B.Sc, University of British Columbia, Vancouver, Canada, 1988 A THESIS S U B M I T T E D IN P A R T I A L F U L F I L L M E N T O F T H E REQUIREMENTS F O R T H E D E G R E E OF M A S T E R O F SCIENCE in T H E F A C U L T Y O F G R A D U A T E STUDIES (DEPARTMENT OF C O M P U T E R  SCIENCE)  We accept this thesis as conforming to the required standard  T H E UNIVERSITY O F BRITISH C O L U M B I A July 1990 © Kai-Chung Ko, 1990  In  presenting  degree freely  at  this  the  University  available  copying  of  for  this  department  or  publication  thesis  of  this  of  reference  thesis by  in  for  his  fulfilment  British  Columbia,  and  study.  scholarly  or  thesis  partial  for  her  financial  .  ,  of  COMPUTER  ^  The University of British Vancouver, C a n a d a  Date  -6  (2/88)  1st  August.  SCIENCE  Columbia  1990  I further  purposes  gain  the  requirements  I agree  that  agree  may  be  It  is  representatives.  permission.  Department  of  shall  not  that  the  Library  permission  granted  by  understood be  for  allowed  an  advanced  shall for  the that  without  make  it  extensive  head  of  copying my  my or  written  Abstract  This thesis addresses two major issues in protocol conformance testing: test sequence generation and test result analysis. For test sequence generation, a new approach based on the constraint satisfaction problem (CSP) techniques, which is widely used in the A l community, is presented. This method constructs a unique test sequence for a given F S M by using an initial test sequence, such as a transition tour or an UIO test sequence, and incrementally generating a set of test subsequences which together represent the constraints imposed on the overall structure of the F S M . The new method not only generates test sequence with fault coverage which is at least as good as the one provided by the existing methods, but also allows the implementation under test (IUT) to have a larger number of states than that in the specification. In addition, the new method also lends itself naturally to both test result analysis and fault coverage measurement. For test result analysis, the CSP method uses the observed sequence as the initial sequence, constructs all fault models which satisfy the initial sequence and introduces additional subsequences to pinpoint the IUT fault model. In addition, a second method for test result analysis is proposed, which is originated from a model of diagnostic reasoning from first principle, another well-known A l techniques which produces all minimal diagnoses by considering the overall consistency of the system together with the observation. Unlike the first method, the second method does not require the computation of all fault models explicitly, and hence is considered to be more suitable for large systems. To our knowledge, the proposed methods in this thesis represent the first attempt in applying A l techniques to the problem of protocol test sequence generation and analysis.  u  Contents  Abstract  ii  List of Figures  v  List of Tables  vi  Acknowledgement 1  vii  Introduction  1  1.1 1.2 1.3  1 4 5  Background and Motivations Contributions Thesis Outline  2  Test Sequence Generation Methods 2.1 The Finite state Machine Model 2.2 Checking Experiment 2.3 Checking Experiment Based Methods 2.3.1 T-Method 2.3.2 DS-Method 2.3.3 W-Method 2.3.4 UIO-Method 2.3.5 UIOv-Method 2.3.6 Preformance Analysis  6 6 10 12 12 14 18 20 24 25  3  Fault Coverage measurement 3.1 The Uniqueness Criterion 3.2 Arbitrariness in Test Sequence Generation and Fault Coverage Metric  28 28 30  4  The Constraints Satisfaction Problem(CSP) Approach 4.1 Definition of CSP  33 33  iii  4.2  4.3  Test Sequence Generation Procedure 4.2.1 Initial Sequence Selection 4.2.2 Algorithm for Solving the CSP 4.2.3 Generation of Additional Subsequences The CSP Technique - Examples 4.3.1 Example A - F S M with all UIOSs 4.3.2 Example B - F S M with a state that has no UIOS 4.3.3 Example C - Higher Order UTSi  34 36 37 39 41 41 46 48  5  Test Result Analysis - Two approaches 5.1 The CSP Approach for Test Result Analysis 5.1.1 Example - Test Result Analysis Via CSP Method 5.2 Test Result Analysis - from First Principle ; 5.2.1 System Description 5.2.2 Constraint Suspension 5.2.3 Some Important Definitions 5.2.4 Algorithm for Computing Minimal Diagnoses 5.2.5 Example - Test Result Analysis from First Principle  52 52 54 57 58 61 62 65 68  6  Conclusions 6.1 Thesis Summary  71 71  6.2  73  Future Work  Bibliography  74  A Test Sequence Generation Tools  79  B  93  C S P Problem Solver  iv  List  of  Figures  2.1 2.2 2.3 2.4 2.5  A3-stateFSM A Distinguishing-Tree for the F S M in Fig. 2.1 A 5-state F S M A tree for constructing the W set A UIOS-Tree for the F S M in Fig. 2.1  16 17 21 22 24  4.1 4.2 4.3 4.4 4.5 4.6  A search tree for the CSP Two solutions to the CSP A n F S M whose state C has no UIOSs A faulty IUT Three solutions to the CSP in Example B The F S M solutions for Example C  44 45 46 47 49 51  5.1 5.2 5.3 5.4 5.5  A fault model for the observed output sequence All possible fault models for the observed output sequence A 3-state F S M with COMPONENTS=[tl,t2,t3M,t5,t6] A n HS-treeior F={(1,3,5),(2,3),(2,4,6),(2,4),(2,3,6),(1,6)} A HS-Tree for the system description in Example 4  55 56 59 64 69  v  List  2.1  of  Tables  Upper bound for The Five Test Sequence Generation Methods  vi  Acknowledgement  I would like to thank Dr. Son Vuong, my thesis supervisor, for his guidance and support, both moral and financial. I would also like to thank Dr. Chanson for his helpful comments and careful reading of the final draft. Thanks to Runping Qi and Glin Lin for their constructive criticism. I am also indebted to Mr. Shen Liang for his encouragements and advices that I should pursue a career in Computer Science. Finally, I would like to dedicate this thesis to my parents for their unconditional love and support.  vn  Chapter  1  Introduction  1.1  Background and Motivations  Communication protocols are sets of rules and procedures that govern the interactions among communicating entities and so they are crucial for the functioning of computer communication networks and distributed systems. The increasing use of these systems demands reliable communication protocols which are developed using formal techniques and whose implementations are subjected to conformance testing to ensure their interoperability. The problem of systematic generation of test sequences for the conformance testing of protocols has been a major research subject in the area of protocol engineering. Generally speaking, a protocol specification can be viewed as consisting of two parts: a control part and a data part, which may be addressed separately in the context of conformance testing. The testing of the data part, which concerns with checking the parameters o f input and output primitives and local variables, has  1  2  been investigated by a number of researchers using some forms of static data flow analysis[Ural87, Vuon89, Wu90] and functional testing approach[Sari87]. In this thesis, we are only concerned with the conformance testing of the control portion of protocol specifications modeled as finite state machines (FSMs). Several techniques, such as W[Chow78], DS[Gone70], UIO[Sabn85] and UIOv [Chan89b] methods have been introduced for generating test sequences for protocols modeled as FSMs. These methods are similar in their approaches in that a set of state identifying subsequences of a given FSM is used in combination with transition testing to form the final test sequence. Usually, each transition checking is followed by some state checking for the transition.  This checking experiment is known as  /^-testing which differs from a-testing where only state checking is performed without transition checking, and 7-testing where every pair of transitions is tested and is followed by a tail state checking for the pair of transitions.  The generation of  a, 3,7-testing and the arbitrariness of test sequence generation are well discussed in [Sidh89a]. a-testing and 7-testing are not popular because in a-testing, only states are tested, giving very poor fault coverage, whereas in 7-testing, a coverage which is at least as good as the one of /9-testing is achieved, but 7-testing produces much longer test sequences than /^-testing. (3-testing is henceforth adopted or implied in existing methods such as the W , DS, UIO and UIOv methods. In general, the W-method tends to produce excessively long test sequences. The DS, UIO and UIOv methods produce  3  comparable test sequences[Sidh89b, Chan89b]. The problem with the DS method is that a distinguishing sequence (DS) may not exist. The UIO method is more widely applicable, but it does not provide the same fault coverage as the DS method as recently found out [Chan89b]. The UIOv method was henceforth introduced which enjoys both "full" coverage and wide applicability at the price of somewhat longer test sequences [Chan89b, Vuon89]. However, there are several limitations which these methods have in common:  • These methods all assume the number of states in the IUT to be no more than that of the specification. They may not be able to detect a faulty IUT that has more states than the specification.  • These methods do not provide a fault coverage measuring tool for test sequences, therefore qualitative comparison of test sequences is impossible.  • These methods, in general, do not lend themselves to locating errors in test result analysis, especially if optimized test sequences are used. As test sequences are optimized, it is no longer possible to distinguish between the transition checking portions and the state identification portions. Thus, occurring errors cannot be determined as transition or transfer (i.e. state) errors.  4  1.2  Contributions  In the thesis, we have introduced two well known A l techniques, namely, the constraint satisfaction problems(CSPs) technique and diagnostic reasoning from first principle, to the area of protocol conformance testing. Henceforth, we have made the following main contributions:  1. We have developed a new test sequence generation method that provides better fault coverage without increasing the length of the test sequence.  The new  method is also more flexible, in the sense that it allows the number of states in the IUT to be larger than that in the specification. We have also implemented our new method and have tested it on several F S M examples.  2. We have introduced two novel procedures for locating errors in test result analysis. The first procedure is based on the new test sequence generation method which pinpoints the fault model of the IUT by solving the CSP with the observed sequence as the initial sequence , thus identifies all transfer and transition errors. The second procedure is originated from a model of diagnostic reasoning from first principle which computes all minimal diagnoses by considering the overall consistency of the system together with the observation. The second procedure is deemed to be more applicable to large systems than the first procedure since it does not require the computation of all fault models explicitly.  5  3. We have defined a fault coverage metric, thus providing a way of objective comparison of test sequences for a particular F S M .  4. We have also presented a survey on existing test sequence generation methods and have developed clear algorithms for the methods. Most of these algorithms have also been implemented and tested.  1.3  Thesis Outline  The remainder of the thesis is organized as follows. In Chapter 2, an F S M model is presented together with a brief introduction to the checking experiment. In this chapter, a detailed discussion of the existing test sequence generation methods are also presented. Chapter 3 discusses the uniqueness criterion and arbitrariness in test sequence generation and introduces a fault coverage metric at the conclusion of the chapter. In Chapter 4 we introduce the CSP approach. The details of the approach, such as initial sequence selection and CSP algorithm are presented in this Chapter. This chapter also contains several illustrative examples of the CSP method. Chapter 5 describes two methods for test result analysis. The first method is based on the CSP method introduced in Chapter 3. In the second method, we adopt a model from diagnostic reasoning. Finally, Chapter 6 summarizes the main contributions of the thesis and offers suggestions for future research.  Chapter Test  2  Sequence  Generation  M e t h o d s  2.1  The Finite state Machine Model  In this thesis, the control portion of the protocol specification is assumed to be modeled by a finite state machine (FSM). A F S M can be represented as a quintuples:  M=(Q,/,O,/,<7,S ) 0  where Q = the set of states in the F S M I = the set of input symbols 0 = the set of output symbols / = the next state function from Q x 7 to Q g = the output function from Q x I to O So = the set of start states.  6  7  Four assumptions have also been made in the discussion of test sequence generation methods, the FSMs are assumed to be (i)minimal, (ii) strongly connected, (iii) deterministic, and (iv) completely specified.  Definition 1 A FSM M is minimal iff M does not possess any pair of states  5,-  and  Sj such that Si is equivalent to Sj.  Definition 2 A FSM M is strongly connected if for all 5,-,  Sj  G Q, there is a transi-  tion path from s,- to Sj.  Definition 3 A deterministic FSM is a FSM which obeys the following rules: 1. Let S{, Sj and Sk G Q and i G /. f(si,i)=  2.  k  and si G Q,i  f(s i)=  f(sj,i)=  s  k)  Let Si,Sj,Sk  f(si,i)=  s  k>  iff Sj -  s  Let Si,Sj,Sk  i}  3.  Sj and f(si,i)=  s. t  s. k  G  Then, a,- ^ Sj if s  k  and si G Q, i G / 01,02 G  s  h  O,  g(si,i)= oi , f(sj,i)= s ,g(sj,i)= l  ^  o . Then, 5,- ^ Sj if o ^ o . 2  x  2  Rule 1 simply states that accepting an input symbol at a state, a F S M can only go to one and only one state. Rule 2 is merely the negation of Rule 1: the two states from which a F S M moves to two different states, upon receiving the same input symbol,  8  must be different. Rule 3 states that if two states produce different output symbols for the same input symbol, these two states must not be the same.  Definition 4 A FSM M is completely specified iff for each s,- € Q, there is a transition path for each i € I.  In practice, a given F S M is often incompletely specified and inputs received at a given state of the F S M can be classified as follows:  • proper:syntactically correct and a transition defined for it.  • inopportune:syntactically correct and no transition defined for it.  • z7/e<7a/:syntactically incorrect.  In this thesis, a completeness assumption is adopted whenever a F S M is not fully specified, i.e. "unexpected" (inopportune and illegal) inputs will cause the F S M to remain in the same state and to produce null outputs. These four assumptions will be called the four assumptions in the remainder of this thesis. A deterministic F S M model of the control structure of the protocol can be represented as a labeled digraph, G=(V,E), where V is a set of vertices corresponds to the state set of the F S M and E is a set of edges corresponds to the possible transitions between states. Each edge has a label i/o where i and o are input and output  9  operations. The labeled digraph notation will be used to represent the FSMs in this thesis. During the conformance testing, the protocol IUT is treated as a black box with an input and an output port. The inputs to the black box are given at its input port and the outputs can be observed at its output port. A protocol entity typically has an upper interface for its user which may be an upper-layer protocol, and a lower interface for a lower-layer protocol. The inputs and the outputs for both interfaces are merged into a single set of inputs, / , and a single set of outputs, O. All the transitions in a F S M specification together represent the core behavior of a protocol. The corresponding edges and I/Os in the F S M graph are henceforth referred to as core edges and core I/Os respectively. In general, there are two levels of conformance in protocol conformance testing:  • Strong Conformance: If both the IUT and the specification produce the same outputs for all core inputs, and for non-core inputs, the completeness assumption used in the specification is identical to that in the IUT.  •  Weak Conformance: Both the IUT and the specification produce the same outputs for all core inputs. The IUT may not produce the same outputs as the specification for the non-core inputs.  10  This thesis focuses on strong conformance testing since it provides test sequence with better fault coverage.  2.2  Checking Experiment  A checking experiment [Henn64, Koha67, Koha78], also known as a fault-detection experiment, is an experiment designed to take a given F S M through all its transitions, in such a way that a definite conclusion can be reached as to whether or not the machine is operating correctly. Checking experiments have long been used in sequential machine design and have been later introduced to protocol engineering for conformance testing of protocols to standards, yielding test sequence generation methods such as T , D S , W, UIO and UIOv. In a checking experiment, the F S M under test is assumed to be minimal, strongly connected and completely specified.  Moreover, the number of states of the F S M  is assumed to be no more than a maximum number (the number of states in the specification). The goal of a checking experiment is to distinguish a given n-state F S M from all other n-state FSMs. The checking experiments, under certain conditions, can be used to check whether the control part of a protocol implementation conforms to the specification. Generally speaking, if a F S M passes the state identifying sequences based checking experiment, it is ensured to be isomorphic to the F S M model of the specification,  11  with the assumption that all the state identifying sequences are unique to their corresponding states. In this case, the checking experiment is said to have provide full fault coverage for the F S M under test. However, it has been shown that the uniqueness of these state identifying sequences may be questionable in some cases[Chan89b], and not all state identifying sequences based methods provide full fault coverage. A typical checking experiment consists of a set of /^-sequences. Each /^-sequence verifies the uniqueness of a transition. A /^-sequence is constructed as follows:  1. Apply the reset input, ri, to bring the F S M to its initial state.  2. Find the shortest path, SP(si),  to the start state, s,', of the transition to be  verified.  3. Apply the input symbol I of the transition such that the F S M arrives at the end state Sj of the transition.  4. Apply the state identifying sequence, SI(SJ),  for the state Sj.  A /3-sequence for a transition which starts at the state  and arrives at the state Sj  is thus,  8 =ri@SP{si)@I@SI(sj) itj  Recently, some researchers [Aho88, Chan89a] have incorporated the state identifying sequences into the transition tour. This approach eliminates the reset and preamble  12  sequences (i.e.  steps 1 and 2), thus resulting in a shorter overall test sequence.  However, this approach is not applicable to all F S M specifications in general.  2.3  Checking Experiment Based Methods  In this section, five existing test sequence generation methods are discussed. Some of the implementations of these methods can be found in the appendices.  2.3.1  T-Method  A transition tour of an F S M is an input sequence which takes the F S M from its start state, traverses every transition in the F S M at least once, and returns to the start state. This method of obtaining a test sequence is called the T-method[Nait81]. The T-method generates test sequences that are usually shorter than other methods. However, the fault coverage provided by the T-method is also inferior to the other methods since it does not perform state checking. Generally, T-method can detect all the transition errors provided that there is no transfer errors but the detection of transfer errors is not guaranteed. T-method is applicable to all FSMs that satisfy the four assumptions. The followings is a depth-first algorithm that computes a transition tour:  13  Algorithm for Computing a Transition Tour The algorithm uses the Dijkstra algorithm to compute the short path from one transition to its closest untraversed transition. Algorithm 1 Let E=[e\, e , e ] , where e,-, i = l , . . . , n are the edges of the FSM. 2  n  Let Si be the start state of the FSM. We also introduce the following variables: • CS: the current state;  • ST: the transition subtour; Moreover, we assume there is a function SP(i,j)  which computes the shortest path  between state i and state j. 1. Remove an edge e from E whose start state is at Si. Let ST=e k  and CS=Sj,  k  the end state of e . k  2. If there exists an e Remove e  m  m  £ E whose start state is CS then  from E. Let ST=ST@e , m  let CS=Si, the end state of e  Else Remove an edge e from E, let x  ST=ST@SP(CS,S )@e , s  x  where S is the start state of e , let CS=St, the end state of e . a  3.  x  IfE=® return ST@SP(CS,Sij  as the transition tour  x  m  14  Else Go to 2.  2.3.2  DS-Method  In the DS-method[Gone70], a distinguishing sequences(DS) is used as state identifying sequence. A n input sequence is said to be a distinguishing sequence for a F S M if the output sequence produces by the F S M is different for each different starting state. Test sequences generated by the DS-method guarantee to identify an n-FSM from all other n-FSM, thus detecting both transfer and transition errors. The DS-method is not applicable to all FSMs since some FSMs may not possess a DS. DS can be computed by constructing a Distinguishing-Tree [Koha78]. The following algorithm computes a minimal length DS for an FSM:  A l g o r i t h m for C o m p u t i n g D S s A l g o r i t h m 2 Let S ,Si,...,S -i 0  n  be the states of the given n-FSM. Let the root of  the tree, Root, be a singleton set with the single element States=[So, S\,S -iJ.  The  n  Distinguishing- Tree is constructed as follows:  1. Initially, the current node of the tree is Node=Root, i.e.  2. If all elements in Node are singleton sets then Stop. The input path from Root to Node is a DS  Node=[[Sr,,S -\]]. n  15  Else Terminate the node if Node satisfies one of the two conditions: (a) Node is identical to one of its ancestor. (b) One of the element Ni 6 Node contains identical elements. Else Continue.  3. For each input symbol, ik DO  (a) For each Ni, where Ni e Node, DO i. For each Sj, where Sj G Ni, DO A. Apply ik to Sj. B. Update Sj to the end state, Sj, after applying ikii. For each output symbol, o\, resulting from applying ik DO Collect all the S'-s which have the same output symbol 0/ into a set Nf. (b) Let Node be a set of all N(s, go to 2.  E x a m p l e 1 Fig. 2.2 shows a distinguishing-Tree for the FSM in Fig. 2.1. The sequence a.a is the shortest DS for the FSM. The branch labeled [[3,3,1]] is cut off because it contains identical elements 3:  17  [[1,2,3]]  [[2],[1,2]]  [[1],[2],[1]]  [[3,3,1]]  [[3],[2,3]]  a.a is the shortest distinguishing sequence.  Figure 2.2: A Distinguishing-Tree for the F S M in Fig. 2.1  18  2.3.3  W-Method  A characterization set W of a F S M is derived and used for state identification for the F S M in the W-method [Chow78]. A characterization set W for a F S M is a set consisting of input strings ( a  l 5  a ) k  such that the output symbols observed from  the application of these strings (in a fixed order) are different at each state of the F S M . Like the DS-method, test sequences generated by the W-method guarantee to detect both transfer and transition errors under the four assumptions. Unlike the DS-method, the W-method is applicable to all FSMs that satisfy the four assumptions. The W set can be computed by constructing a tree similar to the Distinguishing-tree. The following algorithm builds a tree by which a W set can be computed:  A l g o r i t h m for computing the W set Before we describe the algorithm, we need to introduce some new notations.  Definition 5 Let two sets R=[r ,r J x  n  and S—[si,..,s ] whose elements r- 's and m  t  Sj's are also sets. We define the set operation R n S as:  R n S = [r C\si,...,ri x  Ds  m  Definition 6 Consider the set S=[Si, ...,S J m  we define the set F(S)=[first(Si),...,first(S )] m  , r  n  Ds  u  where Si —  r fl s ] n  m  [s(xi,yi),...,s(x ,y )J, ni  where first(Si)—[xi, ...,x J). n  ni  19  The following algorithm computes a W set for an n-FSM.  Algorithm 3 Let So, Si,S„_i  be the states of the n-FSM  and  SingletonS=[[So],...,[S -iJJ-  Let the root of the tree. Root, be a singleton set with the single element  States=[s(S , 0  where for every s(Si,Sj), the current state,  So), s(Si, Si),s(5 _i, n  S„_i)7  Si denotes the original state of the path and Sj represents  we also let Wset=§  and CW=Root.  The tree is constructed as  follows:  1. Initially,  the current node of the tree is  2. If SingletonS  Node=Root.  C CW then Stop, W set is in Wset.  3. For each input symbol, ik DO  (a) For each Ni, where Ni € Node, DO i. For each Sj, where Sj € Ni, DO A.  Apply ik to Sj.  B.  Update Sj to the end state, Sj, after applying ik-  ii. For each output symbol, o\, resulting from applying ik DO collect all the S'jS which have the same output symbol o\ into a set N[. iii. Let Node be a set of all N[s.  n  20  iv. If CW l~l F(Node) contains more singleton set than CW then A.  Wset=Wset+path from Root to Node  B. CW=CWV\  F(Node)  v. Go to 2. (b). Let Node be a set of all N(s, go to 2.  E x a m p l e 2 Fig. 2-4 shows a tree from which the W set can be constructed for the FSM shown in Fig. 2.3.  2.3.4  UIO-Method  The UlO-method uses a set of unique input/output sequences(UIOSs) as the state identifying sequences. A n UIOS for a state is an I/O behavior not exhibited by any other state in the F S M . Sometimes, an UIOS may not exist for a state, in this case, a state signature is used. A state signature is a sequence formed by concatenating a set of input sequences, each of which distinguishes the state from one other state in the F S M . The UlO-method has the same applicability as the W-method. The test sequences generated by the UlO-method have fault coverage comparable to those produced by the W- and DS-method in most cases. However, it has been shown that some errors may go undetected in some cases [Chan89b].  Figure 2.3: A 5-state F S M  22  [[s(0,0),s(l,l),s(2,2),s(3,3),s(4,4)]] Wset=[A] CW=[0,2,3],[1,4]]  ^  /  X.  X  X  [[s(0,3),s(3,4),s(2,l)],[s(l,4),s(4,2)]]  Wset=[A,B]  \CW=[[2],[3],[1,4],[0]]  [[s(2,3)],[s(3,3),s(l,2),s(4,0)],[s(0,0)]]  Wset=[A,B,AA] CW=[[0],[1],[2],[3],[4]] / [[s(0,4)],[s(3,2),s(2,4)],[s(l,2)],[s(4,l)]]  Figure 2.4: A tree for constructing the W set UIOSs can be computed in a similar fashion as the DSs, i.e. constructing an UIOSTree. The algorithm is similar to that of the DS-method with some modifications in the terminating conditions of the nodes. The shortest UIOS is computed as follows:  Algorithm for Computing UIOS Algorithm 4 Let S ,Si, . . . , S _ i be the states of a given n-FSM. Let the root of the 0  n  tree, Root, be a singleton set with the single element States=[s(S , S ), s(Si, 5 ) , s ( S „ . i,S -i)J 0  Q  a  n  where Si denotes the original state of the node and Sj represents the current state. The UlOS-Tree is constructed as follows: 1. Initially, the current node of the tree is Node=Root.  23  2. If each state  3. If Node  has at least one UIOS,  contains  elements  For each singleton  stop.  that are singleton  set element  sets  then  s(S{, Sj),  record the path from Root to Node as an UfOS  for Sj  Else Terminate  the node if Node satisfies  (a) Node is identical (b) All elements singleton  one of the two  to one of its  conditions:  ancestor.  in the N('s £ Node contains  sets or sets with all identical  either  elements  Else  Continue.  4- For each input symbol,  ik DO  (a) For each Ni, where Ni £ Node, i. For each Sj, where Sj G Ni,  DO DO  A.  Apply ik to Sj.  B.  Update Sj to the end state,  ii. For each output symbol, Collect  Sj, after applying ik-  o\, resulting  from  applying ik DO  all the 5's which have the same output symbol o; into a set N{.  24  (b) Let Node be a set of all Njs, go to 2.  Example 3 Fig. 2.5 shows a UIOS-Tree for the FSM in Fig. 2.1. [[s(Sl,Sl),s(S2,S2),s(S3,S3)]] singleton set a is an UIOS for S i .  [[s(Sl,S3),s(S2,S3),s(S3,Sl)]]  [[s(Sl,S2)],[s(S2,Sl),s(S3,S2)]]  [[s(Sl,Sl)],[s(S2,S2)],[s(S3,Sl)]]  [[s(Sl,S2),s(S2,S2)],[s(S3,S2j  [[s(S ,S3)], s(S2,S3),s(S3,S3)]] 1  [  singleton sets a.a is an UIOS for SI, S2 and S3. singleton set a.b is an UIOS for SI.  ,^  ^  ^  ^  singleton set b.a is an UIOS for S3.  Figure 2.5: A UIOS-Tree for the F S M in Fig. 2.1  2.3.5  UIOv-Method  In the UIOv-method[Chan89b], an UIOSs uniqueness verifying procedure is added to the UlO-method. The purpose of this procedure is to verify the uniqueness of the UIOSs, thus detecting errors which may be undetected due to non-unique UIOSs. The  ^  25  resulting TJIOv-method provides test sequences that have as good a fault coverage as those provided by the W- and the DS-method without sacrificing its applicability.  U I O S verifying procedure  Suppose we have a set of XJlOSs=[UIOS\,UIOS ], m  each UlOSi is the UIOS for a  set of state 5,. We also assume there is a reset symbol, ri, which takes the F S M back to its initial state. Moreover, the function SP(s,-,.$j) is available which computes the shortest path from state i to state j. Let s be the initial state of the F S M . We can 0  carry out the procedure as follows: For each UlOSi <E UIOSs Do For each Sj £ Si apply the sequence  2.3.6  ri@SP(so,Sj)@UIOSi  Preformance Analysis  In this section, we compare the performance of the five test sequence generation methods in terms of the length of the test sequence. The upper bound for T - , W- and DS- method have been given in [Sari84]. In the followings, we prove the upper bound for UIO and UIOv methods.  T h e o r e m 1 The upper bound of the length of a test sequence generated by the UIOmethod is of 0(kn ). 4  26  P r o o f 1 Let G be a strongly connected digraph representing a deterministic FSM M with n states and k. input symbols, and the maximum number of edges in G is kn. In the worst case, a state signature is required for each state. The length of a state signature is of 0(n ) [Koha78j. Since G is strongly connected, it takes at most n2  1 transitions from one edge to any other edge. Thus, the overall length of the test sequence is of  0(kn)*0(n )*0(n-l)  —• 0(kn )  2  4  T h e o r e m 2 The upper bound of the length of a test sequence generated by the UIOvmethod is ofn . 5  P r o o f 2 The complexity of the UfOv-method is equal to the sum of the complexity of the UIO method and the UIOv procedure. The complexity of the UIOv procedure is of 0(n )*0(n 2  — l)*0(n)*0(n  — 1) — > 0(n ).  The n term is for the state-identifying  h  2  sequence (UIOS or state signature), the first n — 1 term is for the verifying procedure for the other n — 1 states, the n term is for the n states of the FSM and the last n — 1 term is the premable for bringing the FSM to the desired state. Since k <n, therefore the complexity of the UlOv-method is of 0(n ) + 0(kn ) — • 0 ( n ) . h  4  5  The complexity of the five methods is summarized in Table 2.3.6. Although the T method has the best upper bound, it does not detect any transfer error. Among the  27  Table 2.1: Upper bound for The Five Test Sequence Generation Methods T-method 0(kn ) 0(kn ) DS-method W-method 0(kn ) 0{kn ) UlO-method UlOv-method 0(n ) 2  n+2  4  4  5  remaining four methods, the UlO-method is the most widely used method. Although the W- , the DS- and the UIOv- methods produce test sequences with slightly better fault coverage than the UlO-method, the W- and the UIOv- method produce longer test sequence and the DS-method is not applicable to all FSMs since DS may not exist for some FSMs.  Chapter Fault  3.1  3  Coverage  measurement  The Uniqueness Criterion  The goodness of a test sequence depends primarily on its fault coverage. To provide the absolute full fault coverage for a given F S M , the test sequence must uniquely identify the F S M among all possible FSMs.  Such a test sequence is said to be an  unique test sequence (UTS) for the FSM. However, it is not always possible to distinguish one F S M from another (e.g. isomorphic). Therefore, the definition of U T S must take into account such factors. In order to define U T S , first of all a notion of equivalence, similar to that of [Dahb88], has to be defined.  Definition 7 For two FSMs Ml and M2, Ml is a subset of that of M2.  Then, U T S can be defined as follows:  28  contains M2 iff the behavior of M2  29  Definition 8 A test sequence TS is an UTS for a FSM M iff for any FSM M' which accents TS and generates the same outputs as M, M' must contains M.  In general, the domain of FSMs considered is unbounded if we do not impose a bound (e.g. on the number of states of the FSMs). Consequently, a true U T S has to be infinitely long and a finite test sequence can only be an approximation of the UTS. The goal of test sequence generation is thus to generate a good approximation of the UTS taking into the consideration the tradeoffs among fault coverage and length of test sequence, and computing time. In this section, we introduce a new definition for an achievable "unique test sequence" by relaxing the uniqueness criterion. This definition will then be used in the next section to define a fault coverage metric. The FSMs considered in test sequence generation are, in general, assumed to be minimal, strongly connected and completely specified (under the Completeness Assumption). Furthermore, we assume the FSMs considered have an upper bound, L, on the number of states. If L = n + i, where n is the number of states of the given F S M , we define UTSi to be the test sequence for this F S M such that only this F S M and no other FSMs of k states, where k < L, can generate the same input/output sequence. Although not explicitly stated, methods such as DS, UIO and W assume L = n and generate only UTSq.  In some cases, UIO method may not generate 3  sequences which are an LTS'o[Chan89b].  The assumption L = n limits the fault  30  coverage of the generated test sequences.  If there are more than n states in the  IUT F S M , These method will not guarantee the uniqueness of the generated state identifying sequences owing to the extra state in the IUT F S M .  3.2  Arbitrariness in Test Sequence Generation and Fault Coverage Metric  Arbitrariness in test sequence generation was noted in [Sidh89a]. In checking experiment methods, there are several arbitrary decisions involved , for examples: (i)the selection of the method for generating state identifying sequences (e.g. W , DS, UIO), UIOv), (ii)selection of the number of transitions in the transition testing part of each subsequence(e.g.  8 sequence is typically selected among a, 8, 7,... sequence), and  (iii) choice of a method for combining the set of (8) subsequences( e.g. whether reset and preamble, or the Chinese Postman Algorithm and/or overlapping of subsequences are used). Due to such arbitrariness, several test sequences are possible for a given test sequence generation method, whether it is the DS- , W- or UIO method, for a protocol F S M . Moreover, these test sequences may not have the same fault coverage. Therefore, in order to assess the quality of an overall test sequence generation method in term of coverage, it is important to define a fault coverage metric. In this section, we use the definition introduced in last section to present a fault coverage metric that allows the objective comparison of fault coverages of test sequences.  31  In the last section, we have defined the UTSi.  It is obvious that fault coverage  increases with the increasing index i of the UTSi since more FSMs with a larger bound on the number of states would be taken into consideration . Each UTSi, thus, uniquely identifies a given F S M under the assumptions of minimal, strongly connected FSMs having no more than n + i states. In the next chapter, we will present a test sequence generation method that can handle extra states and is applicable to UTSi in general. However, the larger the extra number of states, i, is allowed, the longer the UTSi would be. We note the correspondence between the arbitrariness of generated test sequences UTSi based on number of extra states, i, and the arbitrariness defined by Sidhu and Valluruoalli on the state and transition relationship in a F S M : a state can be uniquely identified by a sequence of transitions (UIO sequence). Consequently, the larger number of transitions are used(e.g. in 7 sequences) the larger number of states can be identified. In this last section, we have relaxed the uniqueness criterion for U T S by assuming the limit, L = n + i, on the number of states of the FSMs to be considered. With this assumption, we now redefine an UTSi to be a test sequence which uniquely identifies a given n-state F S M from all IUT FSMs having at most L = n + i states. Let k be the number of non-equivalent FSMs with at most n + i states, which can accept a given test sequence TSj, i.e. the number of FSMs that the test sequence TSj fails to distinguish from the given F S M . Then a relative measure of fault coverage for the  32  test sequence TSj can be defined as follows:  A test sequence with fewer such FSMs that it fail to distinguish from the given F S M will have a better fault coverage than the one with more such FSMs. In particular, if Fd(UTSi)  = 1, the UTSi for the F S M provides the "full" fault coverage since there  is only one F S M , the given one, that accepts the UTS,. This metric thus provides a way of comparing the goodness (fault coverage) of given test sequences for a particular F S M . In general, the absolute fault coverage can be defined as follows:  FdiTSj)  =  =  NM{n,i)RFd(TSj)  where NM(n, i) is the number of FSMs with the number of states < n + i To compute the relative fault coverage RFC{ for a given test sequence TSj, TSj is used as the initial sequence for the CSP. If there are k solutions to the CSP, then RFCi(TSj)  =\.  Chapter T h e  4  Constraints Satisfaction  P r o b l e m ( C S P )  4.1  A p p r o a c h  Definition of CSP  Techniques for solving the constraint satisfaction problems(CSPs) have been an active research area in the A l community for many years. Its application has extended to many other areas such as operations research and hardware design. A CSP involves a set of variables x  x  , x  n  having domains D \ , D  values. A constraint dj(xi,Xj)  n  where these variables take their  between the variables X{ and Xj (i<j) specifies which  values of the variables x; and Xj are compatible with each other. In general, a constraint C,...A:(x,-,Xk) specifies the values Vi,...,v , where u,- G Di,...,v k  k  € Dk, which  the variables can take on. The CSP is the problem to find all sequences of values V{,...,v for a set of variables z,-,...,x n  n  that satisfy all the given constraints. CSPs  are in general iVP-complete problems. However, by exploiting domain knowledge and manipulating constraints cleverly, researchers like [Fike70], [Mont74] and [Mack77]  33  34  have all shown that some CSPs can be solved efficiently. In the test sequence generation problem, each edge with label i/o form a constraints on the two state variables connected by this edge. The i/o constraints combined with the global constraints described in Section 2.1 give a set of stronger local constraints which restricts the values the states variables can take on. Even though the problem of test sequence generation is based on the CSP, this problem is different from the conventional CSPs in that a set of constraints instead of the solution itself, is to be found such that the given F S M is the only solution to the CSP.  4.2  Test Sequence Generation Procedure  The overall test sequence generation procedure consists of three steps:  1. Select an initial sequence and derive the corresponding constraints.  2. Find the FSMs which satisfy the constraints derived from the initial sequence.  3. Generate additional sequences to distinguish the given F S M from the remaining ones.  Before describing the steps of the procedure, it is helpful to explain how a test sequence can be represented by a set of constraints. In general, a test sequence i\/o\  i /o P  p  can be expressed as a set of constraints using the notation described in Section 2.1, as follows:  35  f(xi,n) = x , 2  The variables Xi,...,x  p  must satisfy this set of constraints together with the basic  constraints described in Section 2.1. D -\ v  C  g(xi,ii) = oi  The domains for these variables D  2  = ... =  the set of states in the F S M . In this thesis, we also introduce a fourth  constraint in order to make the CSP more tractable. This constraint states that every generated test subsequence must start and e nd at SQ £ So- With no loss of generality, a reset input symbol r is introduced which brings the F S M from any state back to the start state So and back to the start state. This ensures the fourth constraint can be satisfied.  Therefore, we must have D\ — s , the start state of the F S M , from 0  the fourth constraint. Each solution is a set of values Vi,...,v , p  where U i , . . . , u  p  £ Q,  which represents a F S M . The problem of generating an UTSi is thus to find a set of subsequences such that there is only one solution to the CSP. Suppose a set of subsequences produces r solutions. Then, there are r FSMs whose number of states equal to m i , m  s  ,  that can accept the set of subsequences. In this  case, additional subsequences must be introduced to distinguish the given F S M from  36  the remaining ones. The procedure for generating these additional subsequences can be easily automated. Since the structures of all the FSMs are known, the length of the subsequence needed to distinguish two minimal FSMs with the number of states ni and n is at most n , where nj < n . In order to keep the number of FSMs that 2  2  2  can accept a test sequence reasonably small, the initial sequences must be carefully selected. This issue of initial sequence selection is considered in the next section.  4.2.1  Initial Sequence Selection  Generally speaking, any transition tour of the F S M can be used as the initial sequence. Other initial sequences may be more desirable if they contain more knowledge (constraints) on the structure of the F S M than the transition tour. These initial sequences, which may be longer and harder to generate, would reduce the complexity of the CSP to be solved. For instance, if the initial sequence adopted is the test sequence derived using the DS method, the corresponding CSP will have only a single solution. In this case, the unique test sequence UTSQ is precisely the initial sequence and the CSP method simply verifies the uniqueness of the initial sequence. As noted earlier, a test sequence based on the DS method may not exist or its length may be too long. A test sequence derived from the UIO method is generally considered as a practical choice for the initial sequence. This sequence can be derived using the algorithm described in [Sabn85] with the following modification. Whenever a state does not possess an  37  UIO sequence of length less than or equal to n, the subsequence which checks this state will be omitted ( In [Sabn85], a state signature would be used if the UIOS is of length exceeding n ). The initial sequence generated using this method, contains 2  more knowledge (constraints) on the structure of the F S M than the transition tours generated by the T method [Nait81]. Yet its length is no longer than kn , where 2  k is the maximum out-degree (the number of different input symbols) and n is the number of states. For generating higher order UTSi, we choose to adopt the scheme describes in [Sidh89a]. For a given i, we check i + 1 transitions before state checking, i.e. 8testing for i = 0, 7-testing for i=l, etc... It is possible that some F S M solution may contain the target F S M , we use the containment algorithm described in [Dahb88] to eliminate all the F S M solution that contain the target F S M . In the next section, we will present an efficient algorithm for solving the CSP.  4.2.2  Algorithm for Solving the CSP  A l g o r i t h m 5 Given a test sequence TS of length I that covers all the edges of a k-state FSM M, the following algorithm computes all the s-state FSMs (s <k) that satisfy TS. Let S = {so,Sk-i}  be a set of k states, and X = {xi,...,x } (m < I) be a m  set of state variables such that each x- £ X can take on a value Sj £ S, and let Si t  38  and S C S. Furthermore, let EQ and NEQ be two sets of constraints such that each 2  constraint e = (y ,  is either in EQ or NEQ, e G EQ V e G NEQ, where y,- G X is  t  a state variable and yj € S\JX can be a state variable or a state value. Ifyi,yj G X are both state variables, then i > j. Each constraint e = (y,,yj) represents a relation between yi and yj. If yi = yj then e G EQ, otherwise if yi ^ yj then e G NEQ. An algorithm for solving the CSP can be presented as follow:  1. Convert TS to a set of equalities E as shown in Section 4-2, and construct the set X from E.  2. Initially S\ ={s } d an  0  $2 —  --^fc-i}-  3. If (S ^ 0,) then 2  Si = Si + s  x  and 5 = S — s 2  2  x  where s G S x  2  4- Apply rules 1 to 3 in Section 2 to obtain EQ and NEQ. For each e = (yi,yj) G EQ, remove yi from X, replace yi by yj in NEQ and E.  5. Remove an element x G X and let Sj, = S\. For each e = (y,-,j/j) G NEQ 3  where yi = x and yj G Si, remove yi from Sd3  6. For each s G Sd, let x = s . g  s  g  If E is consistent with rules 1 to 3 in Section 2 under the assignment for x do s  39  If X = 0, then a solution is found else go to 3.  7. stop.  The use of Si and S in steps 2 and 3 are necessary to avoid to consider the FSMs 2  which differ only by state renaming. Steps 4 and 5 help eliminating some impossible solution candidates. Step 6 examines all possible solution candidates and tests everyone of them. The algorithm stops when all possibilities are considered.  4,2.3  Generation of Additional Subsequences  The above algorithm finds all the FSMs that satisfy the initial sequence. To generate additional subsequences to distinguish amongst the FSMs, the following algorithm is used:  1. Select a FSM from the set L; generate a subsequence ts that distinguishes the target FSM from the selected one; and delete the selected FSM from L.  2. Apply ts to the remaining FSMs in L and delete from L all the FSMs that do not produce the same output as the target FSM.  3. Stop if there is only one FSM, i.e. the target FSM, left in L. Otherwise, go to 1.  40  Initially L is the set of all F S M solutions and when the algorithm stops, the overall additional sequence comprise all subsequences generated in step 1. In step 1, a breathfirst algorithm is used to distinguish between a pair of FSMs.  For two strongly  connected n-state FSMs M i and M to be different, there must exist a pair of states 2  i in M i and j in M such that the transition functions (i.e. outputs) of i and j are 2  different. Since the FSMs are strongly connected, it takes at most n transitions to go from the start state to i and j in FSMs M i and M respectively,, and once in i and 2  j, an extra transition is needed to distinguish between M i and M . 2  Therefore, the  maximum length of an additional sequence is of order 0(n), and breath-first search will guarantee this length can be achieved. Moreover, if k is the maximum out-degree, there are at most kn distinct edges. Once an edge has appeared once in the breathfirst tree, the next time it appears again, that branch of the tree can be cut off. Hence, the maximum number of state comparisons is kn and each comparison may consist of at most k i/o comparisons. Thus, the overall time complexity of generating an additional sequence is of 0(k n). 2  This test sequence generation procedure has been implemented as a Quintus Prolog program running on Sun workstations. appendices.  The source code can be found in the  41  4.3  The CSP Technique - Examples  In this section, we illustrate the CSP technique of test sequence generation using some simple examples.  4.3.1  Example A - FSM with all UIOSs  In this example, we show how an UTS is constructed for the F S M in Figure 2.1. We 0  select the initial sequence which is derived from the modified UIO method described in Section 4.2.1(see also [Vuon89] or [Chan89b]):  r/ -  .a/l.a/O./a/l  r/ -  .a/l.b/l.b/l.a/1  rj -  .b/l.b/l.a/1  rf - .a/1.6/l.a/0.a/0.a/l  When converted to the Prolog's clausal representation, the initial sequence can be expressed as follows:  c(s ,X , a/l),c(X ,X a/0),c(X 0  0  0  u  X , a/1)  u  2  c(a , X , a/l),c(X , X , b/l),c(X , X , 6/1), c(X ,X , 0  3  3  4  4  5  5  6  a/1)  c(s , X , b/l),c(X , X , b/l),c(X , X , a/1) Q  c(s , X , a/l),c(X , 0  1 0  w  X  7  1U  b/l),c{X  7  lu  8  8  9  X , a/0), c ( X , X , a/0), c ( X , X , a/1) 1 2  12  a 3  13  1 4  42  The first clause represents a transition from the initial state 3Q to some state XQ with an I/O a/1. Similarly, the second clause represents a transition from some state XQ to some state X\ with an I/O a/0, etc... Applying rule 1 of Chapter 2, we obtain the following constraints  XQ  Constraints XQ = X = X 3  c(s , XiQ,a/l). 0  = X = 3  and X4 = X\\  XIQ  are derived from clauses c(so, XQ, a/l),c(so, X3, a/1) and  w  Similarly, X = X 4  n  is obtained from c(X , X , 6/1) and c(X , X , 6/1). 3  4  w  n  After renaming and removing duplicate clauses, the following clauses remain: c(s , XQ, a/l),c(X , Q  X ,a/Q),c(X ,X ,  0  1  1  c(s , X , b/l),c(X ,X , 0  a  4  0  7  b/l),c(X ,  X , a/1)  X , b/l),c(X ,  X , a/1)  5  c(s , X , b/l),c(X , 7  5  8  c(X , X , a/0),c(X ,X , 4  12  12  a/1)  2  e  8  9  a/0),c(X , X  13  13  1 4  , a/1)  The following set of inequalities constraints can also be derived by applying rules 2 and 3 of Chapter 2 to the clauses above: $0, XQ  ^0  7^  X4  7^ 5 , 0  ^  7^  X\, XQ 7^ X , 5  X  4  7^  7^  Xg, Xo  7^  Xi  7^  Xg, -^4  7^  Xi3  X , X4 5  X\2 7^ ^0,-^12 7^ ^15-^12 7^ - ^ 5 , ^ 1 2 7^  3  X12 7^ X 1 3  For example, X 7^ s is derived from clauses c ( s , X , a / l ) and c(X ,Xi,a/0) 0  0  0  0  o  since  applying the same input symbol a to X and s results in different output symbol. 0  0  43  The state variables are now reordered in the descending order of the number of their occurrences in the clauses so that the variable with most occurrences, i.e. the most important constraints, will always be considered first. In this way, we will achieve the most efficient cutoff in the search tree since assigning values to such variable will impose the most constraints to the structure of the F S M . The following order is obtained:  Xo, X ,Xi, 4  X5, Xr, X$, X12, X\3, X2, Xq, Xg, X\  4  The search tree for the CSP is shown in Figure 4.1. The assignments in N O D E 1 is obtained from the clauses c(X0,XI,a/0) assignments XO = 51 and XA = 51.  and c ( X 4 , X l 2 , a / 0 ) The assignment XI  considering the inequalities XO ^ XI and XI assignment XO = 51 and X4 = 52.  and the previous  = 50 is obtained by  ^ 52 together with the previous  All other nodes are generated in the similar  fashion. Two solutions are obtained for the CSP and the two corresponding FSMs are shown in Figure 4.2. As can be easily verified, the target F S M can be distinguished from the faulty F S M by applying the subsequence 6/1.a/0 . The overall test sequence is thus:  r/r/-  .a/l.a/Q./a/l .a/l.b/l.b/l.a/l  r/ - .6/1.6/l.a/l  44  NODE 1  X4=S2  X1=X12 X4=X5  contradiction lction NODE 2  X1=S0  \  X5=S0 X6=<  X7=S0 X8=S0 X9=S1  X7=S1 X8=X4  X7=S2 X8=S0  :a=si  contradiction  X12=S1  X12=S1  X12=S2 X13=X12  I  X13=S0 X14=S1  contradiction  X13=S0 X14=S1 X2=S1 solution  X2=S1 solution  Figure 4.1: A search tree for the CSP  45  (  Y'  1  b/1  Figure 4.2: Two solutions to the CSP  46  r/ -  .a/l.b/l.a/O.a/O.a/1 rj - .fe/l.a/O  4.3.2  Example B - F S M with a state that has no UIOS  Figure 4.3: An F S M whose state C has no UIOSs  Figure 4.3 shows an F S M whose state C has no UIOS. We follow the procedure described in [Sabn85] to construct a test sequence based on the UIO method. After optimization, the following sequence is obtained:  rj - .0/1.0/0.0/1.1/0 r/-.1/0.0/0.0/1 rj - .1/0.1/1.0/0.0/1.1/0 rj - .0/1.1/0.1/1  47  Note that a signature, 0/0.0/1.1/0, is used for state C. The UIOSs for states A and B are 0/1 and 1/1 respectively. This test sequence, however, fails to detect the faulty IUT shown in Figure 4.4. A n unique test sequence(£/T.So) for the given F S M can be  V  J 1/1  Figure 4.4: A faulty IUT  constructed by using the CSP method. The following modified UIO sequence is used as the initial sequence:  rf - .0/1.0/0.0/1 r/-.1/0.0/0.0/1 r/-.1/0,1/1 rf - .0/1.1/0.1/1  48  Applying the same procedure presented in Section 4.2 and Example A to solve the CSP, three FSMs solution are obtained as shown in Figure 4.5. To distinguish the target F S M (the leftmost F S M in Figure 4.5) from the remaining two FSMs, the following subsequences can be used as can be easily verified: rj-  .1/0.1/1.0/0  r / - .0/1.1/0.1/1.1/0 After optimization (removing subsequences that are contained in other subsequences) we have the following overall test sequence: rj - .1/0.1/1.0/0 rj - .1/0.0/0.0/1 rj - .0/1.0/0.0/1 rj - .0/1.1/0.1/1.1/0 It is interesting to note that in this example, the test sequence generated by the CSP method is not only shorter than the one generated by the UIO method (17 for the CSP and 19 the for UIO), but it also provides a better fault coverage, it can detect the faulty IUT F S M of Figure 4.4.  4.3.3  Example C - Higher Order  In this example, we show how an UTSi  UTSi  can be generated for the F S M shown in Fig.  2.1. The initial sequence is generated by the procedure described in Section 4.2.1.  49  Figure 4.5: Three solutions to the CSP in Example B  50  We use the 7 approximation since we want to compute UTS\. State C has no UIOS, therefore we omit state checking for all transitions that end at state C. Then, the initial sequence, an UTSQ obtained using the 7 approximation is shown as follows:  r/-.a/l.b/l.b/l.a/l r/-.a/l.b/l.a/0.a/0.a/l r/-.a/l.a/0.a/l.a/0.a/l r/-..a/l.a/0.b/l.b/l.a/l r/-.b/l.b/l.b/l.b/l.a/l r/-.b/l.b/l.a/l.a/0.a/l r/-.b/l.a/0.a/0.a/l r/-.b/l.a/0.b/l.b/l.a/l  After feeding to our Prolog program, we obtain nine F S M solutions. After eliminating the F S M solutions that contain the target F S M , Figure 4.6 shows the remaining three F S M solutions. The sequence a/1.a/0.b/1.a/0 can serve to distinguish the target FSM from the other two solutions.  51  Figure 4.6: The F S M solutions for Example C  Chapter Test  5  Result  Analysis -  T w o  approaches  In this chapter, we discuss two different methods for test result analysis. The first method is based on the CSP technique introduced in the previous chapter.  This  method constructs all possible fault models for the observed output sequence by solving the corresponding CSP. The second method which is deemed to be more effective than the first method in dealing with large protocols, computes all minimal diagnoses by reasoning from first principles, i.e. using the structural description and the observation of its behavior.  5.1  The CSP Approach for Test Result Analysis  In test result analysis, an observed test sequence is analysed to check if errors occur in an IUT, and to locate and determine the type of these errors in the specification. Most existing methods for test sequence generation, e.g. DS[Gone70], UIO [Sabn85]  52  53  and W [Chow78] methods, generate test sequences by combining state checking with transition checking and do not lend themselves directly to test result analysis. When multiple errors occur in an implementation under test (IUT), it is very difficult to identify the types of errors (state errors or transition errors) and to locate them. Specially when optimized test sequences are used, the task of identifying and locating errors becomes even more difficult. In this section, a procedure for test result analysis is introduced. An UTSi can detect both transfer (i.e. state) and transition errors under the four assumptions. Pure transition errors can be easily located since they are observable. However, when there are multiple transfer errors or combinations of transfer and transition errors, locating errors can become a very difficult task. In the CSP method, a F S M fault model that represents the structure of the faulty IUT is constructed from the observed inputs/outputs sequence and allows errors to be identified and located. Given an observed inputs/outputs sequence to be analyzed, the observed inputs/outputs sequence can be used as the initial sequence for the CSP method. After solving the CSP, each solution represents a possible FSM model for the IUT. If none of the solutions is the specification F S M , the observed sequence indicates the IUT fails the test. At this stage, new subsequences can be added to pinpoint the structure of the faulty IUT in order to identify and locate the error(s). It is worth noting that the CSP may have no solutions. In this case, we conclude that our basic assumptions  54  are violated; the IUT may have more states than expected.  5.1.1  Example - Test Result Analysis Via CSP Method  To illustrate how the CSP method can be used to locate errors in a faulty IUT, we use the same F S M as given in Example B of Section 4.3.2, and we use the UIO based test sequence in the same example to test the IUT. The result is as follow:  Input:  rOOOlrlOOrllOOlrOll  Expected Output:  -1010-001-01010-101  observed Output:  -1010-000-00010-100  Just by looking at the output sequence, we may conclude that the IUT contains a transfer error from state B to state C ( l / 1 becomes 1/0) and a transition error in the outgoing edge of state B(the 0/0 edge from B to A ends up in C), thus yielding the fault model in Figure 5.1. obtained!  However, by solving the CSP, six fault models are  Each of these fault models can produce the observed output sequence.  These fault models are shown in Figure 5.2. In order to pinpoint the fault model, we need to introduce some new subsequences. Since these FSMs all satisfy the observed sequence, they all share some common edges (0/0 from C to A , 0/1 from A to C , 1/0 from A to B and 1/0 from B to C). Note that the algorithm described in Section 4.4 eliminates all isomorphic machines and it also adopts a consistent naming system. Therefore, we can compare the edges of these FSMs. These FSMs can be distinguished  55  Q  Q i/o  1/0,0/0  1/0  1/0  Specification  Fault Model  Figure 5.1: A fault model for the observed output sequence by their free edges, i.e. edges that together unique to these FSMs and not shared by any other F S M . For instance, F S M 1 can be distinguished by the edges 1/0 from C to A and 0/0 from B to C; no other FSMs possess both of these edges. For this example, the fault model can be identified by the following sequence:  input sequence: rOlOOrlOOO outputs (FSM1): -1010-0001 (FSM2): -1010-0000 (FSM3): -1001-0001 (FSM4): -1001-0000 (FSM5): -1000-0000 (FSM6): -1000-0001  56  FSM 5  0/0  FSM 6  Figure 5.2: A l l possible fault models for the observed output sequence  57  By applying the above input sequence to the IUT, we can tell which of the above six FSMs corresponds to the IUT from the observed output sequence. It is interesting to note that the transition from states B to A and the transition from states B to C are defective in all six fault models.  5.2  Test Result Analysis - from First Principle  In the last section, the proposed CSP method for test result analysis requires explicit computation of all fault models. When dealing with large system such approach may not be feasible. In this section, we introduce a new approach which does not require explicit computation of all fault models. Instead, this approach computes the minimal diagnoses for a given F S M based on the system description and the observation of the F S M . Over the past few years, many diagnostic reasoning systems have been developed that reason from first principles. Davis[Davi84],Genesereth[Gene84] and De Kleer[dKle87] all have developed systems that based on this approach. This approach offers some features that other approaches such as the empirical associations used in some rule-based systems(e.g. Mycin[Shor76]) seem to lack. First, systems based on this approach are highly machine independence. Second, systems based on this approach are easier to construct because there is a way of systematically enumerating the required knowledge: structure and behavior of the device.  58  Generally speaking, there are three major components in a system that reasons from first principle. These components have been given in Davis' paper[Davi84]. They are:  1. a language for describing structure,  2. a language for describing behavior, and  3. a set of principles for trouble shooting that use the two descriptions to guide their investigation. This component consists of two functional units:  1. a unit for checking system consistency, and 2. a unit for effectively generating candidates  In this section, we will fit the problem of test result analysis for protocols modeled as FSMs into the framework of diagnostic reasoning from first principle.  5.2.1  System Description  The system description of an F S M consists of two parts:  1. The structural description which consists of:  (a) COMPONENTS,  the individual transitions, is a finite set of constants.  (b) MD, a machine description which describes the relations of the states and the edges in the F S M , and other general properties of the machine (de-  59  terministic property in our case), which are assumed to be valid at all time.  2. The behavioral description which consists of:  (a) OBS, the observation of the F S M , the observed I/O sequence. (b) FD, the functional description of all the COMPONENTS the behavior of the COMPONENTS  which describes  under both normal and abnormal  conditions.  Figure 5.3: A 3-state F S M with  COMPONENTS=[tl t2,t3,t4,t5,t6]  Example 4 One of the possible system descriptions is given as follows: C0MP0NENTS=[tl,t2,  t3, U t5,t6] h  l  of the FSM shown in Fig. 5.3  60  • MD: -  edge(A,tl) edge(A,t3)  -  edge(B,t4) edge(B,t5)  -  edge(C,tl) edge(C,t6)  -  The rules described in Chapter 2 regarding the deterministic property.  • OBS:  -  inputs/outputs :r/-. 1/0.1/1.0/0. r/-. 1/0.0/0.0/1  • FD: -  input(T,X,r)  => output(T,A,-)  -  Initial (A)  -  not.ab(tl) A input(tl,C,0) => output(tl,A,0)  -  not.ab(t2) A input(t2,A,0)  -  not-ab(tS) A input(tS,A,l) =• output(t3,B,0)  -  not.ab(t4) A input(t4,B,0) =>• output(t4,A,0)  -  not.ab(t5) A input(t5,B,l)  -  not.ab(t6) A input(t6,C,l) => output(t6,B,0)  output(t2,C,l)  output(t5,C,l)  61  The first FD is for the reset symbol r, X is a variable, i.e. can be any state. The predicate initial(A)  indicates that the FSM is always started at state A.  The predicate not.ab(x) indicates that x is in normal condition. Both the input and output are two value predicates with the first value representing a state and the second value representing a symbol.  5.2.2  Constraint Suspension  The technique used for checking consistency in our method is similar to the Constraint Suspension technique used in Davis' system[Davi84]. The idea behind this technique is very simple. Given a set of components COMP= (compi,...,comp ), n  in a system S.  In order to determine the global consistency of COMP, the following procedures are followed:  1. For all compi, compi € C O M P A ab(comp,), we let the output predicate be output(comp,,X,Y), where X , Y are variables regardless of the FD of compi.  2. All the other rules (i.e. system discription of S) are allowed to run to quiescence to determine whether there is some set of values for the output(comp,-,X,Y)s of compi,...,comp  n  consistent with the inputs and observed outputs.  62  5.2.3  Some Important Definitions  Definition 9 A minimal diagnosis for ( M D , F D , O B S , C O M P O N E N T S ) is a minimal set A C C O M P O N E N T S such that  M D U F D U OBS U {not_ab(c)| c G C O M P O N E N T S - A } U {ab(c)|cG A}  is consistent.  In the context of protocol testing, a minimal diagnosis is a minimal set of transitions which are erroneous.  Definition 10 A conflict set for ( M D , F D , C 0 M P 0 N E N T S , 0 B S )  is a set {c  u  ...,c }  C C O M P O N E N T S such that  M D U F D U OBS U {not_ab(c!),...,not_ab(c^)}  is inconsistent.  Definition 11 Suppose C is a collection of sets. A hitting set for C is a set  HC{JS sec  such that HOS  ^ {} for each S € C.  A hitting set for C is minimal iff no proper subset of it is a hitting set for C .  k  63  T h e o r e m 1:  A C COMPONENTS  is a diagnosis for (MD,FD, COMPONENTS,  minimal hitting set for the collection of conflict sets for  OBS) iff A is a  (MD,FD,COMPONENTS,OBS).  Definition 12 The definition for HS-Tree was originally given by Reiter [Reit87]. Suppose F is a collection of sets. An edge-labeled and node-labeled tree T is an HS-Tree for F iff it is a smallest tree with the following properties:  1. Its root is labeled "yj" ifF is empty. Otherwise, its root is labeled by a set o / F .  2. If n is a node of T , define H(n) to be the set of edge labels on the path in T from the root node to n. If n is labeled by " yj", it has no successor nodes in T . Ifn  is labeled by a set ^2 o / F , then for each a € Yl>  n  a  is a set S GF such that S  joined to n by an edge labeled by a. The label for n  a  s a  successor node n„  n  fl H(n^) = {} if such a set S exists. Otherwise, na is labeled "y/". Figure 5-4 shows an example of an HS-tree.  E x a m p l e 5 In this example, we consider the FSM in the previous example. Let not-ab(x) where  X=t2,t3,t6 and OBS =r/-. 0/1.0/0.0/1.1/0. r/-. 1/0.0/0.0/0. r/-. 1/0.1/0.0/0.0/1.1/0.  [2,4,5]  [1,3,5]  X v / x ^ x  [1,3,5]  V \/x  V  [2,4,6]  x  [1,2,3]  X  X  [2,4]  X  Figure 5.4: A n HS-trte for F={(1,3,5),(2,3),(2,4,6),(2,4),(2,3,6),(1,6)}.  65  We then allow the observed sequence to trace its path in the FSM, using the system description shown in the last example. The following set of FD is consistent with other system description, therefore t2,t3,t6 is not a conflict set.  • ab(tl) A input(tl,C,0) => output(tl,A,0)  • not.ab(tS) A input(t2,A,0)  output(t2,C,l)  • not.ab(tS) A input(t3,A,l)  output(t3,B,0)  • ab(t4) A input(t4,B,0)  output(t4,C,0)  • ab(t5) A input(t5,B,l)  output(t5,C,0)  • noLab(t6) A input(t6,C,l) =>• output(t6,B,0)  5.2.4  Algorithm for Computing Minimal Diagnoses  This approach was first proposed by Reiter[Reit87]. Theorem 1 stated that minimal diagnoses can be computed by computing the minimal hitting sets. This algorithm can be precisely described by a straightforward recursive procedure pruntree(branch(Components,Arcs),Diagnoses) that relies upon some auxiliary predicates.  • branch(Components,Arcs) a two place predicate denoting the current branch of the HS-tree.  66  •  tp (branch (Components,  A res),  ConflictSet)  the procedure that returns a conflict set such that ArcsD conflict  set can be found then branch(Components,Arcs)  is a diagnosis (it uses the constraint  • split(branch(  Components,  suspension  Conflict  Set =[]. If no  will be cut off and Arcs  technique to check consistency).  Arcs),ConflictSet)  the procedure is responsible for growing and branching the HS-Tree. rithm for this procedure is given in Algorithm 6.  •  node  a list of branches that are still alive.  t  diagnoses  a list of minimal diagnoses found.  A l g o r i t h m 6 Procedure  split(branch(Components,Arcs),ConflictSet)  Begin  For every s € ConflictSet  Do  Begin NewArcs=Arcs-hs Node=Node+Branch(Components~s,New  Arcs)  The algo-  67  End End Since pruntree is denned as a recursive procedure, it is necessary to specify how it should be called initially.  It takes two parameters, a structure that contains the  current set of components and the current path, and the diagnoses computed so far. So the initial call to compute the minimal diagnoses from the root of the HS- Tree for a circuit with COMPONENTS=[a ,a ] 1  n  should be  pruntree (branch([a^,a J,[]),[]) n  Initially, diagnoses is empty and node contains only the root(i.e. branch([a\,a ],[]). n  contains only  The followings describe the algorithm in detail.  Algorithm for prunning the HS-Tree A l g o r i t h m 7 pruntree(branch(Components,Arcs),ConflictSet) 1. //node is empty then stop, all the minimal diagnoses are stored in diagnoses  2. Otherwise, select a node=branch(Comp,A) which has the shortest Arcs (path) and use procedure tp(branch(Comp,A),ConflictSet) to generate a conflict set for branch(Comp,A).  3. If the conflict set generated is empty(i.e. there is no conflict set) then add A to diagnoses and go to 1.  68  4- Otherwise, use split(branch(Comp,A),ConflictSet) to update the HS-Tree.  5. Remove all dead branches in node according to the following conditions 1. / / A r c s C D where DeDiagnoses, remove branch(Comp,Arcs) from node. 2. Remove branch(Comp,Arcs) if there exists a branch(C,A) such that A=Arcs  6. Go back to 1.  5.2.5  Example - Test Result Analysis from First Principle  In this section, we will repeat the test result analysis example given in the last section to illustrate the different between the two approaches. The system description of this example has been given in Example 4. We apply the algorithm described above and obtain the HS-Tree shown in Figure 5.5. The numbers in Figure 5.5 indicate the order in which node labels are generated or branches are eliminated. In this example, we first obtain a random conflict set, [tl,t4,t5,t6] (1). In the next level, we generated [t4,t5] (2), and since [t4,t5] is a subset of the original conflict set, we know we could have started with [t4,t5], therefore, we can cut off the edges labeled t l (3) and t6 (4). At the node numbered by (8), there is no conflict set in the remaining components, therefore, the edge labels t4,t5 is a minimal diagnosis. The node numbered by (10) is terminated since its edge labels contain a existing minimal diagnosis. The remainder of the HS-Tree is generated in a similar fashion. After prunning the HS-Tree, there  69  Figure 5.5: A HS-Tree for the system description in Example 4.  only one minimal diagnosis, [t4,t5], for this example.  Chapter  6  Conclusions  6.1  Thesis Summary  In this thesis, we have developed new approaches for both test sequence generation and analysis based on the existing Al techniques. For test sequence generation, we have developed a new constraint satisfaction approach (CSP) based on the constraint satisfaction problem techniques. The new method not only generates test sequence with fault coverage which is at least as good as the one provided by the existing methods, but also allows the implementation under test (IUT) to have a larger number of states than that in the specification. In addition, the new method also lends itself naturally to both test result analysis and fault coverage measurement. Previous approaches such as [Gone70, Chow78, Sabn85, Chan89b], although not stated explicitly, limit the number of states in the IUT to be less than or equal to that in the specification.  The CSP approach is more flexible in that it allows the  limit of the number of states in the IUT to be arbitrarily chosen at the beginning of  71  72  the test sequence generation procedure, thus providing a better fault coverage. This limit, however, should not be substantially larger than the number of states of the given F S M , since the complexity of the corresponding CSP also increases with the extra number of states. The CSP approach can also be viewed as complementing the existing methods such as the UIO method[Sabn85] and the data flow method [Ural87] in term of fault coverage. The (optimized)test sequences produced by these methods can be used as the initial sequence for the CSP method. This way, the uniqueness of the UIO test sequence can be verified and the control flow fault coverage of the data flow test sequence can be improved. If the UIO test sequence is not an unique test sequence  (UTS ), Q  i.e. it does not provide the "full" fault coverage, this can be detected by the number of FSMs solutions computed by the CSP method, and additional subsequences can be generated to ensure its uniqueness. The resulting overall test sequence, in general, is expected to be shorter than the one produced by the UIOv method [Chan89b]. For test result analysis, the CSP method uses the observed sequence as the initial sequence, constructs all fault models which satisfy the initial sequence and introduces additional subsequences to pinpoint the IUT fault model.  In addition, a second  method for test result analysis is proposed, which produces all minimal diagnoses by considering the overall consistency of the system together with the observation. Unlike the first method, the second method does not require the computation of all  73  fault models explicitly, and hence is considered to be more suitable for large systems.  6.2  Future Work  We have developed tools for both test sequence generation and test result analysis in this thesis.  However, these tools are only for the control portion of protocols.  There are a few approaches which can be used to extend our tools to cover the data portion of protocols.  For test sequence generation, we can use an initial sequence  that is generated by the data flow analysis approach proposed in [Ural87], such initial sequences cover all the def-use paths of the data and the CSP method ensures the control portion is also tested thoroughly. Nevertheless, the best approach is to convert all data flow requirements into a set of constraints and the test sequence can be constructed by solving the overall CSP. In this way, we can achieve global optimization on the length of the resulting test sequence. The test result analysis method we have developed is very general, in the sense that we can define the system description regardless of the rest of the procedure. We can extend the system description to covers more aspects of protocol behavior without modifying the general mechanism of the method.  Moreover, we can replace our  diagnostic reasoning model by a more sophisticated one such as the ATMS [dKle87] which can be implemented as a concurrent system.  Bibliography  [Aho88]  Aho, A . V . , Dahbura, A . T . , Lee, D. and Uyar, U . M . , "An Optimization Technique for Protocol Conformance Test Generation Based on UIO Sequences and Rural Chinese Postman Tours," Proceeding Eighth  International Symposium on Protocol Specification, Testing, and Verification, Atlantic City, N.J., 1988. [Chan89a]  Chan, W . Y . L . , Vuong, S. and Ito, M.R., "On Test Generation for Protocols," Proceeding Nineth International Symposium on Protocol  Specification, Testing, and Verification, The Netherlands, June 1989. [Chan89b]  Chan, W . Y . L . , Vuong, S. and Ito, M . R . , "An Improved Protocol Test Generation Procedure Based on UIOs," Proceedings ACM Sig-  comm '89 Symposium, Communications Architectures and Protocols, Austin, Texas, September 1989.  [Chow78]  Chow, T . , "Testing Software Design Modeled by Finite-State Machine," IEEE  Tran. on Software Eng.,vol. SE-4, no.3, 1978, pp.178-  74  75  187.  [Dahb88]  Dahbura, A. and Sabnani, K . , "An Experience in Estimating Fault Coverage of A Protocol Test," IEEE Infocom, 1988, pp71-79.  [Davi84]  R. Davis, "Diagnostic reasoning based on structure and behavior", Artificial  [Fike70]  Intelligence,24,1984,347-410.  Fikes, R . E . , " R E F - A R F : A System for Solving Problems Stated as Procedures" Artificial Intelligence,!,  [Gene84]  1970,pp.27-120.  M . R. Genesereth, "The use of design descriptions in automated diagnosis", Artificial Intelligence,!^, 1984,411-436.  [Gone70]  Gonene, G . , " A Method for the Design of Fault Detection Experiments," IEEE Tran. on Computers,vol C-19, no. 6, June 1970.  [Henn64]  Hennie, F. C , "Fault Detection Experiments for Sequential Circuits," Proc. 5th Ann. Symp. Switch. Theory and Logical Design, 1964, pp. 95-110.  [dKle86]  de Kleer, J., " An Assumption-based TMS," Artificial Intelligence, 28, 1986, pp.127-162.  76  [dKle87]  J . de Kleer, B. C. Williams, "Diagnosing multiple faults", Artificial Intelligence,32,1987,97-130.  [Koha67]  Kohavi, I. and Lavallee P., "Design of Sequential Machines with Faultdetection Capabilities," IEEE Trans. Electron. Computers, vol. E C 16, pp.473-483, August, 1967.  [Koha78j  Kohavi, Z., Switching and Finite Automata Theory, McGraw-Hill Book Company, 2nd Edition, 1978.  [Kuan62]  Kuan, M-K,"Graphic Programming Using Odd or Even Points," Chinese Math, Vol.1, pp.273-277, 1962.  [Mack77]  Mackworth, A . K . , "Consistency in Networks of Relations," Artificial Intelligence, 8(l),1977,pp. 99-118.  [Mont74]  Montanari, U., "Networks of Constraints:Foundamental Properties and Applications to Picture Processing," Information Science, 7(2), 1974,pp.95-132.  [Nait81]  Naito S. and Tsunyama M . , "Fault detection for sequential machines by transition tours," Proc. IEEE Fault Tolerant Comput. Confi, 1981.  [Reit87]  R. Reiter, "A Theory of diagnosis from first principles", Artificial Intelligence,32,1987,57'-95.  77  [Sabn85]  Sabnani, K. K. and Dahbura, A . T . , "A New Technique for Generating Protocol Tests," Proceedings of 9th Data Communications Symposium, I E E E Computer Society Press, Sept. 1985, pp.36-43.  [Sabn88]  Sabnani, K . K. and Dahbura, A . T . , "A Protocol Test Generation Procedure," Computer Networks, vol. 15, no.4, 1988, pp.285-297.  [Sari84]  Sarikaya, B. and Bochmann, G . v. "Synchronization and Specification Issues in Protocol Testing," IEEE  Tran. on Communication , vol.  COM-32, no.4, April 1984, pp.389-395.  [Sari87]  Sarikaya, B., Bochmann, G . v. and Cerny, E . , "A Test Design Methodology for Protocol Testing," IEEE Tran. on Software Eng., vol. SE-13, no.5, May 1987. pp.518-531. J  [Shor76]  E . Shortliffe, Computer-Based Medical Consultations:Mycin, (American Elsevier, New York, 1976).  [Sidh89a]  Sidhu, D. P. and Vallurupalli R., "On Arbitrariness in Protocol Conformance Test Generation," Summitted for publication, 1989.  [Sidh89b]  Sidhu, D. P. and Leung, T . K . "Formal Methods for Protocol Testing: A Detailed Study," IEEE Tran. on Software Eng., vol. SE-15, no. 4, April 1989.  78  [Ural87]  Ural, H . and Yang, B., "Test Sequence Selection Based on Static Data Flow Analysis," Computer Communications,vol.  10, no.5 , Oct. 1987,  pp.234-242.  [Vuon89]  Vuong, S.T. , Chan, W . and Ito, M . , "The UlOv-method for Protocol Test Sequence Generation," Second International  Workshop on  Protocol Test System, IFIP and GMD, Berlin , West Germany, Oct., 1989.  [Wu90]  Wu, J-P. and Chanson, S., "Test Sequence Derivation Based on External Behaviour Expression," Proceedings of the IFIP TC 6 Second International  Workshop on Protocol Test Systems, 1989, pp.177-196.  A p p e n d i x Test  A  Sequence  Generation  Tools  :-dynamic already_done/2.  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx '/. The predicate tseq(Method,File) reads the FSM specification from File */, '/, and generates a test sequence for the FSM using the method specified X X by Method. X  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx tseq(X.Y):-reset.start(Y),uio,ess,sequence(X,L).writeseq(L). writeseq(L):-write_aux(10,L). write_aux(_, [] ) : - n l . write_aux(0,L):-nl,write_aux(lO,L). write_aux(N,[LllL]):-Nl is N-l,write(Ll),write(' '),write_aux(Nl,L). sequence(uio.Seq):-file(File), see(File), form_sub_seq(Seq), seen. sequence(t,Seq):-branch(_,_,_),find_tour(Seq). sequence(css,Seq):-find_tour(T),trace_tour(l,T,Seq). trace_tour(_, [] , []) . trace_tour(X,[Ll|Ls],Seq):-get_seq(X,E,L1,S1), trace_tour(E,Ls,Seqs),  79  append(Sl,Seqs,Seq) . get_seq(A,B,Ll,[LI]):-branch(A,B,[LI]),already_done(A,B) . get_seq(A,B,L1,[Ll]):-uio(A,[Ll]),branch(A,B,[Ll] ). get_seq(A,B,Ll,S):-branch(A,B,[Ll]),shortest_css(A,L2), append(L2,[Ll],S), assert (already_done(A,B)). shortest_css(A,L):-setof(css(A,L2),css(A,L2),LL), find_min_css(LL,L). find_min_css([css(_,L)],L). find_min_css([css(_,Ll),css(_,L2)],L1):-length(Ll,N1), length(L2.N2), NKN2. find_min_css([css(_,_),css(_,L2)] ,L2). find_min_css([css(_,Ll),css(_ L2)|Css],L):length(Ll,Nl),length(L2,N2), NKN2, ! , find_min_css([css(_,Ll)ICss],L). find_min_css([css(_,Ll),css(_,L2)ICss],L):length(Ll,N1),length(L2,N2), \+ (NKN2),! , find_min_css([css(_,L2)ICss],L). form_sub_seq(Seq):-form_beta_seq, get_test_seq(Seq). <  form_beta_seq:-read(X), insert_trans(X). insert.trans(end_of_file):-optimize. insert.trans((A,B,C)):-shortest_path(l,A,SP), find_chosen_uio(B,X), append(SP,[C],Sl), append(Sl,X,S2), find_end(B,X,E), assert(beta(A,E,S2)), form_beta_seq.  81  get_test_seq(S):-setof(beta(A,E,S).beta(A.E.S),L) , get_test_seq_aux(L,S). get_test_seq_aux( [ ] , [ ] ) . get_test_seq_aux([beta(_,E,Sl)IBs],S):-shortest_path(E,1,SP1) , append(Sl,SPl,SSl), get_test_seq_aux(Bs,S3), append(SSI,S3,S). find_chosen_uio(A,B):-chosen_uio(A,B). find_chosen_uio(A,B):-uio(A,B). -dynamic uio/2. -dynamic not_unique/l. -dynamic path/4. -dynamic state/1. -dynamic maxlen/1. -dynamic more/0. -dynamic continue/0.  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx X The p r e d i c a t e uio f i n d s a l l the shortest uios f o r a FSM. X In order t o use t h i s predicate, the database must be properly set up X by using the predicate start(FileName), where FileName i s the F i l e X the FSM d e s c r i p t i o n . The predicate uio (Filename) can be used t o write X a l l the uios to a f i l e Filename or to d i s p l a y them on screen i f uio (user) '/, i s used.  v •/ •/ v v v •/ v •/ v •/ v •/ v v v v •/ •/ v v v«/ v •/ •/ •/ •/ •/ •/ v •/ v •/ •/ v •/ •/ •/ v •/ •/ v •/ •/ v •/ •/ •/ •/ •/ v •/ •/ •/ v •/ •/ •/ •/ v •/ •/ v v •/ •/ v v v •/ •/ •/ •/ v •/ •/  uio:-get.state(State), find.length(State), find.uios(State,State,yes) . find.length(S):-length(S,N),N1  i s (2*N*N).assert(maxlen(Nl)) .  get_state(States):-state(States). get.state(States):-setof(X/Y,tree(X,Y).Trees), extract_state(Trees.States), asserta(state(States)).  extract_state( [ ] , [ ] ) . extract_state( [X/_|Ts], [X|Y]):-extract_state(Ts,Y). find_uios([],_,_). find_uios([Sl|SR] .S.Flagl):-set.path(SI), find_sio(Sl,S,Flagl,Flag2), find_uio(l,Sl,S,[],Flagl,Flag2), find_uios(SR,S.Flagl). find_sio(Sl,S,F,done):-setof(path(Sl,1,C,_),path(Sl,1,C,_),L), check_uniqueness(S,Sl,L,F) . find_sio(_,_,_,not_done). check_uniqueness(S,Sl, [path(_,_,C,_)|Y],yes):-unique(S,SI,C,yes) set_flag, check_uniqueness(S,Sl,Y,yes). check_uniqueness(S,Sl, [path(_,_,C,_)|_] ,no):-unique(S,Sl,C,no) . check_uniqueness(S,Sl, [_|Y].Flag):-check.uniqueness(S.Sl.Y,Flag) check.uniqueness(_,_, [],_):-more,retractall(more). f ind_uio(_,_,_,_,_,done). find.uio(_,_,_, [],_,not_done):- more,retractall(more). find_uio(N,Sl,S,[].Flagl,not_done):setof(path(Sl,N,LBs,End), path(Sl.N.LBs,End),L), Nl is N+l, find.uio(Nl,SI ,S.L.Flagl,not_done). find_uio(N,_,S,[Ll|_],no.not.done):-maxlen(Nl), N<N1, expand(Ll,S,no). find_uio(N,Sl,S, [Ll|L2],yes,not_done):-maxlen(Nl), N<N1, expand(Ll.S.yes).set.flag, f ind.uio(N,S1,S,L2,yes,not_done). find_uio(N,Sl,S, [JL],Flagl.not.done):-maxlen(Nl), N<N1. ! , find.uio(N,SI,S,L.Flagl,not.done). find.uio(_,SI,S,_,_,not.done):find_state_sig(Sl,S,no).  find_state_sig(S,Ss,F):-find_sig(S,Ss,Sig,F),assert(uio(S.Sig)) . find_sig(S,[SllSs],[SigllSigs],F):-find_single_sig(S,S1,Sigl,F), find_sig(S,Ss,Sigs). find_single_sig(S,Sl,Sigl,F):-find_uios([S],[SI],F), retract(partial_uio(X,Y)), find_end(X,Y,End), shortest_path(End,X,Path), append(Y,Path,Sigl). find_end(X,[Y],End):-tree(X,Branches), match_label([Y].Branches,End). find_end(X,[YllYs].End):-tree(X,Branches) , match.label([YI],Branches,E), find_end(E,Ys,End). set_flag:-more. set_flag:-assert(more). match_label(L,[branch(L.E)l_],E). match_label(L, LIB] ,E) :-match_label(L,B,E) . expand(path(S1,N,Label,End),S,FG):tree(End,Branches), new_path(SI,N,Label.Branches,S,FG). new.path(_,_,_,[],_,_):-continue,retractall(continue). new_path(_,_,_,[],_,_):- \+ continue,!.fail. new_path(Sl,Nl,Label,[branch(C.E)|B],S,F):append(Label,C,Newlabel), assert(path(Sl,N1.Newlabel.E)), unique(S,S1,Newlabel,F), set_flag, new_path(Sl,Nl,Label,B.S.F). new_path(Sl,N,L,[_|Bs],S,F):-new_path(Sl,N,L,Bs,S,F). set_path(Sl):-tree(Sl,Branches),  84  add.path(SI.Branches). add_path(_, []) . add.path(SI,[branch(C,End)IBs]):assert (path(Sl,1.C.End)), add_path(Sl,Bs). unique(States,S,L,F):- \+ not.unique(L), trace_path(States,S,L), add_uio(S,L,F). unique(_,_,L,_):- \+ not.unique(L), assert(not_unique(L)),!,fail. add_uio(S,L,yes):-assert(uio(S,L)). add_uio(S,L,no):-assert(partial_uio(S,L)) . trace_path([],_,_). trace_path([SIISs],S1,L):-!,trace_path(Ss,S1 trace_path([Sl|Ss],S,L):-!,trace(Sl,L),!, trace_path(Ss,S,L).  ,L) .  trace(_,[]):-!.fail. trace(Sl,[L1|L2]):-tree(Sl,Bs), in_tree([Ll],Bs,New_node),!, trace(New_node,L2). trace(_,_). in_tree(_,[],_):-!.fail. in_tree(Ll,[branch(Ll,N)|_],N). in_tree(Ll,[_|B],N):-in_tree(Ll,B,N).  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx X The predicate find.tour(Tour) finds a transition tour a graph. X tour traverses every transition at least once.  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx :-dynamic not_done/3. find.tour(Tour):-set,tt(1,Tour). set:-setof(branch(A,B.C).branch(A,B,C),L),setl(L) .  The X X  85  setl([]) . set 1([branch(A,B,C)|L]):-assert(not_done(A,B,C)), setl(L). tt(State,TOUR):-not.done(State,Next,C), branch(State,Next,C), update(State,Next,C), tt(Next.Ls), append(C,Ls,TOUR). tt(State,TOUR):-not_done(X,Y C), goto(State,X,Ll), branch(X,Y,C), update(X,Y,C), append(Ll,C,L2), tt(Y.Ls), append(L2,Ls,T0UR). )  tt(S,SP):-shortest_path(S,l,SP). goto(X.Y.Ll):-shortest_path(X,Y,Ll), check_path(X,Ll). check_path(_, • ). check_path(X,[LlLs]):-branch(X,Y,[L]), updatel(X,Y,[L]), check_path(Y,Ls). updatel(X,Y,Z):-not_done(X,Y,Z),retract(not_done(X,Y,Z)). updatel(_,_,_). update(X.Y.Z):-retract(not.done(X.Y.Z)).  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx X The predicate shortest_path(FROM,TO,LABELS) finds the shortest path from X X start FROM to state TO and return the labels of the arcs used in LABELS. X X Dijka algorithm is used for finding the shortest path. X  shortest_path(FR0M,TO,LABELS):dijka([[FROM, []]] ,A, [] , • ,T0), find_labels(A,LABELS). find_labels([[_,Labels]|_].Labels). dijka(_,PAcc,PAcc,_,END):-member([END,_],PAcc). dij ka(01dtemps.Answer,PAcc,TAcc,END):generate(Qldtemps,Newtemps,Perm,PAcc,TAcc), dijka(Newtemps,Answer,[PermlPAcc],TAcc,END). generate(Oldtemps,Newtemps,Perm,PAcc,TAcc):extract(Oldtemps,Perm,Nexttemps), revi se(Nexttemps,Perm,Newtemps,PAcc,TAcc). extract(Temps,Perm,Nexttemps):mind(Temps,Perm), jtlist(Before,[Perm I After].Temps), jtlist(Before,After.Nexttemps). revise(01d,[P.Dp],New,PAcc,TAcc):branch(P,Next,D), \+ member([Next,_],PAcc), \+ member([Next,_],TAcc), append(Dp,D,D2), modify(01d,Next,D2,D3), revise(01d,[P,Dp],New,PAcc,[[Next,D3]iTAcc]).  revise(Old,_,Result,_,TAcc):-combine(Old,TAcc,Result). combine([],Sec,Sec). combine([[A,_]|T],Sec,Answer):-member([A,_],Sec), combine(T,Sec,Answer). combine([HIT],Sec,[HlTail]):-combine(T,Sec,Tail). modify(Old,Next,D2,D3):-member([Next,Dn],01d), smaller(Dn,D2,D3).  87  modify(_,_,D2,D2). smaller (A,B, A) :-length (A,NI) , length (B,N2) ,NKN2. smaller(_,B,B). mind([[N,D]],[N,D]). mind([[Nl,Dl],[_,D2]iTail].Result):-length(Dl,LI),length(D2,L2), LKL2, mind([[Nl,Dl]ITail].Result) . mind([_|Tail].Result):-mind(Tail,Result). member (H, [ H | J ) . member(H,[_|T]):-member(H,T). j t l i s t ( [ ] ,A,A) . jtlist([H|T],Sec,[H|R] ) : - j t l i s t ( T , S e c , R ) . append([],A,A). append([H|T],L, [H|L1]):-append(T,L,Ll). :-dynamic chosen_uio/2.  7x///x/x/////x/xm  7, The predicates uio (File) and ess (File) are for writing the UIOs and CSSs 7, 'It found to a f i l e F i l e . If File=user then they w i l l be shown on screen. '/,  mmmmmmmmmmmmmmmmmmmmmmimmxm uio(user):-show_uio('UIOs') . uio(X):-telling(X), told, tell(X), show_uio('UIOs') , told, tell(X). show_uio(S):-setof(uio(X.Y),uio(X,Y) , L ) , write('STATE '),write(S),nl, showl(L). showl([]) : - n l .  88  showl([uio(X,Y)lUios]):-write(' write(Y),nl, showl(Uios).  ') ,write(X),write(  1  '),  css(user):-show_seq('CSSs'). css(X):-telling(X), told, tell(X), show_seq('CSSs') , told, tell(X). show_seq(S):-setof(css(X.Y),css(X,Y),L), write('STATE '),write(S),nl, show2(L). show2([]) :~nl. show2([css(X,Y)iCSSs]):-write(' write(Y),nl, show2(CSSs).  '),write(X),write('  choose(X,Y):-assert(chosen_uio(X,Y)). reset:-retractall(uio(_,_)),retractall(not.unique(_)), retractall(path(_,_,_,_)).retractall(state(_)), retractall(maxlen(_)).retractall(more) , retractall(continue),retractall(transition(_,_,_)), retractall(beta(_,_,_)).retractall(branch(_,_,_)), retractall(already_done(_,_)).retractall(ess(_,_)), retractall(file(_)), retractall(tree(_,_)),retractall(chosen_uio(_,_)). :-dynamic branch/3. :-dynamic tree/2. :-dynamic f i l e / 1 .  '),  89  % The predicate start (File) is used to set up the database for the predicate '/• uio. F i l e contains the description of a FSM.  '/, X  mmmmammmmmmmrammmmmmmmmmmiimm start(File):-see(File), assert(file(File)), preprocess, seen. preprocess:-read(X), process(X). process(end.of_file). process((A,B,C)):-retract(tree(A,Branches)),! , assert(branch(A,B,[C])), assert(tree(A,[branch([C],B)iBranches])), preprocess. process((A,B,C)):-assert(tree(A,[branch([C],B)])) , assert(branch(A,B,[C])), preprocess. :-dynamic beta/3.  y////x///x///.xxxyxm X '/,  The predicate optimize optimizes a test sequence by eliminating a l l the beta sequences that are contained in other beta sequence.  opt imize:-retract(beta(X,Y,S1)), contain(beta(X,Y,Sl)). optimize.  contain(beta(_,_,Sl)):-beta(_,_,S2), subset(SI,S2),!, optimize. contain(beta(A,B,Sl)):-beta(X,Y,S2), subset(S2,SI),!, retract(beta(X,Y,S2)), assertz(beta(A,B,Sl)),  '/, X  90  optimize. contain(beta(A,B,C)):-assertz(beta(A,B,C)),!.fail, subset(SI,S2):-get_input(Sl,Il), get_input(S2,I2), append(Il,_,I2). get_input([] , []) . get_input([I/_|T],[I|T1]):-get.input(T,T1). :-dynamic transition/3.  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx X '/, '/, */, y. '/. y. y.  The predicate complete_spec(File!n,FileOut) accepts a incompletely specified FSM in F i l e l n and completes the FSM by adding an arc with label x/null to i t s e l f for any unused input symbol x. The format of F i l e l n is as follows: i,2,a/ . 2,3,b/y. . . x  X */, X '/. y. y. y. y.  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx complete_spec(FileIn,FileOut):see(Fileln), do, seen, complete(FileOut). do:-read(X), process_trans(X). process_trans(end_of_file). process_trans((X,Y,Z)):-assert(transition(X,Y,Z)), do. complete(F):-setof(X/Y/Z,transition(X,Y,Z),L), collect_state(L,Ll).collect.label(L,L2), remove.dup(Ll.Lll),remove_dup(L2,L22), complete.fsm(Lll,L22), writeOutput(F).  91  collect_state( [ ] , [ ] ) . collect_state([X/_/_|T],[XITX]):-collect.state(T,TX). collect . l a b e l ([] , []) . collect.label([_/./(I/_)IT],[I|TX]):-collect_label(T,TX). remove_dup( [ ] , [ ] ) . remove_dup([XIY],[X|Z]):- \+ member(X,Y), remove_dup(Y,Z). remove_dup([_IY],Z):-remove_dup(Y,Z). complete_fsm([], _). complete.fsm([Ll|L2],L):-check_completeness(Ll,L), complete.!sm(L2,L). check_completeness(_,[]). check_completeness(Ll,[X|Y]):-transition(Ll,_,X/_), check_completeness(Ll,Y). check_completeness(Ll, [X| Y] ) : -assert (transition(Ll ,L1,X/null)) , clieck_completeness(Ll ,Y) . writeOutput(F):-telling(X), told, tell(F), write_trans, told.tell(X). write_trans:-transition(A,B,C), write(A),write(','),write(B) , write(','),write(C),write('.'),nl, retract(transition(A,B,C)) , write.trans. write_trans. :-dynamic css/2.  mmmmmmmmmmmmmmmmmmmmmmiimiim '/, The predicate ess is used for finding the State Signature of the states in '/, 7, a FSM. This predicate can only be used after the predicate uio has 7,  X succeeded.  css:-uio(X,Y), form_css(X,Y). ess. form_css(X,Y):-find_end(X,Y,E), shortest_path(E,X,SP), append(Y,SP,Css), assert(ess(X.Css)),!, fail.  '/.  A p p e n d i x C S P  B  P r o b l e m  Solver  *********** ***************************************** ********************* •The following program accepts a test sequence and computes a l l n-FSMs * •for a given n which satisfy this test sequence. * ************************************************************************* :-dynamic :-dynamic :-dynamic :-dynamic •.-dynamic :-dynamic  inconsistent/0. equal/2. not_equal/2. c/3. solution/1. counter/2.  csp_solver(Seq,Num_of_States .Solutions,Num_of.Solutions):cleanup, convert(Seq.Cs), get_state_values(Num_of_States.Values), solve(Cs.Values), collect_solution(Solutions), length(Solutions,Num_of.Solutions). cleanup:-retractall(solution(_)). convert(Seq.Cs):convert(0,Seq,Cs,x(0)). convert(_, [] ,[],_).  93  94  convert(N,[r/nullHQs],Cs,_):NI is N+l, convert(Nl,I0s,Cs,s(0)). convert(N,[I0|I0s],Cc(s(0),x(N),10)|Cs],s(0)):convert(N,IOs,Cs,x(N)). convert(N,[IOlIOs],[c(x(N),x(Nl),10)|Cs],_) : NI is N+l, convert(NI,IDs,Cs,x(Nl)). get_state_values(N,S):get_state_valuesl(N,0,Sl), split(Sl.S). get_state_valuesl(N,N,[]). get_state_valuesl(N,Nl,[s(Nl)|S]):N2 is Nl+1, get_state_valuesl(N,N2,S). split([Sl|Ss],([S1],Ss)). add_one((X,[]),(X,[])). add_one(([X|Xl],[Y|Yl]),([Y,X|Xl] ,Y1)). collect_solution(L):-setof(solution(S),solution(S),L). collect_solution([]). solve(Cs,Vs):add_one(Vs,Vsl), solve(Cs,Vsl,[]). solve(Cs,Vs,NEs):setupworkdb(NEs), reduce(Cs,Csl), set_flag(Flag), cleanupworkdb(not.equal,2), solve_aux(Flag,Csl,Vs). solve_aux(inconsistent,_,_). solve_aux(consistent,Cs,Vs):-  95 find_inequalities(Cs,NEs), cleanupworkdb(not_equal,2), collect_varsl(Cs,Vars), set.flag(Flag), assign_values(Flag,Cs,NEs,Vars,Vs). collect_varsl(A,B):-collect_vars(A,B). assign.valuesCinconsistent,_,_,_,_) . assign_valu.es(consistent,Cs,_, [] ,_) :-assert(solution(Cs)). assign.values(consistent,Cs,NEs,[H|_],(Vsl,Vs2)):eliminate_values(Vsl,Vs,NEs,x(H)), unify(Vs,x(H),NEs,Cs,(Vsl,Vs2)) . unify([], _ , . , . , _ ) . unify([VIIVs],Var,NEs,Cs,Vals):update([equal(VI,Var)],Cs,NCs), solve(NCs.Vals), unify(Vs,Var,NEs,Cs,Vals). eliminate_values(Vsl,Vs,NEs,Var):setupworkdb(NEs), eliminate(Vsl,Vs,Var), cleanupworkdb(not_equal,2). eliminate([] , [ ] , _ ) . eliminate([Sl|Ss],S,Var):not.equal(SI,Var), eliminate(Ss,S,Var). eliminate([Sl|Ss] , [S1|S],Var):eliminate(Ss,S,Var). collect_vars([],Vars):-order_vars(l,Vars), cleanupworkdb(counter,2). collect_vars([c(Xl,X2,_)|Cs],Vars):count_vars(XI), count_vars(X2), collect_vars(Cs,Vars).  count_vars(x(N)):-increment.counter(N). count_vars(_). increment .counter (N) :-retract (counter (N, Count)) , Countl is Counz+l, assert(counter(N,Countl)). increment.counter(N):-assert(counter(N,1)). order.vars(N,Vars):-counter(_,_), collect_counters(N,L), NI is N+l, order_vars(Nl,Varsl), append(Vars1,L,Vars). order_vars(_,[]). collect_counters(N,L):setof(X,counter(X,N),L), retractall(counter(_,N)). collect_counters(_,[]). find_inequalities(Cs,NEs):separate(Cs,CH,CT), find_inequalities(CH,CT,NEs). separate([CHICT],CH,CT). f ind_inequalities(_, [],[]). f ind_ inequalit i e s(CH, CT,NEs):check_rule2(CH,CT,NEl), check_rule3(CH,CT,NE2), separate(CT,Ch,Ct), retractall(Ch), find_inequalities(Ch,Ct,NE3), append(NE1,NE2,NE4), append(NE4.NE3,NEs). check_rule2(_, [ ] , • ) . check_rule2(C,[Cl|Cs],NEs):check2(C,Cl,NEl),  check_rule2(C,Cs,NE2), append(NE1.NE2,NEs). check_rule3(_, [ ] , [ ] ) . check_rule3(C,[CI|Cs],NEs):check3(C,Cl,NEl), check_rule3(C,Cs,NE2), append(NE1.NE2,NEs). check2(c(s(Nl),.,11/01),c(s(N2),_,11/01),[]) \+ N1=N2. check2(c(Xl,X2,11/01),c(X3,X4,11/01),P):not_the_same(X2,X4), check.add(not.equal,XI,X3,P) . check2(.,.,[]). check3(c(s(Nl),_,Il/_),c(s(N2),_,Il/_), • ) : \+ N1=N2. check3(c(Xl,_,11/01),c(X2,_,11/02),P):\+ 01=02, check.add(not_equal,X1,X2,P) . check3(_,_, []) . check_add(_,X,X,[]):-assert(inconsistent) . check.add(NE,X,Y,[P]):add(NE,X,Y,P), insert(P) . insert(X):- \+ X, assert(X). insert(_). append([],X,X). append([X|Y],Z,[X|Z1]):-append(Y,Z,Zl) . not_the_same(X,Y):-not_equal(X,Y). not_the_same(X,Y):-not.equal(Y,X). not_the_same(s(Nl),s(N2)):- \+ N1=N2.  reduce(Cs.NCs):find_equality(Cs,E), replace_var([E],Cs,NCs). replace.var ( [ [] ] , C, C) . replace.var([equal(XI,X2)],Cs,NCs):consistent(XI,X2), i  •  >  update([equal(XI,X2)],Cs,Csl), reduce(Csl.NCs). replace.var(_,_,_):-assert(inconsistent). set_flag(inconsistent):-inconsistent, i  • >  retractall(inconsistent). set_flag(consistent). inconsistent(s(N),s(Nl)):- \ + N - N l . inconsistent(XI,X2):-not_equal(Xl,X2). inconsistent(XI,X2):-not_equal(X2,X1). consistent(Xl,X2):-  \+  inconsistent(XI,X2).  find_equality([CIICs],E):setupworkdb(Cs), check.rulel(CI,Cs,E). check_rulel(c(XO,X,A/_),_,E):c(X0,Y,A/_), \+ X=Y, add(equal,X,Y,E), cleanupworkdb(c,3).  check.rulel(_,[CI ICs],E):retractall(CI), check.rulel(CI,Cs,E). check.rulel (_, [ ] , [ ] ) . add(equal,X,X,[]). add(PName,x(Nl) ,x(N2) ,P) : - NKN2,! ,  P=..[PName,x(Nl),x(N2)] add(PName,x(Nl),x(N2),P):- N1>=N2, * >  P=..[PName,x(N2),x(Nl)] add(PName,s(Nl),s(N2) P):- NKN2,! , P=..[PName,s(Nl),s(N2)] add(PName,s(Nl),s(N2),P):- N1>=N2, J  i  • >  P=..[PName,s(N2),s(Nl)] add(PName,X,Y,P):-variable(X), value(Y), • >  P-..[PName.Y.X]. add(PName,X,Y,P):-variable(Y), value(X), i •  »  P=..[PName.X.Y]. variable(x(_)) . value(s(_)).  update(E,Cs,NCs):rename_vars(Cs,E,Cs1), remove_dup_clauses(Csl,NCs). setupworkdb( [] ) . setupworkdb([XlY]):-assert(X), setupworkdb(Y). rename.vars(Cs,E,NCs):setupworkdb(E), renaming(Cs,NCs), retractall(equal(_,_)). renaming(Cs,NCs):-retract(equal(X,Y)),!, renaming(Cs,Csl,Y,X), renaming(Cs1,NCs).  100  renaming(Cs,Cs). renaming([] ,[],_,_). renamingCCCl ICs] , [NCllNCs] ,01dName,NewName) : functor(Cl,Fun,_), Cl=..[Fun IVars], ren(Vars,NewVars,OldName,NewName), NC1=..[Fun INewVars], renaming(Cs.NCs,OldName,NewName). ren([], [ ] , . , . ) . ren([OV|Vs],[NVlNVs],OV,NV):ren(Vs,NVs,OV,NV). ren([V|Vs],[V|NVs],0V,NV):ren(Vs,NVs,OV,NV). remove_dup_clauses(Csi,NCsl):setupworkdb(Csl), rm_dup(NCsl). rm_dup([c(A,B,C)|Cs]):c(A,B,C), retractall(c(A,B,C)), rm_dup(Cs). rm_dup([]) . cleanupworkdb(C,2):-Cl=..[C,_,_] , retractall(Cl). cleanupworkdb(C,3):-Cl=..[C,_,.,_] , retractall(CI) .  ********************************************** *This program interprets the solutions computed by the CSP solver into * *a more readable format. * ************************************************************************* :-dynamic fsm/1. interpret(user,Ss):-  101  organize(Ss). interpret(Filename,Ss):tell(Filename), organize(Ss), told. organize ( [] ) . organize([solution(Sl)|Ss]):-organize_solution(Sl), organize(Ss). organize_solution(Cs):write('FROM al, setupworkdb(Cs), » collect_edges(0), cleanupworkdb(c,3).  TO  collect.edges(N):-setof((X,Y),c(s(N),X,Y),L), sort_states(L,Ll), write.fsm(s(N),L1), NI is N+l, collect_edges(Nl). collect_edges(_):-nl,nl. sort_states( [ ] , [ ] ) . sort_states([X|Y],Y1):sort_states(Y,Y2), insert(X,Y2,YI). insert (X, [] , [X]) . insert(X,[XIIY],[X,X11Y]):gt(Xl,X). insert(X, [XIIY] , [XII YI] ) : insert(X.Y.Yl). gt((s(N),_),(s(Nl),_)):-N>Nl. write_f sm(_, [] ) . write_fsm(From,[(To,10)IPs]):-  I/O'),  write(From), write(' write(To), write(' write(IO), nl, write.fsm(From,  


Citation Scheme:


Citations by CSL (citeproc-js)

Usage Statistics



Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            async >
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:


Related Items