Does TLSF support only constant arithmetic expressions?

[johnyf]

From the description of TLSF, it appears that there are only 2 types of variables:

1. Boolean variables, for example x, and
2. vectors of Boolean variables ("buses"), for example y[5] declares the elements y[0]..y[4].

Integer variables seem to not be part of TLSF.

Integer constants though seem to be part of TLSF. In other words, g[k] where k has been defined as a fixed integer value, or ranges over a fixed set of integers that is enumerated to generate an output spec from syfco. In Sec. "Numerical expressions", p.6, this seems to correspond to "n identifier (bound to a numerical value)" (and also in the repository examples).

One of the reasons for asking this is that, if TLSF includes only Boolean variables (scalar or vector), then the syfco translation in any high level output format (for example structured Slugs or Promela) will contain only Boolean variables, even if a reduction to "basic TLSF" is not requested from syfco.

This implies that any tool that accepts structured Slugs will not have to do any bitblasting (as done by omega.logic.bitvector in my case), because there won't be any integers left to bitblast. Does syfco ensure that no integers (neither integer variables nor integer constants like 4) will appear in any output format?

[johnyf]

Another note is that if only Boolean variables (like x and y_0 for some bus element) appear in syfco output, then no variable type information (as in bus=array, integer, or Boolean) is needed. So, all variable identifiers in open Promela output (#5) known to be generated by syfco could be assumed to be Booleans.

Nonetheless, ownership information (env, sys) would still be needed. There is no shortcut in defining this information in open Promela, so the variables would then still be declared as bool.

[kleinreact]

Syfco resolves all integer, set and bus variables into pure boolean formulas such that the resulting specification contains only boolean and temporal operators. This is done for all output formats except full. Thus, you do not have to bother about any bitblasting or other representation issuses.

For future releases, it might be possible to allow only a partial evaluation, which is adapted to the higher level constructs supported by the corresponding output format. This might be especially of interest if the specification would explode otherwise. However, such a feature is not implemented yet.