Data

Tools

Indexes

Applications

Experiments

Open Source Science

omega

Specify and synthesize systems using symbolic algorithms

https://github.com/tulip-control/omega

Science Score: 36.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ○
    .zenodo.json file
  • ✓
    DOI references
    Found 22 DOI reference(s) in README
  • ○
    Academic publication links
  • ✓
    Committers with academic emails
    1 of 3 committers (33.3%) from academic institutions
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (7.2%) to scientific vocabulary

Keywords

automata bitvector logic-minimization python rabin streett symbolic synthesis temporal-logic

Keywords from Contributors

abstraction control-systems feedback-systems hybrid-systems state-machine verification
Last synced: 6 months ago · JSON representation

Repository

Specify and synthesize systems using symbolic algorithms

Basic Info
Statistics
  • Stars: 50
  • Watchers: 4
  • Forks: 5
  • Open Issues: 5
  • Releases: 0
Topics
automata bitvector logic-minimization python rabin streett symbolic synthesis temporal-logic
Created almost 11 years ago · Last pushed over 1 year ago
Metadata Files
Readme License

README.md

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.

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

```python import omega.symbolic.fol as _fol

ctx = fol.Context() ctx.declare( x=(0, 10), y=(-2, 5), z='bool') u = ctx.addexpr( r'(x <= 2) /\ (y >= -1)') v = ctx.addexpr( r'(y <= 3) => (x > 7)') r = u & ~ v expr = ctx.toexpr(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.

Owner

  • Name: Temporal Logic Planning (TuLiP) toolbox
  • Login: tulip-control
  • Kind: organization

GitHub Events

Total
  • Watch event: 6
  • Fork event: 1
Last Year
  • Watch event: 6
  • Fork event: 1

Committers

Last synced: over 1 year ago

All Time
  • Total Commits: 922
  • Total Committers: 3
  • Avg Commits per committer: 307.333
  • Development Distribution Score (DDS): 0.004
Past Year
  • Commits: 90
  • Committers: 1
  • Avg Commits per committer: 90.0
  • Development Distribution Score (DDS): 0.0
Top Committers
Name Email Commits
Ioannis Filippidis j****s@g****m 918
Scott C. Livingston s****n@c****u 3
Nok Wongpiromsarn t****n@g****m 1
Committer Domains (Top 20 + Academic)
cds.caltech.edu: 1

Issues and Pull Requests

Last synced: 6 months ago

All Time
  • Total issues: 13
  • Total pull requests: 1
  • Average time to close issues: 6 months
  • Average time to close pull requests: 10 days
  • Total issue authors: 5
  • Total pull request authors: 1
  • Average comments per issue: 1.69
  • Average comments per pull request: 9.0
  • Merged pull requests: 1
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Issue authors: 0
  • Pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
  • johnyf (7)
  • glarange (2)
  • slivingston (2)
  • thisiscam (1)
  • DangMinh24 (1)
Pull Request Authors
  • tichakornw (1)
Top Labels
Issue Labels
enhancement (6) documentation (4) question (1)
Pull Request Labels
enhancement (1)

Packages

  • Total packages: 1
  • Total downloads:
    • pypi 80,121 last-month
  • Total dependent packages: 2
  • Total dependent repositories: 9
  • Total versions: 19
  • Total maintainers: 3
pypi.org: omega

Symbolic algorithms for solving games of infinite duration.

  • Versions: 19
  • Dependent Packages: 2
  • Dependent Repositories: 9
  • Downloads: 80,121 Last month
  • Docker Downloads: 0
Rankings
Docker downloads count: 4.2%
Dependent packages count: 4.7%
Dependent repos count: 4.9%
Average: 9.0%
Stargazers count: 10.0%
Forks count: 14.2%
Downloads: 15.9%
Maintainers (3)
johnyf murrayrm slivingston
Last synced: 6 months ago

Dependencies

requirements.txt pypi
  • gitpython *
setup.py pypi
  • astutils *
  • dd *
  • humanize *
  • natsort *
  • networkx *
  • ply *
  • pydot *
.github/workflows/main.yml actions
  • actions/checkout v2 composite
  • actions/setup-python v2 composite