#define LNT2LOTOS_EXPERT_FNT 5.8 /* * This ``.fnt'' file is a programming trick used to speed up the state space * exploration. As we know that devices 3, 4, 5, 6 will be absent from the * system, there is no need to iterate on all the possible values for the * corresponding fields of the WIRE tuple: Setting these fields directly to 0 * (instead making them enumerate the domain {0, 1}) is sufficient. This * reduces the number of possible WIRE values from 256 to 16, without * altering the result (the generated state space would have the same size, * but its generation would be about 10 times slower) */ /* ------------------------------------------------------------------------- */ #define W1 (ACCESS_WIRE (*W, 0)) #define W2 (ACCESS_WIRE (*W, 1)) #define W3 (ACCESS_WIRE (*W, 2)) #define W4 (ACCESS_WIRE (*W, 3)) #define W5 (ACCESS_WIRE (*W, 4)) #define W6 (ACCESS_WIRE (*W, 5)) #define W7 (ACCESS_WIRE (*W, 6)) #define W8 (ACCESS_WIRE (*W, 7)) /* ------------------------------------------------------------------------- */ int ENUM_NEXT_FUNCTION_WIRE (W) WIRE *W; { if (!W8) { *W = MAKE_WIRE (W1, W2, W3, W4, W5, W6, W7, 1); return 1; } #ifdef __SKIP_THIS__ if (!W7) { *W = MAKE_WIRE (W1, W2, W3, W4, W5, W6, 1, 0); return 1; } if (!W6) { *W = MAKE_WIRE (W1, W2, W3, W4, W5, 1, 0, 0); return 1; } if (!W5) { *W = MAKE_WIRE (W1, W2, W3, W4, 1, 0, 0, 0); return 1; } if (!W4) { *W = MAKE_WIRE (W1, W2, W3, 1, 0, 0, 0, 0); return 1; } #endif /* __SKIP_THIS__ */ if (!W3) { *W = MAKE_WIRE (W1, W2, 1, 0, 0, 0, 0, 0); return 1; } if (!W2) { *W = MAKE_WIRE (W1, 1, 0, 0, 0, 0, 0, 0); return 1; } if (!W1) { *W = MAKE_WIRE (1, 0, 0, 0, 0, 0, 0, 0); return 1; } return 0; } /* ------------------------------------------------------------------------- */