{
    "info": {
        "author": "Alberto Casagrande",
        "author_email": "acasagrande@units.it",
        "bugtrack_url": null,
        "classifiers": [
            "Development Status :: 4 - Beta",
            "Environment :: Console",
            "Intended Audience :: Developers",
            "Intended Audience :: Information Technology",
            "License :: OSI Approved :: GNU General Public License v2 (GPLv2)",
            "Operating System :: OS Independent",
            "Programming Language :: Python",
            "Programming Language :: Python :: 2.7",
            "Programming Language :: Python :: 3.6",
            "Topic :: Scientific/Engineering"
        ],
        "description": "# pyModelChecking\n*pyModelChecking* is a small Python model checking package. Currently, it is able to represent\n[Kripke structures][Kripke], [CTL][CTL], [LTL][LTL], and [CTL*][CTLS] formulas and\nit provides [model checking][modelchecking] methods for LTL, CTL, and CTL*.\nIn future, it will hopefully support symbolic model checking.\n\n[Kripke]: https://en.wikipedia.org/wiki/Kripke_structure_%28model_checking%29\n[CTL]: https://en.wikipedia.org/wiki/Computation_tree_logic\n[modelchecking]: https://en.wikipedia.org/wiki/Model_checking\n[LTL]: https://en.wikipedia.org/wiki/Linear_temporal_logic\n[CTLS]: https://en.wikipedia.org/wiki/CTL*\n\n### Documentation\n\n[Here][last_doc] you can find the *pyModelChecking* documenation. It contains:\n* a brief introduction to Kripke structures, temporal logics and model checking\n* the user manual and some examples\n* the API manual  \n\n[last_doc]: https://pymodelchecking.readthedocs.io/\n\n### Examples\n\nFirst of all, import all the functions and all the classes in the package.\n\n```python\n>>> from pyModelChecking import *\n```\n\nIn order to represent a Kripke structure use the `Kripke` class.\n\n```\n>>> K=Kripke(R=[(0,0),(0,1),(1,2),(2,2),(3,3)],\n...          L={0: set(['p']), 1:set(['p','q']),3:set(['p'])})\n```\n\nCTL can be represented by importing the `CTL` module.\n\n```python\n>>> from pyModelChecking.CTL import *\n\n>>> phi=AU(True,Or('q',Not(EX('p'))))\n\n>>> print(phi)\n\nA(True U (q or not (EX p)))\n```\n\nWhenever a non-CTL formula is built, an exception is thrown.\n\n```python\n>>> psi=A(F(G('p')))\nTraceback (most recent call last):\n  File \"<stdin>\", line 1, in <module>\n  File \"pyModelChecking/CTL/language.py\", line 42, in __init__\n    self.wrap_subformulas(phi,StateFormula)\n  File \"pyModelChecking/CTLS/language.py\", line 59, in wrap_subformulas\n    phi.__desc__,phi))\nTypeError: expected a CTL state formula, got the CTL path formula G p\n```\n\nIt is also possible to parse a string representing a CTL formula by using the `Parser` class in the module `CTL`.\n\n```python\n>>> parser = Parser()\n\n>>> psi = parser(\"A(true U (q or not E X p))\")\n\n>>> print(psi)\n\nA(True U (q or not EX p))\n\n>>> print(psi.__class__)\n\n<class 'pyModelChecking.CTL.language.A'>\n```\n\nThe function `modelcheck` in the module `CTL` finds the states of Kripke structure that model a given CTL formula.\n\n```python\n>>>  modelcheck(K,phi)\n\nset([1, 2])\n```\n\nThe formula `AFG p`, which we tried to build above, is a LTL formula.\nThe `LTL` module can be used to represent and\nmodel check it over any Kripke structure.\n\n```python\n>>> from pyModelChecking.LTL import *\n\n>>> psi=A(F(G('p')))\n\n>>> print(psi)\n\nA(G(F(p))\n\n>>> modelcheck(K,psi)\n\nset([3])\n```\n\nStrings representing formulas in the opportune language can be used too as a parameter of the model checking function.\n\n```python\n>>> modelcheck(K,'A G F p')\n\nset([3])\n```\n\nThe module `CTLS` is meant to deal with CTL* formulas. It can also combine and model checks CTL and LTL formulas.\n\n```python\n>>> from pyModelChecking.CTLS import *\n\n>>> eta=A(F(E(U(True,Imply('p',Not('q'))))))\n\n>>> print(eta,eta.__class__)\n\n(A(F(E((True U (p --> not q))))), <class 'pyModelChecking.CTLS.language.A'>)\n\n>>> rho=A(G(And(X('p'),'p')))\n\n>>> print(rho,rho.__class__)\n\n(A(G((X(p) and p))), <class 'pyModelChecking.CTLS.language.A'>)\n\n>>> gamma=And(phi, psi)\n\n>>> print(gamma,gamma.__class__)\n\n(A(True U (q or not (EX p))) and A(G(F(p)))), <class 'pyModelChecking.CTLS.language.And'>)\n\n>>> modelcheck(K,eta)\n\nset([0, 1, 2, 3])\n\n>>> modelcheck(K, psi)\n\nset([3])\n\n>>> modelcheck(K, gamma)\n\nset([])\n\n```\n\nWhenever a CTL* formula is a CTL formula (LTL formula), CTL (LTL) model checking can\nbe applied to it.\n\n```python\n>>> import pyModelChecking.CTL as CTL\n\n>>> CTL.modelcheck(K,eta)\n\nset([0, 1, 2, 3])\n\n>>> CTL.modelcheck(K,rho)\nTraceback (most recent call last):\n  File \"<stdin>\", line 1, in <module>\n  File \"pyModelChecking/CTL/model_checking.py\", line 183, in modelcheck\n    raise RuntimeError('%s is not a CTL formula' % (formula))\nRuntimeError: A(G((X(p) and p))) is not a CTL formula\n\n>>> import pyModelChecking.LTL as LTL\n\n>>> LTL.modelcheck(K,rho)\n\nset([3])\n```\n\n### Copyright and license\n\npyModelChecking\nCopyright (C) 2015-2019  Alberto Casagrande <acasagrande@units.it>\n\npyModelChecking is free software; you can redistribute it and/or\nmodify it under the terms of the GNU General Public License\nas published by the Free Software Foundation; either version 2\nof the License, or (at your option) any later version.\n\nThis program is distributed in the hope that it will be useful,\nbut WITHOUT ANY WARRANTY; without even the implied warranty of\nMERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the\nGNU General Public License for more details.\n\nYou should have received a copy of the GNU General Public License\nalong with this program; if not, write to the Free Software\nFoundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.\n\n\n",
        "description_content_type": "text/markdown",
        "docs_url": null,
        "download_url": "",
        "downloads": {
            "last_day": -1,
            "last_month": -1,
            "last_week": -1
        },
        "home_page": "https://github.com/albertocasagrande/pyModelChecking",
        "keywords": "model checking temporal logics kripke structure",
        "license": "GNU General Public License, version 2",
        "maintainer": "",
        "maintainer_email": "",
        "name": "pyModelChecking",
        "package_url": "https://pypi.org/project/pyModelChecking/",
        "platform": "",
        "project_url": "https://pypi.org/project/pyModelChecking/",
        "project_urls": {
            "Documentation": "https://readthedocs.org/projects/pymodelchecking/",
            "Homepage": "https://github.com/albertocasagrande/pyModelChecking",
            "Source Code": "https://github.com/albertocasagrande/pyModelChecking"
        },
        "release_url": "https://pypi.org/project/pyModelChecking/1.2.0/",
        "requires_dist": [
            "lark-parser"
        ],
        "requires_python": "",
        "summary": "A simple Python model checking package",
        "version": "1.2.0"
    },
    "last_serial": 5199819,
    "releases": {
        "0.1.1": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "857bd454ecfa989d89834dc910a4d607",
                    "sha256": "3369067a77fc73c31a15102a30e6f6990d98011c7be6cea6a00721dc063f11df"
                },
                "downloads": -1,
                "filename": "pyModelChecking-0.1.1-py2-none-any.whl",
                "has_sig": false,
                "md5_digest": "857bd454ecfa989d89834dc910a4d607",
                "packagetype": "bdist_wheel",
                "python_version": "py2",
                "requires_python": null,
                "size": 34479,
                "upload_time": "2018-11-05T11:50:01",
                "url": "https://files.pythonhosted.org/packages/5d/43/07d3588c6451a477219c3747f7e0d3c05e635bde36b0e05034cb6a2317f9/pyModelChecking-0.1.1-py2-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "c7ee6c252e34166fcc9720671ed25575",
                    "sha256": "5ebca2761b7bd79cfa137db9fe182afb1e3cb7f5f44898edbf15c715b9ae5d15"
                },
                "downloads": -1,
                "filename": "pyModelChecking-0.1.1.tar.gz",
                "has_sig": false,
                "md5_digest": "c7ee6c252e34166fcc9720671ed25575",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 22858,
                "upload_time": "2018-11-05T11:50:03",
                "url": "https://files.pythonhosted.org/packages/f3/bf/2b3f95165aad5ed68f833773bac9702ee8c3d85382bfb7f6865f83ff19dd/pyModelChecking-0.1.1.tar.gz"
            }
        ],
        "0.1.5": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "db0b14c5f395c1bbb7edc19760c842ed",
                    "sha256": "7509a6b806a2eb808cddfac605f39a3e7ad7a110d23da3b14bd30c1f08399c2c"
                },
                "downloads": -1,
                "filename": "pyModelChecking-0.1.5-py2-none-any.whl",
                "has_sig": false,
                "md5_digest": "db0b14c5f395c1bbb7edc19760c842ed",
                "packagetype": "bdist_wheel",
                "python_version": "py2",
                "requires_python": null,
                "size": 36074,
                "upload_time": "2018-11-05T13:24:17",
                "url": "https://files.pythonhosted.org/packages/8e/73/c20e1a361fcd3a9ecd95902b4d41c1ae2a17fa803bff0aad63828a7dea33/pyModelChecking-0.1.5-py2-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "c8c449650ec050cf6bebfe873b851cdd",
                    "sha256": "41f8f07473e74d53bf30fcf5d3962011011cfab0fc083d2553098087205b075a"
                },
                "downloads": -1,
                "filename": "pyModelChecking-0.1.5.tar.gz",
                "has_sig": false,
                "md5_digest": "c8c449650ec050cf6bebfe873b851cdd",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 25188,
                "upload_time": "2018-11-05T13:24:19",
                "url": "https://files.pythonhosted.org/packages/c4/ca/eb56d43ffd67db81a2e09578dc0df383d12bff5a47fd11402a8bf28ed002/pyModelChecking-0.1.5.tar.gz"
            }
        ],
        "0.2": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "aa050f8219beed2f153f47ac3b9a80d2",
                    "sha256": "5443a75a3880142024d239e0afd53ae566bd76f9cd7e167c4ee9adac5b197400"
                },
                "downloads": -1,
                "filename": "pyModelChecking-0.2-py2-none-any.whl",
                "has_sig": false,
                "md5_digest": "aa050f8219beed2f153f47ac3b9a80d2",
                "packagetype": "bdist_wheel",
                "python_version": "py2",
                "requires_python": null,
                "size": 37159,
                "upload_time": "2018-11-26T08:56:03",
                "url": "https://files.pythonhosted.org/packages/8f/6a/08dff640207d8c22d0d2ba71451150609367029ed30496c36e7e1ff17368/pyModelChecking-0.2-py2-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "8fa85227266f39d7826df5440d33f830",
                    "sha256": "1ee62ae4eb16bfa86fd102d35344bffa00dfb7ec61fc089bcf9c7f073e6c8f25"
                },
                "downloads": -1,
                "filename": "pyModelChecking-0.2.tar.gz",
                "has_sig": false,
                "md5_digest": "8fa85227266f39d7826df5440d33f830",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 25784,
                "upload_time": "2018-11-26T08:56:05",
                "url": "https://files.pythonhosted.org/packages/7f/81/5dc9a572e4c5378ad6f2995b8158993d58b2b7783ac5dbd4660b5265e16f/pyModelChecking-0.2.tar.gz"
            }
        ],
        "1.0": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "e0ef9fed2142fc552a9fa71b21544e2c",
                    "sha256": "6aa0ee4ac7b85c710eb3ed4eae27a286c002e78d371bad14bd1da13968ea9a5b"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.0-py2-none-any.whl",
                "has_sig": false,
                "md5_digest": "e0ef9fed2142fc552a9fa71b21544e2c",
                "packagetype": "bdist_wheel",
                "python_version": "py2",
                "requires_python": null,
                "size": 37321,
                "upload_time": "2019-04-01T23:08:54",
                "url": "https://files.pythonhosted.org/packages/9a/2c/a8c827c073ab1df85017add709ab1e798cc1e985628f5240fef0c8e1804d/pyModelChecking-1.0-py2-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "fa1c1efeb85402db09ae8a99d5a645fb",
                    "sha256": "294f926acce6a74010e69ef4590817ec4edb36b1fbb9b3a55c708d27ee8f0a73"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.0-py3-none-any.whl",
                "has_sig": false,
                "md5_digest": "fa1c1efeb85402db09ae8a99d5a645fb",
                "packagetype": "bdist_wheel",
                "python_version": "py3",
                "requires_python": null,
                "size": 37321,
                "upload_time": "2019-04-01T23:08:55",
                "url": "https://files.pythonhosted.org/packages/c4/15/77af5ea7532956c435f0c4c0c0292df219d937b049ccbf90d43518f2686a/pyModelChecking-1.0-py3-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "a4b47ed5e5ae808a567dc1184941e8c4",
                    "sha256": "bf41b2bfa8ff8d125389c52cf14a5848f5ba89e048fa0b896684c460b18eef0d"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.0.tar.gz",
                "has_sig": false,
                "md5_digest": "a4b47ed5e5ae808a567dc1184941e8c4",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 44296,
                "upload_time": "2019-04-01T23:08:57",
                "url": "https://files.pythonhosted.org/packages/e6/dc/22f226a6f19633eba5d2815e3df6abff59a2633a95f70678410fb8188e89/pyModelChecking-1.0.tar.gz"
            }
        ],
        "1.0.1": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "acc9d812f385bfbea9a596266adba185",
                    "sha256": "0e0268cac59605ac16fa3b60b22df41c96d82c181d0a14694cbf5a25ae8e2986"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.0.1-py2-none-any.whl",
                "has_sig": false,
                "md5_digest": "acc9d812f385bfbea9a596266adba185",
                "packagetype": "bdist_wheel",
                "python_version": "py2",
                "requires_python": null,
                "size": 36279,
                "upload_time": "2019-04-02T10:09:53",
                "url": "https://files.pythonhosted.org/packages/58/fb/17e633d0ff2412396bfda49de94aa9d9a717f071a75d9400f718898dedc9/pyModelChecking-1.0.1-py2-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "9fc5f15efd4be5e4a4ae42adb4870f6e",
                    "sha256": "8e5b3c6251db8753745584dcb469cb3857ef89bf8912d7477f982e0b4684266d"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.0.1-py3-none-any.whl",
                "has_sig": false,
                "md5_digest": "9fc5f15efd4be5e4a4ae42adb4870f6e",
                "packagetype": "bdist_wheel",
                "python_version": "py3",
                "requires_python": null,
                "size": 36281,
                "upload_time": "2019-04-02T10:09:55",
                "url": "https://files.pythonhosted.org/packages/65/87/f1b2f2dfffda7da5330ea1081eada9d7771a844159e6f00a7dd5b87c4c7e/pyModelChecking-1.0.1-py3-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "983e6c869467ce549b5bee50b9c175c4",
                    "sha256": "dd2324201cc276232d545a11b979ff1ba99452ffd81dc3ea04a405521981f373"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.0.1.tar.gz",
                "has_sig": false,
                "md5_digest": "983e6c869467ce549b5bee50b9c175c4",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 44547,
                "upload_time": "2019-04-02T10:09:56",
                "url": "https://files.pythonhosted.org/packages/3d/67/08ddbf2eda782f151aebe4dfecb513ae704e3b5724b3458e55d8a3c6a5be/pyModelChecking-1.0.1.tar.gz"
            }
        ],
        "1.1.1": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "6002a97e9de116ee2b94326c77a5267b",
                    "sha256": "dec0331940114ebdd7791e999e8666e5900b6ddf4adf82dd1f1873a6d5c961c1"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.1.1-py2-none-any.whl",
                "has_sig": false,
                "md5_digest": "6002a97e9de116ee2b94326c77a5267b",
                "packagetype": "bdist_wheel",
                "python_version": "py2",
                "requires_python": null,
                "size": 45878,
                "upload_time": "2019-04-19T14:59:38",
                "url": "https://files.pythonhosted.org/packages/b6/02/de096f91f61f01207a7b3ea93c8ac92c980efd1da2a61ed886e1a04041c3/pyModelChecking-1.1.1-py2-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "a64a4d47d6a237ed1660c07d3d811f44",
                    "sha256": "71f1b32904a1d3bf72f609f2295b4716f1213bbc307c3ffe28fb4ef7b08d244e"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.1.1-py3-none-any.whl",
                "has_sig": false,
                "md5_digest": "a64a4d47d6a237ed1660c07d3d811f44",
                "packagetype": "bdist_wheel",
                "python_version": "py3",
                "requires_python": null,
                "size": 45878,
                "upload_time": "2019-04-19T14:59:39",
                "url": "https://files.pythonhosted.org/packages/1d/38/243665d9cf53dab654e76a0e35fd99309c117bad54dc54e515048a6ae779/pyModelChecking-1.1.1-py3-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "65beb30f156fdd9878382ef22129770d",
                    "sha256": "cfc137df91778f17c041b65dcf0185a8614e56086b3ed4bf3c05db1d1e6d59dc"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.1.1.tar.gz",
                "has_sig": false,
                "md5_digest": "65beb30f156fdd9878382ef22129770d",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 49085,
                "upload_time": "2019-04-19T14:59:41",
                "url": "https://files.pythonhosted.org/packages/f0/d5/bc95d76fbf2991f408e31c0aea6e51485dbca78dbcf61c386e12e43244da/pyModelChecking-1.1.1.tar.gz"
            }
        ],
        "1.2.0": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "3c6b2c6a84d60551baa852225e36289d",
                    "sha256": "cdde4e552e2527dbb6c5a94b28460d39556021d1214be4e27efe2f430a11d429"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.2.0-py2.py3-none-any.whl",
                "has_sig": false,
                "md5_digest": "3c6b2c6a84d60551baa852225e36289d",
                "packagetype": "bdist_wheel",
                "python_version": "py2.py3",
                "requires_python": null,
                "size": 46637,
                "upload_time": "2019-04-28T14:16:46",
                "url": "https://files.pythonhosted.org/packages/fa/06/dd5c4c0ab976e22b8609ad2df644228fd3c49cebfca19eff52eb58be0a5d/pyModelChecking-1.2.0-py2.py3-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "db0aeb2184dbbc310105148a826f273e",
                    "sha256": "301daa495a4f726e3aaa28d20ba01b8521c676a9418d042633565c900c6c1497"
                },
                "downloads": -1,
                "filename": "pyModelChecking-1.2.0.tar.gz",
                "has_sig": false,
                "md5_digest": "db0aeb2184dbbc310105148a826f273e",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": null,
                "size": 31130,
                "upload_time": "2019-04-28T14:16:49",
                "url": "https://files.pythonhosted.org/packages/75/e3/32b2b922f521b29047a3338e646a843a84b66d29740df3d500b61819ebd8/pyModelChecking-1.2.0.tar.gz"
            }
        ]
    },
    "urls": [
        {
            "comment_text": "",
            "digests": {
                "md5": "3c6b2c6a84d60551baa852225e36289d",
                "sha256": "cdde4e552e2527dbb6c5a94b28460d39556021d1214be4e27efe2f430a11d429"
            },
            "downloads": -1,
            "filename": "pyModelChecking-1.2.0-py2.py3-none-any.whl",
            "has_sig": false,
            "md5_digest": "3c6b2c6a84d60551baa852225e36289d",
            "packagetype": "bdist_wheel",
            "python_version": "py2.py3",
            "requires_python": null,
            "size": 46637,
            "upload_time": "2019-04-28T14:16:46",
            "url": "https://files.pythonhosted.org/packages/fa/06/dd5c4c0ab976e22b8609ad2df644228fd3c49cebfca19eff52eb58be0a5d/pyModelChecking-1.2.0-py2.py3-none-any.whl"
        },
        {
            "comment_text": "",
            "digests": {
                "md5": "db0aeb2184dbbc310105148a826f273e",
                "sha256": "301daa495a4f726e3aaa28d20ba01b8521c676a9418d042633565c900c6c1497"
            },
            "downloads": -1,
            "filename": "pyModelChecking-1.2.0.tar.gz",
            "has_sig": false,
            "md5_digest": "db0aeb2184dbbc310105148a826f273e",
            "packagetype": "sdist",
            "python_version": "source",
            "requires_python": null,
            "size": 31130,
            "upload_time": "2019-04-28T14:16:49",
            "url": "https://files.pythonhosted.org/packages/75/e3/32b2b922f521b29047a3338e646a843a84b66d29740df3d500b61819ebd8/pyModelChecking-1.2.0.tar.gz"
        }
    ]
}