Client-server example for Mypyvy, ported from Ivy

client_server.pyv

# https://github.com/Microsoft/ivy/blob/master/doc/examples/client_server_example.md#discovering-a-safety-invariant

sort client
sort server

mutable relation link(client, server)
mutable relation semaphore(server)

init semaphore(S)
init !link(C, S)

# The atomic actions of the system are declared as "transitions", 
# which are written as two-state formulas possibly parameterized 
# by some values (such as `c` in `connect` here).
# Each transition also specifies an optional `modifies` clause, 
# whose meaning is to add "doesn't change" conjuncts for all
# elements of the state that are not modified.
transition connect(c: client, s: server)
    modifies link, semaphore

    old(semaphore(s)) &
    (link(C, S) <-> old(link(C, S)) | C = c & S = s) &
    (semaphore(S) <-> old(semaphore(S)) & S != s)
    
transition disconnect(c: client, s: server)
    modifies link, semaphore

    link(c, s) &
    (link(C, S) <-> old(link(C, S)) & C != c & S != s) & # verbose syntax for "remove `c` from the `link` relation"
    semaphore(S) <-> old(semaphore(S)) | S = s

safety [mutex] link(C1, S) & link(C2, S) -> C1 = C2

invariant !(exists c0:client, c1: client, s0:server. c0 != c1 & link(c0, s0) & link(c1, s0))
invariant !(exists c0:client, c1: client, s0:server. c0 != c1 & link(c0, s0) & semaphore(s0))