转换与理论分析机

安装

• 安装 Rust
• 安装 z3

sudo apt install z3

• 安装 Tatam

cargo install tatam

安装 Vscode 扩展 tatam-lang (可选)

cd ~/.vscode/extensions
git clone https://github.com/DavidD12/tatam-lang.git

示例

cst x: Int
var y: Int

init inits {
    y = 0
}

inv invariants {
    x > y
}

trans tr_inc {
    y < 10 and y' = y + 1
}

trans tr_loop {
    y >= 10 and y' = 0
}

prop = G(F (y = 1))

search infinite solve

执行

tatam -f file.tat

文档

部分文档可在此处找到 here