// Operations on LTSs supported by LTSA // STATE MACHINE COMPOSITION // Example state machine A = (a -> b -> c -> A | b -> c -> a -> A). // Q1: What are the execution sequences of this state machine ? // Another state machihne B = (a -> c -> B | c -> c -> a -> B | b -> B). // Composition with rendezvous for all interactions that are in the alphabets of both machines ||S = (A || B). // Q2: Why is there a deadlock ? // replace second A by STOP - which means deadlock ||A1 = A. // replace second A by END - which means desired end (a "good" deadlock) // check again ||A1 = A. // delete third alternative of B // check again ||S // Q3: Why is there no deadlock ? (Answer: b is not in the alphabet of B) // TESTING // Testing means to check whether a given execution sequence can be realized by the state machine // This is done by composing the specification of the sequence with the specificatio of the machine. // for instance, the sequence a, b, c, b, c T1 = (a -> b -> c -> b -> c -> END). ||TEST1 = (T1 || A). // PROJECTION set ImportantInteractions = {a, c} ||A2 = (A) @ ImportantInteractions. // this means A projected onto the ImportantInteractions (b is not visible) // look at drawing (it shows the invisible transitions with label tau - sometimes calle lambda or epsilon // perform the Minimize operation - this is the real projection where the invisible transitions are eliminated // and an equivalent state machine is constructed (based on the reduced alphabet) // PROPERTIES - introduction of a FAIL STATE // the following state machine is equivaltent to the determinized projection above C = (a -> c -> C | c -> a -> C). ||S1 = (A || C). //look at C - by the way, S1 has no deadlock because the alphabet of C does not incolude the b property CC = (a -> c -> CC | c -> a -> CC). // This is the same state machine, but LTSA adds a FAIL STATE (error state) // which is reached for any transition that is not in CC ||S2 = (A || CC). // since CC is the projection of the "good" transitions of A, this composition S2 will never all that CC goes to the error state // however, we may want to check that also the projection of B only performs transitions that are "allowed" by CC // by checking ||S3 = (B || CC). // CONCLUSION: combining a state machine with a property allows to check whether // the execution sequences of the state machine are included in the execution sequences of the property machine // In the case that the alphabet of the property machine is smaller than the alphabet of the checked machine // the behavior of the checked machine will first be projected onto the alphabet of the property machine // This is a check of TRACE INCLUSION // (a typical safety check: Are all execution sequences of the machine allowed according to the requirements ? )