Pingpong

object intf = {
    action ping
    action pong
}

type side_t = {left,right}

specification {
    individual side : side_t
    after init {
        side := left
    }

    before intf.ping {
        require side = left;
        side := right
    }

    before intf.pong {
        require side = right;
        side := left
    }
}

implementation {
    isolate left_player = {
        individual ball : bool
        after init {
            ball := true
        }

        action hit = {
            if ball {
                call intf.ping;
                ball := false
            }
        }

        implement intf.pong {
            ball := true
        }

        invariant ball -> side = left
    } with this

    isolate right_player = {
        individual ball : bool
        after init {
            ball := false
        }

        action hit = {
            if ball {
                call intf.pong;
                ball := false
            }
        }

        implement intf.ping {
            ball := true
        }

        invariant ball -> side = right
    } with this
}

export left_player.hit
export right_player.hit