зеркало из https://github.com/microsoft/ivy.git
64 строки
1.3 KiB
Python
64 строки
1.3 KiB
Python
|
|
import ivy.ivy_module as ivy_module
|
|
from ivy.ivy_compiler import ivy_from_string
|
|
from ivy.tk_ui import new_ui
|
|
import ivy.ivy_utils as iu
|
|
|
|
prog = """#lang ivy1.5
|
|
|
|
type client
|
|
type server
|
|
|
|
relation link(X:client, Y:server)
|
|
relation semaphore(X:server)
|
|
|
|
init semaphore(W) & ~link(X,Y)
|
|
|
|
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
|
|
}
|
|
|
|
action test = {
|
|
assert ~(X ~= Z & link(X,Y) & link(Z,Y))
|
|
}
|
|
|
|
export connect
|
|
export disconnect
|
|
export test
|
|
"""
|
|
|
|
with ivy_module.Module():
|
|
iu.set_parameters({'ui':'cti','ext':'ext'})
|
|
main_ui = new_ui()
|
|
ui = main_ui.add(ivy_from_string(prog))
|
|
main_ui.answer("OK")
|
|
ui.check_inductiveness()
|
|
# ui = ui.cti
|
|
cg = ui.current_concept_graph
|
|
cg.show_relation(cg.relation('link(X,Y)'),'+')
|
|
cg.gather()
|
|
main_ui.answer("OK")
|
|
cg.strengthen()
|
|
main_ui.answer("OK")
|
|
ui.check_inductiveness()
|
|
cg.show_relation(cg.relation('semaphore'),'+')
|
|
cg.gather()
|
|
main_ui.answer("OK")
|
|
cg.minimize_conjecture(bound=2)
|
|
main_ui.answer("OK")
|
|
cg.strengthen()
|
|
main_ui.answer("OK")
|
|
if not ui.check_inductiveness():
|
|
print "result of inductiveness check should have been true"
|
|
exit(1)
|
|
|
|
|