gLTSdiff is a library for comparing the structures of two or more Generalized Labeled Transition Systems (GLTSs), and merging them into a single combined GLTS. gLTSdiff can be used and customized to compare and merge various types of directed graphs, labeled transition systems (LTSs), state machines, automata, and so on.
Out of the box, GLTs, LTSs, automata and difference automata can be compared. Their comparison can be configured to use different comparison algorithms that allow for a trade-off between performance and the number of differences in the result. The result may be post-processed to get rid of undesired patterns in the comparison result. Furthermore, gLTSdiff is designed with extensibility in mind. You may add your own representations, and customize the comparison, merging, output, and so on.
gLTSdiff is a generalization of the LTSdiff algorithm proposed by Neil Walkinshaw and Kirill Bogdanov, and implemented in the StateChum library. gLTSdiff is however more than only a generalization. It also offers significant performance improvements over LTSdiff, and adds additional features like post-processing to improve comparison results.
gLTSdiff was first introduced, and formally defined, in the following article:
- Dennis Hendriks and Wytse Oortwijn, "gLTSdiff: A Generalized Framework for Structural Comparison of Software Behavior", 26th International Conference on Model Driven Engineering Languages and Systems (MODELS), pages 285-295, 2023, doi:10.1109/MODELS58315.2023.00025.
You can read more about it in subsequent publications:
- Dennis Hendriks and Wytse Oortwijn, "gLTSdiff: a generalized framework for structural comparison of software behavior", Software and Systems Modeling (SoSyM), 2024, doi:10.1007/s10270-024-01239-0.
- Dennis Hendriks, "Model Inference and Comparison for Software Evolution in Large Component-Based Systems", PhD thesis, 2024, doi:10.54195/9789493296640.
gLTSdiff is also used in the Model Inference and Differencing Suite (MIDS).
To get a feel of what is possible with gLTSdiff, here are a few simple examples.
Two difference automata (in red and green) may be compared and combined. Their common parts are shown in black, while their differences remain in red and green:
| Input 1 | Input 2 | Result |
Any number of version-annotated automata could be combined as follows:
| Input 1 | Input 2 | Input 3 | Result |
Examples:
- Comparing two difference automata
- Post-processing difference automata
- Merging three version-annotated automata
Using and extending gLTSdiff:
Copyright (c) 2021-2023 Contributors to the GitHub community
This program and the accompanying materials are made available under the terms of the MIT License.
SPDX-License-Identifier: MIT