Pingpong ex

As an exercise, 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 & ...;
    side := right
    }

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

    before intf.pong {
    assert side = right & ...;
    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
    ...  # hint: remember something so the value increments

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

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

}


object right_player = {
    var ball : bool
    init ~ball
    ...

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

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

}


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