Groove
Groove is a short for GRaphs for Object-Oriented VErification. Groove is a project centered around the use of simple graphs for modelling the design-time, compile-time, and run-time structure of object-oriented systems, and graph transformations as a basis for model transformation and operational semantics. This entails a formal foundation for model transformation and dynamic semantics, and the ability to verify model transformation and dynamic semantics through an (automatic) analysis of the resulting graph transformation systems, for instance using model checking.

The Groove tool set includes an editor for creating graph production rules, a simulator for visually computing the graph transformations induced by a set of graph production rules, a generator for automatically exploring state spaces, a model checker that supports CTL and LTL formulas and an imaging tool for converting graphs to images.

A list of features:
Here is a brief list of the features supported by Groove. For details please consult the included user manual or quick reference poster, or the demos on the web site.
  • Visual editing and simulation of graphs and graph transformation rules
  • Global rule priorities or control program
  • State space exploration using customised exploration strategies
  • Model checking generated transition systems over CTL and LTL formulae
  • Regular expression matching and label wildcards in transformation rules
  • Primitive data types (int, string, bool and real) with corresponding operations
  • Nested (i.e., quantified) rules
  • Typing and inheritance through node types
  • Prolog querying of graphs and state space

System requirements
  • Minimum Java version 1.6ga5

Groove on an eComStation machine with Open JDK


Installing Groove
Download groove-4_8_7-bin.zip. Create a directory (folder) "Groove". Open the zip file and go in the subdirectory (folder) "groove-4_8_7". Copy all files and subdirectories to the new created directory (folder) "Groove". Next version (groove-4_9_0) needs Java 1.7 and latest version (groove-5_5_6) needs Java 1.8.
You also need to download the example grammars groove-4_8_7-samples.zip. Open the zip file and go in the subdirectory (folder) "groove-4_8_7". Copy the subdirectory (folder) "samples" to to the new created directory (folder) "Groove". That's it! More examples can be found by checking out the svn repository, but here you'll have to search the right version by date rather than release nr. I have added the "ferryman.gps" to the file "groove-ecs.zip", because the ferryman problem is used in the "Introduction to Groove" and is not supplied with the samples files. To install this problem go into the zipfile en go into the subdirectory "samples". Copy the subdirectory (folder) "ferryman.gps" to the subdirectory (folder) "Groove\samples".

The simulator.cmd file
Groove works with Open JDK in OS/2-eCS. It is a tool with a few programs, please read the enclosed manual. There are also some demo's and the "Introduction to Groove" uses the simulator. Therefore I have made a simulator.cmd file with the following contents;
@echo off
set path=[drive: java]\JAVA160ga5\bin
set BEGINLIBPATH=[drive: java]\JAVA160ga5\bin
set CLASSPATH=
[drive: groove]
cd [drive: groove]\Groove
java -Duser.home=[drive: groove]\Groove -jar .\bin\Simulator.jar 2>groove-bugs.txt
I use 2 separate folders (directories), one for Java and one for Groove with the files created by this program. The references used in the cmd file;

  • [drive: java] = drive with Java
  • [drive: groove] = drive with Groove

should be replaced with real drive letters. Edit and save the file "simulator.cmd" from the distribution. This file is copied to the "Groove" directory (folder). Furthermore, different paths?, adjust according to your needs.
Create a new program object. Specify the path and file name: "[drive: groove]\Groove\simulator.cmd". In the tabpage Session check the boxes "OS/2 window", "Running as an icon" and "Close Window to end program". In the tabpage General you can enter the name "Groove". You find enclosed in the file a suitable OS/2 icon.

Parameters / options explained
  • The specification "-Duser.home=[drive: groove]\Groove" ensures that Groove will save all necessary files in own directory instead of saving them in the home directory.
  • The addition "2>groove-bugs.txt" ensures that errors are saved in the file "groove-bugs.txt". The 2 in "2>" is not a typo!

Download
In the file you can find the above command file (all driveletters are set to C:) and OS/2 Groove icons. Included is also the example used in the demo "Introduction to Groove". There are more programs, if needed you can use the commandfile and make some modifications: groove-ecs.zip.

revision September 11, 2016