A java tool for trimming/improving the looks of Mealy machine .dot models using Graphviz and automatalib libraries. It assumes the model is a Mealy machine, wherein each .dot edge corresponding to a transition contains a label describing it in the form "input / output".
To install, simply run:
bash prepare.sh
mvn install
The main use cases of dot-trimmer are:
- removing inputs
- merging transitions with the same outputs and lead to the same state under a custom input label
- removing states not on path to some end-goal output which is identified by a regex expression
- coloring edges in the resulting .dot file
- replacing inputs/outputs by applying string replacement transformations
dot-trimmer allows you to remove inputs from a given .dot file. After removal, dot-trimmer will minimize the model before exporting it to .dot.
java -jar dot-trimmer.jar --input aut.dot --removeInputs "INP1,INP2,INP3"
dot-trimmer can merge transitions which have the same output and lead to the same state, replacing them by a single transition with a custom input and the common output. By default, dot-trimmer uses Other as the custom input, but the user can choose a different string. To enable merging transitions, the user needs the supply thresh, which is the minium number of transitions with same output for which merging can be performed. Example:
java -jar dot-trimmer.jar --input aut.dot --thresh 3 --label "DifferentOther"
dot-trimmer can remove states for which there does not exist a path to a transition carrying an output corresponding to a regex. This functionality can be useful in analyzing models of protocol implementations, which may contain many states, but few states from which a handshake can be completed. The latter likely are more interesting. If a state of handshake completion can be identified by some output (we term, an end-goal output) which does not occur in other states, the user can use this output to retain only interesting states (states en-route to a handshake). For TLS, an end-goal output may be "Application", the command becoming:
java -jar dot-trimmer.jar --input tls-model.dot -ego "Application"
dot-trimmer has basic support for coloring transitions of a .dot model:
- color all transitions on way from the initial state to a given state (there is primitive support for this currently)
- color all transitions traversed by executing supplied sequences of inputs
This function requires a .json describing the coloring, see the example directory.
dot-trimmer allows a user to apply replacement rules over the inputs/outputs. These rules comprise 4 components:
- a matching string, an input/output should match this string in order for the rule to be triggered
- replacee string, a regex to be replaced
- replacement string, a regex describing the replacement
- final, determines whether this is the last rule to be processed.
Rules are processed in the order they appear in the replacements .json file, and are applied sequentially on the input/output, in a pipeline fashion. In case a rule is final or the end of the .json file is reached, the resulting input/output is returned, and is written in the place of the old input/output. The rules are described in .json, see the example directory.
Things I hope to add in the future are coloring, which could be done in two ways:
- better algorithm for state-based coloring, ability to choose two states between which all transitions are colored
- being able to configure which trimming/coloring options to apply
- a more generic framework for applying transformations. These might be performing string replacements, merging transitions, coloring states ...
But we shall see if I find the time to do this.