зеркало из https://github.com/microsoft/ivy.git
merged with master
This commit is contained in:
Ken McMillan
Коммит
b034cbcae6
15
README.md
15
README.md
|
|
@ -8,6 +8,21 @@ proofs, and supports a use model in which the human protocol designer
|
|||
and the automated tool interact to expose errors and prove
|
||||
correctness.
|
||||
|
||||
#Installation
|
||||
Linux
|
||||
On Debian-based linux ditributions such as Ubuntu, download and install the file ms-ivy_X.X_YYYY.deb where X.X is the IVy version and YYYY is the machine architecture. Use your system’s package manager to install this package, or the following commands:
|
||||
```
|
||||
$ sudo dpkg -i ms-ivy_X.X_YYYY.deb
|
||||
$ sudo apt-get install -f
|
||||
```
|
||||
The first command will report missing dependencies, which will be installed by the second command.
|
||||
|
||||
Windows
|
||||
The Windows binary distribution is in the form of a zip archive. Download the file ivy.X.Y-.Windows-z86.zip, where X.X is the IVy version (this will work on both 32-bit and 64 bit Intel Windows). Use Windows Explorer to extract this archive in the directory C:\. This should give you a directory C:\ivy. To use IVy in a command window, first execute this command:
|
||||
```
|
||||
> C:\ivy\scripts\activate
|
||||
```
|
||||
|
||||
## Further Reading
|
||||
|
||||
For further information on IVy, see [the IVy web site](http://microsoft.github.io/ivy/).
|
||||
|
|
|
|||
|
|
@ -11,13 +11,18 @@ from __future__ import division
|
|||
|
||||
from collections import deque, defaultdict
|
||||
|
||||
from pygraphviz import AGraph
|
||||
import platform
|
||||
if platform.system() == 'Windows':
|
||||
from ivy_graphviz import AGraph
|
||||
else:
|
||||
from pygraphviz import AGraph
|
||||
|
||||
|
||||
from ivy_utils import topological_sort
|
||||
|
||||
import ivy_utils as iu
|
||||
|
||||
import pygraphviz
|
||||
# import pygraphviz
|
||||
|
||||
def cubic_bezier_point(p0, p1, p2, p3, t):
|
||||
"""
|
||||
|
|
@ -92,7 +97,7 @@ def get_approximation_points(bspline):
|
|||
def _to_position(st):
|
||||
global y_origin
|
||||
sp = st.split(',')
|
||||
assert len(sp) == 2
|
||||
assert len(sp) == 2, st
|
||||
return {
|
||||
"x": float(sp[0]),
|
||||
"y": y_origin-float(sp[1]),
|
||||
|
|
|
|||
|
|
@ -357,7 +357,7 @@ def create_strat_map(assumes,asserts,macros):
|
|||
|
||||
# Simulate the Skolem functions that would be generated by AE alternations.
|
||||
|
||||
for fmla,ast in assumes + macros + asserts:
|
||||
for fmla,ast in all_fmlas:
|
||||
make_skolems(fmla,ast,True,[])
|
||||
|
||||
# Construct the stratification graph by calling `map_fmla` on all
|
||||
|
|
|
|||
|
|
@ -0,0 +1,190 @@
|
|||
# This is an interface to pydot that replaces pygraphviz, which is
|
||||
# difficult to install on Windows.
|
||||
|
||||
import pydot
|
||||
import tempfile
|
||||
import os
|
||||
from subprocess import Popen, PIPE
|
||||
|
||||
## Work around a bug in pydot parser
|
||||
|
||||
def add_elements(g, toks, defaults_graph=None,
|
||||
defaults_node=None, defaults_edge=None):
|
||||
|
||||
if defaults_graph is None:
|
||||
defaults_graph = {}
|
||||
if defaults_node is None:
|
||||
defaults_node = {}
|
||||
if defaults_edge is None:
|
||||
defaults_edge = {}
|
||||
|
||||
for elm_idx, element in enumerate(toks):
|
||||
|
||||
if isinstance(element, (pydot.Subgraph, pydot.Cluster)):
|
||||
|
||||
pydot.dot_parser.add_defaults(element, defaults_graph)
|
||||
g.add_subgraph(element)
|
||||
|
||||
elif isinstance(element, pydot.Node):
|
||||
|
||||
pydot.dot_parser.add_defaults(element, defaults_node)
|
||||
g.add_node(element)
|
||||
|
||||
elif isinstance(element, pydot.Edge):
|
||||
|
||||
pydot.dot_parser.add_defaults(element, defaults_edge)
|
||||
g.add_edge(element)
|
||||
|
||||
elif isinstance(element, pydot.dot_parser.ParseResults):
|
||||
|
||||
for e in element:
|
||||
add_elements(g, [e], defaults_graph,
|
||||
defaults_node, defaults_edge)
|
||||
|
||||
elif isinstance(element, pydot.dot_parser.DefaultStatement):
|
||||
|
||||
if element.default_type == 'graph':
|
||||
|
||||
g.obj_dict['attributes'].update(element.attrs)
|
||||
|
||||
elif element.default_type == 'node':
|
||||
|
||||
defaults_node.update(element.attrs)
|
||||
|
||||
elif element.default_type == 'edge':
|
||||
|
||||
defaults_edge.update(element.attrs)
|
||||
|
||||
else:
|
||||
raise ValueError(
|
||||
'Unknown DefaultStatement: {s}'.format(
|
||||
s=element.default_type))
|
||||
|
||||
elif isinstance(element, pydot.dot_parser.P_AttrList):
|
||||
|
||||
g.obj_dict['attributes'].update(element.attrs)
|
||||
|
||||
else:
|
||||
raise ValueError(
|
||||
'Unknown element statement: {s}'.format(s=element))
|
||||
|
||||
# pydot.dot_parser.add_elements = add_elements
|
||||
|
||||
# work around some pydot parser bugs
|
||||
|
||||
def fix_parsed_graph(g):
|
||||
for n in g.get_node('graph'):
|
||||
g.attr.update(n.attr)
|
||||
g.del_node('graph')
|
||||
g.del_node('node')
|
||||
g.del_node('edge')
|
||||
for l in g.obj_dict['nodes'].values():
|
||||
for n in l:
|
||||
fix_attrs(n)
|
||||
for l in g.obj_dict['edges'].values():
|
||||
for e in l:
|
||||
fix_attrs(e)
|
||||
fix_attrs(g.obj_dict)
|
||||
if 'bb' not in g.attr:
|
||||
g.attr['bb'] = "0,0,0,0" # empty graphs won't get bounding boxes
|
||||
for sg in g.get_subgraphs():
|
||||
fix_parsed_graph(sg)
|
||||
|
||||
def fix_attrs(t):
|
||||
t['attributes'] = dict((x,y.strip('"').replace('\\\n','')) for x,y in t['attributes'].iteritems())
|
||||
|
||||
class AGraph(object):
|
||||
def __init__(self,**kwargs):
|
||||
self.g = pydot.Dot(**kwargs)
|
||||
def add_node(self,name,**kwargs):
|
||||
return self.g.add_node(pydot.Node(name,**kwargs))
|
||||
def add_edge(self,src,dst,id,**kwargs):
|
||||
e = pydot.Edge(src,dst,id=id,**kwargs)
|
||||
return self.g.add_edge(e)
|
||||
def add_subgraph(self,nbunch=None,name=None,**kwargs):
|
||||
res = pydot.Subgraph(graph_name=name)
|
||||
if nbunch:
|
||||
ids = set(nbunch)
|
||||
edges = self.g.obj_dict['edges']
|
||||
sub_edges = res.obj_dict['edges']
|
||||
for n in self.g.get_node_list():
|
||||
if n.get_name() in ids:
|
||||
self.g.del_node(n)
|
||||
res.add_node(n)
|
||||
for e in self.g.get_edge_list():
|
||||
src,dst = e.get_source(), e.get_destination()
|
||||
if src in ids and dst in ids:
|
||||
self.g.del_edge(src,dst)
|
||||
res.add_edge(e)
|
||||
self.g.add_subgraph(res)
|
||||
def layout(self,prog='dot'):
|
||||
tmp_fd, tmp_name = tempfile.mkstemp()
|
||||
# print 'temp_name={}'.format(tmp_name)
|
||||
os.close(tmp_fd)
|
||||
self.g.write(tmp_name)
|
||||
process = Popen(['dot','-Tdot',tmp_name], stdout=PIPE)
|
||||
txt,_ = process.communicate()
|
||||
exit_code = process.wait()
|
||||
# txt = self.g.create(prog=prog,format='dot')
|
||||
# print txt
|
||||
self.g = pydot.dot_parser.parse_dot_data(txt)[0]
|
||||
fix_parsed_graph(self.g)
|
||||
def nodes(self):
|
||||
res = self.g.get_node_list()
|
||||
for sub in self.g.get_subgraphs():
|
||||
res.extend(sub.get_node_list())
|
||||
return res
|
||||
def get_edge(self,src,dst,id,g = None):
|
||||
g = g or self.g
|
||||
for e in g.get_edge(src,dst):
|
||||
if e.attr['id'] == id:
|
||||
return e
|
||||
for sg in g.get_subgraphs():
|
||||
e = self.get_edge(src,dst,id,sg)
|
||||
if e is not None:
|
||||
return e
|
||||
return None
|
||||
def get_node(self,name,g = None):
|
||||
g = g or self.g
|
||||
for e in g.get_node(name):
|
||||
return e
|
||||
for sg in g.get_subgraphs():
|
||||
e = self.get_node(name,sg)
|
||||
if e is not None:
|
||||
return e
|
||||
return None
|
||||
def subgraphs(self):
|
||||
return self.g.get_subgraphs()
|
||||
|
||||
|
||||
|
||||
def __str__(self):
|
||||
return str(self.g)
|
||||
|
||||
pydot.Common.attr = property(lambda self: self.obj_dict['attributes'])
|
||||
pydot.Subgraph.graph_attr = property(lambda self: self.obj_dict['attributes'])
|
||||
pydot.Subgraph.name = property(lambda self: self.get_name())
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
g = AGraph()
|
||||
g.add_node('1',label='foo')
|
||||
g.add_node('2',label='bar')
|
||||
g.add_edge('1','2','e1')
|
||||
g.add_subgraph(name='cluster_1',nbunch=['1','2'])
|
||||
g.add_node('3',label='foo')
|
||||
g.add_node('4',label='bar')
|
||||
g.add_edge('3','4','e1')
|
||||
g.add_subgraph(name='cluster_2',nbunch=['3','4'])
|
||||
print g
|
||||
g.layout()
|
||||
print g
|
||||
print 'nodes: {}'.format(g.g.get_node_list())
|
||||
for n in g.nodes():
|
||||
print n
|
||||
print g.get_edge('1','2','e1')
|
||||
print g.get_node('1')
|
||||
for sg in g.subgraphs():
|
||||
print sg.graph_attr['bb']
|
||||
|
||||
|
||||
|
|
@ -428,7 +428,9 @@ class ConceptGraphUI(ivy_graph_ui.GraphWidget):
|
|||
|
||||
ag = self.parent.new_ag()
|
||||
with ag.context as ac:
|
||||
post = ac.new_state(ag.init_cond)
|
||||
# post = ac.new_state(ag.init_cond)
|
||||
ag.add_initial_state(ag.init_cond)
|
||||
post = ag.states[0]
|
||||
if 'initialize' in im.module.actions:
|
||||
init_action = im.module.actions['initialize']
|
||||
post = ag.execute(init_action, None, None, 'initialize')
|
||||
|
|
|
|||
12
ivy/tk_cy.py
12
ivy/tk_cy.py
|
|
@ -25,9 +25,15 @@ def get_coord(position):
|
|||
# Get arrow information generated by dot
|
||||
|
||||
def get_arrowend(element):
|
||||
p1 = get_coord(element['data']['bspline'][-1])
|
||||
p2 = get_coord(element['data']['arrowend'])
|
||||
return p1 + p2
|
||||
d = element['data']
|
||||
if 'arrowend' in d:
|
||||
p1 = get_coord(d['bspline'][-1])
|
||||
p2 = get_coord(d['arrowend'])
|
||||
return p1 + p2
|
||||
else:
|
||||
p1 = get_coord(d['bspline'][0])
|
||||
p2 = get_coord(d['arrowstart'])
|
||||
return p2 + p1
|
||||
|
||||
# Return the dimension of an elenent as (x,y,w,h) where x and y are
|
||||
# center coords.
|
||||
|
|
|
|||
|
|
@ -1,116 +1,159 @@
|
|||
;;; ivy-mode.el --- A major mode for IVy source files
|
||||
|
||||
(setq ivy-keywords '(
|
||||
"relation"
|
||||
"individual"
|
||||
"axiom"
|
||||
"conjecture"
|
||||
"schema"
|
||||
"instantiate"
|
||||
"derived"
|
||||
"concept"
|
||||
"init"
|
||||
"action"
|
||||
"state"
|
||||
"assume"
|
||||
"assert"
|
||||
"set"
|
||||
"null"
|
||||
"old"
|
||||
"from"
|
||||
"update"
|
||||
"params"
|
||||
"in"
|
||||
"match"
|
||||
"ensures"
|
||||
"requires"
|
||||
"modifies"
|
||||
"true"
|
||||
"false"
|
||||
"fresh"
|
||||
"module"
|
||||
"type"
|
||||
"if"
|
||||
"else"
|
||||
"local"
|
||||
"let"
|
||||
"call"
|
||||
"entry"
|
||||
"macro"
|
||||
"interpret"
|
||||
"forall"
|
||||
"exists"
|
||||
"returns"
|
||||
"mixin"
|
||||
"before"
|
||||
"after"
|
||||
"isolate"
|
||||
"with"
|
||||
"export"
|
||||
"delegate"
|
||||
"import"
|
||||
"include"
|
||||
"progress"
|
||||
"rely"
|
||||
"mixord"
|
||||
"extract"
|
||||
"function"
|
||||
"class"
|
||||
"object"
|
||||
"method"
|
||||
"execute"
|
||||
"destructor"
|
||||
"some"
|
||||
"maximizing"
|
||||
"maximizing"
|
||||
"private"
|
||||
"implement"
|
||||
"using"
|
||||
"property"
|
||||
"while"
|
||||
"invariant"
|
||||
"struct"
|
||||
"definition"
|
||||
"ghost"
|
||||
"alias"
|
||||
"trusted"
|
||||
"this"
|
||||
"var"
|
||||
"instance"
|
||||
"attribute"
|
||||
"variant"
|
||||
"of"
|
||||
"proof"
|
||||
"specification"
|
||||
"implementation"
|
||||
"decreases"
|
||||
"require"
|
||||
"ensure"
|
||||
"around"
|
||||
"parameter"
|
||||
) )
|
||||
;; Copyright (c) Microsoft Corporation
|
||||
|
||||
(setq ivy-types '("bool" "int" "bv"))
|
||||
(setq ivy-constants '())
|
||||
(setq ivy-events '())
|
||||
(setq ivy-functions '())
|
||||
;; Author: Microsoft
|
||||
;; Version: 1.0
|
||||
;; URL: http://github.com/Microsoft/ivy
|
||||
;; Keywords: languages, ivy
|
||||
|
||||
(setq ivy-keywords-regexp (regexp-opt ivy-keywords 'words))
|
||||
(setq ivy-type-regexp (regexp-opt ivy-types 'words))
|
||||
(setq ivy-constant-regexp (regexp-opt ivy-constants 'words))
|
||||
(setq ivy-event-regexp (regexp-opt ivy-events 'words))
|
||||
(setq ivy-functions-regexp (regexp-opt ivy-functions 'words))
|
||||
;; Permission is hereby granted, free of charge, to any person
|
||||
;; obtaining a copy of this software and associated documentation
|
||||
;; files (the "Software"), to deal in the Software without
|
||||
;; restriction, including without limitation the rights to use, copy,
|
||||
;; modify, merge, publish, distribute, sublicense, and/or sell copies
|
||||
;; of the Software, and to permit persons to whom the Software is
|
||||
;; furnished to do so, subject to the following conditions:
|
||||
;;
|
||||
;; The above copyright notice and this permission notice shall be
|
||||
;; included in all copies or substantial portions of the Software.
|
||||
;;
|
||||
;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
;; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
|
||||
;; MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
;; NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
|
||||
;; HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
;; WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
;; OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
|
||||
;; DEALINGS IN THE SOFTWARE.
|
||||
|
||||
(setq ivy-font-lock-keywords
|
||||
`(
|
||||
(,ivy-type-regexp . font-lock-type-face)
|
||||
(,ivy-constant-regexp . font-lock-constant-face)
|
||||
(,ivy-event-regexp . font-lock-builtin-face)
|
||||
(,ivy-functions-regexp . font-lock-function-name-face)
|
||||
(,ivy-keywords-regexp . font-lock-keyword-face)
|
||||
))
|
||||
;;; Commentary:
|
||||
|
||||
(defvar ivy-indent-offset 4
|
||||
"*Indentation offset for `ivy-mode'.")
|
||||
;; A major mode for editing IVy source files.
|
||||
|
||||
;; To use this, place this file somewhere in your emacs load-path and
|
||||
;; add this code to your emacs init file:
|
||||
|
||||
;; (add-to-list 'auto-mode-alist '("\\.ivy\\'" . ivy-mode))
|
||||
;; (autoload 'ivy-mode "ivy" "Major mode for editing IVy code" t)
|
||||
|
||||
;;; Code:
|
||||
|
||||
(defconst ivy-keywords
|
||||
'("relation"
|
||||
"individual"
|
||||
"axiom"
|
||||
"conjecture"
|
||||
"schema"
|
||||
"instantiate"
|
||||
"derived"
|
||||
"concept"
|
||||
"init"
|
||||
"action"
|
||||
"state"
|
||||
"assume"
|
||||
"assert"
|
||||
"set"
|
||||
"null"
|
||||
"old"
|
||||
"from"
|
||||
"update"
|
||||
"params"
|
||||
"in"
|
||||
"match"
|
||||
"ensures"
|
||||
"requires"
|
||||
"modifies"
|
||||
"true"
|
||||
"false"
|
||||
"fresh"
|
||||
"module"
|
||||
"type"
|
||||
"if"
|
||||
"else"
|
||||
"local"
|
||||
"let"
|
||||
"call"
|
||||
"entry"
|
||||
"macro"
|
||||
"interpret"
|
||||
"forall"
|
||||
"exists"
|
||||
"returns"
|
||||
"mixin"
|
||||
"before"
|
||||
"after"
|
||||
"isolate"
|
||||
"with"
|
||||
"export"
|
||||
"delegate"
|
||||
"import"
|
||||
"include"
|
||||
"progress"
|
||||
"rely"
|
||||
"mixord"
|
||||
"extract"
|
||||
"function"
|
||||
"class"
|
||||
"object"
|
||||
"method"
|
||||
"execute"
|
||||
"destructor"
|
||||
"some"
|
||||
"maximizing"
|
||||
"maximizing"
|
||||
"private"
|
||||
"implement"
|
||||
"using"
|
||||
"property"
|
||||
"while"
|
||||
"invariant"
|
||||
"struct"
|
||||
"definition"
|
||||
"ghost"
|
||||
"alias"
|
||||
"trusted"
|
||||
"this"
|
||||
"var"
|
||||
"instance"
|
||||
"attribute"
|
||||
"variant"
|
||||
"of"
|
||||
"proof"
|
||||
"specification"
|
||||
"implementation"
|
||||
"decreases"
|
||||
"require"
|
||||
"ensure"
|
||||
"around"
|
||||
"parameter"))
|
||||
|
||||
(defconst ivy-types '("bool" "int" "bv"))
|
||||
(defconst ivy-constants '())
|
||||
(defconst ivy-events '())
|
||||
(defconst ivy-functions '())
|
||||
|
||||
(defconst ivy-keywords-regexp (regexp-opt ivy-keywords 'words))
|
||||
(defconst ivy-type-regexp (regexp-opt ivy-types 'words))
|
||||
(defconst ivy-constant-regexp (regexp-opt ivy-constants 'words))
|
||||
(defconst ivy-event-regexp (regexp-opt ivy-events 'words))
|
||||
(defconst ivy-functions-regexp (regexp-opt ivy-functions 'words))
|
||||
|
||||
(defconst ivy-font-lock-keywords
|
||||
`((,ivy-type-regexp . font-lock-type-face)
|
||||
(,ivy-constant-regexp . font-lock-constant-face)
|
||||
(,ivy-event-regexp . font-lock-builtin-face)
|
||||
(,ivy-functions-regexp . font-lock-function-name-face)
|
||||
(,ivy-keywords-regexp . font-lock-keyword-face)))
|
||||
|
||||
(defgroup ivy nil
|
||||
"Major mode for IVy source files."
|
||||
:group 'languages)
|
||||
|
||||
(defcustom ivy-indent-offset 4
|
||||
"Indentation offset for `ivy-mode'."
|
||||
:type 'integer
|
||||
:group 'ivy)
|
||||
|
||||
(defun ivy-indent-line ()
|
||||
"Indent current line for `ivy-mode'."
|
||||
|
|
@ -130,29 +173,27 @@
|
|||
(setq indent-col (- indent-col ivy-indent-offset))))
|
||||
(indent-line-to indent-col)))
|
||||
|
||||
;(defvar ivy-syntax-table nil "Syntax table for `ivy-mode'.")
|
||||
(setq ivy-syntax-table
|
||||
(let ((synTable (make-syntax-table)))
|
||||
(defvar ivy-syntax-table
|
||||
(let ((synTable (make-syntax-table)))
|
||||
|
||||
;; bash style comment: “# …”
|
||||
(modify-syntax-entry ?# "< b" synTable)
|
||||
(modify-syntax-entry ?\n "> b" synTable)
|
||||
;; bash style comment: “# …”
|
||||
(modify-syntax-entry ?# "< b" synTable)
|
||||
(modify-syntax-entry ?\n "> b" synTable)
|
||||
|
||||
synTable))
|
||||
synTable)
|
||||
"Syntax table for `ivy-mode'.")
|
||||
|
||||
;;;###autoload
|
||||
(define-derived-mode ivy-mode text-mode "Ivy"
|
||||
"Mode for editing Ivy files."
|
||||
"Major mode for editing Ivy files."
|
||||
(make-local-variable 'ivy-indent-offset)
|
||||
(set (make-local-variable 'indent-line-function) 'ivy-indent-line)
|
||||
(set (make-local-variable 'comment-start) "#")
|
||||
(set-syntax-table ivy-syntax-table)
|
||||
(setq font-lock-defaults '((ivy-font-lock-keywords))))
|
||||
|
||||
|
||||
; add this code to your .emacs:
|
||||
|
||||
; (add-to-list 'auto-mode-alist '(""\\.ivy\\'" . ivy-mode))
|
||||
; (autoload 'ivy-mode "ivy" "Major mode for editing Ivy code" t)
|
||||
|
||||
(provide 'ivy-mode)
|
||||
;; Local Variables:
|
||||
;; indent-tabs-mode: nil
|
||||
;; End:
|
||||
;;; ivy-mode.el ends here
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче