channel CIO {
    out force(f:Pair, gravity(y:Double)) == pair(0.0, y)
    out time(t:Double, gravity(y)) == t + 0.01
}
channel CIO2 {
    out move(v:Pair, moveX(x:Double)) == pair(x, snd(v))    
    out move(v, moveY(y:Double)) == pair(fst(v), y) 
}
channel CIO3 {
    out mass(m:Double, setMass(x:Double)) == x
}
channel CIO4 {
    out ground(g:Bool, openHole) == false
    out ground(g, closeHole) == true
}
channel C1 {
    ref onground(o, update1(f2, m2, o))
    in force(f, update1(f2, m2, o)) == f2
    in mass(m, update1(f2, m2, o)) == m2
    out acceleration(a:Pair, update1(f2, m2, o)) == if(o, pair(fst(f2) / m2, 0.0), pair(fst(f2) / m2, snd(f2) / m2))
}
channel C2 {
    ref onground(o, update3(a2, o))
    in acceleration(a, update3(a2, o)) == a2
    out velocity(v:Pair, update3(a2, o)) == if(and(o, lt(snd(v), 0.0)), 
                                                    pair(fst(v) + 0.01 * fst(a2), 0.0), 
                                                    pair(fst(v) + 0.01 * fst(a2), snd(v) + 0.01 * snd(a2)))
}
channel C3 {
    ref onground(o, update4(m2, o))
    in move(m, update4(m2, o)) == m2
    out velocity(v:Pair, update4(m2, o)) == if(and(o, ge(snd(m2), 0.0)), m2, v)
}
channel C4 {
    in velocity(v, update5(v2, g)) == v2
    ref ground(g, update5(v2, g))
    out position(p:Pair, update5(v2, g)) == if(and(eq(g, true), lt(snd(p) + 0.01 * snd(v2), 0.0)), 
                                                    pair(fst(p) + 0.01 * fst(v2), 0.0), 
                                                    pair(fst(p) + 0.01 * fst(v2), snd(p) + 0.01 * snd(v2)))
}
channel C5 {
    in position(p, update2(p2, g2)) == p2
    in ground(g, update2(p2, g2)) == g2
    out onground(o:Bool, update2(p2, g2)) == and(eq(g2, true), le(snd(p2), 0.0))
}
channel C6 {
    in position(p, update6(p2)) == p2
    out clear(c:Bool, update6(p2)) == if(gt(fst(p2), 100.0), true, false)
    out gameover(go:Bool, update6(p2)) == if(lt(snd(p2), -1.0), true, false)
}