byte g1 = 0;
byte g2 = 0;
byte g3 = 0;
byte r1 = 0;
byte r2 = 0;
byte r3 = 0;

#define forallfrogs1(p) \
:: p(g1) \
:: p(g2) \
:: p(g3) \
:: p(r1) \
:: p(r2) \
:: p(r3)

#define forallfrogs2(p) \
:: p(g1, r1) \
:: p(g2, r2) \
:: p(g3, r3) \
:: p(r1, g1) \
:: p(r2, g2) \
:: p(r3, g3)

#define jumpon(x) (!(g1 == 1 || g2 == 1 || g3 == 1 || r1 == 1 || r2 == 1 || r3 == 1) && (x == 0)) -> x = 1
#define jumpfromstone(x1, x2) ((x1 == 1) && (x2 == 2)) -> x1 = 2
#define jumpacross(x1, x2) ((x2 == 1) && (x1 == 0)) -> x1 = 2

init {
    do
    forallfrogs1(jumpon)
    forallfrogs2(jumpfromstone)
    od
}

ltl win {[]!(g1 == 2 && g2 == 2 && g3 == 2 && r1 == 2 && r2 == 2 && r3 == 2 ) }