tslsynth: "True" cannot be part of an AST.

[w14]

tslsynth is happy with this program:

always assume {
	f x <-> X u;
}

always guarantee {
	false -> [ u <- false ];
	false -> [ u <- true ];
}

but unhappy when you replace the last "false" with "true". The error is:

tslsynth: "True" cannot be part of an AST.

Is this the intended behavior? If not, I will fix it.

[santolucito]

doesn't seem like intended behavior. I guess the issue is with the HOA to code writer. Overall it seems the support of booleans as values for update terms isn't working too well. It is a bit of a different case than regular values since with booleans we want to cross between the data-level and the control-level (where an update terms value is directly evaluated by the control structure). Might be worth making sure we aren't doing something that doesn't fit into the theory here...

[leoqiao18]

Reviving this after a discussion with @santolucito .

First, the error message is correct, intended behavior. true and false are constructs that live within the metatheory/logic, while the RHS of an update term should be terms from the theory (whether it is UF, EUF, LIA). Specifically, a true/false in the metatheory and a true/false in a theory are different. Take the following spec as an example (I think it's from some version of a GameOfLife spec in TSL_LLM_Benchmark):

always guarantee {
    (alive && neighbors < 2) -> [alive <- false];
    (alive && (neighbors = 2 || neighbors = 3)) -> [alive <- true];
    (alive && neighbors > 3) -> [alive <- false];
    (!alive && neighbors = 3) -> [alive <- true];
}

From a pedantic view, [alive <- false] would not make sense, because we are using false (a metatheory construct) as a function term (a theory construct). The most correct way to write this would be:

always assume {
    [alive <- t()] -> X (isT alive);
    [alive <- f()] -> X !(isT alive);
}

always guarantee {
    (isT alive && neighbors < 2) -> [alive <- f()];
    (isT alive && (neighbors = 2 || neighbors = 3)) -> [alive <- t()];
    (isT alive && neighbors > 3) -> [alive <- f()];
    (!(isT alive) && neighbors = 3) -> [alive <- t()];
}

This works but is not totally satisfactory, because, intuitively, the previous one kind of makes sense. Again, the root of the problem is that an update term is only defined when the LHS and RHS are both at the theory level. The side effect of this is that it forces all cells and outputs (the LHS) to be theory-level variables.

Our intuition really comes down to the idea that cells and outputs could also be metatheory-level variables. To make this happen, we would need to allow an update term to have LHS and RHS that are at the metatheory level.

After this whole explanation, here is a concrete roadmap for how to make this happen. The goal is to make the first code snippet work.

1. We need to identify which cells and outputs are metatheory level. This is easy: any cell/output that is of Boolean type should be now treated as a metatheory level variable.

2. Desugar the update terms for these Boolean cells/outputs. Using the first code snippet as the example, it should now be transformed to:

always guarantee {
    (alive && neighbors < 2) -> X !alive;
    (alive && (neighbors = 2 || neighbors = 3)) -> X alive;
    (alive && neighbors > 3) -> X !alive;
    (!alive && neighbors = 3) -> X alive;
}

The rewrite rules are:

• [y <- true] --> X y
• [y <- false] --> X !y
• [y <- ...] --> X y <-> ... (Note: originally Mark and I thought it would be X (y <-> ...), but that would be incorrect! Because y in the next time step should take the Boolean value of ... in this time step.)

3. Remember to set these cells and outputs as "outputs" in TLSF for LTLSYNT. If we forget to do this, these cells and outputs would be regarded as "inputs" by the current TSL pipeline, and would result in a semantically different spec for LTLSYNT.

4. Codegen needs to remember to codegen these cells and outputs as updates (a.k.a. assignments in the synthesized program):

• y --> y = true
• !y --> y = false

[santolucito]

Great write up @leoqiao18 ! @ravenrothkopf this is a good issue for you to tackle as we discussed. No rush, this is just a nice-to-have and a fun project rather than a blocking feature.

We also should start by making this more explicit from a theory side too. We'll want to make an update to the TSL grammar and formalize how we allow this crossing the language/meta language divide (on this note, just a thought, how does this relate to dependent typing?).

[santolucito]

Ah seeing now that this is an issue @w14 first raised. @w14 you're also more than welcome to tackle this if you like ofc. Again I think this is a low priority at the moment though compared to our TSL LLM work.