X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.h;h=bcab49871e51fc25258b787cad733df84793dc2c;hb=03c6e2f515f6516448ec39aa40a439b9fc20c4c8;hp=2ec291814baabbef16b2319d45be6f14597ca997;hpb=0a8ebd63de0624a2fc002a78e092694893016d41;p=mc1516pa.git diff --git a/modelchecker/coord.h b/modelchecker/coord.h index 2ec2918..bcab498 100644 --- a/modelchecker/coord.h +++ b/modelchecker/coord.h @@ -3,7 +3,26 @@ #include "sokoban.h" -BDD encode_screen(sokoban_screen *screen); +typedef struct { + BDDSET varset; + int size; +} variables; + +typedef struct +{ + BDD bdd; + variables vars; +} state; + +typedef struct +{ + BDD bdd; + variables varset; +} trans; + +typedef enum { LEFT, UP, RIGHT, DOWN } direction; + +state *encode_screen(sokoban_screen *screen); BDD encode_rel(sokoban_screen *screen);