TLSF initial condition quantification

[johnyf]

#14 concerns the correspondence between TLSF and AIGER initial conditions. If a unique 0 initial state is defined in TLSF, then that fixes the AIGER initial state, and there is no question of quantification.

If not, i.e., multiple initial conditions are admissible in TLSF, then it seems that universal quantification is to be understood for these initial conditions. In other words, that the winning states should include all initial states. (In slugs, this is called "robotics semantics". In gr1c there is an option to choose the initial quantification, see "Interpretations of initial conditions".)

If alternating quantification is used (ALL_ENV_EXIST_SYS_INIT in gr1c, default behavior of slugs), then there should be a way for the synthesizer to express within the AIGER circuit what initial values of the Xc latches it chooses.

In more detail, there are two options for alternation, \forall Xu: \exists Xc and \exists Xc: \forall Xu:

• \exists Xc: \forall Xu: then the synthesizer would have to pick a fixed initial value for the Xc latches that works for all possible Xu. I think that there is a way for the synthesizer to incorporate such an initial condition in AIGER: under the assumption that all latches are initially 0, negate latches in the circuit, in order to obtain a negative initial condition for that variable.

  For example, variable x would no more be the latch a, but the signal ! a for a latch a. The problem with this approach is that the latch names can no more be those of variables. Nonetheless, this can be rectified by a suitable definition of outputs as negated latches, accordingly.

• \forall Xu: \exists Xc: then the synthesizer would produce a function that takes the initial condition Xu (some latches) and produces the initial condition Xc = f(Xu). This f would itself be a combinational circuit involving latches only, but defining it seems to be outside the scope of AIGER.

So, in TLSF, will a single initial state, or multiple universally quantified states, or multiple \exists \forall states be given?