<commit_before>.TH gr1c "1"
.SH NAME
gr1c \- a software suite for GR(1) synthesis and related activities
.SH SYNOPSIS
.B gr1c
.RB [\| \-vlspriP ]\|
.RB [\| \-n
.IR INIT ]\|
.RB [\| \-t
.IR TYPE ]\|
.RB [\| \-o
.IR FILE ]\|
.RI [\| FILE ]\|
.br
.B gr1c
.I COMMAND
.R "[\|...]\|"
.br
.B gr1c
.RB [\| \-hV ]\|
.SH DESCRIPTION
.B 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 http://scottman.net/2012/gr1c<commit_msg>DOC: Add options and example to manual page<commit_after>.TH gr1c "1"
.SH NAME
gr1c \- a software suite for GR(1) synthesis and related activities
.SH SYNOPSIS
.B gr1c
.RB [\| \-vlspriP ]\|
.RB [\| \-n
.IR INIT ]\|
.RB [\| \-t
.IR TYPE ]\|
.RB [\| \-o
.IR FILE ]\|
.RI [\| FILE ]\|
.br
.B gr1c
.I COMMAND
.R "[\|...]\|"
.br
.B gr1c
.RB [\| \-hV ]\|
.SH DESCRIPTION
.B 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.
.PP
The citable URL is http://scottman.net/2012/gr1c
.PP
As usual for UNIX command-line programs,
.B \-\-
can be used to disable option parsing, e.g., if a file named "-beef" is to be
read.
.PP
Besides being a command on its own,
.B gr1c
provides access to other commands in the suite when invoked as
.RS
.B gr1c
.I COMMAND
.R "[\|...]\|"
.RE
where COMMAND is one of the following:
.BR rg ,
.BR patch ,
.BR help .
When applicable, any arguments after COMMAND are passed on to the appropriate
program. Use
.B \-h
to get the corresponding help message.
.SH OPTIONS
.IP "\-h, \-\-help"
this help message
.IP "\-V, \-\-version"
print version and exit
.IP \-v
be verbose; use
.B -vv
to be more verbose
.IP \-l
enable logging
.IP "\-t TYPE"
strategy output format; default is
.BR json ;
supported formats:
.BR txt ,
.BR dot ,
.BR aut ,
.BR json ,
.BR tulip
.IP "\-n INIT"
initial condition interpretation, selected as
one of the following (not case sensitive):
.BR ALL_ENV_EXIST_SYS_INIT \ (default),
.BR ALL_INIT ,
.BR ONE_SIDE_INIT
.IP \-s
only check specification syntax (return 2 on error)
.IP \-p
dump parse trees to DOT files, and echo formulas to screen
.IP \-r
only check realizability; do not synthesize strategy
(return 0 if realizable, 3 if not)
.IP \-i
interactive mode
.IP "\-o FILE"
output strategy to FILE, rather than stdout (default)
.IP \-P
create Spin Promela model of strategy;
output to stdout, so requires
.B -o
flag to also be used.
.SH EXAMPLE
More examples are available in the gr1c release.
.in
.SS Specification
\&
.nf
ENV: x;
SYS: y;

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

SYSINIT: y;
SYSTRANS:;
SYSGOAL: []<>(y&x) & []<>(!y);
.fi
.SH AUTHORS
<NAME>  <<EMAIL>>
{'fraction_non_alphanumeric': 0.14295676429567644, 'fraction_numerical': 0.012552301255230125, 'mean_word_length': 3.029494382022472, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 10, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7263059', 'n_tokens_mistral': 1111, 'n_tokens_neox': 1043, 'n_words': 447}