{
"metadata": {
"name": "",
"signature": "sha256:83724638edf025d8183ef0d5193234734b94f7e3470d9034bea411e730c834c6"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This first chunk just makes sure the version of divine instaled accepts the `--LTSmin` option. If that is not the case, this notebook should be skipped by the test suite: `sys.exit(77)` does that."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"import os, sys\n",
"srcdir = os.environ.get('srcdir', '.')\n",
"# Make sure we have divine and that it is patched to accept the --LTSmin option.\n",
"import shutil\n",
"if shutil.which(\"divine\") == None:\n",
" sys.exit(77)\n",
"import subprocess\n",
"out = subprocess.check_output(['divine', 'compile', '--help'], stderr=subprocess.STDOUT)\n",
"if b'LTSmin' not in out:\n",
" sys.exit(77)"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The real test case starts here."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot\n",
"import spot.ltsmin\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"m = spot.ltsmin.load(srcdir + '/../ltsmin/finite.dve')\n",
"m"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"text": [
"ltsmin model with the following variables:\n",
" P: ['x']\n",
" P.a: int\n",
" P.b: int"
]
}
],
"prompt_number": 3
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"m.info()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"text": [
"{'state_size': 3,\n",
" 'variables': [('P', 0), ('P.a', 1), ('P.b', 1)],\n",
" 'types': [('P', ['x']), ('int', [])]}"
]
}
],
"prompt_number": 4
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"k = m.kripke([\"P.a<1\", \"P.b>2\"])\n",
"k"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 5,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f95344639c0> >"
]
}
],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.translate('\"P.a<1\" U \"P.b>2\"'); a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 6,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f9534463de0> >"
]
}
],
"prompt_number": 6
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.otf_product(k, a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 7,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f95344637e0> >"
]
}
],
"prompt_number": 7
}
],
"metadata": {}
}
]
}