We present a solution to the State Elimination Case of the Transformation Tool Contest 2017, based on the Henshin model transformation language. The main task is to convert a nite state automaton (FSA) into a regular expression; two extensions include the simpli cation of FSAs as well as the conversion of probabilistic FSAs. The distinguishing feature of our solution is its largely declarative speci cation, based on Henshin's concepts of rules and composite units for specifying modi cations and control ow. We present the results of the performance and scalability evaluation from the provided benchmark suite. Similar to the reference solution, our solution did not scale up to all test models in the benchmark suite; yet, compared to this solution, it achieved a speed-up by two orders of magnitude for some of the larger models.
Finite state automata (FSAs) are a modeling concept with many practical applications, including program analysis, pattern matching, speech recognition and behavioral software modeling. In its basic form, a FSA comprises a set of states and a set of labelled transitions between the states; some of the states are designated as initial and nal states. An important feature of FSAs is their fundamental relationship to regular expressions. While converting a regular expression into a corresponding FSA is easy, the opposite task is more sophisticated; current solutions su er from nonlinear algorithmic complexity [GVP+17].
The TTC 2017 state elimination case [GVP+17] aims to study how transformation tools may contribute to more e cient solutions. The case description speci es three tasks|a main task and two extensions|dealing with three kinds of FSAs: (i) basic FSAs with at least one initial and at least one nal state, (ii) simple FSAs with exactly one initial and exactly one nal state, and (iii) probabilistic FSAs, in which transitions are annotated with probabilities. Simple FSAs are a subset of basic ones, whereas probabilistic FSAs generalize basic ones. The main task is to transform a simple FSA to a regular expression. Extension 1 involves transforming a basic to a simple FSA, and extension 2 deals with transforming a probabilistic FSA to a stochastic regular expression.
In this paper, we present a complete solution based on the Henshin model transformation language [ABJ+10]. Henshin is a graph-based transformation language providing support for the declarative speci cation of in-place model transformations. The basic features of Henshin's tool set are a suite of editors and an interpreter kernel; more sophisticated features include code generation for parallel graph pattern matching and support for various transformation analyses.
Copyright c by the paper's authors. Copying permitted for private and academic purposes.
Figure 1: Solution for main task: state elimination in FSAs.
A distinguishing feature of Henshin is its expressive visual syntax which aims to facilitate usability during transformation development [SBG+17]. To provide a largely declarative solution, we use Henshin's concepts for the speci cation of control ow and model modi cations. Control ow is speci ed using composite units that orchestrate the execution of a set of sub-units and rules, for example, by applying them in sequential order or in a counted loop. Model modi cations are speci ed using rules, expressing basic match-and-change patterns. 2
Solution In what follows, we present our solution in detail. We start with the main task and continue with the two extension tasks. The solution is available via GitHub at https://github.com/dstrueber/stateelim-henshin. The URL of the associated SHARE image is made available on the GitHub site. 2.1
Our solution to the main task follows the state elimination algorithm presented in [GVP+17]. We implemented this algorithm using 8 rules, which are orchestrated in a control ow of 6 composite units, as shown in Fig. 1. As required by the speci cation, the produced result is a string representing the output regular expression. On the way to this result, we manipulate state labels using string operations, thus enabling a compact speci cation.
The overall goal is to remove all non-initial and non- nal states from the FSA. To achieve this goal, our starting point is the loop unit main which executes its inner unit eliminateNode as often as possible. The aim of eliminateNode is twofold: rst, it checks whether any state is to be removed and, if this is the case, identi es it. This is done using the rule hasRemaining, a simple rule for matching a non-initial and non- nal state. Second, if such state is found, it is stored in the parameter cur (for current ) and passed to the sequential unit eliminate. The eliminate unit proceeds in the following steps: rst it \ xes" the incoming and outgoing transitions of state cur by replacing them, then it deletes cur, and nally, it uni es any redundant transitions arising in the process.
To x the transitions, conditional unit xTransitions rst checks if cur is a looped state, that is, a state with a loop transition. Depending on the result, one of the rules xTransitionsUnlooped and xTransitionsLooped is triggered, which only di er in their treatment of the loop. Both rules make use of rule-nesting: they have a kernel rule|the \ at" states in the visual syntax|and a multi-rule|the \layered" states with asterisk signs. When applying either rule to the input model, the kernel rule is matched rst, and then, based on the identi ed match, the multi-rule is applied with a for-all semantics, that is, as often as possible. Based on the provided state cur, all pairs of incoming and outgoing transitions are identi ed, and a new transition is created for each of these pairs. The label of the newly created transition is composed of the labels of the pair (plus in the loop case, the loop label), which are stored and propagated using the variables a, b (and l ). Rule delete works in a similar manner by deleting state cur via the kernel rule, and its adjacent transitions via separate multi-rules.
As a result of the xTransitions step, the model may temporarily contain pairs of states with multiple transitions. These redundant transitions are now uni ed, using separate loop units for cases where the transitions are non-loops and loops, respectively. Each of these units calls a rule which nondeterministically identi es redundant pair of transitions, removes one of the transitions, and joins its label with the label of the remaining transition.
The main unit terminates when there are no remaining nodes to be eliminated. To escape from the SequentialUnit main ConditionalUnit simplifyInitial ConditionalUnit simplifyFinal loop, a break rule is required, which speci es an im- if hasMultipleInitialStates if hasMultipleFinalStates aptostshieblseampaettteimrne)(,hseorei,taalnwoadyestehvaatluisatinesittiaolfaanlsde. Anaf-l ssiimmpplliiffyyIFninitaiall createUnifyitnhgeInnitialStateelse createUnifyingFtihneanlState else ter the whole process, there is only the initial and the noop noop nal state left, possibly with various transitions be- Rule hasMultipleFinalStates Rule hasMultipleInitialStates Rule noop tawceoenncitsheemma.nTnoero,batasihnotrhteJanvaalrroeugtui nlaerpeuxtpsretossgieotnheinr :«SptariestFesienravle=»true :«SptariestFesienravle=»true :«SptariestIesneirtviael»=true :«SptariestIesneirtviael»=true their labels according to Listing 4 in [GVP+17]. 2.2
Rule createUnifyingInitialState Rule createUnifyingFinalState «create» «create» «preserve» «create» «create» «preserve» :State states :TransitionGraph :State states :TransitionGraph «:«TsccrorraeileusanaaIrbsntctieeeeittil**io=»a»n"l=eptrsu"e «tcarregaette*t:«Sr«»patcarnirestesIesinatetiirotevin*ae»ls*=»tr«upesr-et>astefearsvlsee*» «:«TcctrraraeilersanagaFbsttieieenettil*a*o=»»ln="e«tprcusree"a«tecsr*oe»uartcete*ra»n:«sSpittariieostFesniesnravle=*t»r«upesr-tea>stfeearslvsee*» initial state. Second, if there are multiple nal states, these states become non- nal states with an outgoing -transition to a newly created nal initial state. Our solution represents these steps via two sub-units simplifyInitial and simplifyFinal, which are applied in sequential order using a sequential main unit.
The simplifyInitial unit uses a rule hasMultipleInitialStates to check if the simpli cation treatment becomes necessary, and, if, this is the case, performs the simpli cation using the rule createUnifyingInitialState. Specifically, rule hasMultipleInitialStates checks whether two separate initial states exist in the input FSA. Rule createUnifyingInitialState again uses the concept of rule-nesting to achieve a for-all semantics. The kernel rule speci es the creation of an additional initial state. The multi-rule matches all earlier initialState, turns them into non-initial states and creates an incoming -transition for each of them.
The treatment of nal states based on unit simplifyFinal is completely dual. 2.3
The solution for extension 2 extends the solution for the main task with small modi cations concerning the treatment of labels and probabilities. Since the original case description did not specify how the labels and probabilities are to be computed (in fact, the probabilities in the computed regular expression are ignored in the correctness evaluation), we followed the speci cation of the reference implementation (https://github.com/sinemgetir/ state-elimination-mt/). Details about the reference implementation's speci cation were obtained in our communication with the case authors.
According to this speci cation, the conversion process includes a preprocessing of the input automaton where the probabilities of the outgoing transitions for each state are recalculated, such that (i) loop and transitions are ignored, (ii) the probabilities of the other transitions are added up to derive \the new 100%", and (iii) each transition obtains its original probability divided by \the new 100%" as its new probability. Fig. 3 shows our transformation for implementing this speci cation: Unit recalculateProbs speci es that its two contained rules are applied in sequential order. Rule recalculateProbsTemps uses rule nesting to iterate over all outgoing nonloop/empty/ transitions of all states, so that their probabilities are stored in variable a. The sum of all values of a is stored in a newly created Trace object, using Henshin's Aggregations helper class to compute the sum. Rule recalculateProbsUpdate performs the same iteration as before to update the probabilities of the involved transitions. Given the old probability b, the new value is b=a, where a is the aggregate percentage stored in the Trace object. In this process, the Trace objects become obsolete and are consequently deleted.
The remaining conversion process is the same except for the label and probabilities handling, where we adhere to the speci cation: \when we concatenate two labels we multiply their probabilities. When we 'or' two labels, we add their probabilities."
For example, in the rule xTransitionsLooped, for the transition beingly newly created, the probability needs to account for the probabilities of the original transitions, and the label needs to represent the probability of the loop transition. To this end, we modi ed this rule as shown in Fig. 3. During the matching process, we now store the labels as well as the probabilities of the matched transition in variables (fa; b; lg and fpa; pb; plg, respectively). In the multi-rule, we then use these variables in the label and probability of each newly created transition. The label includes the probability of the loop transition, the probabilities is made up from the probabilites of the input transitions. In this section, we apply the evaluation criteria from the case description to our solution. The solution was executed on a Windows 10 system (Intel Core i7-5600U, 2.6 GHz; 8 GB of RAM, Java 8, 2 GB Xms). We ran the experiment with a timeout duration of max. 1 hour per model, following the reference solution.
Correctness. When applied to the provided test models, our solution produced correct results in all cases. For the main task and extension 2, we used the provided benchmark framework for verifying our solution. We slightly extended the framework so it supports the execution against user-speci ed timeout durations.
For extension 1, unfortunately, we could not follow the evaluation process described in the case description: The FSA data structure used by the reference implementation does not support input FSAs with more than one initial state, rendering it infeasible as a baseline for the correctnes check. Instead, we performed a light-weight validation by checking if the numbers of states, initial states, nal states, and transitions changed as expected.
Suitability. With our solution, we aimed at providing a primarily declarative solution. We achieved this goal by specifying all parts of the state elimination algorithm (Listing 2 and 3 in [GVP+17]) using Henshin's declarative rule and control ow concepts. In addition, our solution includes two minor imperative parts, written in Java: A driver to trigger the execution of the Henshin interpreter with the speci cation, and a part to convert the output of state elimination to an expression (Listing 4 in [GVP+17]).
Performance. Table 1 shows the performance measurements in comparison to the available data for the reference solution. For the three smallest test models, we observed a slow-down. For all of the remaining models, we observed an increasingly growing speedup, amounting to an order of two magnitudes in the case of the largest input model 4 4. A complexity analysis to substantiate this observation is left to future work.
4
Outlook
(#states)
Reference Henshin
nario for our ongoing work on the variability of model transformations [SRA+16, SS16]. It features variability in two dimensions: variability in the language of the input automata (plain and probabilistic FSAs), and variability in the solution artifacts of the transformations (repeatedly, we handle a looped case di erently from an unlooped case). We intend to use this scenario as a case study for extending our work towards language-level variability. [SS16]