Rusty Razor is a tool for constructing finite models for first-order theories. The model-finding algorithm is inspired by the chase for database systems. Given a first-order theory, Razor constructs a set of homomorphically minimal models for the theory.
Check out Razor's documentation for more information about the project and introductory examples.
rusty-razor is written in Rust, so you will need Rust 1.48.0 or newer to compile it. To build rusty-razor:
git clone https://github.com/salmans/rusty-razor.git
cd rusty-razor
cargo build --release
This puts rusty-razor's executable in /target/release
.
Use the solve
command to find models for a theory written in an <input>
file:
razor solve -i <input>
The --count
parameter limits the number of models to construct:
razor solve -i <input> --count <number>
Unlike conventional model-finders such as Alloy, Razor doesn't require the user to provide a bound on the size of the models that it constructs. However, Razor may never terminate when running on theories with non-finite models -- it can be shown that a run of Razor on an unsatisfiable theory (i.e., a theory with no models) is guaranteed to terminate (although it might take a very very long time).This is a direct consequence of semi-decidability of first-order logic.
To guarantee termination, limit the size of the resulting models by the number of their elements using the --bound
option with a value for the domain
parameter:
razor solve -i <input> --bound domain=<number>
Use the --scheduler
option to choose how Razor processes search branches. The fifo
scheduler (the default scheduler)
schedules new branches last and is a more suitable option for processing theories with few small satisfying models.
The lifo
scheduler schedules new branches first, and is more suitable for processing theories with many large models.
razor solve -i <input> --scheduler <fifo/lifo>
Consider the following example:
// 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
You can download the example file here and run the razor
command-line tool on it:
razor solve -i theories/examples/toy.raz
Razor returns only one model with e#0
and e#1
as elements that denote 'duchess
and
'ducky
respectively. The facts Cat(e#0)
, Squishy(e#1)
, and Toy(e#1)
in the model
are directly forced by the last two formula in the input theory. The fact Loves(e#0, e#1)
is deduced by 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's documentation describes the syntax of Razor's input and contains more examples.