type
  Dir {forward, backward, off};
  State {sink, cp_off, source};
  Load_26 [0..26];

variable
  bool P3_powered;
  Dir L3_dir;
  Load_26 L3_load;
  bool S5_powered;
  Dir L4_dir;
  Load_26 L4_load;
  bool S4_powered;
  Dir L10_dir;
  Load_26 L10_load;
  Dir L9_dir;
  Load_26 L9_load;
  Dir L8_dir;
  Load_26 L8_load;
  bool S7_powered;
  bool S6_powered;
  Dir L13_dir;
  Load_26 L13_load;
  Dir L7_dir;
  Load_26 L7_load;
  bool P2_powered;
  Dir L5_dir;
  Load_26 L5_load;
  bool S3_powered;
  Dir L6_dir;
  Load_26 L6_load;
  Dir L11_dir;
  Load_26 L11_load;
  bool S2_powered;
  Dir L12_dir;
  Load_26 L12_load;
  Dir L2_dir;
  Load_26 L2_load;
  bool S1_powered;
  Dir L1_dir;
  Load_26 L1_load;
  bool P1_powered;

rule
//Line L9
  (((L9_dir != off) && ((L10_dir == backward))) >> (L9_dir == backward)) &&
  ((L9_dir == backward) >> ((L9_dir != off) && ((L10_dir == backward))));
  (((L9_dir != off) && ((L4_dir == forward) || (L8_dir == backward))) >> (L9_dir == forward)) &&
  ((L9_dir == forward) >> ((L9_dir != off) && ((L4_dir == forward) || (L8_dir == backward))));
  (L9_dir == forward) >> (L9_load == L10_load + ((S4_powered >> 2) && (!S4_powered >> 0)) );
  (L9_dir == backward) >> (L9_load == L4_load + L8_load );
  (L9_dir == off) >> (L9_load == 0);

//Line L10
  (((L10_dir != off) && ((L6_dir == forward) || (L11_dir == backward))) >> (L10_dir == backward)) &&
  ((L10_dir == backward) >> ((L10_dir != off) && ((L6_dir == forward) || (L11_dir == backward))));
  (((L10_dir != off) && ((L9_dir == forward))) >> (L10_dir == forward)) &&
  ((L10_dir == forward) >> ((L10_dir != off) && ((L9_dir == forward))));
  (L10_dir == forward) >> (L10_load == L6_load + L11_load );
  (L10_dir == backward) >> (L10_load == L9_load + ((S4_powered >> 2) && (!S4_powered >> 0)) );
  (L10_dir == off) >> (L10_load == 0);

//Line L4
  (((L4_dir != off) && ((L8_dir == backward) || (L9_dir == backward))) >> (L4_dir == backward)) &&
  ((L4_dir == backward) >> ((L4_dir != off) && ((L8_dir == backward) || (L9_dir == backward))));
  (((L4_dir != off) && ((L3_dir == backward))) >> (L4_dir == forward)) &&
  ((L4_dir == forward) >> ((L4_dir != off) && ((L3_dir == backward))));
  (L4_dir == forward) >> (L4_load == L8_load + L9_load );
  (L4_dir == backward) >> (L4_load == L3_load + ((S5_powered >> 1) && (!S5_powered >> 0)) );
  (L4_dir == off) >> (L4_load == 0);

//Line L2
  (((L2_dir != off) && ((L7_dir == backward) || (L12_dir == forward))) >> (L2_dir == backward)) &&
  ((L2_dir == backward) >> ((L2_dir != off) && ((L7_dir == backward) || (L12_dir == forward))));
  (((L2_dir != off) && ((L1_dir == forward))) >> (L2_dir == forward)) &&
  ((L2_dir == forward) >> ((L2_dir != off) && ((L1_dir == forward))));
  (L2_dir == forward) >> (L2_load == L7_load + L12_load );
  (L2_dir == backward) >> (L2_load == L1_load + ((S1_powered >> 2) && (!S1_powered >> 0)) );
  (L2_dir == off) >> (L2_load == 0);

//Line L5
  P2_powered >> ( (L5_dir != backward) );
  !P2_powered >> (
  ((((L5_dir != off) && ((L6_dir == backward))) >> (L5_dir == backward)) &&
  ((L5_dir == backward) >> ((L5_dir != off) && ((L6_dir == backward))))));
  (L5_dir == forward) >> (L5_load == L6_load + ((S3_powered >> 2) && (!S3_powered >> 0)) );
  (L5_dir == backward) >> (L5_load == 0);
  (L5_dir == off) >> (L5_load == 0);

//Line L12
  (((L12_dir != off) && ((L2_dir == forward) || (L7_dir == backward))) >> (L12_dir == backward)) &&
  ((L12_dir == backward) >> ((L12_dir != off) && ((L2_dir == forward) || (L7_dir == backward))));
  (((L12_dir != off) && ((L11_dir == forward))) >> (L12_dir == forward)) &&
  ((L12_dir == forward) >> ((L12_dir != off) && ((L11_dir == forward))));
  (L12_dir == forward) >> (L12_load == L2_load + L7_load );
  (L12_dir == backward) >> (L12_load == L11_load + ((S2_powered >> 2) && (!S2_powered >> 0)) );
  (L12_dir == off) >> (L12_load == 0);

//Line L7
  (((L7_dir != off) && ((L8_dir == forward) || (L13_dir == forward))) >> (L7_dir == backward)) &&
  ((L7_dir == backward) >> ((L7_dir != off) && ((L8_dir == forward) || (L13_dir == forward))));
  (((L7_dir != off) && ((L2_dir == forward) || (L12_dir == forward))) >> (L7_dir == forward)) &&
  ((L7_dir == forward) >> ((L7_dir != off) && ((L2_dir == forward) || (L12_dir == forward))));
  (L7_dir == forward) >> (L7_load == L8_load + L13_load );
  (L7_dir == backward) >> (L7_load == L2_load + L12_load );
  (L7_dir == off) >> (L7_load == 0);

//Line L11
  (((L11_dir != off) && ((L12_dir == backward))) >> (L11_dir == backward)) &&
  ((L11_dir == backward) >> ((L11_dir != off) && ((L12_dir == backward))));
  (((L11_dir != off) && ((L6_dir == forward) || (L10_dir == forward))) >> (L11_dir == forward)) &&
  ((L11_dir == forward) >> ((L11_dir != off) && ((L6_dir == forward) || (L10_dir == forward))));
  (L11_dir == forward) >> (L11_load == L12_load + ((S2_powered >> 2) && (!S2_powered >> 0)) );
  (L11_dir == backward) >> (L11_load == L6_load + L10_load );
  (L11_dir == off) >> (L11_load == 0);

//Line L13
  (((L13_dir != off) && ((L7_dir == forward) || (L8_dir == forward))) >> (L13_dir == backward)) &&
  ((L13_dir == backward) >> ((L13_dir != off) && ((L7_dir == forward) || (L8_dir == forward))));
    (L13_dir != forward);
  (L13_dir == forward) >> (L13_load == L7_load + L8_load );
  (L13_dir == backward) >> (L13_load == ((S7_powered >> 2) && (!S7_powered >> 0)) + ((S6_powered >> 2) && (!S6_powered >> 0)) );
  (L13_dir == off) >> (L13_load == 0);

//Line L3
  P3_powered >> ( (L3_dir != forward) );
  !P3_powered >> (
  ((((L3_dir != off) && ((L4_dir == backward))) >> (L3_dir == forward)) &&
  ((L3_dir == forward) >> ((L3_dir != off) && ((L4_dir == backward)))))
  );
  (L3_dir == forward) >> (L3_load == 0);
  (L3_dir == backward) >> (L3_load == L4_load + ((S5_powered >> 1) && (!S5_powered >> 0)) );
  (L3_dir == off) >> (L3_load == 0);

//Line L1
  P1_powered >> ( (L1_dir != backward) );
  !P1_powered >> (
  ((((L1_dir != off) && ((L2_dir == backward))) >> (L1_dir == backward)) &&
  ((L1_dir == backward) >> ((L1_dir != off) && ((L2_dir == backward))))));

  (L1_dir == forward) >> (L1_load == L2_load + ((S1_powered >> 2) && (!S1_powered >> 0)) );
  (L1_dir == backward) >> (L1_load == 0);
  (L1_dir == off) >> (L1_load == 0);

//Line L6
  (((L6_dir != off) && ((L10_dir == forward) || (L11_dir == backward))) >> (L6_dir == backward)) &&
  ((L6_dir == backward) >> ((L6_dir != off) && ((L10_dir == forward) || (L11_dir == backward))));
  (((L6_dir != off) && ((L5_dir == forward))) >> (L6_dir == forward)) &&
  ((L6_dir == forward) >> ((L6_dir != off) && ((L5_dir == forward))));
  (L6_dir == forward) >> (L6_load == L10_load + L11_load );
  (L6_dir == backward) >> (L6_load == L5_load + ((S3_powered >> 2) && (!S3_powered >> 0)) );
  (L6_dir == off) >> (L6_load == 0);

//Line L8
  (((L8_dir != off) && ((L7_dir == forward) || (L13_dir == forward))) >> (L8_dir == backward)) &&
  ((L8_dir == backward) >> ((L8_dir != off) && ((L7_dir == forward) || (L13_dir == forward))));
  (((L8_dir != off) && ((L4_dir == forward) || (L9_dir == backward))) >> (L8_dir == forward)) &&
  ((L8_dir == forward) >> ((L8_dir != off) && ((L4_dir == forward) || (L9_dir == backward))));
  (L8_dir == forward) >> (L8_load == L7_load + L13_load );
  (L8_dir == backward) >> (L8_load == L4_load + L9_load );
  (L8_dir == off) >> (L8_load == 0);

//Sink S2
  S2_powered >> (L11_dir == forward || L12_dir == backward);

//Sink S7
  S7_powered >> (L13_dir == backward);

//Sink S5
  S5_powered >> (L3_dir == backward || L4_dir == backward);

//Sink S4
  S4_powered >> (L9_dir == forward || L10_dir == backward);

//Sink S6
  S6_powered >> (L13_dir == backward);

//Sink S3
  S3_powered >> (L5_dir == forward || L6_dir == backward);

//Sink S1
  S1_powered >> (L1_dir == forward || L2_dir == backward);