gr1c 0.13.1
Loading...
Searching...
No Matches
Introduction

The citable URL is https://scottman.net/2012/gr1c. The public Git repo can be cloned from

https://github.com/tulip-control/gr1c.git

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. Relevant papers can be found in the bibliography.

Releases are posted at https://github.com/tulip-control/gr1c/releases. Pre-built binaries for several platforms are available, though the preferred distribution form is as a source bundle. Read the installation page for instructions about installing gr1c from source code. Beware the code is still experimental. If you find a possible bug or have comments, recommendations, or feature requests, then please open an issue on GitHub or contact Scott C. Livingston at slivi.nosp@m.ngst.nosp@m.on@cd.nosp@m.s.ca.nosp@m.ltech.nosp@m..edu

In the documentation below, we assume that gr1c is on the shell path. To get a summary of possible command-line arguments,

gr1c -h

Examples

Many specification files are provided under the examples directory. Begin by reading examples/README.txt. Then read the file formats and specification input pages. As a simple first step, consider the following specification, which is examples/trivial.spc after removing comments.

ENV: x;
SYS: y;

ENVINIT: !x;
ENVTRANS: [](x <-> !x');
ENVGOAL: []<>x;

SYSINIT: y;
SYSTRANS:;
SYSGOAL: []<>(y&x) & []<>(!y);

which is represented by the LTL formula

\[ \newcommand{\Feventually}{\style{display: inline-block; transform: rotate(45deg); padding: 0.2em;}{\Box}} \left( \neg x \wedge \Box \left( x \leftrightarrow \neg x' \right) \wedge \Box \Feventually x \right) \implies \left( y \wedge \Box \Feventually (y \wedge x) \wedge \Box \Feventually \neg y \right). \]

The only environment variable is x, and the only system variable is y; both are Boolean-valued. We require that initially x is False and y is True. Given the assumption that the environment will infinitely often set x to True, we must ensure that there are infinitely many states visited such that both y and x are True, and such that y is False. Obviously there must be at least two states in any play winning for the system because the two guaranteed formulas (y&x and !y) cannot simultaneously be True. It is assumed that the environment will flip the variable x at each step, as indicated by the transition rule ENVTRANS. Finally, there is no restriction on transitions by the system, as indicated by the empty SYSTRANS:;. Equivalently, the safety component of the guarantee is True. To check whether the specification is realizable,

gr1c -r  examples/trivial.spc

A message indicating realizability, such as "Realizable," will be printed. Now, to synthesize a strategy for it, output the result into a DOT file, and create a PNG called temp.dot.png from that output, try

gr1c -t dot examples/trivial.spc > temp.dot
dot -Tpng -O temp.dot

Organization

Besides using the API directly and linking to relevant source files (cf. the developer's introduction), several executable programs are built, some of which are considered experimental due to inclusion of methods involving active research. A summary of these programs follows:

gr1c

the basic program for synthesis of strategies for GR(1) formulae as defined in [KPP05] (GR(1) is referred to as "generalized Streett[1]" in that paper). An original motivating algorithm was implemented by Yaniv Sa'ar [BJPPS12], though the implementation in gr1c differs somewhat.

When the invocation of gr1c is of the form gr1c COMMAND [...], it acts as a base program for using other commands, which are described below.

gr1c rg

a tool for solving "reachability games," which are similar to GR(1) formulae except with at most one system goal and where that system goal need only be reached once (not necessarily infinitely often). The input specifications are slightly different.

gr1c patch

(experimental.) a command-line tool for using implementations of incremental synthesis (or "patching") algorithms, mostly from recent research publications. E.g., patch_localfixpoint() (cf. patching.h) concerns the method in [LPJM13].

gr1c autman
(auxiliary.) a command-line tool for manipulating automata. Currently it only supports gr1c automaton format.

Exit codes

The exit code is also known as "return code" or "status code." It is the integer returned at the end of execution. While the particular meaning of an exit code depends on the activity being performed, in all cases an exit code of zero is interpreted as success. We reserve negative exit codes for indication of internal errors and positive exit codes for activity-specific non-success. An example of an internal error is a failed call to the standard library malloc() because no more memory is available. (Notice that an "internal error" may be due to an external event.) Currently all internal errors are indicated by -1, but other negative values may be used in the future. Below is a list of invocation summaries and interpretations of exit codes.

Common exit codes for all activities:

  • 1 : invalid command-line usage
  • 2 : syntax error

gr1c -s (check syntax)

  • 0 : correct syntax

gr1c -r (check realizability)

  • 0 : realizable
  • 3 : unrealizable

gr1c (perform basic GR(1) synthesis)

  • 0 : success
  • 3 : unrealizable

gr1c -i (interactive)

  • 3 : unrealizable

rg -s (check syntax)

  • 0 : correct syntax

autman

  • 2 : syntax error in the reference specification (not necessarily given)
  • 3 : syntax error in the automaton description

Further reading

License

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.