SUSHI-experiments

About

This repository contains the source code for various SUSHI experiment subjects: data structures (AVL tree, doubly linked list, node caching linked list, and treemap), GanttProject, and TSAFE.

Checking out the project

This repository contains an Eclipse project that is configured to work together with the Eclipse projects for SUSHI. Import in an empty Eclipse workspace the projects in the SUSHI repository, by following the instructions in the README file in it. Then, import this repository in the same workspace: On the Eclipse main menu select File > Import..., in the dialog that pops up select Projects from Git, insert the URI of this repository, and when asked for a wizard for importing projects answer Import Existing Eclipse Projects.

Fixing the paths

Before launching the experiments you must set a few configuration variables to reflect the paths where you installed the code. Under the sushi-src source folder you find the class common.Settings. Open it and edit the definitions of the GIT_REPO_ROOT, and Z3_PATH variables to reflect the paths on your system where the Git repositories and the binary of the Z3 SMT solver are installed.

Launching the experiments

The project contains a set of Eclipse launch configurations that can be used to launch the experiments:

• Sushi_AvlTree_accurate.launch for the AvlTree experiment with accurate invariants;
• Sushi_AvlTree_partial.launch for the AvlTree experiment with partial invariants;
• Sushi_DllHard.launch for the doubly linked list example;
• Sushi_GanttProject_<accurate|partial>.launch for the GanttProject experiment with accurate/partial invariants;
• Sushi_NodeCachingLinkedList_<accurate|partial>.launch for the NodeCachingLinkedList experiment with accurate/partial invariants;
• Sushi_TreeMap_<accurate|partial>.launch for the TreeMap experiment with accurate/partial invariants;
• Sushi_Tsafe_<accurate|partial>.launch for the TSAFE experiment with accurate/partial invariants.

You will also find an Eclipse launch configuration Sushi_help.launch, that launches SUSHI without parameters so it prints a help screen on the console.

Gathering the results

All the temporary files generated by SUSHI will reside in a subdirectory of the sushi-out/ folder that will have as name the date and time when SUSHI was launched. The generated tests will be put in the sushi-test/ source folder (note that multiple runs of SUSHI might overwrite the tests generated by previous runs).