зеркало из https://github.com/microsoft/ivy.git
Added ivy_bmc.py and hide redundent graphs and buttons from IvyMain widget.
This commit is contained in:
Oded Padon
Родитель
c37af5048c
Коммит
262bd8c981
|
|
@ -67,7 +67,7 @@ instantiate total_order(le)
|
|||
|
||||
# A function relating a node to its id
|
||||
individual idn(X:node) : id
|
||||
axiom idn(X)=idn(Y) -> X=Y # the id function is injective
|
||||
axiom idn(X)=idn(Y) -> X=Y # the idn function is injective
|
||||
|
||||
# A relation that keeps track of nodes that think they are the leader
|
||||
relation leader(N:node)
|
||||
|
|
@ -119,7 +119,7 @@ conjecture leader(X) -> le(idn(Y), idn(X)) # leader has highest id
|
|||
|
||||
|
||||
# conjectures obtained via CTI's
|
||||
conjecture ~(le(idn(N1),idn(N0)) & pending(idn(N1),N1) & idn(N1) ~= idn(N0))
|
||||
conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.le(N0,N1) & ring.le(N2,N0) & N0 ~= N2 & N1 ~= N0)
|
||||
conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.le(N0,N1) & ring.le(N1,N2) & N1 ~= N0)
|
||||
conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.le(N1,N2) & ring.le(N2,N0) & N0 ~= N2)
|
||||
# conjecture ~(le(idn(N1),idn(N0)) & pending(idn(N1),N1) & idn(N1) ~= idn(N0))
|
||||
# conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.le(N0,N1) & ring.le(N2,N0) & N0 ~= N2 & N1 ~= N0)
|
||||
# conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.le(N0,N1) & ring.le(N1,N2) & N1 ~= N0)
|
||||
# conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.le(N1,N2) & ring.le(N2,N0) & N0 ~= N2)
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@ instantiate total_order(le)
|
|||
|
||||
# A function relating a node to its id
|
||||
individual idn(X:node) : id
|
||||
axiom idn(X)=idn(Y) -> X=Y # the id function is injective
|
||||
axiom idn(X)=idn(Y) -> X=Y # the idn function is injective
|
||||
|
||||
# A relation that keeps track of nodes that think they are the leader
|
||||
relation leader(N:node)
|
||||
|
|
@ -128,5 +128,5 @@ conjecture leader(X) -> le(idn(Y), idn(X)) # leader has highest id
|
|||
|
||||
|
||||
# conjectures obtained via CTI's
|
||||
conjecture ~(le(idn(N1),idn(N0)) & pending(idn(N1),N1) & idn(N1) ~= idn(N0))
|
||||
conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.btw(N0,N1,N2) & N1 ~= N0)
|
||||
# conjecture ~(le(idn(N1),idn(N0)) & pending(idn(N1),N1) & idn(N1) ~= idn(N0))
|
||||
# conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.btw(N0,N1,N2) & N1 ~= N0)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,118 @@
|
|||
#lang ivy1.3
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# A module for axiomatizing a total order
|
||||
#
|
||||
################################################################################
|
||||
|
||||
module total_order(r) = {
|
||||
axiom r(X,X) # Reflexivity
|
||||
axiom r(X, Y) & r(Y, Z) -> r(X, Z) # Transitivity
|
||||
axiom r(X, Y) & r(Y, X) -> X = Y # Anti-symmetry
|
||||
axiom r(X, Y) | r(Y, X) # Totality
|
||||
}
|
||||
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Module describing a ring topology.
|
||||
#
|
||||
# The module includes a ring_head and ring_tail elements, and a ring
|
||||
# total order relation.
|
||||
#
|
||||
# The module also includes get_next and get_prev actions.
|
||||
#
|
||||
# In this module, the ring topology is arbitrary and fixed.
|
||||
#
|
||||
################################################################################
|
||||
|
||||
module ring_topology(carrier) = {
|
||||
individual head:carrier # ring head
|
||||
individual tail:carrier # ring tail
|
||||
relation le(X:carrier,Y:carrier) # total order describing ring topology
|
||||
|
||||
# Axioms that ensure that le is a total order, with head the
|
||||
# minimal element and tail the maximal element.
|
||||
instantiate total_order(le) # total order
|
||||
axiom le(head, X) # head is minimal
|
||||
axiom le(X, tail) # tail is maximal
|
||||
|
||||
action get_next(x:carrier) returns (y:carrier) = {
|
||||
assume (x = tail & y = head) | (le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)))
|
||||
}
|
||||
|
||||
action get_prev(y:carrier) returns (x:carrier) = {
|
||||
assume (x = tail & y = head) | (le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)))
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Types, relations and functions describing state of the network
|
||||
#
|
||||
################################################################################
|
||||
|
||||
type node
|
||||
type id
|
||||
|
||||
# A ring topology of nodes
|
||||
instantiate ring : ring_topology(node)
|
||||
|
||||
# A total order on ids
|
||||
relation le(X:id, Y:id)
|
||||
instantiate total_order(le)
|
||||
|
||||
# A function relating a node to its id
|
||||
individual idn(X:node) : id
|
||||
# BUG - the fact that idn is injective is commented out:
|
||||
# axiom idn(X)=idn(Y) -> X=Y # the idn function is injective
|
||||
|
||||
# A relation that keeps track of nodes that think they are the leader
|
||||
relation leader(N:node)
|
||||
init ~leader(N)
|
||||
|
||||
# A relation for pending messages, a message is just an id
|
||||
relation pending(V:id, N:node) # The identity V is pending at node N
|
||||
init ~pending(V, N)
|
||||
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Protocol description
|
||||
#
|
||||
# Two action: send and receive
|
||||
#
|
||||
################################################################################
|
||||
|
||||
action send = {
|
||||
local n1:node, n2:node {
|
||||
# send my own id to the next node
|
||||
n2 := ring.get_next(n1);
|
||||
pending(idn(n1), n2) := true
|
||||
}
|
||||
}
|
||||
|
||||
action receive = {
|
||||
local n1:node, n2:node, m:id {
|
||||
# receive a message from the right neighbor
|
||||
assume pending(m, n1);
|
||||
pending(m, n1) := *; # abstract the number of pending messages
|
||||
if m = idn(n1) { # Found a leader
|
||||
leader(n1) := true
|
||||
} else {
|
||||
if le(idn(n1), m) { # pass message to next node
|
||||
n2 := ring.get_next(n1);
|
||||
pending(m, n2) := true
|
||||
} # otherwise drop the message...
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
export send
|
||||
export receive
|
||||
|
||||
# The safety property:
|
||||
conjecture leader(X) & leader(Y) -> X = Y # at most one leader
|
||||
|
|
@ -0,0 +1,111 @@
|
|||
#
|
||||
# Copyright (c) Microsoft Corporation. All Rights Reserved.
|
||||
#
|
||||
"""
|
||||
Script to create a new notebook for a given .ivy file, that is
|
||||
used to BMC the conjectures to debug the model.
|
||||
|
||||
Usage:
|
||||
python ivy_bmc.py ivy_filename
|
||||
"""
|
||||
|
||||
import re
|
||||
import sys
|
||||
import os
|
||||
from os.path import dirname, join, pardir, pathsep, abspath
|
||||
|
||||
import IPython
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
#ivy_filename = abspath(sys.argv[1])
|
||||
ivy_filename = sys.argv[1]
|
||||
|
||||
notebook_source = r"""{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"metadata": {
|
||||
"collapsed": false,
|
||||
"scrolled": true
|
||||
},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from IPython.display import display\n",
|
||||
"import z3\n",
|
||||
"z3.set_param('smt.random_seed', 0)\n",
|
||||
"import random\n",
|
||||
"random.seed(0)\n",
|
||||
"from proof import AnalysisSession\n",
|
||||
"from widget_analysis_session import AnalysisSessionWidget\n",
|
||||
"from tactics_api import *\n",
|
||||
"import tactics_api as ta\n",
|
||||
"import ivy_actions\n",
|
||||
"from tactics import *\n",
|
||||
"from logic import *\n",
|
||||
"from ivy_logic_utils import true_clauses, false_clauses, Clauses\n",
|
||||
"import ivy_module\n",
|
||||
"from ivy_interp import EvalContext\n",
|
||||
"m = ivy_module.Module()\n",
|
||||
"m.__enter__()\n",
|
||||
"ctx = EvalContext(check=False)\n",
|
||||
"ctx.__enter__()\n",
|
||||
"ivy_widget = AnalysisSessionWidget()\n",
|
||||
"session = AnalysisSession('leader_election_ring_bug.ivy', ivy_widget)\n",
|
||||
"set_context(session)\n",
|
||||
"ivy_widget.transition_view.conjectures = session.analysis_state.ivy_interp.conjs[:]\n",
|
||||
"ta._ivy_ag.actions.setdefault('initialize', ivy_actions.Sequence())\n",
|
||||
"ta._ivy_ag.actions.setdefault('step', ta.get_big_action())\n",
|
||||
"ivy_widget.transition_view.autodetect_transitive()\n",
|
||||
"display(ivy_widget)\n",
|
||||
"ivy_widget.transition_view.bmc_bound.value = 5\n",
|
||||
"if ivy_widget.transition_view.bmc_conjecture(None, ta.and_clauses(*ta._ivy_interp.conjs), True, False):\n",
|
||||
" for conj in ta._ivy_interp.conjs[-1:]:\n",
|
||||
" if ivy_widget.transition_view.bmc_conjecture(None, conj, True):\n",
|
||||
" break"
|
||||
]
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
"kernelspec": {
|
||||
"display_name": "Python 2",
|
||||
"language": "python",
|
||||
"name": "python2"
|
||||
},
|
||||
"language_info": {
|
||||
"codemirror_mode": {
|
||||
"name": "ipython",
|
||||
"version": 2
|
||||
},
|
||||
"file_extension": ".py",
|
||||
"mimetype": "text/x-python",
|
||||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython2",
|
||||
"version": "2.7.6"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 0
|
||||
}
|
||||
""".replace('IVY_FILENAME', repr(ivy_filename))
|
||||
|
||||
# if X.bmc.ipynb exists, open it, otherwise create a new X.ivy.bmc.ipynb
|
||||
notebook_filename = ivy_filename[:-4] + '.bmc.ipynb'
|
||||
if os.path.isfile(notebook_filename):
|
||||
print "Opening existing notebook: {}".format(notebook_filename)
|
||||
else:
|
||||
notebook_filename = ivy_filename + '.bmc.ipynb'
|
||||
print "Creating new notebook: {}".format(notebook_filename)
|
||||
open(notebook_filename, 'w').write(notebook_source)
|
||||
|
||||
d = dirname(__file__)
|
||||
os.environ['PYTHONPATH'] = pathsep.join([
|
||||
os.environ['PYTHONPATH'],
|
||||
d,
|
||||
join(d, pardir, 'src', 'ivy'),
|
||||
])
|
||||
sys.argv = ['ipython', 'notebook', notebook_filename]
|
||||
sys.argv[0] = re.sub(r'(-script\.pyw|\.exe)?$', '', sys.argv[0])
|
||||
sys.exit(IPython.start_ipython())
|
||||
|
|
@ -897,7 +897,7 @@ class TransitionViewWidget(ConceptSessionControls):
|
|||
|
||||
return result
|
||||
|
||||
def bmc_conjecture(self, button=None):
|
||||
def bmc_conjecture(self, button=None, conjecture=None, verbose=False, add_to_crg=True):
|
||||
import ivy_transrel
|
||||
import ivy_solver
|
||||
from proof import ProofGoal
|
||||
|
|
@ -909,7 +909,11 @@ class TransitionViewWidget(ConceptSessionControls):
|
|||
step_action = ta.get_action('step')
|
||||
n_steps = self.bmc_bound.value
|
||||
|
||||
conj = self.get_selected_conjecture()
|
||||
if conjecture is None:
|
||||
conj = self.get_selected_conjecture()
|
||||
else:
|
||||
conj = conjecture
|
||||
|
||||
assert conj.is_universal_first_order()
|
||||
used_names = frozenset(x.name for x in self.session.analysis_state.ivy_interp.sig.symbols.values())
|
||||
def witness(v):
|
||||
|
|
@ -923,11 +927,23 @@ class TransitionViewWidget(ConceptSessionControls):
|
|||
ac.new_state(ag.init_cond)
|
||||
post = ag.execute(init_action, None, None, 'initialize')
|
||||
for n in range(n_steps):
|
||||
res = ag.bmc(post, clauses, ta._analysis_state.crg)
|
||||
res = ag.bmc(post, clauses, ta._analysis_state.crg if add_to_crg else None)
|
||||
if verbose:
|
||||
if res is None:
|
||||
msg = 'BMC with bound {} did not find a counter-example to:\n{}'.format(
|
||||
n,
|
||||
str(conj.to_formula()),
|
||||
)
|
||||
else:
|
||||
msg = 'BMC with bound {} found a counter-example to:\n{}'.format(
|
||||
n,
|
||||
str(conj.to_formula()),
|
||||
)
|
||||
print '\n' + msg + '\n'
|
||||
if res is not None:
|
||||
ta.step()
|
||||
self.show_result('BMC with bound {} found a counter-example to:\n{}'.format(
|
||||
n_steps,
|
||||
n,
|
||||
str(conj.to_formula()),
|
||||
))
|
||||
return True
|
||||
|
|
@ -1301,28 +1317,28 @@ class AnalysisSessionWidget(object):
|
|||
|
||||
HBox(
|
||||
[
|
||||
HBox(
|
||||
[self.proof_graph],
|
||||
flex=1,
|
||||
height='100%',
|
||||
overflow_x='hidden',
|
||||
overflow_y='hidden',
|
||||
_css=[
|
||||
(None, 'margin-right', '5px'),
|
||||
(None, 'min-width', '150px'),
|
||||
],
|
||||
),
|
||||
HBox(
|
||||
[self.arg],
|
||||
flex=2,
|
||||
height='100%',
|
||||
overflow_x='hidden',
|
||||
overflow_y='hidden',
|
||||
_css=[
|
||||
(None, 'margin-right', '5px'),
|
||||
(None, 'min-width', '150px'),
|
||||
],
|
||||
),
|
||||
# HBox(
|
||||
# [self.proof_graph],
|
||||
# flex=1,
|
||||
# height='100%',
|
||||
# overflow_x='hidden',
|
||||
# overflow_y='hidden',
|
||||
# _css=[
|
||||
# (None, 'margin-right', '5px'),
|
||||
# (None, 'min-width', '150px'),
|
||||
# ],
|
||||
# ),
|
||||
# HBox(
|
||||
# [self.arg],
|
||||
# flex=2,
|
||||
# height='100%',
|
||||
# overflow_x='hidden',
|
||||
# overflow_y='hidden',
|
||||
# _css=[
|
||||
# (None, 'margin-right', '5px'),
|
||||
# (None, 'min-width', '150px'),
|
||||
# ],
|
||||
# ),
|
||||
widgets.HBox(
|
||||
[self.crg],
|
||||
flex=1,
|
||||
|
|
@ -1341,14 +1357,14 @@ class AnalysisSessionWidget(object):
|
|||
(None, 'margin-bottom', '5px'),
|
||||
],
|
||||
),
|
||||
self.select_abstractor,
|
||||
#self.select_abstractor,
|
||||
self.info_area,
|
||||
self.step_box,
|
||||
widgets.HBox(
|
||||
self.buttons,
|
||||
width='100%',
|
||||
overflow_y='hidden',
|
||||
),
|
||||
#self.step_box,
|
||||
# widgets.HBox(
|
||||
# self.buttons,
|
||||
# width='100%',
|
||||
# overflow_y='hidden',
|
||||
# ),
|
||||
]
|
||||
|
||||
self.arg_node_events = [
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче