(* 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. *)

TYPE
  POS : (A_W, A_E, S_MAIN, S_LOOP, S_EAST, OUT_B, OUT_S);
  ASPECT : (RED, GRN);
  POINTS_POS : (NRM, REV);
END_TYPE

FUNCTION_BLOCK FB_STATION_INTERLOCKING
VAR_INPUT
  blue, orange, silver : POS;
  s1, s2, s3 : ASPECT;
  points : POINTS_POS;
END_VAR
VAR_OUTPUT
  PERMIT_CLEAR_S1 : BOOL;
  PERMIT_CLEAR_S2 : BOOL;
  PERMIT_CLEAR_S3 : BOOL;
  PERMIT_THROW_POINTS : BOOL;
END_VAR

  (* clear_s1: rules 1, 2, 4 *)
  PERMIT_CLEAR_S1 := orange <> S_MAIN AND s2 = RED AND s3 = RED AND orange <> S_EAST AND silver <> S_EAST;
  (* clear_s2: rules 1, 2, 4, 5 *)
  PERMIT_CLEAR_S2 := blue <> S_EAST AND silver <> S_EAST AND s1 = RED AND s3 = RED AND (blue = A_W OR blue = OUT_B) AND points = NRM;
  (* clear_s3: rules 1, 2, 4 *)
  PERMIT_CLEAR_S3 := blue <> S_EAST AND orange <> S_EAST AND s1 = RED AND s2 = RED AND (blue = A_W OR blue = OUT_B);
  (* throw: rule 3 *)
  PERMIT_THROW_POINTS := s1 = RED AND s2 = RED AND s3 = RED AND (blue = A_W OR blue = OUT_B) AND orange <> S_EAST AND silver <> S_EAST;
END_FUNCTION_BLOCK