Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built to automated testing and debugging of their implementations after they are built. 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. One issue is that ASTs themselves suffer from exponential growth in their data size due to the limitation that ASTs will often have identical nodes separately listed in the tree. 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. Moreover, with this representation in place, we identify several future applications of CSBASG, including Alloy code generation and automated repair.

翻译：编写声明式模型具有诸多优势，从在构建系统前对设计级属性进行自动推理和修正，到构建后对其实现进行自动测试和调试。然而，模型本身必须正确才能获得这些优势。Alloy是一种常用的建模语言，目前已有多种自动修复故障模型的研究。这些研究采用基于搜索的方法，使用模型的抽象语法树表示，但其扩展性不佳。问题之一在于，抽象语法树会因树中重复节点被单独列出而导致数据规模呈指数增长。为解决这一问题，我们提出了一种新型代码表示模式——复杂结构化平衡抽象语义图，该模式将代码表示为带有复杂权重的有向图，将语义元素作为图中的节点，并对几乎有限可枚举的代码片段确保其结构平衡。我们基于相比抽象语法树的紧凑性评估了CSBASG表示对Alloy模型的效率，并探究了CSBASG能否简化两个Alloy谓词的比较过程。此外，基于该表示，我们确定了CSBASG的若干未来应用，包括Alloy代码生成和自动修复。