State elimination has been proposed in the literature as a viable technique for transforming nite state automata (or nite state machines) into equivalent regular expressions. In this TTC case, we consider this well-known technique as a model transformation problem, aiming at evaluating the suitability, performance and scalability of dedicated model transformation techniques w.r.t. this problem.
Finite state automata (or nite state machines) are used in many applications such as program analysis, data validation, pattern matching, speech recognition as well as in the behavioral modeling of systems and software. Furthermore, quantitative extensions of automata are used to evaluate system behavior together with software pro les in software engineering. Such models are, like Markov chains, probabilistic automata, adding probabilistic distributions to state transitions [BKL08]. Even though the semantically equivalent counterparts of (probabilistic) nite state automata, namely (stochastic) regular expressions, are generally not considered as behavioral models, they may be used in the aforementioned applications interchangeably with nite state automata. In practice, regular expressions are often transformed into nite state automata, e.g. to obtain models from code, to extract behavioral models at runtime, etc. While this is not an expensive task, the transformation of a (probabilistic) nite state automaton into an equivalent (stochastic) regular expression is much more expensive and challenging.
Input: Step 1: Step 2: Step 3: i i i q0 ε b q0 a b a b a q1 a q1 ε a+bb*a
q1 b*a
ε b*a(a+bb*a)* f f f
State elimination [DK01] has been proposed in the literature as a viable solution for doing this kind of transformation. In this TTC case, we consider this well-known technique as a model transformation problem, aiming at evaluating the suitability, performance and scalability of dedicated model transformation techniques w.r.t. this problem.
Section 2 brie y recalls basic principles of state elimination and presents a reference implementation based on a commonly used software package for experimenting with formal languages. Section 3 rephrases the involved problems as model transformation problems and provides the respective task descriptions, some of which are being considered as optional extensions to the main task of doing state elimination. Section 4 presents a set of quality characteristics to evaluate proposed solutions. All resources provided along with the case can be obtained from https://github.com/sinemgetir/state-elimination-mt/ 2
In this section, after recalling some basic de nitions, we describe the state elimination algorithm, a reference implementation using JFLAP [PPR96], and our probabilistic implementation that is an extension to JFLAP in detail. 2.1
In the following, let be a nite set of symbols, called alphabet, and the words over . A regular expression over represents a regular language L( ) for which, according to Kleene's theorem, there exists a nite state automaton accepting this language. An FSA is a tuple (Q; ; ; q0; F ) where Q is a nite set of states, is an alphabet, : Q ! Q is a transition function, q0 2 Q is the initial state, and F Q is a set of nal states. We say that an FSA is uniform if it has has a unique initial state with no incoming transitions and a unique nal state with no outgoing transitions. Uniforming an FSA may be performed as follows: If q0 2 F or if there exists an a 2 and q 2 Q so that (q; a) = q0, then add a new state i to Q with (i; ) = q0 and set i as the new initial state instead of q0.
If jF j 1 or if there exists p 2 F , a 2 and q 2 Q so that (p; a) = q, then add a new state f to Q, add the transition (p; ) = f for all p 2 F and set F = ff g.
The state elimination algorithm [DK01] takes a FSA as input and calculates a regular expression describing its accepted language as output. Given an FSA, state elimination works on its uni ed form. The idea is to iteratively eliminate states which are neither initial nor nal. In each step, a new equivalent generalized transition graph (GTG) is created until only the initial and nal states are left. A GTG generalizes an FSA in that transitions may be labelled by regular expressions instead of single symbols.
Let R( ) be the universe of regular expressions over a given alphabet , then the transition function is generalized to : Q R( ) ! Q. Roughly speaking, regular expressions used as transition labels are utilized to keep track of eliminated states. The regular expression labelling the transition between the two states that remain at the end of the iteration represents the nal output of the algorithm.
In Algorithm 1, let xy be the regular expression for the transition from state x to state y. Moreover, given an FSA A = (Q; ; ; q0; F ), we refer to its uni ed form as A0 = (Q0; ; 0; i; ff g) which we will interpret as GTG during state elimination.
Algorithm 1 State elimination Input: A uniform FSA A0.
Output: A regular expression de ning the regular language accepted by A0.
2: Randomly choose a state k 2 Q0 n fi; f g and remove it from A0. 3: Then for all pairs p; q 2 Q0 n fkg the new regular expression p0q for the transition from p to q is: p0q = pq + pk kk kq 4: until There are only the initial state i and the nal state f left.
Based on Algorithm 1, a small example that demonstrates how to convert an FSA into a regular expression is presented in Figure 1. Step 1 uniforms the given FSA, while steps 2 and 3 showcase the iterative elimination of states. 2.2 We use the common software package JFLAP [PPR96] to transform an FSA into an equivalent regular expression using the state elimination method. The di erence between Algorithm 1 and the JFLAP implementation is that, for the latter one, the initial state can have incoming transitions and the nal state can have outgoing transitions. Considering that, the transformation can be divided into three steps:
(1) Conversion of the given FSA into a simple FSA: A simple FSA is an FSA which is uniform and, in addition, for all pairs of states there is exactly one transition. The simple automaton is created in the following steps:
If the automaton has more than one nal state or the initial state is a nal state, we create a new state s and for all nal states f, add an transition for f ! s and set s as the only nal state. Note that in JFLAP transitions are de ned as transitions with the empty string as the label. If there are several transitions between two states, we combine them into a single transition; the new label is obtained as a disjunction of all transition's labels.
If there are no transitions between two states, we add an empty transition between them. An empty transition is a transition with the label ;.
(2) Conversion to a GTG. Converting a simple automaton obtained from step (2) into an equivalent GTG with only the initial state and the nal state is described by Algorithm 2, which in turn uses the subroutine described in Algorithm 3 in order to obtain a regular expression for a state to be eliminated.
(3) Deriving the regular expression. We now have an equivalent GTG with exactly two states, the initial and the (di erent) nal state. Algorithm 4 describes how we get the nal regular expression. Algorithm 2 convertToGTG Input: A simple automaton A.
Output: An equivalent GTG A0 with only the initial state and the nal state.
1: for k : A:getStates() do 2: newT ransitions [] 3: if k is not initial or nal then 4: for p; q : A:getStates() do 5: if p 6= k and q 6= k then 6: pq getExpressionF orElimination(k; p; q; A) 7: newT ransitions:add(pq) 8: remove k and all its incoming and outgoing transition from A 9: A:add(newT ransitions)
Input: The state k to be eliminated, the state p that reaches k, the state q that is reached from p via k, the automaton A.
Output: The regular expression for the transition from p to q without k.
1: pq the regular expression for the transition from p to q 2: pk the regular expression for the transition from p to k 3: kk the regular expression for the transition from k to k 4: kq the regular expression for the transition from k to q 5: return (pq) + (pk)(kk) (kq))
Input: The GTG A0 with only the initial state and the nal state. Output: An equivalent regular expression for A0.
1: i A0:getInitialState() 2: f A0:getF inalState() 3: ii the regular expression for the transition from i to i 4: if the regular expression for the transition from i to f 5: f f the regular expression for the transition from f to f 6: f i the regular expression for the transition from f to i 7: return ((ii) (if )(f f ) (f i)) (ii) (if )(f f ) 2.3
The case of transforming an FSA into an equivalent regular expression may be extended to converting probabilistic ( nite state) automata (PA) into stochastic regular expressions.
A PA is a tuple (Q; ; P; q0; F ) where Q, , q0 and F are de ned analogously to FSAs, and P : Q Q ! [0; 1] is a transition probability function assigning a probability to each transition such that 8q 2 Q n F : Pq02Q Pa2 8q 2 F : Pq02Q Pa2
P (q; q0; a) = 1, and
P (q; q0; a) = 0
We extend the state elimination algorithm to PAs and provide a reference implementation using JFLAP. When a PA is converted to a regular expression, this regex is also enriched with probabilities and rates, generally referred to as stochastic regular expression (SRE). We present the syntax brie y as follows: E :=
X Ei[ni] i
E1 : E2
E f where 2 [ f g, ni 1000 2 N0, f 2 [0; 1]
Q and Ei is a SRE: Atomic Action : The action
is an atomic action.
Choice/Sum Pi Ei[ni]: One of the provided terms is randomly chosen. The ni denotes the choice number for each term. The ith term is chosen with the probability Pnjinj .
Kleene Closure E f : The term E is repeated random number of times. Each iteration occurs with a probability of f .The termination probability is 1 f .
Concatenation E1 : E2: The terms E1 and E2 are successively interpreted. As the concatenation is associative, parenthesis may be omitted.
State elimination for PAs follows the same basic principles as for FSAs (see Section 2.2). The extended steps for the probabilistic version of the state elimination appears with the probability calculation. In the beginning, the probabilities of all outgoing transitions are recalculated where the probability of the loops remain unchanged. During the \label join", the probabilities are multiplied, remain unchanged and are uniformed to rates (e.g. Constant=1000) when expressions are concatenated, starred and choiced, respectively. During the recalculation of probabilities, we ignore loop transitions from a state to itself, epsilon and empty transitions. We recalculate the probabilities of the remaining outgoing transitions of each state using the follow steps: First, for all transitions, we add their probabilities to get the new "100%". Second, to get the new probability of each transition, we divide its old probability with the sum computed in the rst step.
The reference implementation can be found in the resources provided along with this TTC case. Figure 2 showcases the probabilistic extension of state elimination by means of an example. Note that the probability of the last remaining transition is 1.0, so we omitted it in the gure. 3
The basic idea of this TTC case is to rephrase the well-known problems sketched in Section 2 into dedicated model transformation challenges. A generic meta-model for transition graphs which may be interpreted as FSAs, CTGs and PAs is presented in Figure 3. The nodes of a transition graph represent the states while its edges represent the transitions of an FSA, CTG or PA. States are attached unique identi ers. Transitions may be labelled (carrying either symbols or regular expressions) and, in case of PAs, equipped with probabilities. Since virtually all model transformation tools available in the model transformation research community are based on the Eclipse Modeling technology stack, we provide an implementation of the meta-model presented in Figure 3 in EMF Ecore. Of course, other meta-modeling technologies are allowed in solutions as well. This requires a conversion of the input models serving as experimental data in terms of the evaluation (see Section 4), which we provide in EMF format. 3.1
The main task is to implement a state elimination for FSAs as a model transformation. In this basic setting, we assume that the FSA given as input is uniform. Thus, the task boils down to iterative state removal until there is only the initial state and nal state left, thereby updating regular expressions attached to transitions. As a rst additional yet optional task, we ask to uniform the FSM before applying state elimination. The task is to obtain a uniform FSA containing a unique initial state and a unique nal state from a non-uniform FSA containing multiple initial and nal states.
A second optional extension is to provide a model transformation taking a probabilistic nite state automation as input and producing a stochastic regular expression as output. Extension 2 can be considered independently from Extension 1. 4
To evaluate the quality of the proposed solutions, we give a set of quality characteristics which we consider to be relevant for the presented transformation case. The characteristics are inspired by the ISO/IEC 9126-1 standard, which de nes quality characteristics in the broader scope of software engineering [BBC+04, JKC04]. We also draw inspirations from more recent work dedicated to the quality of model transformations [SG12, GSS14, LMT14]. We re ne each quality characteristic into measurable attributes for each of the tasks presented in Section 3. To obtain concrete measures for their solutions, participants are kindly invited to use the evaluation framework provided with the case resources. This way, most of the measures may be obtained in an automated manner. 4.1
A rst important and rather obvious quality characteristic is the correctness of the provided solutions.
A transformation solving the main task (see Section 3.1) is correct if the regular expression obtained as a nal result of the state elimination is correct. This means that it is semantically equivalent to the regular expression obtained from the reference solution using JFLAP presented in Section 2.2. Although semantically equivalence of regular expressions is decidable in general, we abstain from providing such an automated equivalence proof in our evaluation framework. We choose a testing approach instead, providing sets of positive and negative test cases, i.e., sets of strings to which the produced regular expression should match and should not match. This way, a result is considered to be correct if it passes all tests.
A solution to the rst extension task (see Section 3.2) is correct if the produced model represents a uniform FSA which is equivalent to the one provided as input. This can be con rmed by checking equality of the resulting model to the one produced by a reference implementation in our evaluation framework. This correctness test may be automated using the model comparison tool EMF Compare [BP08], which should report no changes between a produced output model and the corresponding reference output model.
Correctness of solutions to the second extension task (see Section 3.3) can be checked in a similar way as for the main task. We use the same test cases as for the main task, ignoring probabilities of the stochastic regular expressions produced as output of the second extension task.
All tasks are scored by means of the provided test cases. A point is given for each test case which passes successfully, points are summarized over all test cases. This means that a correct solution for the main task may get a maximum number of 11 points, while correct solutions to the rst and second extension task may get a maximum of 3 and 9 points, respectively. 4.2
Since this TTC case basically rephrases a set of well-known problems into a dedicated model transformation challenge, we are particularly interested in the suitability of the transformation speci cations solving these problems. Since general quality metrics from traditional programming languages, such as complexity or modularity, are hardly generalizable for a set of di erent model transformation languages, we choose a rather simple qualitative criterion which can be referred to as the level of abstraction. We follow the approach presented in [LMT14]: The level of abstraction is classi ed as High for primarily declarative solutions, Medium for declarative-imperative solutions, and Low for primarily imperative solutions. All tasks presented in Section 3 are evaluated in the same way.
Since we acknowledge that classifying the abstraction level of a solution according to its declarativeness may be biased by subjective preferences, the scores that may be obtained for this quality characteristic are relatively low to not too much in uence the overall results. All tasks and extension tasks are scored evenly with zero to three points. Zero means the task has not been tackled at all. If it has been solved, solutions may be scored with one, two, or three points, depending on the abstraction level ranging from low, medium, to high. 4.3
Performance is measured in terms of the execution time of a transformation solving the task. This includes the loading of input models and printing or serializing the produced output. The measuring of execution times can be automated by using the evaluation framework provided along with the case description. For the main task and each of its extensions, execution times should be measured for all input models already introduced in Section 4.1.
Performance results of a solution are scored by comparing the execution times with the other solutions. We consider the average execution time for the rst ten input models (see leader3 2 to leader4 4 in Table 1). The fastest solution gets 14 points (maximum number of points for correctness and suitability of a solution to the main task). The remaining solutions get proportional scores w.r.t. their average execution times. 4.4
Since the reference solution using JFLAP su ers from scalability problems when dealing with large input models (cf. Section 4.5), we are particularly interested in whether modern model transformation technologies can improve the scalability of the state elimination. In addition to the FSA models provided for evaluating correctness and scalability, we provide additional larger models comprising up to around one million states. Solutions should gure out which is the largest model they are still able to handle. Scalability is only considered for the main task presented in Section 3.1. As we can see in Table 1, the reference solution based on JFLAP scales up to model leader4 4 containing 812 states.
Scalability is scored by comparing the solutions with each other. The solution which scales up to the largest input model gets a score of six points (analogously to performance). The rest of the solutions get scores which are proportional w.r.t. to the number of participating solutions. 4.5
In this section, we present the evaluation results obtained for the reference solution using JFLAP. Please note that we give the results to better illustrate our evaluation criteria, while it is not intended to compare solutions using dedicated model transformation technologies with the reference solution, but mutually among themselves. We use models produced by the Synchronous Leader Election Protocol from the Prism Benchmark Suite [KNP12]. These models are Discrete Time Markov Chains (DTMC), but we interpret them as FSAs an PAs by using the target state names of transitions as labels. In case of FSAs, we ignore probabilities. For example, the DTMC triple (0,1,0.87) is interpreted as a transition from state s0 to state s1 assigned with the label \s1".
Table 1 summarizes our experimental results obtained for the reference solution using JFLAP. Participants in this case should use the same input models, all of them are available as EMF models conforming to the generic meta-model introduced in Section 3. In Table 1, sizes of input models are indicated by the number of states, execution times are reported in seconds. The used timeout duration was one hour per model. We ran all
experiments on a macOS with 1,6 GHz Intel Core i5 processor and 8 GB of memory (Java 1.8 with the maximum heap size of 2 GB).
This work was partially supported by the DFG (German Research Foundation) under the Priority Programme SPP1593: Design For Future { Managed Software Evolution. [BKL08]
Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of model checking. MIT press, 2008.
Cedric Brun and Alfonso Pierantonio. Model di erences in the eclipse modeling framework. UPGRADE, The European Journal for the Informatics Professional, 9(2):29{34, 2008.
Ding-Shu Du and Ker-I Ko. Problem Solving in Automata, Languages, and Complexity. John Wiley and Sons, 2001.
Christine M Gerpheide, Ramon RH Schi elers, and Alexander Serebrenik. A bottom-up quality model for QVTO. In Int. Conference on the Quality of Information and Communications Technology, pages 85{94. IEEE, 2014. [KNP12] [SG12]