{ "metadata": { "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.5.4" }, "name": "" }, "nbformat": 3, "nbformat_minor": 0, "worksheets": [ { "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "This example is the right part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"." ] }, { "cell_type": "code", "collapsed": true, "input": [ "import spot\n", "import spot.ltsmin\n", "spot.setup(show_default='.abr', max_states=10)\n", "# This extra line ensures that our test-suite skips this test if divine is not installed.\n", "spot.ltsmin.require('divine')" ], "language": "python", "metadata": {}, "outputs": [], "prompt_number": 1 }, { "cell_type": "code", "collapsed": true, "input": [ "%%dve adding\n", "int c=1, x1, x2;\n", "process a1 {\n", " state Q, R, S; init Q;\n", " trans Q -> R { guard c<20; effect x1 = c; },\n", " R -> S { effect x1 = x1 + c; },\n", " S -> Q { effect c = x1; };\n", "}\n", "process a2 {\n", " state Q, R, S; init Q;\n", " trans Q -> R { guard c<20; effect x2 = c; },\n", " R -> S { effect x2 = x2 + c; },\n", " S -> Q { effect c = x2; };\n", "}\n", "system async;" ], "language": "python", "metadata": {}, "outputs": [], "prompt_number": 2 }, { "cell_type": "code", "collapsed": false, "input": [ "adding" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 3, "text": [ "ltsmin model with the following variables:\n", " c: int\n", " x1: int\n", " x2: int\n", " a1: ['Q', 'R', 'S']\n", " a2: ['Q', 'R', 'S']" ] } ], "prompt_number": 3 }, { "cell_type": "code", "collapsed": false, "input": [ "adding.kripke(['a1.Q', 'c==17'])" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 4, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "t\n", "[all]\n", "\n", "\n", "0\n", "\n", "c=1, x1=0, x2=0, a1=0, a2=0\n", "a1.Q & !"c==17" & !dead\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "1\n", "\n", "c=1, x1=1, x2=0, a1=1, a2=0\n", "!a1.Q & !"c==17" & !dead\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "\n", "2\n", "\n", "c=1, x1=0, x2=1, a1=0, a2=1\n", "a1.Q & !"c==17" & !dead\n", "\n", "\n", "0->2\n", "\n", "\n", "\n", "\n", "3\n", "\n", "c=1, x1=2, x2=0, a1=2, a2=0\n", "!a1.Q & !"c==17" & !dead\n", "\n", "\n", "1->3\n", "\n", "\n", "\n", "\n", "4\n", "\n", "c=1, x1=1, x2=1, a1=1, a2=1\n", "!a1.Q & !"c==17" & !dead\n", "\n", "\n", "1->4\n", "\n", "\n", "\n", "\n", "2->4\n", "\n", "\n", "\n", "\n", "5\n", "\n", "c=1, x1=0, x2=2, a1=0, a2=2\n", "a1.Q & !"c==17" & !dead\n", "\n", "\n", "2->5\n", "\n", "\n", "\n", "\n", "6\n", "\n", "c=2, x1=2, x2=0, a1=0, a2=0\n", "...\n", "\n", "\n", "3->6\n", "\n", "\n", "\n", "\n", "7\n", "\n", "c=1, x1=2, x2=1, a1=2, a2=1\n", "...\n", "\n", "\n", "3->7\n", "\n", "\n", "\n", "\n", "4->7\n", "\n", "\n", "\n", "\n", "8\n", "\n", "c=1, x1=1, x2=2, a1=1, a2=2\n", "...\n", "\n", "\n", "4->8\n", "\n", "\n", "\n", "\n", "5->8\n", "\n", "\n", "\n", "\n", "9\n", "\n", "c=2, x1=0, x2=2, a1=0, a2=0\n", "...\n", "\n", "\n", "5->9\n", "\n", "\n", "\n", "\n", "u6\n", "\n", "...\n", "\n", "\n", "6->u6\n", "\n", "\n", "\n", "\n", "u7\n", "\n", "...\n", "\n", "\n", "7->u7\n", "\n", "\n", "\n", "\n", "u8\n", "\n", "...\n", "\n", "\n", "8->u8\n", "\n", "\n", "\n", "\n", "u9\n", "\n", "...\n", "\n", "\n", "9->u9\n", "\n", "\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7fb770097600> >" ] } ], "prompt_number": 4 }, { "cell_type": "code", "collapsed": true, "input": [ "def model_check(model, f):\n", " f = spot.formula(f)\n", " ss = model.kripke(spot.atomic_prop_collect(f))\n", " nf = spot.formula_Not(f).translate()\n", " return spot.otf_product(ss, nf).is_empty()" ], "language": "python", "metadata": {}, "outputs": [], "prompt_number": 5 }, { "cell_type": "code", "collapsed": false, "input": [ "model_check(adding, 'F(\"c==2\")')" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 6, "text": [ "True" ] } ], "prompt_number": 6 } ], "metadata": {} } ] }