{ "metadata": { "name": "", "signature": "sha256:d5994cc04991eaf218539c16319f17128cf42be5d813785fd977ee3d991a5c00" }, "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', ['P.a<1', 'P.b>2'])\n", "m" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 3, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "P.a=0, P.b=0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "1\n", "\n", "P.a=1, P.b=0\n", "\n", "\n", "0->1\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "12\n", "\n", "P.a=0, P.b=1\n", "\n", "\n", "0->12\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "2\n", "\n", "P.a=2, P.b=0\n", "\n", "\n", "1->2\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "9\n", "\n", "P.a=1, P.b=1\n", "\n", "\n", "1->9\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "12->9\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "13\n", "\n", "P.a=0, P.b=2\n", "\n", "\n", "12->13\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "3\n", "\n", "P.a=3, P.b=0\n", "\n", "\n", "2->3\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "4\n", "\n", "P.a=2, P.b=1\n", "\n", "\n", "2->4\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "9->4\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "10\n", "\n", "P.a=1, P.b=2\n", "\n", "\n", "9->10\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "3->3\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & dead\n", "\n", "\n", "5\n", "\n", "P.a=3, P.b=1\n", "\n", "\n", "4->5\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "6\n", "\n", "P.a=2, P.b=2\n", "\n", "\n", "4->6\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "5->5\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & dead\n", "\n", "\n", "7\n", "\n", "P.a=3, P.b=2\n", "\n", "\n", "6->7\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "8\n", "\n", "P.a=2, P.b=3\n", "\n", "\n", "6->8\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "7->7\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & dead\n", "\n", "\n", "8->8\n", "\n", "\n", "!"P.a<1" & "P.b>2" & dead\n", "\n", "\n", "10->6\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "11\n", "\n", "P.a=1, P.b=3\n", "\n", "\n", "10->11\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "11->11\n", "\n", "\n", "!"P.a<1" & "P.b>2" & dead\n", "\n", "\n", "13->10\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "14\n", "\n", "P.a=0, P.b=3\n", "\n", "\n", "13->14\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "14->14\n", "\n", "\n", ""P.a<1" & "P.b>2" & dead\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f40740974e0> >" ] } ], "prompt_number": 3 }, { "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": 4, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "I->1\n", "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", ""P.a<1" & !"P.b>2"\n", "\n", "\n", "0\n", "\n", "\n", "0\n", "\n", "\n", "1->0\n", "\n", "\n", ""P.b>2"\n", "\n", "\n", "0->0\n", "\n", "\n", "1\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f40740977e0> >" ] } ], "prompt_number": 4 }, { "cell_type": "code", "collapsed": false, "input": [ "spot.otf_product(m, a)" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 5, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "P.a=0, P.b=0 * 1\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "1\n", "\n", "P.a=1, P.b=0 * 1\n", "\n", "\n", "0->1\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "2\n", "\n", "P.a=0, P.b=1 * 1\n", "\n", "\n", "0->2\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "3\n", "\n", "P.a=1, P.b=1 * 1\n", "\n", "\n", "2->3\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "4\n", "\n", "P.a=0, P.b=2 * 1\n", "\n", "\n", "2->4\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "5\n", "\n", "P.a=1, P.b=2 * 1\n", "\n", "\n", "4->5\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "6\n", "\n", "P.a=0, P.b=3 * 1\n", "\n", "\n", "4->6\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", "\n", "7\n", "\n", "P.a=0, P.b=3 * 0\n", "\n", "\n", "6->7\n", "\n", "\n", ""P.a<1" & "P.b>2" & dead\n", "\n", "\n", "7->7\n", "\n", "\n", ""P.a<1" & "P.b>2" & dead\n", "\u24ff\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f4074097720> >" ] } ], "prompt_number": 5 }, { "cell_type": "code", "collapsed": false, "input": [], "language": "python", "metadata": {}, "outputs": [], "prompt_number": 5 } ], "metadata": {} } ] }