Client server example mv

type client
type server

relation link(X:client, Y:server)
relation semaphore(X:server)

after init {
    semaphore(W) := true;
    link(X,Y) := false
}

action connect(x:client,y:server) = {

require semaphore(y);

  link(x,y) := true;
  semaphore(y) := false
}

action disconnect(x:client,y:server) = {
  require link(x,y);
  link(x,y) := false;
  semaphore(y) := true
}

invariant link(X,Y) & link(Z,Y) -> X = Z

export connect
export disconnect

interpret client -> {0..2}
interpret server -> {0..1}

attribute method = mc