Pingpong soln

As an exercize, let's try elaborating the pingpong example a bit.

We'll add a numeric parameter to actions ping and pong. We want to specify the the paramater of ping is always even and the parameter of pong is always odd.

type t

object intf = {
    action ping(val:t)
    action pong(val:t)
}

Modify the specification here. Hint: IVy doesn't have a "mod" operator, but you canwrite "x is even" like this: (x/2) * 2 = x.

type side_t = {left,right}

object spec = {
    var side : side_t

    after init {
        side := left
    }

    before intf.ping {
        assert side = left & (val/2)*2 = val;
        side := right
    }

When pong occurs, the ball must be on the rightr. It moves to the left.

    before intf.pong {
        assert side = right & (val/2)*2+1 = val;
        side := left
    }
}

Modify the left player and right players so that the parameter values start at zero and increment with each ping or pong.

object left_player = {
    var ball : bool
    init ball
    var next : t
    after init {
        next := 0;
    }

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

    implement intf.pong(val:t) {
        ball := true;
        next := val + 1;
    }

}


object right_player = {
    var ball : bool
    init ~ball
    var next : t

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

    implement intf.ping(val:t) {
        ball := true;
        next := val + 1;
    }

}


export left_player.hit
export right_player.hit

trusted isolate iso_l = left_player with spec
trusted isolate iso_r = right_player with spec

Remember, we need to interpret the type t:

interpret t -> bv[4]

Now test both isolates. What do you notice about the parameter values generated by the tester?

We can compile and test the two isolates with these commands:

$ ivy_to_cpp target=test isolate=iso_l build=true pingpong.ivy
$ ./pingpong
$ ivy_to_cpp target=test isolate=iso_r build=true pingpong.ivy
$ ./pingpong

Of course, we have to check that we acutally have verified all the assertions. This can be done with the following command:

$ ivy_check pingpong.ivy

Note: to run ivy on the command line in Windows, you need to first do this:

> c:\ivy\scripts\activate.bat