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         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  43                 switch(r->tile){
  44                 case FREE:
  45                         if (state == sylvan_false){
  46
  47                         }
  48                         else {
  49
  50                         }
  51                         printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
  52                         break;
  53                 case WALL:
  54                         if (state == sylvan_false){
  55
  56                         }
  57                         else {
  58
  59                         }
  60                         printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
  61                         break;
  62                 case BOX:
  63                         if (state == sylvan_false){
  64
  65                         }
  66                         else {
  67
  68                         }
  69                         printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
  70                         break;
  71                 case TARGET:
  72                         if (state == sylvan_false){
  73
  74                         }
  75                         else {
  76
  77                         }
  78                         printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
  79                         break;
  80                 case AGENT:
  81                         if (state == sylvan_false){
  82
  83                         }
  84                         else {
  85
  86                         }
  87                         printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
  88                         break;
  89                 case TARGAGENT:
  90                         if (state == sylvan_false){
  91
  92                         }
  93                         else {
  94
  95                         }
  96                         printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
  97                         break;
  98                 case TARGBOX:
  99                         if (state == sylvan_false){
 100
 101                         }
 102                         else {
 103
 104                         }
 105                         printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
 106                         break;
 107                 }
 108         }
 109         return state;
 110 }
 111
 112 BDD encode_rel(sokoban_screen *screen)
 113 {
 114         int num_tiles;
 115         num_tiles = HASH_COUNT(screen);
 116         printf("Number of tiles: %d\n", num_tiles);
 117         return sylvan_true;
 118 }
 119
 120 void test()
 121 {
 122
 123         printf("Test!\n");
 124         BDD a = sylvan_true;
 125         BDD b = sylvan_not(a);
 126         if (b == sylvan_false){
 127                 printf("BDD works!\n");
 128         } else {
 129                 printf("BDD does not work!\n");
 130         }
 131         LACE_ME;
 132         BDD c = sylvan_ithvar(1);
 133         if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
 134         if (sylvan_var(c) == 1) printf("Var works 2\n");
 135 }