🚀 Big News: Socket Acquires Coana to Bring Reachability Analysis to Every Appsec Team.Learn more
Socket
DemoInstallSign in
Socket

omega

Package Overview
Dependencies
Maintainers
3
Alerts
File Explorer

Advanced tools

Socket logo

Install Socket

Detect and block malicious and high-risk dependencies

Install

omega

Symbolic algorithms for solving games of infinite duration.

0.4.0
PyPI
Maintainers
3

Build Status

About

A package of symbolic algorithms using binary decision diagrams (BDDs) for synthesizing implementations from temporal logic specifications. This is useful for designing systems, especially vehicles that carry humans.

  • Synthesis algorithms for Moore or Mealy implementations of:

    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 linear temporal logic (LTL) with rigid quantification and substitution. See omega.logic.lexyacc, omega.logic.ast, and omega.logic.syntax.

  • Bitblaster of quantified integer arithmetic (integers -> bits). See omega.logic.bitvector.

  • Translation from past to future LTL, using temporal testers. See omega.logic.past.

  • Symbolic automata that manage first-order formulas by seamlessly using binary decision diagrams (BDDs) underneath. You can:

    • declare variables and constants
    • translate:
      • formulas to BDDs and
      • 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.

    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.

Examples

import omega.symbolic.fol as _fol

ctx = _fol.Context()
ctx.declare(
    x=(0, 10),
    y=(-2, 5),
    z='bool')
u = ctx.add_expr(
    r'(x <= 2) /\ (y >= -1)')
v = ctx.add_expr(
    r'(y <= 3) => (x > 7)')
r = u & ~ v
expr = ctx.to_expr(r)
print(expr)

Installation

pip install omega

The package and its dependencies are pure Python.

For solving demanding games, install the Cython module dd.cudd that interfaces to CUDD. Instructions are available at dd.

License

BSD-3, see LICENSE file.

Keywords

first-order

FAQs

Did you know?

Socket

Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.

Install

Related posts