omega

omega copied to clipboard

How does logic.past work?

3

Hi, I was studying about past LTL operators, and ran into this repo. Could someone explain how the translate routine omega.logic.past works? Specifically, I wonder what is the returned tuple...

thisiscam

Understand synthesize algorithms ()

4

Hi all, I am quite new to LTL specification, and trying to understand the idea of synthesizing. As far as I understand, synthesizing is the process building controller/automata/strategy that can...

DangMinh24

`omega.symbolic.fol.Context` arranges and uses a refinement of each variable that will be reasoned about for integer values from some finite set by a fixed finite number of variables that will...

johnyf

### [Quantifier bounds](https://en.wikipedia.org/wiki/Bounded_quantifier) and dynamic type hints in `omega` As of f4aa8f8459c65d5491aadef1fef80db23944a792, the formula `\A x: P(x)` means different things, depending on whether it is given to [`omega.symbolic.fol.Context.add_expr`](https://github.com/johnyf/omega/blob/cc37e899fae3d98e356178f092046e4363160945/omega/symbolic/fol.py#L178) with `x`...

johnyf

compile symbolic code into Python code

1

It is convenient to program symbolic code using mathematics (TLA+). Multi-line Python strings and `str.format` are excellent for this job. For development, this works well. For stable code deployment, it...

johnyf