search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

How to debug the following `ivy_check` generated error? #53

Open prpr2770 opened 2 years ago

prpr2770 commented 2 years ago

While using ivy v1.7 and v1.8 and using ivy_check <filename.ivy> we obtain the following error:

Isolate this:
...
RuntimeError: maximum recursion depth exceeded while calling a Python object

The error lines indicated in ... can be accessed at the following gist. An abridged version of it is provided below

  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 675, in int_update
    thing = op.int_update(domain,pvars);
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 1083, in int_update
    v = self.apply_actuals(domain,pvars,v)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 1126, in apply_actuals
    res = res.int_update(domain,pvars)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 675, in int_update
    thing = op.int_update(domain,pvars);
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 1054, in int_update
    return bind_olds_action(self.args[0].int_update(domain,pvars))
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 675, in int_update
    thing = op.int_update(domain,pvars);
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 712, in int_update
    foo = a.int_update(domain, pvars)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 675, in int_update
    thing = op.int_update(domain,pvars);
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 1083, in int_update
    v = self.apply_actuals(domain,pvars,v)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_actions.py", line 1104, in apply_actuals
    v = substitute_constants_ast(v,subst)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 20, in clone
    res = type(self)(*args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_ast.py", line 234, in clone
    return type(self)(self.rep,list(args))
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 178, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_logic_utils.py", line 176, in substitute_constants_ast
    return subs.get(ast.rep,ast)
  File "<string>", line 48, in __hash__