modelchecker/coord.h

   1 #ifndef COORD_H
   2 #define COORD_H
   3
   4 #include "sokoban.h"
   5
   6 typedef struct {
   7         BDDSET varset;
   8         int size;
   9 } variables;
  10
  11 typedef struct {
  12     BDD bdd;
  13     variables vars;
  14 } state;
  15
  16 typedef struct trans {
  17     BDD bdd;
  18     variables varset;
  19         struct trans *next_rel;
  20 } trans_t;
  21
  22 typedef struct {
  23         trans_t *rell;
  24         trans_t *relu;
  25         trans_t *relr;
  26         trans_t *reld;
  27 } rels;
  28
  29 typedef enum { LEFT, UP, RIGHT, DOWN } direction;
  30
  31 state *encode_screen(sokoban_screen *screen);
  32
  33 rels *encode_rel(sokoban_screen *screen);
  34
  35 //int test_relprod();
  36
  37 #endif