Metadata-Version: 2.0
Name: st2smv
Version: 0.1.1
Summary: A tool to convert Structured Text PLC code to an SMV model.
Home-page: https://pypi.python.org/pypi/st2smv
Author: Blake C. Rawlings
Author-email: blakecraw@gmail.com
License: GPLv3
Platform: UNKNOWN
Classifier: Development Status :: 3 - Alpha
Classifier: License :: OSI Approved :: GNU General Public License v3 or later (GPLv3+)
Classifier: Programming Language :: Python :: 2
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering
Requires-Dist: networkx
Requires-Dist: pyparsing
Requires-Dist: six

Overview
========

``st2smv`` is a tool for converting programmable logic controller (PLC)
code to a formal model, and checking whether the model satisfies various
properties (e.g., temporal logic specifications). As its name implies,
``st2smv`` can process PLC code written in a subset of the Structured
Text (ST) programming language, and produces models in the SMV language.

Basic Use
=========

Run the command

.. code:: bash

    st2smv --help

to see a summary of how to use ``st2smv``.

Structure of the Model
======================

In progress...

Advanced Use
============

In progress...

Installation
============

To install ``st2smv`` from the Python Package Index (PyPI), run the
command

.. code:: bash

    pip install st2smv

If you have instead obtained this package from another source and wish
to install that copy, run the command

.. code:: bash

    pip install st2smv_directory

where ``st2smv_directory`` is the location of this directory (i.e., the
directory that contains the file ``setup.py``).

Dependencies
------------

``st2smv`` converts PLC code to a formal model, which then must be
analyzed using a solver. The current version of ``st2smv`` produces
models that can be analyzed using
`SynthSMV <https://bitbucket.org/blakecraw/synthsmv>`__, which must be
installed separately. `NuSMV <http://nusmv.fbk.eu>`__ (which SynthSMV is
based on) can be used to check some, but not all, of the models that
``st2smv`` produces.

License
=======

`GPLv3+ <https://www.gnu.org/licenses/gpl.html>`__: The GNU General
Public License, version 3, or (at your option) any later version.


