rectangle

rectangle.py

import random
# some globals
W = 6

def exe(prog, x):
    T, D, L, R = prog
    i, j = x
    return i >= L and i <= R and j >= T and j <= D

# check if a spec is satisfied
def check_sat(spec, prog):
    for (x, y) in spec:
        if exe(prog, x) != y:
            return False
    return True

# visualize a program and a spec
def visualize_spec(prog, spec):
    # use matplotlib to draw a WxW grid, put the rectangle and spec points on it
    import matplotlib.pyplot as plt
    import matplotlib.patches as patches
    fig, ax = plt.subplots()
    ax.set_xlim(0, W)
    ax.set_ylim(0, W)
    ax.set_aspect('equal')
    ax.set_title("Program: " + str(prog))

    # set a different title
    T, D, L, R = prog
    rect = patches.Rectangle((L, T), R-L, D-T, linewidth=1, edgecolor='r', facecolor='none')
    ax.add_patch(rect)
    for (coord, val) in spec:
        if val:
            ax.scatter(coord[0], coord[1], c='b')
        else:
            ax.scatter(coord[0], coord[1], c='r')
    plt.show()
    plt.clf()
    

if __name__ == '__main__':
    # the rectangle
    f = [1,4,1,5]
    # the grass, is inside
    x1 = (1,1)
    print(exe(f, x1))
    # the mushroom, is outside
    x2 = (4,0)
    print(exe(f, x2))

    # solving a problem by hand:
    spec = [((1,1), True), ((4,0), False), ((4,3), True), ((5,3), True)]
    f = [1,4,1,6]
    assert check_sat(spec, f)
    visualize_spec(f, spec)

    # now you try solve this problem by hand (find a program f that satisfies the spec)
    spec = [((1,1), False), ((4,0), True), ((4,3), True), ((5,3), False)]
    # uncomment the following and solve the problem
    # f = [None, None, None, None]
    # assert check_sat(spec, f)
    # visualize_spec(f, spec)