GitLab

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.