Pecan

Pecan is an automated theorem prover for Büchi automata, with additional features for making it easier to deal with expressing numbers in various numeration systems and working with automatic words.

You can try Pecan online! Just go to http://reedoei.com/pecan.

Installation

NOTE: You can also use Docker (see below), if you have it.

You will need Python 3.6 or higher.

Then, install spot; if you are on a Linux-y system (hopefully including MacOS), the install-spot.sh script in the scripts/ directory of this repository should work for you:

bash scripts/install-spot.sh

Otherwise, follow the instructions on the spot website.

You will also need to install the libraries in requirements.txt:

# Use the appropriate line for your pip installation (if pip --version says 3.x, then you should be good; otherwise use/install pip3)
pip install -r requirements.txt
pip3 install -r requirements.txt

If you are interested in using finite automata (or running all the tests), you will also need the submodule PySimpleAutomata, so you must either clone with --recursive or use git submodule update --init --recursive. Then go to the submodule PySimpleAutomata/ and run pip3 install ./.

Then you can run Pecan files (*.pn) by:

python3 pecan.py FILENAME

or start interactive mode via:

python3 pecan.py -i

You can also add the bin/ directory of this repository to your PATH, and the simply use pecan FILENAME or pecan -i. To do so, add the following to your .bashrc (or whatever your operating system uses):

export PATH=/path/to/Pecan/bin:$PATH

Using Docker

If you have Docker, you can run Pecan with:

./pecan-docker OPTIONS

This will automatically build the image if you don't have it already.

Examples

Below has_zeros and all_ones are expressed as LTL formula.

has_zeros(a) := "!(Ga)"
all_ones(a) := "Ga"

Prove that {
    forall x. if has_zeros(x) then !all_ones(x)
}.

Prove that {
    !(exists x. has_zeros(x) & all_ones(x))
}.

Below we prove basic properties of addition (specifically, binary addition), see (here):

Restrict x, y, z are nat.

Theorem ("Zero is the additive identity", {
    forall x. x + 0 = x
}).

Theorem ("Addition is commutative", {
    forall x,y. x + y = y + x
}).

Theorem ("Addition is associative", {
    forall x,y,z. x + (y + z) = (x + y) + z
}).

Running it gives:

$ python3 pecan.py examples/arith_props.pn
[INFO] Checking if Zero is the additive identity is true.
Zero is the additive identity is true.
[INFO] Checking if Addition is commutative is true.
Addition is commutative is true.
[INFO] Checking if Addition is associative is true.
Addition is associative is true.

Configuration

The PECAN_PATH environment variable controls which paths are searched for files when importing/loading automata. It should be a colon-separated or semicolon-separated list of paths, depending on your operating system (Linux/MacOs uses :, Windows uses ;).

Editor Setup