modelchecker/coord.c

   1 #include <argp.h>
   2 #include <inttypes.h>
   3 #include <locale.h>
   4 #include <stdio.h>
   5 #include <stdlib.h>
   6 #include <string.h>
   7 #include <sys/time.h>
   8
   9 #ifdef HAVE_PROFILER
  10 #include <gperftools/profiler.h>
  11 #endif
  12
  13 #include <sylvan.h>
  14 #include <llmsset.h>
  15 #include <lace.h>
  16
  17 #include "coord.h"
  18 #include "sokoban.h"
  19
  20
  21 /*
  22  * Each coordinate has three related boolean variables. The combination of those boolean variables
  23  * defines tiles:
  24  * 000: Wall
  25  * 001: Free
  26  * 010: Box
  27  * 100: Box on target
  28  * 011: Target
  29  * 101: Agent
  30  * 110: Agent on target
  31  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
  32  * tiles in the shrinked screen.
  33  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
  34  * directly in transition relations.
  35  */
  36
  37 BDD encode_screen(sokoban_screen *screen)
  38 {
  39         BDD state = sylvan_false;
  40         int tile_index = 0;
  41         sokoban_screen *r;
  42         LACE_ME;
  43         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  44                 switch(r->tile){
  45                 case FREE:
  46                         if (state == sylvan_false){
  47                                 state = sylvan_not(sylvan_ithvar(tile_index));
  48                                 tile_index++;
  49                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  50                                 tile_index++;
  51                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
  52                                 tile_index++;
  53                         }
  54                         else {
  55                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  56                                 tile_index++;
  57                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  58                                 tile_index++;
  59                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
  60                                 tile_index++;
  61                         }
  62                         printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
  63                         break;
  64                 case WALL:
  65                         if (state == sylvan_false){
  66                                 state = sylvan_not(sylvan_ithvar(tile_index));
  67                                 tile_index++;
  68                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  69                                 tile_index++;
  70                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  71                                 tile_index++;
  72                         }
  73                         else {
  74                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  75                                 tile_index++;
  76                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  77                                 tile_index++;
  78                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  79                                 tile_index++;
  80                         }
  81                         printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
  82                         break;
  83                 case BOX:
  84                         if (state == sylvan_false){
  85                                 state = sylvan_not(sylvan_ithvar(tile_index));
  86                                 tile_index++;
  87                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
  88                                 tile_index++;
  89                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  90                                 tile_index++;
  91                         }
  92                         else {
  93                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  94                                 tile_index++;
  95                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
  96                                 tile_index++;
  97                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  98                                 tile_index++;
  99                         }
 100                         printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
 101                         break;
 102                 case TARGET:
 103                         if (state == sylvan_false){
 104                                 state = sylvan_not(sylvan_ithvar(tile_index));
 105                                 tile_index++;
 106                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 107                                 tile_index++;
 108                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 109                                 tile_index++;
 110                         }
 111                         else {
 112                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 113                                 tile_index++;
 114                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 115                                 tile_index++;
 116                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 117                                 tile_index++;
 118                         }
 119                         printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
 120                         break;
 121                 case AGENT:
 122                         if (state == sylvan_false){
 123                                 state = sylvan_ithvar(tile_index);
 124                                 tile_index++;
 125                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 126                                 tile_index++;
 127                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 128                                 tile_index++;
 129                         }
 130                         else {
 131                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 132                                 tile_index++;
 133                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 134                                 tile_index++;
 135                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 136                                 tile_index++;
 137                         }
 138                         printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
 139                         break;
 140                 case TARGAGENT:
 141                         if (state == sylvan_false){
 142                                 state = sylvan_ithvar(tile_index);
 143                                 tile_index++;
 144                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 145                                 tile_index++;
 146                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 147                                 tile_index++;
 148                         }
 149                         else {
 150                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 151                                 tile_index++;
 152                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 153                                 tile_index++;
 154                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 155                                 tile_index++;
 156                         }
 157                         printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
 158                         break;
 159                 case TARGBOX:
 160                         if (state == sylvan_false){
 161                                 state = sylvan_ithvar(tile_index);
 162                                 tile_index++;
 163                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 164                                 tile_index++;
 165                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 166                                 tile_index++;
 167                         }
 168                         else {
 169                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 170                                 tile_index++;
 171                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 172                                 tile_index++;
 173                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 174                                 tile_index++;
 175                         }
 176                         printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
 177                         break;
 178                 }
 179         }
 180         return state;
 181 }
 182
 183 BDD encode_rel(sokoban_screen *screen)
 184 {
 185         int num_tiles;
 186         num_tiles = HASH_COUNT(screen);
 187         printf("Number of tiles: %d\n", num_tiles);
 188         return sylvan_true;
 189 }
 190
 191 void test()
 192 {
 193
 194         printf("Test!\n");
 195         BDD a = sylvan_true;
 196         BDD b = sylvan_not(a);
 197         if (b == sylvan_false){
 198                 printf("BDD works!\n");
 199         } else {
 200                 printf("BDD does not work!\n");
 201         }
 202         LACE_ME;
 203         BDD c = sylvan_ithvar(1);
 204         if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
 205         if (sylvan_var(c) == 1) printf("Var works 2\n");
 206 }