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 enum { ROOT, L, U, R, D } path_elt;
  17
  18 typedef struct {
  19     BDD bdd;
  20     variables vars;
  21     path_elt origin;
  22 } state_t;
  23
  24 typedef struct trans {
  25     BDD bdd;
  26     variables varset;
  27         struct trans *next_rel;
  28 } trans_t;
  29
  30 typedef struct {
  31         trans_t *rell;
  32         trans_t *relu;
  33         trans_t *relr;
  34         trans_t *reld;
  35 } rels;
  36
  37 typedef enum { LEFT, UP, RIGHT, DOWN } direction;
  38
  39 state *encode_screen(sokoban_screen *screen);
  40
  41 rels *encode_rel(sokoban_screen *screen);
  42
  43 int test_trans(state *s, trans_t *t);
  44
  45 state *encode_goal(sokoban_screen *screen);
  46
  47 int test_relprod();
  48
  49 #endif