зеркало из https://github.com/microsoft/ivy.git
59 строки
1.2 KiB
Python
59 строки
1.2 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("View")
|
|
cg.bmc_conjecture(bound=1)
|
|
# main_ui.mainloop()
|
|
|
|
|