Skip to content
An automated theorem prover that uses Büchi automata.
Python Other
  1. Python 99.3%
  2. Other 0.7%
Branch: master
Clone or download
ReedOei Fix Ostrowski file, add new optimizations (#32)
* Fix a parsing issue in the ostrowski example

* Everything seems to be working?

* Add missing files

* Remove unused automata

* Kind of fixed everything, allow multiple variables in qutanifier

* Added missing test file

* Add updated version of ostrowski file

* Remove completed TODO

* Add emptiness checking optimization

* Clean up ostrowski file

* Renable some simplication
Latest commit 813f57a Feb 24, 2020

Files

Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
examples Fix Ostrowski file, add new optimizations (#32) Feb 24, 2020
library Fix Ostrowski file, add new optimizations (#32) Feb 24, 2020
pecan Fix Ostrowski file, add new optimizations (#32) Feb 24, 2020
scripts Substitution overhaul (#31) Feb 17, 2020
test Fix Ostrowski file, add new optimizations (#32) Feb 24, 2020
.gitignore Update gitingore Feb 3, 2020
.travis.yml Substitution overhaul (#31) Feb 17, 2020
Dockerfile Add dockerfile Feb 3, 2020
LICENSE Create LICENSE Feb 3, 2020
README.md Fix minor errors in scripts, reorganization Feb 9, 2020
TODO Fix Ostrowski file, add new optimizations (#32) Feb 24, 2020
pecan-docker Substitution overhaul (#31) Feb 17, 2020
pecan-manual.pdf Added manual Jan 23, 2020
pecan.py Substitution overhaul (#31) Feb 17, 2020
pecan.vim Fix bugs/grammar, adding code emitting Jan 19, 2020
requirements.txt Fix Ostrowski file, add new optimizations (#32) Feb 24, 2020
setup.py Improve installation process/scripts (#6) Nov 13, 2019

README.md

Pecan

Build Status

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, the install-spot.sh script may work for you:

bash 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

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

python3 pecan.py FILENAME

or start interactive mode via:

python3 pecan.py -i

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"

prop_true() := forall x. has_zeros(x) => (not all_ones(x))
#assert_prop(true, prop_true)

prop_false() := exists x. has_zeros(x) & all_ones(x)
#assert_prop(false, prop_false)

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

Restrict x, y, z are nat.

add_zero_id() := forall x. x + 0 = x
add_comm() := forall x. forall y. x + y = y + x
add_assoc() := forall x. forall y. forall z. x + (y + z) = (x + y) + z

#assert_prop(true, add_zero_id)
#assert_prop(true, add_comm)
#assert_prop(true, add_assoc)

Running it gives:

$ python3 pecan.py examples/arith_props.pn
[INFO] Checking if add_zero_id is true.
add_zero_id is true.
[INFO] Checking if add_comm is true.
add_comm is true.
[INFO] Checking if add_assoc is true.
add_assoc 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

Currently, the only "supported" editor is Vim, via a syntax file (pecan.vim) in this repository.

You can’t perform that action at this time.