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 {
  13     BDD bdd;
  14     variables vars;
  15 } state;
  16
  17 typedef struct
  18 {
  19     BDD bdd;
  20     variables varset;
  21 } trans;
  22
  23 typedef struct {
  24         BDD *rell;
  25         BDD *relu;
  26         BDD *relr;
  27         BDD *reld;
  28 } rels;
  29
  30 typedef enum { LEFT, UP, RIGHT, DOWN } direction;
  31
  32 state *encode_screen(sokoban_screen *screen);
  33
  34 rels *encode_rel(sokoban_screen *screen);
  35
  36 //int test_relprod();
  37
  38 #endif