Documentation
GROOVE is a general purpose graph transformation tool set that uses simple labelled graphs and single push-out (SPO) transformation rules. The core functionality of GROOVE is to recursively apply all rules from a predefined set (the graph production system — GPS) to a given start graph, and to all graphs generated by such applications. This results in a state space consisting of the generated graphs.
The GROOVE tool set has three components:
- Simulator. A graphical interface tool that allows graphical editing of rules and graphs, and integrates the functionality of the Generator and Model Checker (see below). In addition, the Simulator allows the user to interactive explore the LTS, by manually applying rules to a host graph.
- Generator. A command line tool that generates the state space of a GPS. The state space is stored as a Labelled Transition System (LTS), where each state is a graph and transitions are labelled by the rule applications. The
strategy according to which the state space is explored (e.g., depth-first, breadth-first, etc) can be set as a parameter. - Model Checker. A command line tool that checks if properties expressed in CTL temporal logic hold in a state space model produced by the Generator.
The entire tool set is written in Java and therefore it can be executed in any platform with a Java 17 virtual machine. (Prior to Groove version 6.0.0, you have to use Java 8.)
Each component is provided in separate JAR file (see Download GROOVE).
In most systems, it is sufficient to just double-click the proper .jar file to execute one of the components.
Another option is to use a command line in a shell, such as: java -jar Simulator.jar, for example, to run the Simulator. This assumes that the Java VM is properly accessible from the system PATH.
Please refer to the user manual or the quick reference poster for additional information on how to use the tool or take a look on our demo videos.
