Skip to content

Commit

Permalink
Make rg a command of gr1c
Browse files Browse the repository at this point in the history
E.g., now one can use

    gr1c rg examples/trivial_reach.spc

This results in execution of gr1c-rg, which is the new file name of
"rg". This change has the following motivations.

1. To avoid crowding the PATH namespace, which is important in
   anticipation of packaging and distributing gr1c among other tools.

2. To prepare for additional use of the `gr1c COMMAND ...` idiom,
   which can help organize command-line switches and major modes of
   operation, e.g., removing the "-i" switch and offering `gr1c interact`
  • Loading branch information
slivingston committed Mar 27, 2015
1 parent 48db520 commit 5beb71e
Show file tree
Hide file tree
Showing 5 changed files with 35 additions and 12 deletions.
8 changes: 4 additions & 4 deletions Makefile
@@ -1,8 +1,8 @@
# Build executables and documentation; run tests.
#
# SCL; 2012-2014.
# SCL; 2012-2015.

CORE_PROGRAMS = gr1c rg
CORE_PROGRAMS = gr1c gr1c-rg
EXP_PROGRAMS = grpatch
AUX_PROGRAMS = autman

Expand Down Expand Up @@ -49,7 +49,7 @@ all: core exp aux
gr1c: main.o util.o logging.o interactive.o solve_support.o solve_operators.o solve.o ptree.o automaton.o automaton_io.o gr1c_parse.o
$(CC) -o $@ $^ $(LDFLAGS)

rg: rg_main.o util.o patching_support.o logging.o solve_support.o solve_operators.o solve.o ptree.o automaton.o automaton_io.o rg_parse.o
gr1c-rg: rg_main.o util.o patching_support.o logging.o solve_support.o solve_operators.o solve.o ptree.o automaton.o automaton_io.o rg_parse.o
$(CC) -o $@ $^ $(LDFLAGS)

autman: util.o logging.o solve_support.o ptree.o autman.o automaton.o automaton_io.o gr1c_parse.o
Expand Down Expand Up @@ -121,7 +121,7 @@ expinstall:
$(INSTALL) grpatch $(DESTDIR)$(bindir)

uninstall:
rm -f $(DESTDIR)$(bindir)/gr1c $(DESTDIR)$(bindir)/rg $(DESTDIR)$(bindir)/grpatch
rm -f $(DESTDIR)$(bindir)/gr1c $(DESTDIR)$(bindir)/gr1c-rg $(DESTDIR)$(bindir)/grpatch

check: $(CORE_PROGRAMS) $(EXP_PROGRAMS)
$(MAKE) -C tests CC=$(CC)
Expand Down
2 changes: 1 addition & 1 deletion src/common.h
Expand Up @@ -10,7 +10,7 @@
#define COMMON_H


#define GR1C_VERSION "0.9.1"
#define GR1C_VERSION "0.10.0"
#define GR1C_COPYRIGHT "Copyright (c) 2012-2015 by Scott C. Livingston,\n" \
"California Institute of Technology\n\n" \
"This is free, open source software, released under a BSD license\n" \
Expand Down
25 changes: 24 additions & 1 deletion src/main.c
Expand Up @@ -8,6 +8,7 @@
*/


#include <unistd.h>
#include <string.h>
#include <stdio.h>
#include <stdlib.h>
Expand Down Expand Up @@ -78,6 +79,7 @@ int main( int argc, char **argv )
int input_index = -1;
int output_file_index = -1; /* For command-line flag "-o". */
char dumpfilename[64];
char **command_argv = NULL;

byte verification_model = 0; /* For command-line flag "-P". */
ptree_t *original_env_init;
Expand All @@ -99,6 +101,25 @@ int main( int argc, char **argv )
anode_t *strategy = NULL;
int num_env, num_sys;

/* Try to handle sub-commands first */
if (argc >= 2) {
if (!strncmp( argv[1], "rg", strlen( "rg" ) )) {

/* Pass arguments after rg */
command_argv = malloc( sizeof(char *)*argc );
command_argv[0] = strdup( "gr1c-rg" );
command_argv[argc] = NULL;
for (i = 1; i < argc-1; i++)
command_argv[i] = argv[i+1];

if (execv( "gr1c-rg", command_argv ) < 0) {
perror( "gr1c, execv" );
return -1;
}

}
}

/* Look for flags in command-line arguments. */
for (i = 1; i < argc; i++) {
if (reading_options && argv[i][0] == '-' && argv[i][1] != '-') {
Expand Down Expand Up @@ -196,7 +217,7 @@ int main( int argc, char **argv )

if (help_flag) {
/* Split among printf() calls to conform with ISO C90 string length */
printf( "Usage: %s [-hVvlspriP] [-n INIT] [-t TYPE] [-o FILE] [FILE]\n\n"
printf( "Usage: %s [COMMAND] [-hVvlspriP] [-n INIT] [-t TYPE] [-o FILE] [FILE]\n\n"
" -h this help message\n"
" -V print version and exit\n"
" -v be verbose; use -vv to be more verbose\n"
Expand All @@ -216,6 +237,8 @@ int main( int argc, char **argv )
" -o FILE output strategy to FILE, rather than stdout (default)\n"
" -P create Spin Promela model of strategy;\n"
" output to stdout, so requires -o flag to also be used\n" );
printf( "\nCOMMAND:\n\n"
" rg solve reachability game\n" );
return 1;
}

Expand Down
6 changes: 3 additions & 3 deletions src/rg_main.c
@@ -1,4 +1,4 @@
/* rg_main.c -- main entry point for execution of rg.
/* rg_main.c -- main entry point for execution of gr1c-rg.
*
*
* SCL; 2012-2014.
Expand Down Expand Up @@ -209,7 +209,7 @@ int main( int argc, char **argv )
if (input_index > 0) {
fp = fopen( argv[input_index], "r" );
if (fp == NULL) {
perror( "rg, fopen" );
perror( "gr1c-rg, fopen" );
return -1;
}
stdin_backup = stdin;
Expand Down Expand Up @@ -561,7 +561,7 @@ int main( int argc, char **argv )
if (output_file_index >= 0) {
fp = fopen( argv[output_file_index], "w" );
if (fp == NULL) {
perror( "rg, fopen" );
perror( "gr1c-rg, fopen" );
return -1;
}
} else {
Expand Down
6 changes: 3 additions & 3 deletions tests/test-gr1c.sh
Expand Up @@ -105,9 +105,9 @@ if test $VERBOSE -eq 1; then
fi
for k in `echo $REFSPECS`; do
if test $VERBOSE -eq 1; then
echo "\tComparing rg -t txt $TESTDIR/specs/$k \n\t\tagainst $TESTDIR/expected_outputs/${k}.listdump.out"
echo "\tComparing gr1c-rg -t txt $TESTDIR/specs/$k \n\t\tagainst $TESTDIR/expected_outputs/${k}.listdump.out"
fi
if ! ($BUILD_ROOT/rg -t txt specs/$k | cmp -s expected_outputs/${k}.listdump.out -); then
if ! ($BUILD_ROOT/gr1c-rg -t txt specs/$k | cmp -s expected_outputs/${k}.listdump.out -); then
echo $PREFACE "Reachability game synthesis regression test failed for specs/${k}\n"
exit -1
fi
Expand Down Expand Up @@ -160,7 +160,7 @@ for k in `ls flawed_reach_specs/*.spc`; do
if test $VERBOSE -eq 1; then
echo "\t gr1c -s $k"
fi
if $BUILD_ROOT/rg -s $k > /dev/null 2>&1; then
if $BUILD_ROOT/gr1c-rg -s $k > /dev/null 2>&1; then
echo $PREFACE "Flawed reachability game spec ${k} detected as OK\n"
exit -1
fi
Expand Down

0 comments on commit 5beb71e

Please sign in to comment.