Transition And Theory Analysis Machine

Install

• Install Rust
• Install z3

sudo apt install z3

• Install Tatam

cargo install tatam

Install Vscode extension tatam-lang (Optional)

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

Example

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

Execute

tatam -f file.tat

Documentation

Some documentation can be found here