We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.

翻译：我们提出TACO，一个用于开发与自动验证容错及基于阈值的分布式算法的工具集。该工具集实现了三种针对阈值自动机模型检测的方法，分别对应文献中已知的不同可判定片段，并包含两种超越这些可判定片段的半决策过程。此外，TACO是一个模块化、可扩展且文档完善的框架，支持开发针对阈值自动机的算法与工具。本文介绍了其重要特性，概述了所实现的算法，并通过实验评估了其性能。