repositories
/
mc1516pa.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
bimap helper added
[mc1516pa.git]
/
modelchecker
/
main.c
diff --git
a/modelchecker/main.c
b/modelchecker/main.c
index
16dd229
..
e954c07
100644
(file)
--- a/
modelchecker/main.c
+++ b/
modelchecker/main.c
@@
-2,19
+2,26
@@
#include <stdbool.h>
#include <ctype.h>
#include <time.h>
#include <stdbool.h>
#include <ctype.h>
#include <time.h>
+#include <unistd.h>
#include <sylvan.h>
#include <sylvan.h>
-#include "mc.h"
#include "sokoban.h"
#include "sokoban.h"
+#include "coord.h"
+#include "object.h"
+
+#define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
+#define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
+
+typedef enum {OBJECT, COORD, HYBRID} strategy;
//Global variables
bool DEBUG = false;
strategy strat = HYBRID;
//Global variables
bool DEBUG = false;
strategy strat = HYBRID;
-void usage(char *prg)
{
- fprintf(stderr,
-
"Usage:\n"
+void usage(char *prg)
+{
+
ERRPRINT(
"Usage:\n"
"\t%s [opts] [FILE [FILE [...]]]\n"
"\n"
"Options:\n"
"\t%s [opts] [FILE [FILE [...]]]\n"
"\n"
"Options:\n"
@@
-33,68
+40,82
@@
void usage(char *prg){
"\t when no file is specified stdin will be used\n", prg);
}
"\t when no file is specified stdin will be used\n", prg);
}
-void solve(FILE *inputstream){
+void solve(FILE *inputstream)
+{
clock_t time_start_read, time_end_read;
clock_t time_start_encode, time_end_encode;
time_start_read = clock();
clock_t time_start_read, time_end_read;
clock_t time_start_encode, time_end_encode;
time_start_read = clock();
- //struct sokoban_screen *screen = parse_screen(inputstream);
- parse_screen(inputstream);
+ sokoban_screen *screen = parse_screen(inputstream);
+ if (screen == NULL) printf("Something went wrong...\n");
+ //sokoban_print(screen);
time_end_read = clock();
time_start_encode = clock();
time_end_read = clock();
time_start_encode = clock();
+
+ lace_init(0, 1000000);
+ lace_startup(0, NULL, NULL);
+ LACE_ME;
+ sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
+ sylvan_init_bdd(6);
switch(strat){
switch(strat){
- case COORD:
- if(DEBUG) fprintf(stderr, "Encoding coordinate based\n");
- break;
- case OBJECT:
- if(DEBUG) fprintf(stderr, "Encoding object based\n");
- break;
- case HYBRID:
- if(DEBUG) fprintf(stderr, "Encoding hybrid based\n");
- break;
- default:
- fprintf(stderr, "Huh?");
- exit(2);
+ case COORD:
+ DPRINT("Encoding coordinate based\n");
+ encode_screen(screen);
+ break;
+ case OBJECT:
+ DPRINT("Encoding object based\n");
+ solve_object(screen);
+ break;
+ case HYBRID:
+ DPRINT("Encoding hybrid based\n");
+ DPRINT("Not implemented yet...\n");
+ break;
+ default:
+ ERRPRINT("Huh?");
+ exit(2);
}
}
+ sokoban_free(screen);
time_end_encode = clock();
time_end_encode = clock();
-
- // Future: SMC
- fprintf(stderr, "Reading: %fs\n",
+
+ //SOLVE???
+
+ ERRPRINT("Reading: %fs\n",
((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
-
fprintf(stderr,
"Encoding: %fs\n",
+
ERRPRINT(
"Encoding: %fs\n",
((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
}
((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
}
-int main(int argc, char **argv){
+int main(int argc, char **argv)
+{
int optchar;
while((optchar = getopt(argc, argv, "cdhoy")) != -1){
switch(optchar){
case 'c':
strat = COORD;
int optchar;
while((optchar = getopt(argc, argv, "cdhoy")) != -1){
switch(optchar){
case 'c':
strat = COORD;
-
if(DEBUG) fprintf(stderr,
"Strategy changed to Coordinate based\n");
+
DPRINT(
"Strategy changed to Coordinate based\n");
break;
case 'd':
DEBUG = true;
break;
case 'd':
DEBUG = true;
-
if(DEBUG) fprintf(stderr,
"Debug enabled\n");
+
DPRINT(
"Debug enabled\n");
break;
case 'h':
usage(argv[0]);
return 0;
case 'o':
strat = OBJECT;
break;
case 'h':
usage(argv[0]);
return 0;
case 'o':
strat = OBJECT;
-
if(DEBUG) fprintf(stderr,
"Strategy changed to Object based\n");
+
DPRINT(
"Strategy changed to Object based\n");
break;
case 'y':
strat = HYBRID;
break;
case 'y':
strat = HYBRID;
-
if(DEBUG) fprintf(stderr,
"Strategy changed to Hybrid\n");
+
DPRINT(
"Strategy changed to Hybrid\n");
break;
case '?':
if(isprint(optopt)){
break;
case '?':
if(isprint(optopt)){
-
fprintf(stderr,
"Unknown option `-%c'.\n", optopt);
+
ERRPRINT(
"Unknown option `-%c'.\n", optopt);
} else {
} else {
-
fprintf(stderr,
"Unknown option char `-\\x%x'.\n", optopt);
+
ERRPRINT(
"Unknown option char `-\\x%x'.\n", optopt);
}
return 2;
default:
}
return 2;
default:
@@
-103,17
+124,17
@@
int main(int argc, char **argv){
}
if(optind == argc){
}
if(optind == argc){
-
fprintf(stderr,
"You have not specified a file, reading from stdin\n");
+
ERRPRINT(
"You have not specified a file, reading from stdin\n");
solve(stdin);
}
for(int filepathindex = optind; filepathindex < argc; filepathindex++){
char *currentfilepath = argv[filepathindex];
solve(stdin);
}
for(int filepathindex = optind; filepathindex < argc; filepathindex++){
char *currentfilepath = argv[filepathindex];
-
fprintf(stderr,
"Processing: %s\n", currentfilepath);
+
ERRPRINT(
"Processing: %s\n", currentfilepath);
FILE *currentfile = fopen(currentfilepath, "r");
FILE *currentfile = fopen(currentfilepath, "r");
-
if(DEBUG) fprintf(stderr,
"Opening file\n");
+
DPRINT(
"Opening file\n");
solve(currentfile);
solve(currentfile);
-
if(DEBUG) fprintf(stderr,
"Closing file\n");
+
DPRINT(
"Closing file\n");
fclose(currentfile);
}
return 0;
fclose(currentfile);
}
return 0;