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

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

运行

解决

使用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 将新分支排到最后处理，更适合处理具有少量小满足模型的论题。而 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:

Rusty Razor 是一个用于构建一阶等价理论的有限模型的工具。

模型查找算法受到了数据库系统中的 Chase 算法 的启发。给定一个输入的一阶理论，Rusty Razor 构建一组同态最小模型，这些模型满足理论。

要了解更多关于 Razor 理论基础的信息，请查看我的 博士论文。