Debugging and Fixing Inconsistencies in Clafer Models

Problem: The existing Clafer translator makes Clafer models analyzable by the Alloy Analyzer. The analyzer checks model consistency (i.e. whether it is correct). If it is consistent, then shows an example. Otherwise, it points to constraints that cause inconsistency. The purpose of this project is to implement a human-readable way of presenting Clafer model inconsistencies to the user. Furthermore, the software should also suggest fixing actions that repair those broken models.

Goals of the project:

• Think how to present inconsistencies to the user.
• Create an Eclipse plugin that presents the inconsistencies (e.g., highlights them in a textual Clafer model).
• Implement a way of resolving inconsistencies (there are already algorithms that do that).
• The project will require some interfacing with the Alloy Analyzer to extract contradicting constraints.
• Possibly create API that would allow to detect and remove inconsistencies in Clafer models.
• Usability is an important aspect of this project.