tomas@hp-blesk:~/tools/spot-0.7.1/src/tgbatest$ ./ltl2tgba -r7 -R1q -R1t -R3 -f -x -D -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))"
never { /* XF(Gp2 | F(p0 U (p1 & (!p4 | p3)))) */
T0_init:
  if
  :: (1) -> goto T0_S2
  fi;
T0_S2:
  if
  :: (!p1 || (p4 && !p3)) -> goto T0_S3
  :: (!p1 || (p4 && !p3)) -> goto T0_S2
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  :: ((p2 && !p1) || (p2 && p4 && !p3)) -> goto accept_S5
  fi;
T0_S3:
  if
  :: (!p1 || (p4 && !p3)) -> goto T0_S3
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  fi;
accept_S5:
  if
  :: (p2) -> goto accept_S5
  fi;
accept_all:
  skip
}
tomas@hp-blesk:~/tools/spot-0.7.1/src/tgbatest$ ./ltl2tgba -r7 -R1q -R1t -R3 -f -x -D -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))"
never { /* XF(Gp2 | F(p0 U (p1 & (!p4 | p3)))) */
T0_init:
  if
  :: (1) -> goto T0_S2
  fi;
T0_S2:
  if
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  :: (!p1 || (p4 && !p3)) -> goto T0_S4
  :: (!p1 || (p4 && !p3)) -> goto T0_S2
  :: ((p2 && !p1) || (p2 && p4 && !p3)) -> goto accept_S5
  fi;
T0_S4:
  if
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  :: (!p1 || (p4 && !p3)) -> goto T0_S4
  fi;
accept_S5:
  if
  :: (p2) -> goto accept_S5
  fi;
accept_all:
  skip
}
tomas@hp-blesk:~/tools/spot-0.7.1/src/tgbatest$ ./ltl2tgba -r7 -R1q -R1t -R3 -f -x -D -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))"
never { /* XF(Gp2 | F(p0 U (p1 & (!p4 | p3)))) */
T0_init:
  if
  :: (1) -> goto T0_S2
  fi;
T0_S2:
  if
  :: (!p1 || (p4 && !p3)) -> goto T0_S3
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  :: ((p2 && !p1) || (p2 && p4 && !p3)) -> goto accept_S5
  :: (!p1 || (p4 && !p3)) -> goto T0_S2
  fi;
T0_S3:
  if
  :: (!p1 || (p4 && !p3)) -> goto T0_S3
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  fi;
accept_S5:
  if
  :: (p2) -> goto accept_S5
  fi;
accept_all:
  skip
}
tomas@hp-blesk:~/tools/spot-0.7.1/src/tgbatest$ ./ltl2tgba -r7 -R1q -R1t -R3 -f -x -D -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))"
never { /* XF(Gp2 | F(p0 U (p1 & (!p4 | p3)))) */
T0_init:
  if
  :: (1) -> goto T0_S2
  fi;
T0_S2:
  if
  :: ((p1 && !p4) || (p1 && p3)) -> goto accept_all
  :: ((p2 && !p1) || (p2 && p4 && !p3)) -> goto accept_S4
  :: (!p1 || (p4 && !p3)) -> goto T0_S2
  fi;
accept_S4:
  if
  :: (p2) -> goto accept_S4
  fi;
accept_all:
  skip
}