Pingpong soln

Here is a solution to the exercise.

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 = {
    individual ball : bool
    init ball
    var next : t   # remember the next value to send
    after init {
    next := 0;  # sart with zero
    }

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

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

}


object right_player = {
    individual ball : bool
    init ~ball
    var next : t    # remember the next value to send

    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? Is there something surprising?

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