rusty-razor

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

查看剃刀的 文档 以获取更多关于项目和入门示例的信息。

构建

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）不同，剃刀不需要用户提供它构造的模型大小的限制。然而，当在具有非有限模型的定理上运行时，剃刀可能永远不会终止——可以证明，剃刀在不可满足的定理（即没有模型的定理）上的运行将保证终止（尽管可能需要非常长的时间）。这是第一阶逻辑半可决性的直接结果。

要保证终止，请使用 --bound 选项和 domain 参数的值来限制结果的模型大小

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

模型查找调度器

使用--scheduler选项来选择Razor如何处理搜索分支。默认的调度器是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输入的语法，并包含更多示例。