gr1c is a collection of tools for GR(1) synthesis and related activities. Its core functionality is checking realizability of and synthesizing strategies for GR(1) specifications, though it does much more.
The citable URL is https://scottman.net/2012/gr1c
The public Git repo can be cloned from https://github.com/tulip-control/gr1c.git Documentation for the latest release is at https://tulip-control.github.io/gr1c Bug reports, feature requests, and substantial comments can be submitted via the project issue tracker or via email to the authors.
Executable files for several operating systems (GNU/Linux, Windows, etc.) are available for download in recent releases on GitHub. If you do not find yours there, please ask about it.
Many examples are provided. Begin by reading examples/README.md
.
The main documentation is built from .md
files under the doc
directory and
API comments in the source code. It is possible to read these files directly,
i.e., without building and browsing HTML files.
make doc
will run Doxygen and place the result in doc/build
.
Formulae are rendered using MathJax.
We use GitHub Actions to build and test gr1c from the current source code in the
repository. Current status:
- CUDD, the CU Decision Diagram package by Fabio Somenzi et al. (also read the introduction, and note that the original link for CUDD is http://vlsi.colorado.edu/~fabio/CUDD/)
The following are optional dependencies. Each item is followed by a summary of what is to be gained by building gr1c with it.
-
GNU Readline, for an enhanced command prompt during interactive sessions. Note that there is a built-in prompt.
-
GraphViz, for strategy visualization from the output format type
dot
.
Detailed installation instructions are in the repository at doc/installation.md For the most recent release, a copy of these instructions is on the Web at https://tulip-control.github.io/gr1c/md_installation.html
For Linux and Mac OSX, try the following.
./get-deps.sh
./build-deps.sh
make
make check
Consider using make -j N
where N is the number of jobs to run simultaneously.
The last command runs a test suite. Each testing step is reported if the
environment variable VERBOSE is set to 1. E.g., try VERBOSE=1 make check
.
Finally,
make install
The default installation prefix is /usr/local. Adjust it by invoking make
with something like prefix=/your/new/path
.
This is free software released under the terms of the BSD 3-Clause License. There is no warranty; not even for merchantability or fitness for a particular purpose. Consult LICENSE.txt for copying conditions.
If this software is useful to you, we kindly ask that you cite us:
S. C. Livingston, "gr1c: a tool for interactive and incremental reactive synthesis". Caltech Library, Jan. 21, 2024. doi: 10.7907/5m62h-a4204