Metadata-Version: 2.1
Name: omega
Version: 0.3.0
Summary: Symbolic algorithms for solving games of infinite duration.
Home-page: https://github.com/tulip-control/omega
Author: Caltech Control and Dynamical Systems
Author-email: tulip@tulip-control.org
License: BSD
Description: [![Build Status][build_img]][travis]
        [![Coverage Status][coverage]][coveralls]
        
        
        About
        =====
        
        A package of symbolic algorithms using binary decision diagrams (BDDs)
        for synthesizing implementations from [temporal logic specifications][specs].
        This is useful for designing systems, especially vehicles that carry humans.
        
        
        - [Synthesis][synthesis] algorithms for [Moore][moore] or [Mealy][mealy]
          implementations of:
        
          - [generalized Streett(1)][streett1] specifications (known as [GR(1)][gr1])
          - generalized Rabin(1) specifications ([counter-strategies][rabin1] to GR(1))
          - detection of trivial realizability in GR(1) specifications.
        
          See `omega.games.gr1` and the example `gr1_synthesis_intro`.
        
        
        - Enumeration of state machines (as `networkx` graphs) from the synthesized
          symbolic implementations. See `omega.games.enumeration`.
        
        
        - Facilities to simulate the resulting implementations with little and
          readable user code. See `omega.steps` and the example `moore_moore`.
        
        
        - Code generation for the synthesized *symbolic* implementations.
          This code is correct-by-construction. See `omega.symbolic.codegen`.
        
        
        - *Minimal covering* with a symbolic algorithm to find a minimal cover, and to
          enumerate all minimal covers. Used to convert BDDs to *minimal* formulas.
          See `omega.symbolic.cover` and `omega.symbolic.cover_enum`, and the
          example `minimal_formula_from_bdd`.
        
        
        - [First-order][fol] [linear temporal logic][LTL] (LTL) with
          [rigid quantification][rigid quantification] and substitution.
          See `omega.logic.lexyacc`, `omega.logic.ast`, and `omega.logic.syntax`.
        
        
        - [Bitblaster][bitblasting] of quantified integer arithmetic (integers -> bits).
          See `omega.logic.bitvector`.
        
        
        - Translation from [past][past LTL] to future LTL, using
          [temporal testers][temporal testers]. See `omega.logic.past`.
        
        
        - Symbolic automata that manage first-order formulas by seamlessly using
          [binary decision diagrams][bdd] (BDDs) underneath. You can:
        
          - declare variables and constants
          - translate:
            1. formulas to BDDs and
            2. BDDs to *minimal* formulas via minimal covering
          - quantify
          - substitute
          - prime/unprime variables
          - get the support of predicates
          - pick satisfying assignments (or work with iterators)
          - define operators
        
          See `omega.symbolic.temporal` and `omega.symbolic.fol` for more details.
        
        
        - Facilities to write symbolic fixpoint algorithms.
          See `omega.symbolic.fixpoint` and `omega.symbolic.prime`, and the example
          `reachability_solver`.
        
        
        - Conversion from graphs annotated with formulas to temporal logic formulas.
          These graphs can help specify transition relations.
          The translation is in the spirit of
          [predicate-action diagrams][tla-in-pictures].
        
          See `omega.symbolic.logicizer` and `omega.automata` for more details, and
          the example `symbolic`.
        
        
        - Enumeration and plotting of state predicates and actions represented as BDDs.
          See `omega.symbolic.enumeration`.
        
        
        Documentation
        =============
        
        In  [`doc/doc.md`][doc].
        
        
        Installation
        ============
        
        ```
        pip install omega
        ```
        
        or
        
        ```
        python setup.py install
        ```
        
        The package and its dependencies are pure Python.
        
        For solving demanding games, install the [Cython][cython] module `dd.cudd`
        that interfaces to [CUDD][cudd].
        Instructions are available [at `dd`][dd].
        
        
        License
        =======
        [BSD-3][bsd3], see `LICENSE` file.
        
        
        [specs]: http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
        [synthesis]: http://dx.doi.org/10.1007/BFb0035748
        [moore]: https://web.archive.org/web/20120216141113/http://people.mokk.bme.hu/~kornai/termeszetes/moore_1956.pdf
        [mealy]: http://dx.doi.org/10.1002/j.1538-7305.1955.tb03788.x
        [streett1]: http://dx.doi.org/10.1016/j.ic.2005.01.006
        [gr1]: http://dx.doi.org/10.1007/11609773_24
        [rabin1]: https://online.tugraz.at/tug_online/voe_main2.getvolltext?pCurrPk=47554
        [fol]: https://en.wikipedia.org/wiki/First-order_logic
        [past LTL]: http://dx.doi.org/10.1007/3-540-15648-8_16
        [LTL]: http://dx.doi.org/10.1109/SFCS.1977.32
        [temporal testers]: http://doi.org/10.1007/978-3-540-69850-0_11
        [rigid quantification]: http://dx.doi.org/10.1007/978-1-4612-4222-2
        [bitblasting]: http://dx.doi.org/10.1007/978-3-540-74105-3
        [bdd]: http://dx.doi.org/10.1109/TC.1986.1676819
        [tla-in-pictures]: http://dx.doi.org/10.1109/32.464544
        [doc]: https://github.com/tulip-control/omega/blob/master/doc/doc.md
        [cython]: https://en.wikipedia.org/wiki/Cython
        [cudd]: http://vlsi.colorado.edu/~fabio/CUDD
        [dd]: https://github.com/tulip-control/dd#cython-bindings
        [bsd3]: http://opensource.org/licenses/BSD-3-Clause
        
        [build_img]: https://travis-ci.org/tulip-control/omega.svg?branch=master
        [travis]: https://travis-ci.org/tulip-control/omega
        [coverage]: https://coveralls.io/repos/tulip-control/omega/badge.svg?branch=master
        [coveralls]: https://coveralls.io/r/tulip-control/omega?branch=master
        
Keywords: first-order,propositional,logic,quantifier,forall,exists,fixpoint,mu-calculus,formula,flatten,bitblaster,bitvector,arithmetic,binary decision diagram,symbolic,games,specification,system,assume,guarantee,satisfiability,enumeration,state machine,transition system,automaton,automata,streett,rabin,temporal logic,temporal tester,gr1,generalized reactivity
Platform: UNKNOWN
Classifier: Development Status :: 2 - Pre-Alpha
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: BSD License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 2.7
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.4
Classifier: Programming Language :: Python :: 3.5
Classifier: Programming Language :: Python :: 3.6
Classifier: Programming Language :: Python :: 3.7
Classifier: Programming Language :: Python :: 3.8
Classifier: Topic :: Scientific/Engineering
Description-Content-Type: text/markdown
