rusty-razor

Rusty Razor 是一个用于构建一阶理论有限模型的工具。模型查找算法受到数据库系统中的 Chase算法 的启发。给定一个一阶理论，Razor 构建了一组该理论的 同态最小 模型。

查看Razor的 文档 了解更多关于项目和入门示例的信息。

构建

Rusty Razor是用Rust编写的，因此您需要Rust 1.48.0或更新的版本来编译它。要构建Rusty Razor

git clone https://github.com/salmans/rusty-razor.git
cd rusty-razor
cargo build --release

这将把Rusty Razor的可执行文件放在 /target/release。

运行

solve

使用 solve 命令来查找在 <input> 文件中编写的理论模型

razor solve -i <input>

--count 参数限制了要构建的模型数量

razor solve -i <input> --count <number>

有界模型查找

与像 Alloy 这样的传统模型查找器不同，Razor 不要求用户提供它构建的模型大小的界限。然而，当在具有非有限模型的论理上运行时，Razor 可能永远不会终止 - 已证明在不可满足的论理（即没有模型的论理）上运行Razor是保证终止的（尽管可能需要非常非常长的时间）。这是由于一阶逻辑的半可决性。

要保证终止，请使用 --bound 选项和一个用于 domain 参数的值，通过元素数量限制结果的模型大小

razor solve -i <input> --bound domain=<number>

模型查找调度器

使用 --scheduler 选项来选择Razor如何处理搜索分支。默认调度程序（fifo 调度程序）将新分支排到最后，对于处理具有少量小满意模型的论理来说是更好的选择。默认调度程序（fifo 调度程序）将新分支排到最后，对于处理具有大量大模型的论理来说是更好的选择。而 lifo 调度程序将新分支排到前面，对于处理具有大量大模型的论理来说是更好的选择。

razor solve -i <input> --scheduler <fifo/lifo>

玩具示例

考虑以下示例

// All cats love all toys:
forall c, t . (Cat(c) and Toy(t) implies Loves(c, t));

// All squishies are toys:
forall s . (Squishy(s) implies Toy(s));

Cat('duchess);   // Duchess is a cat
Squishy('ducky); // Ducky is a squishy

您可以在此处下载示例文件 [链接] 并使用 razor 命令行工具对其运行

razor solve -i theories/examples/toy.raz

Razor 返回一个包含 e#0 和 e#1 的模型，分别表示 'duchess 和 'ducky。模型中的事实 Cat(e#0)、Squishy(e#1) 和 Toy(e#1) 是由输入理论中的最后两个公式直接强制的。事实 Loves(e#0, e#1) 由 Razor 推导出

Domain: e#0, e#1

Elements: 'duchess -> e#0, 'ducky -> e#1

Facts: Cat(e#0), Loves(e#0, e#1), Squishy(e#1), Toy(e#1)

Razor 的文档描述了 Razor 输入的 语法 并包含更多 示例。

lib.rs:

提供了一套工具，用于解析和应用于 Razor 语法中一阶公式上的常见逻辑变换。