Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present sweap, a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. sweap implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. sweap supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the ISSY tool, and our own bespoke input. We present a mature version of sweap with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that sweap outperforms its only competitor in this domain.

翻译：近年来，从涉及无限状态空间的规范进行反应式综合的研究兴趣显著增长。本文介绍了sweap——一个用于综合无限状态线性整数算术反应式系统的工具。sweap采用CEGAR方法，将最先进的有限状态综合工具作为黑盒，以解决抽象综合问题。sweap支持无限状态反应式综合问题的主流输入形式：时态流逻辑模理论、反应式程序博弈、ISSY工具的专用输入，以及我们自己的专用输入。我们呈现了sweap的成熟版本，具备多项新功能：提升不可实现性证明能力的双重抽象方法、支持非确定性和无界更新、更通用的变量初始化，以及用于优化的等价可实现约简。实验评估表明，sweap在该领域超越了其唯一竞争对手。