// Station interlocking: dispatcher command permissions, rules 1, 2, 3, 4, 5
// Generated by codegen.py from the rule clauses Foras proved (Foras 0.4.0).
// Equivalence (checked when generated): the compiled C agrees with the clauses on all 768 states x 4 commands,
// and the brute-force search with this code as the guards reaches the same states and verdict.
// Do not edit: regenerate from the clauses.
#include <stdbool.h>

typedef enum { A_W, A_E, S_MAIN, S_LOOP, S_EAST, OUT_B, OUT_S } pos_t;
typedef enum { RED, GRN } aspect_t;
typedef enum { NRM, REV } points_t;
typedef struct { pos_t blue, orange, silver; aspect_t s1, s2, s3; points_t points; } station_t;

/* clear_s1: rules 1, 2, 4 */
bool permit_clear_s1(const station_t *s) {
  return s->orange != S_MAIN && s->s2 == RED && s->s3 == RED && s->orange != S_EAST && s->silver != S_EAST;
}

/* clear_s2: rules 1, 2, 4, 5 */
bool permit_clear_s2(const station_t *s) {
  return s->blue != S_EAST && s->silver != S_EAST && s->s1 == RED && s->s3 == RED && (s->blue == A_W || s->blue == OUT_B) && s->points == NRM;
}

/* clear_s3: rules 1, 2, 4 */
bool permit_clear_s3(const station_t *s) {
  return s->blue != S_EAST && s->orange != S_EAST && s->s1 == RED && s->s2 == RED && (s->blue == A_W || s->blue == OUT_B);
}

/* throw: rule 3 */
bool permit_throw(const station_t *s) {
  return s->s1 == RED && s->s2 == RED && s->s3 == RED && (s->blue == A_W || s->blue == OUT_B) && s->orange != S_EAST && s->silver != S_EAST;
}