tutorials/Reproducibility - model checking.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this notebook, we show how the verification of qualitative regulatory networks can be done with different methods, which should give equivalent results, using *GINsim* and *Pint*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Model loading\n",
    "\n",
    "We load a simple model of Phage Lambda using GINsim, http://ginsim.org/node/47:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<script type=\"text/javascript\" id=\"colomoto-setup-3487121\" class=\"to-be-removed\">\n",
       "        if (typeof Jupyter != 'undefined') {\n",
       "            \n",
       "function detect_import(cell, module) {\n",
       "    var code = cell.get_text();\n",
       "    code = code.replace(/\\\\\\n/g, \"\");\n",
       "    var lines = code.split(\"\\n\");\n",
       "    var r_simple = new RegExp(\"^(\"+module+\")$\");\n",
       "    var r_alias = new RegExp(\"^\"+module+\"\\\\s+as\\\\s+(\\\\w+)$\");\n",
       "    for (var i = 0; i < lines.length; ++i) {\n",
       "        if (/^import\\s/.test(lines[i])) {\n",
       "            code = lines[i].substr(7);\n",
       "            var parts = code.split(\",\")\n",
       "            for (var j = 0; j < parts.length; ++j) {\n",
       "                code = parts[j].trim();\n",
       "                var m = code.match(r_simple);\n",
       "                if (!m) {\n",
       "                    m = code.match(r_alias);\n",
       "                }\n",
       "                if (m) {\n",
       "                    return m[1];\n",
       "                }\n",
       "            }\n",
       "        }\n",
       "    }\n",
       "    return null;\n",
       "}\n",
       "\n",
       "function colomoto_replace_call(cell, orig, dest, args, comment=false) {\n",
       "    var call_regexp = new RegExp(\"\\\\.\"+orig.replace(\".\",\"\\\\.\")+\"\\\\(\");\n",
       "    var call_replacer = new RegExp(\"\\\\.\"+orig.replace(\".\",\"\\\\.\")\n",
       "                    + \"\\\\(\\\\s*([^\\\\)]*)?\\\\)\");\n",
       "    var code = cell.get_text();\n",
       "    var lines = code.split(\"\\n\");\n",
       "    if (args) {\n",
       "        var strargs = \", \"+args.join(\", \");\n",
       "    } else {\n",
       "        var strargs = \"\";\n",
       "    }\n",
       "    for (var i = 0; i < lines.length; ++i) {\n",
       "        if (call_regexp.test(lines[i])) {\n",
       "            var code = \"\"\n",
       "            if (comment) {\n",
       "                code += \"#\"+lines[i]+\"\\n\";\n",
       "            }\n",
       "            code += lines[i].replace(call_replacer, \".\"+dest+\"($1\"+strargs+\")\")\n",
       "            lines[i] = code;\n",
       "        }\n",
       "    }\n",
       "    cell.set_text(code)\n",
       "}\n",
       "\n",
       "function colomoto_upload(Jupyter, ssid, input, py_callback_name, orig, dest) {\n",
       "\n",
       "    function callback(out_data) {\n",
       "        var cell_element = $(\"#\"+ssid).parents('.cell');\n",
       "        var cell_idx = Jupyter.notebook.get_cell_elements().index(cell_element);\n",
       "        var cell = Jupyter.notebook.get_cell(cell_idx);\n",
       "\n",
       "        var filename = out_data.content.text;\n",
       "\n",
       "        var code = cell.get_text();\n",
       "        code = code.replace(new RegExp(\"\\\\b\" + orig.replace('.', '\\\\.')\n",
       "                    + \"\\\\(\\\\s*((\\\\w+)=[^\\\\)]*)?\\\\)\"),\n",
       "                dest+\"(\\\"\"+filename+\"\\\",$1)\");\n",
       "        code = code.replace('\",)', '\")')\n",
       "        cell.set_text(code);\n",
       "\n",
       "        Jupyter.notebook.select(cell_idx);\n",
       "        Jupyter.notebook.execute_cell_and_select_below();\n",
       "    }\n",
       "\n",
       "    if (! (window.File && window.FileReader && window.FileList && window.Blob)) {\n",
       "        alert(\"Interactive file upload is not supported by your browser.\");\n",
       "        return;\n",
       "    }\n",
       "\n",
       "    input.disabled = true;\n",
       "    input.style.cursor = \"wait\";\n",
       "    input.parentElement.style.cursor = \"wait\";\n",
       "\n",
       "    var f = input.files[0];\n",
       "    var reader = new FileReader();\n",
       "    reader.onload = (function(f) {\n",
       "        return function (e) {\n",
       "            var obj = {\n",
       "                content: e.target.result,\n",
       "                name: f.name\n",
       "            };\n",
       "\n",
       "            //var pycb = py_callback_name+\"(\"+JSON.stringify(obj)+\")\"\n",
       "            // hack/workaround:\n",
       "            // it seems that Jupyter does not like very long lines\n",
       "            // so we split the data in chunks\n",
       "            var chunk_length = 100;\n",
       "            var pycb = \"__colomoto_upload_name = \" + JSON.stringify(obj.name) + \"\\n\";\n",
       "            pycb += \"__colomoto_upload_content = \\\\\\n\";\n",
       "            for (var i = 0; i < obj.content.length; i += chunk_length) {\n",
       "                pycb += \"\\\"\" + obj.content.substr(i, chunk_length)+\"\\\"\\\\\\n\"\n",
       "            }\n",
       "            pycb += \"\\n\"\n",
       "            pycb += py_callback_name+\"({'name':__colomoto_upload_name, 'content': __colomoto_upload_content})\\n\";\n",
       "            pycb += \"del __colomoto_upload_name, __colomoto_upload_content\"\n",
       "\n",
       "            IPython.notebook.kernel.execute(pycb, {iopub: {output: callback}});\n",
       "        };\n",
       "    })(f);\n",
       "    reader.readAsDataURL(f);\n",
       "}\n",
       "\n",
       "function resolve_function(tool_api, funcname) {\n",
       "    if (tool_api.hasOwnProperty(funcname)) {\n",
       "        return tool_api[funcname];\n",
       "    } else {\n",
       "        return window[funcname];\n",
       "    }\n",
       "}\n",
       "\n",
       "function colomoto_extension(Jupyter, ssid, name, menu, toolbar, tool_api) {\n",
       "\n",
       "    function insert_snippet_code(snippet) {\n",
       "        var cell = Jupyter.notebook.get_selected_cell();\n",
       "        Jupyter.notebook.edit_mode();\n",
       "        cell.code_mirror.replaceSelection(snippet, 'around');\n",
       "        //cell.focus_editor();\n",
       "    }\n",
       "\n",
       "    /**\n",
       "        from https://github.com/moble/jupyter_boilerplate/blob/master/main.js\n",
       "    */\n",
       "    function callback_insert_snippet (evt) {\n",
       "        // this (or event.currentTarget, see below) always refers to the DOM\n",
       "        // element the listener was attached to - see\n",
       "        // http://stackoverflow.com/questions/12077859\n",
       "        insert_snippet_code($(evt.currentTarget).data('snippet-code'));\n",
       "    }\n",
       "    function build_menu_element (menu_item_spec, direction) {\n",
       "        // Create the menu item html element\n",
       "        var element = $('<li/>');\n",
       "\n",
       "        if (typeof menu_item_spec == 'string') {\n",
       "            if (menu_item_spec != '---') {\n",
       "                return element.html(menu_item_spec)\n",
       "                        .addClass('ui-state-disabled')\n",
       "                        .attr({\"style\": \"padding:2px .4em\"})\n",
       "                       ;\n",
       "            }\n",
       "            return element.addClass('divider');\n",
       "        }\n",
       "\n",
       "        var a = $('<a/>')\n",
       "            .attr('href', '#')\n",
       "            .html(menu_item_spec.name)\n",
       "            .appendTo(element);\n",
       "        if (menu_item_spec.hasOwnProperty('snippet')) {\n",
       "            var snippet = menu_item_spec.snippet;\n",
       "            if (typeof snippet == 'string' || snippet instanceof String) {\n",
       "                snippet = [snippet];\n",
       "            }\n",
       "            a.attr({\n",
       "                'title' : \"\", // Do not remove this, even though it's empty!\n",
       "                'data-snippet-code' : snippet.join('\\n'),\n",
       "            })\n",
       "            .on('click', callback_insert_snippet)\n",
       "            .addClass('snippet');\n",
       "        }\n",
       "        else if (menu_item_spec.hasOwnProperty('internal-link')) {\n",
       "            a.attr('href', menu_item_spec['internal-link']);\n",
       "        }\n",
       "        else if (menu_item_spec.hasOwnProperty('external-link')) {\n",
       "            a.empty();\n",
       "            a.attr('href', menu_item_spec['external-link']);\n",
       "            a.attr({\n",
       "                'target' : '_blank',\n",
       "                'title' : 'Opens in a new window',\n",
       "            });\n",
       "            $('<i class=\"fa fa-external-link menu-icon pull-right\"/>').appendTo(a);\n",
       "            $('<span/>').html(menu_item_spec.name).appendTo(a);\n",
       "        }\n",
       "\n",
       "        if (menu_item_spec.hasOwnProperty('sub-menu')) {\n",
       "            element\n",
       "                .addClass('dropdown-submenu')\n",
       "                .toggleClass('dropdown-submenu-left', direction === 'left');\n",
       "            var sub_element = $('<ul class=\"dropdown-menu\"/>')\n",
       "                .toggleClass('dropdown-menu-compact', menu_item_spec.overlay === true) // For space-saving menus\n",
       "                .appendTo(element);\n",
       "\n",
       "            var new_direction = (menu_item_spec['sub-menu-direction'] === 'left') ? 'left' : 'right';\n",
       "            for (var j=0; j<menu_item_spec['sub-menu'].length; ++j) {\n",
       "                var sub_menu_item_spec = build_menu_element(menu_item_spec['sub-menu'][j], new_direction);\n",
       "                if(sub_menu_item_spec !== null) {\n",
       "                    sub_menu_item_spec.appendTo(sub_element);\n",
       "                }\n",
       "            }\n",
       "        }\n",
       "\n",
       "        return element;\n",
       "    }\n",
       "\n",
       "    function menu_setup (menu_item_specs, sibling, insert_before_sibling) {\n",
       "        for (var i=0; i<menu_item_specs.length; ++i) {\n",
       "            var menu_item_spec;\n",
       "            if (insert_before_sibling) {\n",
       "                menu_item_spec = menu_item_specs[i];\n",
       "            } else {\n",
       "                menu_item_spec = menu_item_specs[menu_item_specs.length-1-i];\n",
       "            }\n",
       "            var direction = (menu_item_spec['menu-direction'] == 'left') ? 'left' : 'right';\n",
       "            var menu_element = build_menu_element(menu_item_spec, direction);\n",
       "            // We need special properties if this item is in the navbar\n",
       "            if ($(sibling).parent().is('ul.nav.navbar-nav')) {\n",
       "                menu_element\n",
       "                    .addClass('dropdown')\n",
       "                    .removeClass('dropdown-submenu dropdown-submenu-left');\n",
       "                menu_element.children('a')\n",
       "                    .addClass('dropdown-toggle')\n",
       "                    .attr({\n",
       "                        'id': name+'_menu',\n",
       "                        'data-toggle' : 'dropdown',\n",
       "                        'aria-expanded' : 'false'\n",
       "                    });\n",
       "            }\n",
       "\n",
       "            // Insert the menu element into DOM\n",
       "            menu_element[insert_before_sibling ? 'insertBefore': 'insertAfter'](sibling);\n",
       "        }\n",
       "    }\n",
       "    /** end from */\n",
       "\n",
       "\n",
       "    function self_cleanup() {\n",
       "        var cell_element = $(\"script[class='to-be-removed']\").parents('.cell');\n",
       "        var cell_idx = Jupyter.notebook.get_cell_elements().index(cell_element);\n",
       "        var cell = Jupyter.notebook.get_cell(cell_idx);\n",
       "        var to_remove = -1;\n",
       "        for (var i = 0; i < cell.output_area.outputs.length; ++i) {\n",
       "            var oa = cell.output_area.outputs[i];\n",
       "            if (oa.output_type == \"display_data\"\n",
       "                && typeof oa.data[\"text/html\"] != 'undefined'\n",
       "                && oa.data[\"text/html\"].indexOf(' class=\"to-be-removed\"') >= 0) {\n",
       "                to_remove = i;\n",
       "                break;\n",
       "            }\n",
       "        }\n",
       "        if (to_remove == -1) {\n",
       "            console.log(\"cannot find toberemoved\");\n",
       "        } else {\n",
       "            cell.output_area.outputs.splice(to_remove, 1);\n",
       "        }\n",
       "    }\n",
       "\n",
       "    function toolbar_setup(actions) {\n",
       "        var buttons = [];\n",
       "        for (var i = 0; i < actions.length; ++i) {\n",
       "            var setup = actions[i].setup;\n",
       "            if (typeof setup.handler == 'string') {\n",
       "                setup.handler = resolve_function(tool_api, setup.handler);\n",
       "            }\n",
       "            buttons.push(Jupyter.actions.register(actions[i].setup,\n",
       "                actions[i].name, name));\n",
       "        }\n",
       "        $(\"#\"+name+\"-toolbar\").remove();\n",
       "        Jupyter.toolbar.add_buttons_group(buttons, name+\"-toolbar\");\n",
       "    }\n",
       "\n",
       "    function replace_menu_snippets(menu_spec, orig, dest) {\n",
       "        if (menu_spec.hasOwnProperty(\"snippet\")) {\n",
       "            var snippet = menu_spec.snippet;\n",
       "            if (typeof snippet == \"string\" || snippet instanceof String) {\n",
       "                menu_spec[\"snippet\"] = snippet.replace(orig, dest);\n",
       "            } else {\n",
       "                for (var i = 0; i < snippet.length; ++i) {\n",
       "                    menu_spec[\"snippet\"][i] = snippet[i].replace(orig, dest);\n",
       "                }\n",
       "            }\n",
       "        }\n",
       "        if (menu_spec.hasOwnProperty(\"sub-menu\")) {\n",
       "            for (var i = 0; i < menu_spec[\"sub-menu\"].length; ++i) {\n",
       "                replace_menu_snippets(menu_spec[\"sub-menu\"][i], orig, dest);\n",
       "            }\n",
       "        }\n",
       "    }\n",
       "\n",
       "    function load_ipython_extension() {\n",
       "\n",
       "        var mycellelt = $(\"#\"+ssid).parents('.cell');\n",
       "        var myidx = Jupyter.notebook.get_cell_elements().index(mycellelt);\n",
       "        var import_cell = Jupyter.notebook.get_cell(myidx);\n",
       "\n",
       "        var alias = detect_import(import_cell, name);\n",
       "        tool_api.module_alias = alias;\n",
       "        if (alias && alias != name) {\n",
       "            var orig = new RegExp(\"\\\\b\"+name+\"\\\\b\", \"g\");\n",
       "            replace_menu_snippets(menu, orig, alias);\n",
       "        }\n",
       "\n",
       "        if (toolbar) {\n",
       "            toolbar_setup(toolbar);\n",
       "        }\n",
       "\n",
       "        $(\"#\"+name+\"_menu\").parent().remove();\n",
       "        menu_setup([menu], $(\"#help_menu\").parent(), true);\n",
       "\n",
       "\n",
       "        if (tool_api.hasOwnProperty(\"post_install_callback\")) {\n",
       "            tool_api.post_install_callback();\n",
       "        }\n",
       "\n",
       "        setTimeout(self_cleanup, 5000);\n",
       "    };\n",
       "\n",
       "    load_ipython_extension();\n",
       "}\n",
       "\n",
       "function resolve_toolbar_handlers(tool_api, toolbar_spec) {\n",
       "    for (var i = 0; i < toolbar_spec.length; ++i) {\n",
       "        func = resolve_function(tool_api, toolbar_spec[i][\"setup\"][\"handler\"]);\n",
       "        toolbar_spec[i][\"setup\"][\"handler\"] = func;\n",
       "    }\n",
       "    return toolbar_spec\n",
       "}\n",
       "\n",
       "\n",
       "    var biolqm_jsapi = {  };\n",
       "    colomoto_extension(Jupyter, \"colomoto-setup-3487121\", \"biolqm\", {\"name\": \"bioLQM\", \"sub-menu\": [{\"name\": \"Upload model\", \"snippet\": [\"lqm = biolqm.upload()\"]}, {\"name\": \"Load model\", \"snippet\": [\"lqm = biolqm.load(\\\"model.sbml\\\")\"]}, \"---\", {\"name\": \"Export to file\", \"sub-menu\": [{\"name\": \"SBML-qual v1.0 (.sbml)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.sbml\\\", \\\"sbml\\\")\"]}, \"Functions formats\", {\"name\": \"BoolNet (.bnet)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.bnet\\\", \\\"bnet\\\")\"]}, {\"name\": \"BooleanNet (.booleannet)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.booleannet\\\", \\\"booleannet\\\")\"]}, {\"name\": \"BoolSim (.boolsim)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.boolsim\\\", \\\"boolsim\\\")\"]}, {\"name\": \"Raw Boolean functions (.boolfunctions)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.boolfunctions\\\", \\\"boolfunctions\\\")\"]}, {\"name\": \"Truth table (.tt)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.tt\\\", \\\"tt\\\")\"]}, \"Petri net formats\", {\"name\": \"APNN (.apnn)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.apnn\\\", \\\"apnn\\\")\"]}, {\"name\": \"INA (.ina)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.ina\\\", \\\"ina\\\")\"]}, {\"name\": \"PNML (.pnml)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.pnml\\\", \\\"pnml\\\")\"]}, \"Dedicated formats\", {\"name\": \"GINML (.ginml)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.ginml\\\", \\\"ginml\\\")\"]}, {\"name\": \"GNA non-xml (.gna)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.gna\\\", \\\"gna\\\")\"]}, {\"name\": \"MaBoSS (.bnd)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.bnd\\\", \\\"bnd\\\")\"]}, {\"name\": \"Pint (.an)\", \"snippet\": [\"biolqm.saveModel(lqm, \\\"mymodel.an\\\", \\\"an\\\")\"]}]}, {\"name\": \"Convert to tool\", \"sub-menu\": [{\"name\": \"MaBoSS\", \"snippet\": [\"masim = biolqm.to_maboss(lqm)\"]}, {\"name\": \"Pint\", \"snippet\": [\"an = biolqm.to_pint(lqm)\"]}]}]}, null, biolqm_jsapi);\n",
       "     }</script><style type=\"text/css\">\n",
       "    #biolqm_menu {\n",
       "        color: #00007f;\n",
       "        background-color: white;\n",
       "    }\n",
       "    </style>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<script type=\"text/javascript\" id=\"colomoto-setup-5173928\" class=\"to-be-removed\">\n",
       "        if (typeof Jupyter != 'undefined') {\n",
       "            \n",
       "    var ginsim_jsapi = {  };\n",
       "    colomoto_extension(Jupyter, \"colomoto-setup-5173928\", \"ginsim\", {\"name\": \"GINsim\", \"sub-menu\": [{\"name\": \"Upload model\", \"snippet\": [\"lrg = ginsim.upload()\"]}, {\"name\": \"Load model\", \"snippet\": [\"lrg = ginsim.load(\\\"model.zginml\\\")\"]}, \"---\", {\"name\": \"Export to file\", \"sub-menu\": [{\"name\": \"MaBoSS (.bnd, .cfg)\", \"snippet\": [\"ginsim.service(\\\"maboss\\\").export(lrg, \\\"mymodel.bnd\\\")\"]}]}, {\"name\": \"Convert to tool\", \"sub-menu\": [{\"name\": \"bioLQM\", \"snippet\": [\"lqm = ginsim.to_biolqm()\"]}, {\"name\": \"MaBoSS\", \"snippet\": [\"masim = ginsim.to_maboss(lrg)\"]}, {\"name\": \"NuSMV\", \"snippet\": [\"smv = ginsim.to_nusmv(lrg)\"]}, {\"name\": \"Pint\", \"snippet\": [\"an = ginsim.to_pint(lrg)\"]}]}, \"---\", {\"name\": \" Display regulatory graph\", \"snippet\": [\"ginsim.show(lrg)\"]}]}, null, ginsim_jsapi);\n",
       "     }</script><style type=\"text/css\">\n",
       "    #ginsim_menu {\n",
       "        color: blue;\n",
       "        background-color: white;\n",
       "    }\n",
       "    </style>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import ginsim"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "Downloading 'http://ginsim.org/sites/default/files/phageLambda4.zginml' to 'gen/colomotoeddv2mxsphageLambda4.zginml'"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "lrg = ginsim.load(\"http://ginsim.org/sites/default/files/phageLambda4.zginml\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Properties to be verified\n",
    "\n",
    "We use the `colomoto` python module which offers a generic interface for declaring temporal properties using either LTL or CTL."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from colomoto.temporal_logics import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "lysogenic = AG(S(CI=2))        # CI is permanently active\n",
    "lytic = AG(EF(S(CI=0,Cro=2)) & EF(S(CI=0,Cro=3)))  # Cro permanently oscillates between levels 2 and 3\n",
    "attractors = AG(EF(lysogenic | lytic))   # all the attractors are either lysogenic or lytic\n",
    "initial_state = S(CI=0,CII=0,Cro=0,N=0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "properties = {\n",
    "    \"s0_lysogenic\": If(initial_state, EF(lysogenic)), # lysogenic state is reachable from initial state  \n",
    "    \"s0_lytic\": If(initial_state, EF(lytic)),  # lytic state is reachable from initial state\n",
    "    \"attractors\": attractors, # all attractors are either lyso or lytic\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Verification using GINsim export to NuSMV"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "smv_ginsim = ginsim.to_nusmv(lrg)\n",
    "smv_ginsim.add_ctls(properties)\n",
    "smv_ginsim.alltrue()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Verification using Pint export to NuSMV"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "You are using Pint version 2017-12-19 and pypint 1.3.94"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import pypint"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We first convert to GINsim model (multi-valued network) to Pint (automata network)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "Source file is in Automata Network (an) format"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "an = ginsim.to_pint(lrg)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "smv_pint = pypint.to_nusmv(an)\n",
    "smv_pint.add_ctls(properties)\n",
    "smv_pint.alltrue()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "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.6.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}