aaltitoad下载aaltitoad源代码下载

aaltitoad

其他源码

v1.2.0

下载

aal borg ti ck ck ck a unotomata vali d ator-可扩展的验证引擎和tick tock automata的模拟器。

什么是tick tock自动机？

TTA的（TICK TOCK Automata）是一种基于自动机理论，可以为各种自动化系统建模并行业务逻辑。 TTA由它们之间的一组位置和过渡组成。每个过渡都可以通过布尔表达来保护，并具有一组变量分配，作为进行过渡的“结果”。

与TTA的一个很好的类比是一种明确的，系统可以从一个状态过渡到另一种状态。下面是一个简单的TTA的示例，该示例基于按钮输入控制光线。

从关闭位置开始，只有一个外向的边缘可以检查btn_is_pressed是否为真。如果是这样，我们将转移到ON位置，并将可变light设置为真实，这是由于进行边缘/过渡。然后，当释放按钮时，我们返回到Off Locaiton，并将light再次设置为False 。

使TTA与任何其他过渡系统不同的是， btn_is_pressed变量是外部变量，这意味着它不能通过过渡系统将其分配给任何值，它只能基于外部输入来更改。当我们不进行过渡时，读取外部输入。语义的这种划分是tick tick tock automata的名称来源：

tick步：评估警卫，应用更新，更改位置
TOCK步骤：阅读外部输入，写外部输出

将语法更进一步，您可以并行运行许多这些TTA，共享同一内部和外部变量池。这样的网络被称为t ock a utomata（ntta）的n ntwork。

进一步阅读

本文介绍了基本刻度TOCK自动机理论
本文详细描述了工具的最新迭代（v1.0.0+）
本文介绍了工具的第一次迭代（v0.10.x）
如果您想自己创建一些TTA，请看一下H-uppaal

编译（Linux）

AALTITOAD是使用CMAKE构建的。您必须具有C ++ 20兼容的编译器， flex ， bison +版本和已安装的标准模板库。所有其他依赖关系都是通过出色的CPM软件包管理器来处理的。

mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make

如果CPM步骤需要很长时间，请尝试使用-DCPM_SOURCE_CACHE=~/.cache/CPM重新设计

测试

要运行单元测试，请编译aaltitoad_tests目标

mkdir build-test && cd build-test
cmake -DCMAKE_BUILD_TYPE=Debug ..
make aaltitoad_tests
# run the tests
./aaltitoad_test -r xml -d yes --order lex

如果要包含代码覆盖统计数据，请提供-DCODE_COVERAGE=ON Cmake标志。

如何使用

AALTITOAD提供了三个主要的汇编目标。所有命令行界面都有一个帮助页面，您可以使用--help参数召唤。

verifier ：验证引擎命令行接口
- 如果您想分析NTTA，请使用此此事
simulator ：运行时命令行接口
- 如果您想执行NTTA并与自定义托克斯链接（请参阅下文），请使用此此事（请参见下文）
aaltitoad ：带有所有内容的图书馆Aaltitoad
- 使用它来创建自己的基于NTTA的应用程序，例如另一个验证程序，运行时甚至编译器

Tocker插件

AALTITOAD支持第三方“ Tocker”库，因此您可以将自定义集成直接注入运行时。该存储库在tocker_plugins目录中提供了一个名为pipe_tocker的示例，以作为示例项目。 “托克”必须定义以下符号：

# include < plugin_system.h > // aaltitoad::* typedefs

extern " C " {
    const char * get_plugin_name (); // Return value of this func dictates the name the next two funcs
    aaltitoad:: tocker_t * create_TOCKER_NAME ( const std::string& argument, const aaltitoad:: ntta_t & ntta);
    void destroy_TOCKER_NAME ( tocker_t * tocker);
    plugin_type get_plugin_type () {
        return plugin_type::tocker;
    }
}

TOCKER_NAME是指get_plugin_name函数提供的C弦。函数名称必须匹配，否则插件将不加载。 Tocker插件必须与aaltitoad共享库链接，并且应作为共享库汇编，例如：

 add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad)

编译后，您可以通过将--tocker / -t与--tocker-dir / -T一起在AALTITOAD命令行中实例化tocker。应该像这样提供--tocker选项：

--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) "

选项的"argument string" - 指的是提供给create_TOCKER_NAME函数的输入参数字符串。现在，您的Tockers应该已经实例化，每次TTA准备计算TTA时， tock都会被调用。

托克类型

第三方Tocker可以扩展两种类型的Tocker接口：

阻止Tockers（默认tocker_t ）
异步Tockers（ async_tocker_t ）

阻止Tocker将以一个线程运行，并将阻止所有tick执行，直到TOCK完成为止，第三方集成只能覆盖tock功能。相比之下，异步托克不会阻止tick执行，而是启动get_tock_values函数的新异步任务。

在实施托克时，应考虑是否要阻止TTA执行。如果您选择实现异步托克，请注意，自发行TOCK以来，输入环境可能已经改变。

解析器插件

如果您不想使用随附的解析器，则可以随时提供自己的服务。只要您提供以下符号（请记住extern "C" ）：

# include < plugin_system.h > // aaltitoad::* typedefs 

extern " C " {
    const char * get_plugin_name ();
    const char * get_plugin_version ();
    aaltitoad:: ntta_t * load ( const std::vector<std::string>& folders, const std::vector<std::string>& ignore_list);
    plugin_type get_plugin_type () {
        return plugin_type::parser;
    }
}