зеркало из https://github.com/microsoft/ivy.git
fixing reporting of implementations and monitors
This commit is contained in:
Родитель
685a633741
Коммит
d644b6c0ff
|
@ -1,22 +1,22 @@
|
||||||
#lang ivy1.6
|
#lang ivy1.7
|
||||||
|
|
||||||
object clock = {
|
isolate clock = {
|
||||||
type t
|
|
||||||
relation (X:t < Y:t)
|
|
||||||
|
|
||||||
property [transitivity] X:t < Y & Y < Z -> X < Z
|
type this
|
||||||
property [antisymmetry] ~(X:t < Y & Y < X)
|
relation (X:clock < Y:clock)
|
||||||
|
action incr(inp:clock) returns (out:clock)
|
||||||
action incr(inp:t) returns (out:t)
|
|
||||||
|
|
||||||
object spec = {
|
object spec = {
|
||||||
|
property [transitivity] X:clock < Y & Y < Z -> X < Z
|
||||||
|
property [antisymmetry] ~(X:clock < Y & Y < X)
|
||||||
|
|
||||||
after incr {
|
after incr {
|
||||||
assert inp < out
|
assert inp < out
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
object impl = {
|
object impl = {
|
||||||
interpret clock.t -> int
|
interpret clock -> int
|
||||||
|
|
||||||
implement incr {
|
implement incr {
|
||||||
out := inp + 1
|
out := inp + 1
|
||||||
|
@ -24,36 +24,45 @@ object clock = {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
object intf = {
|
isolate intf = {
|
||||||
action ping(x:clock.t)
|
|
||||||
action pong(x:clock.t)
|
|
||||||
}
|
|
||||||
|
|
||||||
type side_t = {left,right}
|
action ping(x:clock)
|
||||||
|
action pong(x:clock)
|
||||||
|
|
||||||
object spec = {
|
object spec = {
|
||||||
individual side : side_t
|
|
||||||
individual time : clock.t
|
|
||||||
init side = left & time = 0
|
|
||||||
|
|
||||||
before intf.ping {
|
type side_t = {left,right}
|
||||||
|
individual side : side_t
|
||||||
|
individual time : clock
|
||||||
|
|
||||||
|
after init {
|
||||||
|
side := left;
|
||||||
|
time := 0
|
||||||
|
}
|
||||||
|
|
||||||
|
before ping {
|
||||||
assert side = left & time < x;
|
assert side = left & time < x;
|
||||||
side := right;
|
side := right;
|
||||||
time := x
|
time := x
|
||||||
}
|
}
|
||||||
|
|
||||||
before intf.pong {
|
before pong {
|
||||||
assert side = right & time < x;
|
assert side = right & time < x;
|
||||||
side := left;
|
side := left;
|
||||||
time := x
|
time := x
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
object left_player = {
|
isolate left_player = {
|
||||||
|
|
||||||
individual ball : bool
|
individual ball : bool
|
||||||
individual time : clock.t
|
individual time : clock
|
||||||
init ball & time = 0
|
after init {
|
||||||
|
ball := true;
|
||||||
|
time := 0
|
||||||
|
}
|
||||||
|
|
||||||
action hit = {
|
action hit = {
|
||||||
if ball {
|
if ball {
|
||||||
|
@ -67,13 +76,18 @@ object left_player = {
|
||||||
time := x
|
time := x
|
||||||
}
|
}
|
||||||
|
|
||||||
conjecture ball -> (spec.side = left & spec.time <= time)
|
conjecture ball -> (intf.spec.side = intf.spec.left & intf.spec.time <= time)
|
||||||
}
|
}
|
||||||
|
with intf, clock
|
||||||
|
|
||||||
|
|
||||||
|
isolate right_player = {
|
||||||
|
|
||||||
object right_player = {
|
|
||||||
individual ball : bool
|
individual ball : bool
|
||||||
individual time : clock.t
|
individual time : clock
|
||||||
init ~ball
|
after init {
|
||||||
|
ball := false
|
||||||
|
}
|
||||||
|
|
||||||
action hit = {
|
action hit = {
|
||||||
if ball {
|
if ball {
|
||||||
|
@ -87,14 +101,10 @@ object right_player = {
|
||||||
time := x
|
time := x
|
||||||
}
|
}
|
||||||
|
|
||||||
conjecture ball -> (spec.side = right & spec.time <= time)
|
conjecture ball -> (intf.spec.side = intf.spec.right & intf.spec.time <= time)
|
||||||
}
|
}
|
||||||
|
with intf, clock
|
||||||
|
|
||||||
|
|
||||||
export left_player.hit
|
export left_player.hit
|
||||||
export right_player.hit
|
export right_player.hit
|
||||||
|
|
||||||
isolate iso_l = left_player with spec, clock
|
|
||||||
isolate iso_r = right_player with spec, clock
|
|
||||||
isolate iso_ci = clock
|
|
||||||
|
|
|
@ -257,11 +257,20 @@ def summarize_isolate(mod):
|
||||||
for lf in mod.labeled_conjs:
|
for lf in mod.labeled_conjs:
|
||||||
print pretty_lf(lf)
|
print pretty_lf(lf)
|
||||||
|
|
||||||
|
if mod.isolate_info.implementations:
|
||||||
|
print "\n The following action implementations are present:"
|
||||||
|
for mixer,mixee,action in sorted(mod.isolate_info.implementations,key=lambda x: x[0]):
|
||||||
|
print " {}implementation of {}".format(pretty_lineno(action),mixee)
|
||||||
|
|
||||||
if mod.actions:
|
if mod.isolate_info.monitors:
|
||||||
print "\n The following actions are present:"
|
print "\n The following action monitors are present:"
|
||||||
for actname,action in sorted(mod.actions.iteritems()):
|
for mixer,mixee,action in sorted(mod.isolate_info.monitors,key=lambda x: x[0]):
|
||||||
print " {}{}".format(pretty_lineno(action),actname)
|
print " {}monitor of {}".format(pretty_lineno(action),mixee)
|
||||||
|
|
||||||
|
# if mod.actions:
|
||||||
|
# print "\n The following actions are present:"
|
||||||
|
# for actname,action in sorted(mod.actions.iteritems()):
|
||||||
|
# print " {}{}".format(pretty_lineno(action),actname)
|
||||||
|
|
||||||
if mod.initializers:
|
if mod.initializers:
|
||||||
print "\n The following initializers are present:"
|
print "\n The following initializers are present:"
|
||||||
|
|
|
@ -739,6 +739,8 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
|
||||||
delegates = set(s.delegated() for s in mod.delegates if not s.delegee())
|
delegates = set(s.delegated() for s in mod.delegates if not s.delegee())
|
||||||
delegated_to = dict((s.delegated(),s.delegee()) for s in mod.delegates if s.delegee())
|
delegated_to = dict((s.delegated(),s.delegee()) for s in mod.delegates if s.delegee())
|
||||||
|
|
||||||
|
mod.isolate_info = im.IsolateInfo()
|
||||||
|
|
||||||
impl_mixins = defaultdict(list)
|
impl_mixins = defaultdict(list)
|
||||||
# delegate all the stub actions to their implementations
|
# delegate all the stub actions to their implementations
|
||||||
for actname,ms in mod.mixins.iteritems():
|
for actname,ms in mod.mixins.iteritems():
|
||||||
|
@ -757,6 +759,7 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
|
||||||
raise iu.IvyError(m,'multiple implementations of action {}'.format(m.mixee()))
|
raise iu.IvyError(m,'multiple implementations of action {}'.format(m.mixee()))
|
||||||
action = ia.apply_mixin(m,mod.actions[m.mixer()],action)
|
action = ia.apply_mixin(m,mod.actions[m.mixer()],action)
|
||||||
mod.actions[m.mixee()] = action
|
mod.actions[m.mixee()] = action
|
||||||
|
mod.isolate_info.implementations.append((m.mixer(),m.mixee(),action))
|
||||||
implementation_map[m.mixee()] = m.mixer()
|
implementation_map[m.mixee()] = m.mixer()
|
||||||
|
|
||||||
new_actions = {}
|
new_actions = {}
|
||||||
|
@ -795,6 +798,10 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
|
||||||
new_actions['ext:'+actname] = new_action
|
new_actions['ext:'+actname] = new_action
|
||||||
# TODO: external version is public if action public *or* called from opaque
|
# TODO: external version is public if action public *or* called from opaque
|
||||||
# public_actions.add('ext:'+actname)
|
# public_actions.add('ext:'+actname)
|
||||||
|
|
||||||
|
# record info on usage of implementations and monitors for user
|
||||||
|
if actname not in implementation_map:
|
||||||
|
mod.isolate_info.implementations.append((actname,actname,action))
|
||||||
else:
|
else:
|
||||||
# TODO: here must check that summarized action does not
|
# TODO: here must check that summarized action does not
|
||||||
# have a call dependency on the isolated module
|
# have a call dependency on the isolated module
|
||||||
|
@ -803,6 +810,12 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
|
||||||
new_actions[actname] = add_mixins(mod,actname,action,after_mixins,use_mixin,ext_mod_mixin(after_mixins))
|
new_actions[actname] = add_mixins(mod,actname,action,after_mixins,use_mixin,ext_mod_mixin(after_mixins))
|
||||||
new_actions['ext:'+actname] = add_mixins(mod,actname,action,ext_assumes_no_ver,use_mixin,ext_mod_mixin(all_mixins))
|
new_actions['ext:'+actname] = add_mixins(mod,actname,action,ext_assumes_no_ver,use_mixin,ext_mod_mixin(all_mixins))
|
||||||
|
|
||||||
|
for mixin in mod.mixins[actname]:
|
||||||
|
if use_mixin(mixin.mixer()):
|
||||||
|
mod.isolate_info.monitors.append((mixin.mixer(),mixin.mixee(),mod.actions[mixin.mixer()]))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
# figure out what is exported:
|
# figure out what is exported:
|
||||||
exported = set()
|
exported = set()
|
||||||
export_preconds = defaultdict(list)
|
export_preconds = defaultdict(list)
|
||||||
|
@ -927,6 +940,10 @@ def isolate_component(mod,isolate_name,extra_with=[],extra_strip=None,after_init
|
||||||
|
|
||||||
cone = get_mod_cone(mod,actions=new_actions,roots=exported,after_inits=after_inits)
|
cone = get_mod_cone(mod,actions=new_actions,roots=exported,after_inits=after_inits)
|
||||||
new_actions = dict((x,y) for x,y in new_actions.iteritems() if x in cone)
|
new_actions = dict((x,y) for x,y in new_actions.iteritems() if x in cone)
|
||||||
|
mod.isolate_info.implementations = [(impl,actname,action) for impl,actname,action in mod.isolate_info.implementations
|
||||||
|
if actname in new_actions or 'ext:'+actname in new_actions]
|
||||||
|
mod.isolate_info.monitors = [(mixer,mixee,action) for mixer,mixee,action in mod.isolate_info.monitors
|
||||||
|
if mixee in new_actions or 'ext:'+mixee in new_actions]
|
||||||
|
|
||||||
# Now that we have the accessible axioms, propteries inits, conjectures and actions,
|
# Now that we have the accessible axioms, propteries inits, conjectures and actions,
|
||||||
# action, we can find the accessible definitions.
|
# action, we can find the accessible definitions.
|
||||||
|
@ -1324,6 +1341,8 @@ def create_isolate(iso,mod = None,**kwargs):
|
||||||
if mod.isolates and cone_of_influence.get():
|
if mod.isolates and cone_of_influence.get():
|
||||||
raise iu.IvyError(None,'no isolate specified on command line')
|
raise iu.IvyError(None,'no isolate specified on command line')
|
||||||
# apply all the mixins in no particular order
|
# apply all the mixins in no particular order
|
||||||
|
mod.isolate_info = im.IsolateInfo()
|
||||||
|
implemented = set()
|
||||||
for name,mixins in mod.mixins.iteritems():
|
for name,mixins in mod.mixins.iteritems():
|
||||||
for mixin in mixins:
|
for mixin in mixins:
|
||||||
action1,action2 = (lookup_action(mixin,mod,a.relname) for a in mixin.args)
|
action1,action2 = (lookup_action(mixin,mod,a.relname) for a in mixin.args)
|
||||||
|
@ -1332,6 +1351,16 @@ def create_isolate(iso,mod = None,**kwargs):
|
||||||
action1 = action1.assert_to_assume()
|
action1 = action1.assert_to_assume()
|
||||||
mixed = ia.apply_mixin(mixin,action1,action2)
|
mixed = ia.apply_mixin(mixin,action1,action2)
|
||||||
mod.actions[mixed_name] = mixed
|
mod.actions[mixed_name] = mixed
|
||||||
|
triple = (mixin.mixer(),mixin.mixee(),mod.actions[mixin.mixer()])
|
||||||
|
if isinstance(mixin,ivy_ast.MixinImplementDef):
|
||||||
|
mod.isolate_info.implementations.append(triple)
|
||||||
|
implemented.add(mixin.mixee())
|
||||||
|
else:
|
||||||
|
mod.isolate_info.monitors.append(triple)
|
||||||
|
implemented.add(mixin.mixer())
|
||||||
|
for actname,action in mod.actions.iteritems():
|
||||||
|
if actname not in implemented:
|
||||||
|
mod.isolate_info.implementations.append((actname,actname,action))
|
||||||
# find the globally exported actions (all if none specified, for compat)
|
# find the globally exported actions (all if none specified, for compat)
|
||||||
if mod.exports:
|
if mod.exports:
|
||||||
mod.public_actions.clear()
|
mod.public_actions.clear()
|
||||||
|
|
|
@ -74,6 +74,7 @@ class Module(object):
|
||||||
self.proofs = [] # list of pair (labeled formula, proof)
|
self.proofs = [] # list of pair (labeled formula, proof)
|
||||||
self.named = [] # list of pair (labeled formula, atom)
|
self.named = [] # list of pair (labeled formula, atom)
|
||||||
self.subgoals = [] # (labeled formula * labeled formula list) list
|
self.subgoals = [] # (labeled formula * labeled formula list) list
|
||||||
|
self.isolate_info = None # IsolateInfo or None
|
||||||
|
|
||||||
self.sig = il.sig.copy() # capture the current signature
|
self.sig = il.sig.copy() # capture the current signature
|
||||||
|
|
||||||
|
@ -335,3 +336,11 @@ def sort_dependencies(mod,sortname):
|
||||||
return [s.rep for s in t.args[1:] if s.rep in mod.sig.sorts]
|
return [s.rep for s in t.args[1:] if s.rep in mod.sig.sorts]
|
||||||
return []
|
return []
|
||||||
|
|
||||||
|
# Holds info about isolate for user consumption
|
||||||
|
#
|
||||||
|
# -- implementations is a list of pairs (mixer,mixee,action) for present action implementaitons
|
||||||
|
# -- monitors is a list of triples (mixer,mixee,action) for present monitors
|
||||||
|
|
||||||
|
class IsolateInfo(object):
|
||||||
|
def __init__(self):
|
||||||
|
self.implementations,self.monitors = [],[]
|
||||||
|
|
Загрузка…
Ссылка в новой задаче