зеркало из https://github.com/microsoft/ivy.git
37 строки
552 B
XML
37 строки
552 B
XML
#lang ivy1.7
|
|
|
|
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) = {
|
|
assume semaphore(y);
|
|
link(x,y) := true;
|
|
semaphore(y) := false
|
|
}
|
|
|
|
action disconnect(x:client,y:server) = {
|
|
assume link(x,y);
|
|
link(x,y) := false;
|
|
semaphore(y) := true
|
|
}
|
|
|
|
|
|
invariant [safety] ~(X ~= Z & link(X,Y) & link(Z,Y))
|
|
|
|
interpret client -> {0..5}
|
|
interpret server -> bv[1]
|
|
|
|
attribute method = mc
|
|
|
|
|
|
export connect
|
|
export disconnect
|