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 lurd {
  17     char c;
  18     struct lurd *next;
  19 } lurd_t;
  20
  21 typedef struct {
  22     BDD bdd;
  23     variables vars;
  24     lurd_t *lrd;
  25 } state_t;
  26
  27 typedef struct trans {
  28     BDD bdd;
  29     variables varset;
  30         struct trans *next_rel;
  31 } trans_t;
  32
  33 typedef struct {
  34         trans_t *rell;
  35         trans_t *relu;
  36         trans_t *relr;
  37         trans_t *reld;
  38 } rels;
  39
  40 typedef enum { LEFT, UP, RIGHT, DOWN } direction;
  41
  42 state *encode_screen(sokoban_screen *screen);
  43
  44 rels *encode_rel(sokoban_screen *screen);
  45
  46 int test_trans(state *s, trans_t *t);
  47
  48 state *encode_goal(sokoban_screen *screen);
  49
  50 int check_goal(BDD s, BDD g, BDDSET vars);
  51
  52 int check_visited(BDD s, BDD v, BDDSET vars);
  53
  54 lurd_t *lappend(lurd_t *l, char c);
  55
  56 int test_relprod();
  57
  58 #endif