{
    "info": {
        "author": "Rick Smetsers",
        "author_email": "ricksmet@gmail.com",
        "bugtrack_url": null,
        "classifiers": [
            "Development Status :: 3 - Alpha",
            "Environment :: Console",
            "Intended Audience :: Science/Research",
            "License :: OSI Approved :: MIT License",
            "Operating System :: OS Independent",
            "Programming Language :: Python",
            "Programming Language :: Python :: 2.7",
            "Programming Language :: Python :: 3",
            "Topic :: Scientific/Engineering :: Artificial Intelligence"
        ],
        "description": "Grammatical inference using the Z3 SMT solver\n=============================================\n\nZ3GI is a Python tool and library that uses the [Z3 SMT solver][z3] for learning minimal consistent state machine models from labeled strings or input/output taces.\n\n[z3]: https://github.com/Z3Prover/z3\n\nIntroduction\n------------\n\nGrammatical inference is the research field that is concerned with learning the set of rules that describe the behavior of a system, such as a network protocol, a piece of software, or a (formal) language.\nOne of the best studied problems in grammatical inference is that of finding a deterministic finite automaton (DFA) of minimal size that accepts a given set of positive strings and rejects a given set of negative strings.\nThis problem is can be very hard, as it has been shown to be NP-complete.\nZ3GI provides different ways of solving this (and similar) problem(s) using satisfiability modulo theories (SMT).\n\nInstalling with pip\n--------------------\n\nThe recommended way of installing Z3GI is with `pip`:\n\n```\n$ pip install z3gi\n```\n\nInstalling from sources\n-----------------------\n\nAlternatively, you can install Z3GI by cloning this repository, and installing using `setuptools`:\n\n```\n$ git clone https://gitlab.science.ru.nl/rick/smtgi.git\n$ python smtgi/z3gi/setup.py install\n```\n\nGetting started\n---------------\n\nConsider a deterministic finite automaton (DFA) that accepts strings of `0`s and `1`s in which the number of `0`s minus twice the number of `1`s is either 1 or 3 more than a multiple of 5 (such a DFA is described [here][dfa]).\n\n[dfa]: http://abbadingo.cs.nuim.ie/dfa.html\n\nA training file `train.txt` for this DFA could read (if you have the sources of this package, this file can be found at `docs/train.txt`):\n\n```\n16 2\n1 4 1 0 0 0\n1 4 0 1 0 0\n1 4 0 0 1 0\n1 5 1 0 1 1 1\n1 6 1 1 1 1 0 1\n1 6 0 1 0 0 0 0\n1 6 1 0 0 0 0 0\n1 7 0 0 0 1 1 0 1\n1 7 0 0 0 0 1 0 1\n0 3 1 0 1\n0 4 0 0 0 0\n0 4 1 1 0 1\n0 5 0 0 0 0 0\n0 5 0 0 1 0 1\n0 6 0 1 0 1 1 1\n0 7 1 0 0 0 1 1 1\n```\n\nIn this [Abbadingo file][abbadingo], the first line is a header, giving the number of strings in the file (16) and the number of symbols (2).\nEach line after the header has the format \n\n[abbadingo]: http://abbadingo.cs.nuim.ie/data-sets.html\n\n```\nlabel n symbol1 symbol2 ... symboln\n```\n\nWhere label `1` means accepted, and the label `0` means rejected.\n\nWe can use Z3GI to learn a model for the strings in `train.txt` as follows:\n\n```\n$ python -m z3gi --model -f train.txt\n```\n\nThis produces the following output:\n\n```\nLearned model:\n[state3 = 3,\nstart = 0,\nstate0 = 0,\nn = 5,\nstate2 = 2,\nstate4 = 4,\n1 = INPUT!val!0,\nstate1 = 1,\n0 = INPUT!val!1,\nout = [3 -> True, 4 -> True, else -> False],\ntrans = [(0, INPUT!val!0) -> 3,\n        (0, INPUT!val!1) -> 4,\n        (4, INPUT!val!0) -> 2,\n        (3, INPUT!val!0) -> 4,\n        (3, INPUT!val!1) -> 2,\n        (2, INPUT!val!0) -> 1,\n        (1, INPUT!val!1) -> 3,\n        (4, INPUT!val!1) -> 1,\n        else -> 0]]\n```\n\nWe can interpret this learned model as follows.\n- `0 = INPUT!val!1` and `1 = INPUT!val!0` provide identifiers for `0` and `1`\n- `n = 5` indicates that the learned model has 5 states\n- `state0 = 0` through `state4 = 4` provide the identifiers for these states\n- `out` describes an output function for these states (`True` if it is accepting and `False` if it is rejecting)\n- `trans` desribes a transition function for states and symbols to states (e.g. `(0, INPUT!val!0) -> 3)` describes a transition from `state0` with `1` to `state3`)\n\nUsing z3gi in Python\n--------------------\n\nLet's learn the same model (from `train.txt`) in Python:\n\n1. Open your Python interpreter:\n\n    ```\n    $ python\n    ```\n2. Let's use a different encoder this time:\n\n    ```\n    >>> from z3gi.encoders import expressive\n    >>> encoder = expressive.Encoder()\n    ```\n3. Create a sample:\n\n    ```\n    >>> from z3gi.sample import Sample\n    >>> sample = Sample(encoder)\n    ```\n4. Add constraints for strings in `train.txt` to the sample:\n\n    ```\n    >>> from z3gi.parsers import abbadingo\n    >>> for string, label in abbadingo.read(open('train.txt', 'r'), header=1):\n    ...     sample[string] = label\n    ...\n    ```\n5. Obtain the model!\n\n    ```\n    >>> model = sample.model()\n    >>> print(model)\n    ```\n\n\n",
        "description_content_type": null,
        "docs_url": null,
        "download_url": "",
        "downloads": {
            "last_day": -1,
            "last_month": -1,
            "last_week": -1
        },
        "home_page": "https://gitlab.science.ru.nl/rick/z3gi",
        "keywords": "",
        "license": "MIT",
        "maintainer": "",
        "maintainer_email": "",
        "name": "z3gi",
        "package_url": "https://pypi.org/project/z3gi/",
        "platform": "",
        "project_url": "https://pypi.org/project/z3gi/",
        "project_urls": {
            "Homepage": "https://gitlab.science.ru.nl/rick/z3gi"
        },
        "release_url": "https://pypi.org/project/z3gi/0.1.1/",
        "requires_dist": [
            "z3-solver"
        ],
        "requires_python": "",
        "summary": "Grammatical inference using the Z3 SMT solver",
        "version": "0.1.1"
    },
    "last_serial": 2776500,
    "releases": {
        "0.1.1": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "b625815307e834a43da34be6c9e2eff4",
                    "sha256": "64a812c069d3dbf5914743c97aa37687650e8ffaa0e5f0ab30e6038abe554b07"
                },
                "downloads": -1,
                "filename": "z3gi-0.1.1-py2.py3-none-any.whl",
                "has_sig": false,
                "md5_digest": "b625815307e834a43da34be6c9e2eff4",
                "packagetype": "bdist_wheel",
                "python_version": "py2.py3",
                "requires_python": null,
                "size": 15933,
                "upload_time": "2017-04-11T11:14:48",
                "url": "https://files.pythonhosted.org/packages/59/60/d6514364a5a729e2b0206541c9716c4f46f0dc1782d067242fc1cad5d24d/z3gi-0.1.1-py2.py3-none-any.whl"
            }
        ]
    },
    "urls": [
        {
            "comment_text": "",
            "digests": {
                "md5": "b625815307e834a43da34be6c9e2eff4",
                "sha256": "64a812c069d3dbf5914743c97aa37687650e8ffaa0e5f0ab30e6038abe554b07"
            },
            "downloads": -1,
            "filename": "z3gi-0.1.1-py2.py3-none-any.whl",
            "has_sig": false,
            "md5_digest": "b625815307e834a43da34be6c9e2eff4",
            "packagetype": "bdist_wheel",
            "python_version": "py2.py3",
            "requires_python": null,
            "size": 15933,
            "upload_time": "2017-04-11T11:14:48",
            "url": "https://files.pythonhosted.org/packages/59/60/d6514364a5a729e2b0206541c9716c4f46f0dc1782d067242fc1cad5d24d/z3gi-0.1.1-py2.py3-none-any.whl"
        }
    ]
}