A tool demo for testing distributed system changes based on Mocket. The repository contains two parts:
- A java project ImplDiffIdentifier: identifying changes in two Java projects.
- Python files: imocket.py: the main process of iMocket; tla_parser.py: constructing TLA+ specification into ASTs; extract_changes.py: extracting changes from TLA+ specifications; identify_affected_regions.py: identifying affected nodes and edges in the changed graph; path_generator.py: growth-based graph traversal
JDK 8 Maven 3 Python 3 Python NetworkX package
Using iMocket involves three steps:
- Using ImplDiffIdentifier to identify changes in two distributed system implementations.
- Using imocket.py to get paths as incremental test cases.
- Using Mocket to test these incremental test cases.
In the directory of ImplDiffIdentifier, we use Maven to build the project.
mvn clean package
A jar file "impldiffidentifier.jar" is generated in "target/".
Use the following command to get changes between two Java projects:
java -jar impldiffidentifier.jar <path/to/project1> <path/to/project2> <path/to/output_file>
Use the following command to get incremental test cases:
py imocket.py original_spec.tla modified_spec.tla original_graph.json modified_graph.json action_changes.txt allowed_actions.txt forbidden_actions.txt output_paths.json
Refer to Mocket.