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 K O B.A.Sc , University of British Columbia, Vancouver, Canada, 1987 B.Sc, University of British Columbia, Vancouver, Canada, 1988 A THESIS SUBMITTED IN PARTIAL F U L F I L L M E N T OF 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 OF G R A D U A T E STUDIES ( D E P A R T M E N T 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 COLUMBIA July 1990 © Kai-Chung Ko, 1990 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. . , COMPUTER S C I E N C E Department of ^ The University of British Columbia Vancouver, Canada Date 1st A u g u s t . 1990 -6 (2/88) A b s t r a c t 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 FSM. 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 C o n t e n t s Abstract ii List of Figures v List of Tables vi Acknowledgement vii 1 Introduction 1 1.1 Background and Motivations 1 1.2 Contributions 4 1.3 Thesis Outline 5 2 Test Sequence Generation Methods 6 2.1 The Finite state Machine Model 6 2.2 Checking Experiment 10 2.3 Checking Experiment Based Methods 12 2.3.1 T-Method 12 2.3.2 DS-Method 14 2.3.3 W-Method 18 2.3.4 UIO-Method 20 2.3.5 UIOv-Method 24 2.3.6 Preformance Analysis 25 3 Fault Coverage measurement 28 3.1 The Uniqueness Criterion 28 3.2 Arbitrariness in Test Sequence Generation and Fault Coverage Metric 30 4 The Constraints Satisfaction Problem(CSP) Approach 33 4.1 Definition of CSP 33 iii 4.2 Test Sequence Generation Procedure 34 4.2.1 Initial Sequence Selection 36 4.2.2 Algorithm for Solving the CSP 37 4.2.3 Generation of Additional Subsequences 39 4.3 The CSP Technique - Examples 41 4.3.1 Example A - FSM with all UIOSs 41 4.3.2 Example B - F S M with a state that has no UIOS 46 4.3.3 Example C - Higher Order UTSi 48 5 Test Result Analysis - Two approaches 52 5.1 The CSP Approach for Test Result Analysis 52 5.1.1 Example - Test Result Analysis Via CSP Method 54 5.2 Test Result Analysis - from First Principle ; 57 5.2.1 System Description 58 5.2.2 Constraint Suspension 61 5.2.3 Some Important Definitions 62 5.2.4 Algorithm for Computing Minimal Diagnoses 65 5.2.5 Example - Test Result Analysis from First Principle 68 6 Conclusions 71 6.1 Thesis Summary 71 6.2 Future Work 73 Bibliography 74 A Test Sequence Generation Tools 79 B CSP Problem Solver 93 iv L i s t o f F i g u r e s 2.1 A3-stateFSM 16 2.2 A Distinguishing-Tree for the FSM in Fig. 2.1 17 2.3 A 5-state FSM 21 2.4 A tree for constructing the W set 22 2.5 A UIOS-Tree for the F S M in Fig. 2.1 24 4.1 A search tree for the CSP 44 4.2 Two solutions to the CSP 45 4.3 An F S M whose state C has no UIOSs 46 4.4 A faulty IUT 47 4.5 Three solutions to the CSP in Example B 49 4.6 The F S M solutions for Example C 51 5.1 A fault model for the observed output sequence 55 5.2 All possible fault models for the observed output sequence 56 5.3 A 3-state FSM with COMPONENTS=[tl,t2,t3M,t5,t6] 59 5.4 An HS-treeior F={(1,3,5),(2,3),(2,4,6),(2,4),(2,3,6),(1,6)} 64 5.5 A HS-Tree for the system description in Example 4 69 v L i s t o f T a b l e s 2.1 Upper bound for The Five Test Sequence Generation Methods vi A c k n o w l e d g e m e n t 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 C h a p t e r 1 I n t r o d u c t i o n 1.1 Background and Motivations Communication protocols are sets of rules and procedures that govern the interac-tions 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 the-sis, 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 proto-cols 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 with-out 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 FSM examples. 2. We have introduced two novel procedures for locating errors in test result anal-ysis. 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 FSM. 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 FSM 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. C h a p t e r 2 T e s t S e q u e n c e G e n e r a t i o n 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 mod-eled by a finite state machine (FSM). A FSM can be represented as a quintuples: M=(Q, / ,O , / ,<7 , S 0 ) where Q = the set of states in the FSM 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 genera-tion 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)= Sj and f(si,i)= sk iff Sj - sk. 2. Let Si,Sj,Sk and si G Q,i G f(si}i)= sk) f(sj,i)= st. Then, a,- ^  Sj if sk ^ sh 3. Let Si,Sj,Sk and si G Q, i G / 01,02 G O, f(si,i)= sk> g(si,i)= oi , f(sj,i)= sl,g(sj,i)= o2. Then, 5,- ^  Sj if ox ^ o2. Rule 1 simply states that accepting an input symbol at a state, a FSM can only go to one and only one state. Rule 2 is merely the negation of Rule 1: the two states from which a FSM 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 tran-sition path for each i € I. In practice, a given FSM is often incompletely specified and inputs received at a given state of the FSM 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 FSM 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 FSM model of the control structure of the protocol can be rep-resented as a labeled digraph, G=(V,E), where V is a set of vertices corresponds to the state set of the FSM and E is a set of edges corresponds to the possible transi-tions 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 FSM specification together represent the core behavior of a protocol. The corresponding edges and I/Os in the FSM 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 assump-tion 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 FSM through all its transi-tions, 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,DS, W, UIO and UIOv. In a checking experiment, the FSM 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 FSM passes the state identifying sequences based check-ing 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 corre-sponding 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 FSM 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 FSM 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, 8itj=ri@SP{si)@I@SI(sj) 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 FSM 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 FSM 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 fol-lowings 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 tran-sition to its closest untraversed transition. Algorithm 1 Let E=[e\, e 2 , e n ] , where e,-, i = l , . . . ,n are the edges of the FSM. 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 ek from E whose start state is at Si. Let ST=ek and CS=Sj, the end state of ek. 2. If there exists an em £ E whose start state is CS then Remove em from E. Let ST=ST@em, let CS=Si, the end state of em Else Remove an edge ex from E, let ST=ST@SP(CS,Ss)@ex, where Sa is the start state of ex, let CS=St, the end state of ex. 3. IfE=® return ST@SP(CS,Sij as the transition tour 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. An input sequence is said to be a distinguishing sequence for a FSM if the output sequence produces by the FSM 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 DSs A l g o r i t h m 2 Let S0,Si,...,Sn-i 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\,Sn-iJ. The Distinguishing- Tree is constructed as follows: 1. Initially, the current node of the tree is Node=Root, i.e. Node=[[Sr,,Sn-\]]. 2. If all elements in Node are singleton sets then Stop. The input path from Root to Node is a DS 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 ik-ii. 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. Example 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]] [[3,3,1]] [[1],[2],[1]] [[3],[2,3]] a.a is the shortest distinguishing sequence. Figure 2.2: A Distinguishing-Tree for the FSM in Fig. 2.1 18 2.3.3 W-Method A characterization set W of a FSM 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 FSM. 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: Algor i thm for computing the W set Before we describe the algorithm, we need to introduce some new notations. Definition 5 Let two sets R=[rx,rnJ and S—[si,..,sm] whose elements rt- 's and Sj's are also sets. We define the set operation R n S as: R n S = [rx C\si,...,ri D s m , r n D su rn fl sm] Definition 6 Consider the set S=[Si, ...,SmJ where Si — [s(xi,yi),...,s(xni,yni)J, we define the set F(S)=[first(Si),...,first(Sm)] where first(Si)—[xi, ...,xnJ). 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],...,[Sn-iJJ-Let the root of the tree. Root, be a singleton set with the single element States=[s(S0, So), s(Si, Si),s(5n_i, S„_i)7 where for every s(Si,Sj), Si denotes the original state of the path and Sj represents the current state, we also let Wset=§ and CW=Root. The tree is constructed as follows: 1. Initially, the current node of the tree is Node=Root. 2. If SingletonS 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. 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. Example 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. An UIOS for a state is an I/O behavior not exhibited by any other state in the FSM. 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 FSM. 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 FSM 22 Wset=[A] CW=[0,2,3],[1,4]] [[s(0,0),s(l,l),s(2,2),s(3,3),s(4,4)]] ^ / X. Wset=[A,B] X X\CW=[[2],[3],[1,4],[0]] [[s(0,3),s(3,4),s(2,l)],[s(l,4),s(4,2)]] [[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)]] UIOSs can be computed in a similar fashion as the DSs, i.e. constructing an UIOS-Tree. 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 S0,Si, . . . , S n _ i be the states of a given n-FSM. Let the root of the tree, Root, be a singleton set with the single element 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. Figure 2.4: A tree for constructing the W set States=[s(S0, SQ), s(Si, 5 a ) , s ( S „ . i,Sn-i)J 23 2. If each state has at least one UIOS, stop. 3. If Node contains elements that are singleton sets then For each singleton set element s(S{, Sj), record the path from Root to Node as an UfOS for Sj Else Terminate the node if Node satisfies one of the two conditions: (a) Node is identical to one of its ancestor. (b) All elements in the N('s £ Node contains either singleton sets or sets with all identical elements Else Continue. 4- For each input symbol, ik DO (a) For each Ni, where Ni £ 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 ik-ii. For each output symbol, o\, resulting from applying ik DO Collect 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 Si. [[s(Sl,S2)],[s(S2,Sl),s(S3,S2)]] [[s(Sl,S3),s(S2,S3),s(S3,Sl)]] [[s(Sl,Sl)],[s(S2,S2)],[s(S3,Sl)]] [[s(Sl,S2),s(S2,S2)],[s(S3,S2j [[s(S1,S3)],[s(S2,S3),s(S3,S3)]] , ^ ^ ^ ^ ^ singleton set b.a is an UIOS for S3. singleton sets a.a is an UIOS for SI, S2 and S3. singleton set a.b is an UIOS for SI. 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. UIOS verifying procedure Suppose we have a set of XJlOSs=[UIOS\,UIOSm], each UlOSi is the UIOS for a set of state 5,. We also assume there is a reset symbol, ri, which takes the FSM 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 0 be the initial state of the FSM. We can carry out the procedure as follows: For each UlOSi <E UIOSs Do For each Sj £ Si apply the sequence ri@SP(so,Sj)@UIOSi 2.3.6 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. Theorem 1 The upper bound of the length of a test sequence generated by the UIO-method is of 0(kn4). 26 Proof 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(n2) [Koha78j. Since G is strongly connected, it takes at most n-1 transitions from one edge to any other edge. Thus, the overall length of the test sequence is of 0(kn)*0(n2)*0(n-l) —• 0(kn4) Theorem 2 The upper bound of the length of a test sequence generated by the UIOv-method is ofn5. Proof 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(n2)*0(n — l)*0(n)*0(n — 1) —> 0(nh). The n2 term is for the state-identifying 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(nh) + 0(kn4) — • 0(n 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(kn2) DS-method 0(knn+2) W-method 0(kn4) UlO-method 0{kn4) UlOv-method 0(n5) 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. C h a p t e r 3 F a u l t C o v e r a g e m e a s u r e m e n t 3.1 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 dis-tinguish one F S M from another (e.g. isomorphic). Therefore, the definition of UTS must take into account such factors. In order to define UTS, 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 contains M2 iff the behavior of M2 is a subset of that of M2. Then, UTS can be defined as follows: 28 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 UTS 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 FSM, we define UTSi to be the test sequence for this F S M such that only this FSM 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 FSM, These method will not guarantee the uniqueness of the generated state identifying sequences owing to the extra state in the IUT FSM. 3.2 Arbitrariness in Test Sequence Generation and Fault Coverage Metric Arbitrariness in test sequence generation was noted in [Sidh89a]. In checking exper-iment 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 FSM. 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 FSM 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 FSM: 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 UTS 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 FSM 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 FSM. 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 FSM provides the "full" fault coverage since there is only one FSM, 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 FSM. 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) =\. C h a p t e r 4 T h e C o n s t r a i n t s S a t i s f a c t i o n P r o b l e m ( C S P ) A p p r o a c h 4.1 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 n where these variables take their values. A constraint dj(xi,Xj) 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 con-straint C,...A:(x,-,Xk) specifies the values Vi,...,vk, where u,- G Di,...,vk € Dk, which the variables can take on. The CSP is the problem to find all sequences of values V{,...,vn for a set of variables z,-,...,xn 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 con-straints on the two state variables connected by this edge. The i/o constraints com-bined 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 FSM 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\ iP/op can be expressed as a set of constraints using the notation described in Section 2.1, as follows: 35 f(xi,n) = x2, g(xi,ii) = oi The variables Xi,...,xp must satisfy this set of constraints together with the basic constraints described in Section 2.1. The domains for these variables D2 = ... = Dv-\ C the set of states in the FSM. 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 FSM 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\ — s0, the start state of the F S M , from the fourth constraint. Each solution is a set of values Vi,...,vp, where U i , . . . , u p £ Q, which represents a FSM. 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 FSM 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 2 is at most n 2 , where nj < n 2 . In order to keep the number of FSMs that 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 FSM can be used as the initial sequence. Other initial sequences may be more desirable if they contain more knowledge (con-straints) on the structure of the FSM 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 n2). The initial sequence generated using this method, contains more knowledge (constraints) on the structure of the FSM than the transition tours generated by the T method [Nait81]. Yet its length is no longer than kn2, where 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. 8-testing for i = 0, 7-testing for i=l, etc... It is possible that some FSM 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 FSM. In the next section, we will present an efficient algorithm for solving the CSP. 4.2.2 Algorithm for Solving the CSP Algori thm 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,...,xm} (m < I) be a set of state variables such that each xt- £ X can take on a value Sj £ S, and let Si 38 and S2 C S. Furthermore, let EQ and NEQ be two sets of constraints such that each constraint e = (yt, is either in EQ or NEQ, e G EQ V e G NEQ, where y,- G X is 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 0} and $2 — --^fc-i}-3. If (S2 ^ 0,) then Si = Si + sx and 5 2 = S2 — sx where sx G S2 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 x3 G X and let Sj, = S\. For each e = (y,-,j/j) G NEQ where yi = x3 and yj G Si, remove yi from Sd-6. For each sg G Sd, let xs = sg. If E is consistent with rules 1 to 3 in Section 2 under the assignment for xs do 39 If X = 0, then a solution is found else go to 3. 7. stop. The use of Si and S2 in steps 2 and 3 are necessary to avoid to consider the FSMs which differ only by state renaming. Steps 4 and 5 help eliminating some impossi-ble 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 FSM solutions and when the algorithm stops, the overall additional sequence comprise all subsequences generated in step 1. In step 1, a breath-first algorithm is used to distinguish between a pair of FSMs. For two strongly connected n-state FSMs M i and M2 to be different, there must exist a pair of states i in M i and j in M2 such that the transition functions (i.e. outputs) of i and j are 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 2 respectively,, and once in i and j, an extra transition is needed to distinguish between M i and M2. 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 breath-first 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(k2n). This test sequence generation procedure has been implemented as a Quintus Pro-log program running on Sun workstations. The source code can be found in the appendices. 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 UTS0 is constructed for the FSM in Figure 2.1. We 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(s0,X0, a/l),c(X0,Xua/0),c(Xu X2, a/1) c(a0, X3, a/l),c(X3, X4, b/l),c(X4, X5, 6/1), c(X5,X6, a/1) c(sQ, X7, b/l),c(X7, X8, b/l),c(X8, X9, a/1) c(s0, X 1 0 , a/l),c(Xw, X1U b/l),c{Xlu X 1 2 , a/0), c (X 1 2 , X a 3 , a/0), c (X 1 3 , X 1 4 , a/1) 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 = X3 = XIQ and X4 = X\\ Constraints XQ = X3 = Xw are derived from clauses c(so, XQ, a/l),c(so, X3, a/1) and c(s0, XiQ,a/l). Similarly, X4 = Xn is obtained from c(X3, X4, 6/1) and c(Xw, Xn, 6/1). After renaming and removing duplicate clauses, the following clauses remain: c(sQ, XQ, a/l),c(X0, X1,a/Q),c(X1,X2, a/1) c(s0, Xa, b/l),c(X4,X5, b/l),c(X5, Xe, a/1) c(s0, X7, b/l),c(X7, X8, b/l),c(X8, X9, a/1) c(X4, X12, a/0),c(X12,X13, a/0),c(X 1 3, X 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 7^ $0, XQ ^ X\, XQ 7^  X 5 , 7^ X g , X o 7^ X i 3 X4 7^ 5 0 , 7^  X 4 7^  X 5 , X4 7^ X g , - ^ 4 7^  Xi3 X\2 7^ ^0,-^12 7^  ^15-^12 7^  - ^ 5 , ^ 1 2 7^ X12 7^ X 1 3 For example, X0 7^  s0 is derived from clauses c ( s 0 , X 0 , a / l ) and c(Xo,Xi,a/0) since applying the same input symbol a to X0 and s0 results in different output symbol. 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 FSM. The following order is obtained: Xo, X4,Xi, 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) and c ( X 4 , X l 2 , a / 0 ) and the previous assignments XO = 51 and XA = 51. The assignment XI = 50 is obtained by considering the inequalities XO ^ XI and XI ^ 52 together with the previous assignment XO = 51 and X4 = 52. 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/- .a/l.a/Q./a/l r/- .a/l.b/l.b/l.a/l r/ - .6/1.6/l.a/l 44 NODE 1 X1=X12 X4=X5 contradiction l oX7=S0 X8=S0 X9=S1 X12=S1 X13=S0 X14=S1 I X2=S1 solution NODE 2 X1=S0 \ X5=S0 X6=< X7=S1 X8=X4 contradiction X4=S2 X7=S2 X8=S0 :a=si X12=S1 X13=S0 X14=S1 X2=S1 solution X12=S2 X13=X12 contradiction 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 - FSM with a state that has no UIOS Figure 4.3: An FSM whose state C has no UIOSs Figure 4.3 shows an FSM 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. An unique test sequence(£/T.So) for the given FSM 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 FSM (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 FSM of Figure 4.4. 4.3.3 E x a m p l e C - H i g h e r O r d e r UTSi In this example, we show how an 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 FSM solutions. After eliminating the F S M solutions that contain the target FSM, Figure 4.6 shows the remaining three FSM 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 FSM solutions for Example C C h a p t e r 5 T e s t R e s u l t A n a l y s i s - T w o a p p r o a c h e s 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 FSM 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 in-puts/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. However, by solving the CSP, six fault models are obtained! 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, FSM 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: All 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 FSM. Over the past few years, many diagnostic reasoning systems have been devel-oped 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 ap-proach 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 FSM 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 FSM, 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 FSM, the observed I/O sequence. (b) FD, the functional description of all the COMPONENTS which describes the behavior of the COMPONENTS under both normal and abnormal conditions. Figure 5.3: A 3-state FSM with COMPONENTS=[tllt2,t3,t4,t5,t6] Example 4 One of the possible system descriptions of the FSM shown in Fig. 5.3 is given as follows: C0MP0NENTS=[tl,t2, t3, Uh t5,t6] 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) output(t2,C,l) - 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) output(t5,C,l) - not.ab(t6) A input(t6,C,l) => output(t6,B,0) 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,...,compn), 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,...,compn consistent with the inputs and observed outputs. 62 5.2.3 Some Important Definitions Definition 9 A minimal diagnosis for (MD,FD,OBS,COMPONENTS) is a minimal set A C C O M P O N E N T S such that MD U FD U OBS U {not_ab(c)| cGCOMPONENTS-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 (MD,FD,C0MP0NENTS,0BS) is a set {cu ...,ck} C C O M P O N E N T S such that MD U FD 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. 63 Theorem 1: A C COMPONENTS is a diagnosis for (MD,FD, COMPONENTS, OBS) iff A is a minimal hitting set for the collection of conflict sets for (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 n a s a successor node n„ joined to n by an edge labeled by a. The label for na is a set S GF such that S fl H(n^) = {} if such a set S exists. Otherwise, na is labeled "y/". Figure 5-4 shows an example of an HS-tree. Example 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] [1,3,5] [2,4,6] X v / x ^ x V \/x V x [1,2,3] [2,4] X X X Figure 5.4: An 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 mini-mal diagnoses can be computed by computing the minimal hitting sets. This al-gorithm can be precisely described by a straightforward recursive procedure prun-tree(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 =[]. If no conflict set can be found then branch(Components,Arcs) will be cut off and Arcs is a diagnosis (it uses the constraint suspension technique to check consistency). • split(branch( Components, Arcs),ConflictSet) the procedure is responsible for growing and branching the HS-Tree. The algo-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. Algorithm 6 Procedure split(branch(Components,Arcs),ConflictSet) Begin For every s € ConflictSet Do Begin NewArcs=Arcs-hs Node=Node+Branch(Components~s,New Arcs) 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=[a1,an] should be pruntree (branch([a^,anJ,[]),[]) Initially, diagnoses is empty and node contains only the root(i.e. contains only branch([a\,an],[]). The followings describe the algorithm in detail. Algorithm for prunning the HS-Tree Algori thm 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 tl (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. C h a p t e r 6 C o n c l u s i o n s 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 se-quence 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 (UTSQ), 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. B i b l i o g r a p h y [Aho88] Aho, A . V . , Dahbura, A.T. , Lee, D. and Uyar, U.M. , "An Optimiza-tion Technique for Protocol Conformance Test Generation Based on UIO Sequences and Rural Chinese Postman Tours," Proceeding Eighth International Symposium on Protocol Specification, Testing, and Ver-ification, 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 Ma-chine," 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 Intelligence,24,1984,347-410. [Fike70] Fikes, R.E. , " R E F - A R F : A System for Solving Problems Stated as Procedures" Artificial Intelligence,!, 1970,pp.27-120. [Gene84] M . R. Genesereth, "The use of design descriptions in automated di-agnosis", Artificial Intelligence,!^, 1984,411-436. [Gone70] Gonene, G. , "A Method for the Design of Fault Detection Experi-ments," 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 Fault-detection 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," Chi-nese 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 Generat-ing Protocol Tests," Proceedings of 9th Data Communications Sym-posium, IEEE 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 Method-ology 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, (Amer-ican Elsevier, New York, 1976). [Sidh89a] Sidhu, D. P. and Vallurupalli R., "On Arbitrariness in Protocol Con-formance 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 Pro-tocol 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 Ex-ternal 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 A T e s t S e q u e n c e G e n e r a t i o n T o o l s :-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(_, [] ) : -nl. 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 predicate uio finds a l l the shortest uios for a FSM. X In order to use this 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 description. The predicate uio (Filename) can be used to write X a l l the uios to a f i l e Filename or to display them on screen i f uio (user) '/, is 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 ,L) . trace_path([Sl|Ss],S,L):-!,trace(Sl,L),!, trace_path(Ss,S,L). trace(_,[] ) : - ! . fai l . trace(Sl,[L1|L2]):-tree(Sl,Bs), in_tree([Ll],Bs,New_node),!, trace(New_node,L2). trace(_,_). in_tree(_,[] ,_):-! . fai l . 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. The X X tour traverses every transition at least once. X 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) . 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] ):-jtlist(T,Sec,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 wil 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(X),write(1 '), write(Y),nl, showl(Uios). 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(X),write(' '), write(Y),nl, show2(CSSs). 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(f i le(_)) , 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. Fi le 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. X 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)), 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 The predicate complete_spec(File!n,FileOut) accepts a incompletely specified X '/, FSM in Fi le ln and completes the FSM by adding an arc with label x/null to */, '/, i tself for any unused input symbol x. X */, The format of Fileln is as follows: '/. y. i , 2 , a / x . y. '/. 2,3,b/y. y. 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 . label ([] , []) . 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, te l l (F) , write_trans, told.tel l (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)),!, f a i l . A p p e n d i x B C S P P r o b l e m S o l v e r *********** ***************************************** ********************* •The following program accepts a test sequence and computes a l l n-FSMs * •for a given n which satisfy this test sequence. * ************************************************************************* :-dynamic inconsistent/0. :-dynamic equal/2. :-dynamic not_equal/2. :-dynamic c / 3 . •.-dynamic solution/1. :-dynamic 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)JP):- NKN2,! , P=..[PName,s(Nl),s(N2)] add(PName,s(Nl),s(N2),P):- N1>=N2, 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 TO I/O'), a l , setupworkdb(Cs), » collect_edges(0), cleanupworkdb(c,3). 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]):-write(From), write(' write(To), write(' write(IO), n l , 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