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 value and what does "initial condition" mean?

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 is slow. Calling the parser and bitblaster takes long time compared to lightweight to medium size BDD operations (that don't last minutes). The delay becomes especially noticeable for TLA+ expressions that appear inside tight loops, and profiling showed that it dominates runtime.

The manual approach that addresses this problem is to simply write code calling directly functions that operate on BDDs, instead of a TLA+ string. Automate this conversion, so that it never need to happen in user code. This can be done by compiling TLA+ to Python code objects and using a decorator to memoize them. A similar approach was used in tulip.spec.form.GRSpec.compile_init.

A more traditional approach would be to translate the Python module and replace such strings by the equivalent Python code, but it introduces an inconvenient extra step and requires syntactically recognizing the strings to replace, which isn't a clearly defined problem (it is implicit). The proposed approach is explicit, and easier to implement.

As of a808dc1,doc.md is about to start becoming outdated:

• The viewpoint has now shifted to untyped logic: describe role of refinement mappings.
• First-order logic is directly available in omega.symbolic.fol: explain how to use it.
• Describe enumeration of symbolic entities.
• The cumbersome unidirectional two-stage building of omega.symbolic.symbolic.Automaton will be replaced, by subclassing from fol.Context.
• De-emphasize enumerated "transition systems" and "automata".
• Demonstrate Streett and Rabin solvers via examples (strategies, counter-strategies).
• Mini howto for fixpoint computations.

Quantifier bounds and dynamic type hints in omega

As of f4aa8f8, the formula \A x: P(x) means different things, depending on whether it is given to omega.symbolic.fol.Context.add_expr with x declared as an "integer" with "domain" 2..7 in Automaton.vars, "domain" -15..100, or x declared as a "Boolean". In transition to mathematics (following [1]), bounds will be introduced (as anticipated by this note in the module fol.py). All sentences will then have the same meaning in any Context.

In principle, this should allow automatically inferring what refinement to use (for satisfiability and construction of witnesses for a variable quantified over a known finite set 0..N, using variables that are restricted to take only Boolean values--also known as "bits"). In other words, utilizing the quantifier bounds as type hints [1]. This kind of refinement process is colloquially known as "bitblasting".

Thus, we could imagine "dynamically" extending the domain of variables (in terms of the current implementation, this means dynamically changing the "domain" of an integer stored in Context.vars), depending on what bounds are used in a sentence that contains quantifiers.

Quantifier bounds aren't obligatory. If P(x) is of the form (x \in Foo) => Q(x), then the formula \A x: P(x) is equivalent to \A x \in Foo: Q(x), where the quantifier is bounded. The antecedent form is more difficult to handle, because the bound has to be (syntactically) detected in the formula P(x), and there are infinitely many formulae equivalent to P(x). For this reason, bounded quantification will be syntactically required in omega.

Formulae with free variables (i.e., not sentences) will still remain differently encoded between Contexts. That shouldn't be a problem, because whenever one wants to quantify the variables in a formula, they should bound the quantifiers. In the presence of static Boolean refinements (type hint declarations), if too large a bound is used, then an error will be raised.

The methods Context.pick, pick_iter, count, forall, exist should be understood as (implicitly) bounded using the type hint declarations. From a programming perspective, it is cumbersome to pass a bound every time these methods are called within a solver. So, the explicit bounds will be required in syntax, but not in each method's signature, because the method is attached to a Context instance, unlike a formula as string.

The above will introduce a limited amount of set theory (0..N and {0, 1, 3}) and syntactic definitions (Foo == 0..N or Foo == P(x)), so a small amount of TLA+. This additional expressive power should be regarded as a paradigm change, rather than full-fledged support for set theory.

I'm not sure whether it even makes sense to think of recognizing bounds within P(x) semantically (via BDDs or other model-theoretic means), because by the time one has converted the proof-theoretic object (the formula) to a BDD, they have already made assumptions about the domain of interpretation (i.e., they have bounded the values that the variables can take, in order to represent them. This isn't an artifact of infinite sets--different finite ranges suffice to cause problems).

TLC supports only quantifiers that are explicitly bounded, likely because the bound is then readily available, and because any specification that we want to write in practice will contain bounds, either as antecedents, or on the quantifiers, so better to place them directly on the quantifiers. A formula that contains "genuinely unbounded" quantifiers probably doesn't mean what the specifier intended.

Quantifier bounds in dd?

dd is limited to propositional reasoning (single type for all variables), and its parsing capabilities are intended more for convenience, rather than specification. Also, its computation involves primarily BDDs, which belong to the semantic level. Requiring from users to keep writing \A x \in BOOLEAN: ... for all variables is unnecessarily cumbersome, given that the bound BOOLEAN is the same for all BDD variables.

Explicit is better than implicit, but simple is better than complex. Special cases aren't special enough to break the rules, although practicality beats purity [PEP 20]. So, I will let quantifier syntax omit bounds in dd, and antecedents of the form x \in BOOLEAN aren't supported either, making dd syntax typed (all BDD variables typed as BOOLEAN).

References

[1] Leslie Lamport, Lawrence C. Paulson
"Should your specification language be typed?"
ACM Transactions on Programming Languages and Systems
Vol.21, No.3, pp.502--526, 1999

[2] Hernán Vanzetto
"Proof automation and type synthesis for set theory in the context of TLA+", PhD Thesis, Computer Science. Université de Lorraine, 2014

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 be reasoned about for Boolean values only, using BDDs.

In lack of a better name, let's call the latter variables "bits". Do not mistake them for typed variables. It's just the case that we aren't going to reason about non-Boolean assignments to those "bit" variables.

In order to select how many bits to use, Context takes type hints, via the method add_vars. The user can then create new BDDs from expressions over the integer-valued variables. However, if the user uses values outside the type hints, no warning is printed.

One reason is that a 32 bit ALU is used for operators. Nevertheless, it would probably be useful to catch errors early.

We could print a warning if any numeral in the expression is outside the range of the type hint of any variable. We cannot associate such warnings with any specific variable, because addition and multiplication render it unclear which variables a potential error is associated with. Of course, we can report the variables that appear in the expression, as a hint to where an error might be.

For example:

from omega.symbolic.fol import Context

c = Context()
c.add_vars(dict(x=dict(type='int', dom=(0, 4))))  # type hint: x \in 0 .. 4
>>> c.vars
{'x': {'bitnames': ['x_0', 'x_1', 'x_2'],
  'dom': (0, 4),
  'signed': False,
  'type': 'int',
  'width': 3}}
u = c.add_expr('5 <= x /\ x <= 8')
>>> u = c.add_expr('5 <= x /\ x <= 8')
True
>>> list(c.pick_iter(u))
[{'x': 6}, {'x': 5}, {'x': 7}]

At most a warning will be raised, not an error. The variables are untyped, and there is no clear evidence that such a situation is the result of an error.

Is it possible to convert the Automoton 'aut' below to an MDD? If so, how?
Thanks, Gui

from omega.symbolic import temporal as trl

aut = trl.Automaton()
aut.declare_variables(x=(1, 3), y=(-3, 3))
u = aut.add_expr('x = 1 /\ y \in 1..2')

code from: tulip-control/dd#71 (comment)

contrct_maker.Automaton is a modification of omega.symbolic.symbolic.Automaton to store multiple state machines. Arguably, it should be possible to model any component with two entities only: environment (lumping other players) and system. These correspond to the two quantifiers: universal and existential. So, a multi-player symbolic Automaton data structure would be superfluous in that respect.

Nevertheless, it turns out that, in practice, it is more convenient to store multiple state machines in dictionaries. The changes are relatively small, because Automaton.init and Automaton.action are already dicts. It is Automaton.win that should be come a dict too, and changes relevant to this.

This issue serves as a heads up to users about the forthcoming API change.

The required changes are relatively few, mainly related to dict.iteritems and its siblings. Python 3 syntax will be preferred, with the potential of affecting performance in Python 2. The latter is expected to be avoided by using the future package.

at the time of opening this issue, I notice out-of-date URLs in the root README. other documentation must be checked, too.

N.B., this is not critical because GitHub redirects automatically.

How do I plot the graph for the expression u below? Thanks, Gui

aut = trl.Automaton()
aut.declare_variables(x=(0, 3))
u=aut.add_expr('x = 3')```

Migration guide.

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 satisfies predefined GR(1) specification. But I can not find any sample document about such procedure.

Could anyone please help with some reference? Much appreciate

should be https://travis-ci.org/tulip-control/omega

related: tulip-control/dd#45