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                         break;
  63                 case WALL:
  64                         if (state == sylvan_false){
  65                                 state = sylvan_not(sylvan_ithvar(tile_index));
  66                                 tile_index++;
  67                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  68                                 tile_index++;
  69                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  70                                 tile_index++;
  71                         }
  72                         else {
  73                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  74                                 tile_index++;
  75                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  76                                 tile_index++;
  77                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  78                                 tile_index++;
  79                         }
  80                         break;
  81                 case BOX:
  82                         if (state == sylvan_false){
  83                                 state = sylvan_not(sylvan_ithvar(tile_index));
  84                                 tile_index++;
  85                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
  86                                 tile_index++;
  87                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  88                                 tile_index++;
  89                         }
  90                         else {
  91                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  92                                 tile_index++;
  93                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
  94                                 tile_index++;
  95                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
  96                                 tile_index++;
  97                         }
  98                         break;
  99                 case TARGET:
 100                         if (state == sylvan_false){
 101                                 state = sylvan_not(sylvan_ithvar(tile_index));
 102                                 tile_index++;
 103                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 104                                 tile_index++;
 105                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 106                                 tile_index++;
 107                         }
 108                         else {
 109                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 110                                 tile_index++;
 111                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 112                                 tile_index++;
 113                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 114                                 tile_index++;
 115                         }
 116                         break;
 117                 case AGENT:
 118                         if (state == sylvan_false){
 119                                 state = sylvan_ithvar(tile_index);
 120                                 tile_index++;
 121                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 122                                 tile_index++;
 123                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 124                                 tile_index++;
 125                         }
 126                         else {
 127                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 128                                 tile_index++;
 129                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 130                                 tile_index++;
 131                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 132                                 tile_index++;
 133                         }
 134                         break;
 135                 case TARGAGENT:
 136                         if (state == sylvan_false){
 137                                 state = sylvan_ithvar(tile_index);
 138                                 tile_index++;
 139                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 140                                 tile_index++;
 141                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 142                                 tile_index++;
 143                         }
 144                         else {
 145                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 146                                 tile_index++;
 147                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 148                                 tile_index++;
 149                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 150                                 tile_index++;
 151                         }
 152                         break;
 153                 case TARGBOX:
 154                         if (state == sylvan_false){
 155                                 state = sylvan_ithvar(tile_index);
 156                                 tile_index++;
 157                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 158                                 tile_index++;
 159                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 160                                 tile_index++;
 161                         }
 162                         else {
 163                                 state = sylvan_and(state, sylvan_ithvar(tile_index));
 164                                 tile_index++;
 165                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 166                                 tile_index++;
 167                                 state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
 168                                 tile_index++;
 169                         }
 170                         break;
 171                 }
 172         }
 173         printf("%d tiles were encoded\n", tile_index);
 174         return state;
 175 }
 176
 177 BDD encode_rel(sokoban_screen *screen)
 178 {
 179         int num_tiles;
 180         num_tiles = HASH_COUNT(screen);
 181         printf("Number of tiles: %d\n", num_tiles);
 182         return sylvan_true;
 183 }
 184
 185 void test()
 186 {
 187
 188         printf("Test!\n");
 189         BDD a = sylvan_true;
 190         BDD b = sylvan_not(a);
 191         if (b == sylvan_false){
 192                 printf("BDD works!\n");
 193         } else {
 194                 printf("BDD does not work!\n");
 195         }
 196         LACE_ME;
 197         BDD c = sylvan_ithvar(1);
 198         if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
 199         if (sylvan_var(c) == 1) printf("Var works 2\n");
 200 }