Merge remote-tracking branch 'origin/lurd'

Conflicts:
	modelchecker/main.c

diff --git a/modelchecker/benchmark.sh b/modelchecker/benchmark.sh
new file mode 100644 (file)
index 0000000..05808dd
--- /dev/null
+++ b/modelchecker/benchmark.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+make
+for i in 2000 107 1001 387 372 792 747 38 754 2; do
+       echo "Problem: $i"
+       time ./main -v ../sokobanzip/screens/screen.$i
+done

diff --git a/modelchecker/main.c b/modelchecker/main.c
index bdf8a12..1f518eb 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -22,9 +22,7 @@ void usage(char *prg)
                "\t%s [opts] [FILE]\n"
                "\n"
                "Options:\n"
-//             "\t-l LURD  lURD verification strategy\n"
-//             "\t-r      show all positions that are a valid solution\n"
-               "\n"
+               "\t-l LURD lURD verification strategy\n"
                "\t-v      enable verbose output\n"
                "\t-h      show this help\n"
                "\n"
@@ -42,7 +40,7 @@ BDD subsolve(trans_t *t, BDD new){
        return new;
 }
 
-int solve(FILE *inputstream)
+int solve(FILE *inputstream, char *lurd)
 {
        clock_t time_start_read, time_end_read, time_start_scr, time_end_scr,
                time_start_goal, time_end_goal, time_start_rel, time_end_rel,
@@ -79,10 +77,32 @@ int solve(FILE *inputstream)
        rels *rls = encode_rel(screen);
        time_end_rel = clock();
 
+
        //Actually solve
        time_start_solve = clock();
        BDD old = sylvan_false;
        BDD new = init->bdd;
+       //Do lurd
+       while(*lurd != '\0'){
+               switch(*lurd){
+               case 'l':
+                       new = subsolve(rls->rell, new);
+                       break;
+        case 'u':
+                       new = subsolve(rls->relu, new);
+                       break;
+               case 'r':
+                       new = subsolve(rls->relr, new);
+                       break;
+               case 'd':
+                       new = subsolve(rls->reld, new);
+                       break;
+               default:
+                       printf("Unknown character in lucd: '%c'\n", *lurd);
+                       exit(2);
+               }
+               lurd++;
+       }
        int iteration = 0;
        bool found = false;
        while(new != old){
@@ -119,9 +139,14 @@ int solve(FILE *inputstream)
 int main(int argc, char **argv)
 {
        int optchar;
+       char *lurd = "";
 
-       while((optchar = getopt(argc, argv, "vh")) != -1){
+       while((optchar = getopt(argc, argv, "vhl:")) != -1){
                switch(optchar){
+               case 'l':
+                       DPRINT("Lurd detected: `%s'\n", optarg);
+                       lurd = optarg;
+                       break;
                case 'v':
                        VERBOSE = true;
                        DPRINT("Debug enabled\n");
@@ -143,13 +168,12 @@ int main(int argc, char **argv)
 
        if(optind == argc){
                DPRINT("You have not specified a file, reading from stdin\n");
-               return solve(stdin);
+               return solve(stdin, lurd);
        } else {
                DPRINT("Processing: %s\n", argv[optind]);
-               DPRINT("Thus skipping the other %d files\n", argc-optind);
                FILE *currentfile = fopen(argv[optind], "r");
                DPRINT("Opening file\n");
-               return solve(currentfile);
+               return solve(currentfile, lurd);
                DPRINT("Closing file\n");
                fclose(currentfile);
        }