A Pattern-based declarative model debugger
For assessing the idea of debugging with discriminating examples, we have developed Margaux. Given an Alloy model, Margaux generates discriminating examples by mu- tating the simulacrum of the model using predefined patterns. By reviewing focused discriminating-examples, the user explores different corners of the model and finds out whether the model suffers from under or over-constraint issues.
