iPython kernel crash, modelcheck function
The following code makes an iPython kernel crash:
# coding: utf-8
# In[3]:
import spot
# In[4]:
import spot.ltsmin
spot.setup()
# In[5]:
get_ipython().run_cell_magic('dve', 'm', 'int f = 3;\nprocess R {\n int p = 1, found = 0;\n state i, e;\n init i;\n trans\n i -> i {guard p != f; effect p = p + 1;},\n i -> e {guard p == f; effect found = 1;},\n e -> e {};\n}\nsystem async;')
# In[6]:
m
# In[7]:
k = m.kripke(['R.found']); k
# In[8]:
a = spot.translate('!(F (G "R.found"))', 'ba'); a
# In[9]:
p = spot.otf_product(k, a); p
# In[10]:
p.is_empty()
# In[11]:
def modelcheck(ltl_formula, model):
a = spot.translate(ltl_formula)
k = m.kripke([ap.ap_name() for ap in a.ap()])
p = spot.otf_product(k, a)
return p.is_empty()
# In[12]:
p = modelcheck('X "R.found"', m)
However, when modelcheck
returns p
instead of p.is_empty()
and we then call p.is_empty()
outside the modelcheck
function, it doesn't crash.