Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Spot Spot
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 132
    • Issues 132
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SpotSpot
  • SpotSpot
  • Issues
  • #152
Closed
Open
Issue created Feb 16, 2016 by toogy@viovene

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.

Assignee
Assign to
Time tracking