gr1c: a tool for interactive and incremental reactive synthesis

gr1c is an open source tool suite for GR(1) synthesis and related activities. Development is motivated by current research in formal methods for robotics, including motion planning with temporal logic specifications. It has several novel features beyond a fast implementation of basic GR(1) synthesis. Users can interact with binary decision diagrams (BDDs) and make live queries to intermediate values of a μ-calculus fixed-point computation, which in turn provide the basis for strategy automaton construction. Another novel feature is the ability to load an existing strategy and modify parts of it following changes to the original specification. Besides visual formats intended for human review, gr1c can produce output in standard formats, including JSON, that enable integration with other tools. To support verifying results, output can be in Promela, which allows model checking by Spin.