AlloyASG: Alloy Predicate Code Representation as a Compact Structurally Balanced Graph

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties to automated testing and debugging of system implementations. Unfortunately, the model itself needs to be correct to gain these benefits. Alloy is a commonly used modeling language that has several existing efforts to repair faulty models automatically. Currently, these efforts are search-based methods that use an Abstract Syntax Tree (AST) representation of the model and do not scale, as ASTs suffer from exponential growth in their data size due to duplicate nodes. To address this issue, we introduce a novel code representation schema, Complex Structurally Balanced Abstract Semantic Graph (CSBASG), which represents code as a complex-weighted directed graph that lists a semantic element as a node in the graph and ensures its structural balance for almost finitely enumerable code segments. We evaluate the efficiency of our CSBASG representation for Alloy models in terms of it's compactness compared to ASTs, and we explore if a CSBASG can ease the process of comparing two Alloy predicates. Lastly, we identify several future applications of CSBASG, including Alloy code generation and automated repair.