add functions as arguments

[ravenrothkopf]

always assume{
}
always guarantee{
    [x <- x + sin t];
}

generates

if (currentState ==  0 ){
    if (true){
        x = add(x, sin, t);
        currentState = 0;
    }
}

instead of

add(x, sin(t))

[leoqiao18]

This is a bug in the updateToAssignment implementations in HOA/Python.hs and HOA/JavaScript.hs modules.

The current (incorrect) implementation assumes that there is only a single level of function application in the RHS of the update term.

The fix can be a function term parser for the RHS? @santolucito If you think that is a good idea, I can go ahead and implement it in a PR.

[santolucito]

Yes awesome! In fact we want a function term parser for predicate terms as well

[leoqiao18]

Actually, there are a few more problems.

1. the preprocessor does not correctly translate binary operators. For example, [x <- x + 1 - 1] gets preprocessed to [x <- sub add x int1() int1() ]. This can be easily fixed by adding parentheses around binary operations.
2. the HOA representation has curried function application. For example, TSLMT [x <- g x x] is preprocessed to TSL [x <- g x x], which becomes [x <- ((g x) x)] in the HOA synthesis output.

The second problem is a lot more severe, because even if we fix the first problem, we still have the following sequence:

# TSLMT
[x <- x - 1 + 1]

# TSL
[x <- (add (sub x int1()) int1()) ]

# HOA synthesis output
[x <- ((add ((sub x) int1())) int1())]

which can be correct in languages that support partial application but incorrect in languages that don't (e.g. Python, Javascript).

[leoqiao18]

The encoding of the function term is correct all throughout the pipeline. The problem happens at the decodeOutputAP function, which is called in code generation. The function is defined in Logic.hs.

The function tries to parse the encoded string to a SignalTerm, and one possible signal term is a FunctionTerm. A function term is defined as the following ADT:

data FunctionTerm a =
    FunctionSymbol a
  | FApplied (FunctionTerm a) (SignalTerm a)
  deriving (Eq, Ord, Show)

which only curries all the applications (any function application must be a single-argument application).

[leoqiao18]

To solve these problems, I think it is best to define distinct (or at last the function term) ast's for TSLMT and TSL. The problems all seem to be coming from a lack of a clear TSLMT ast. For example in the above, using the TSL FunctionTerm is insufficient for us to recover the more expressive TSLMT function terms.

@wonhyukchoi What do you think?

[leoqiao18]

I think it might be worth it to spend some time refactoring/cleaning up some parts of the tsltools repo.

[wonhyukchoi]

@LeoQiao18 I added support for this a while back, check out Ast.hs

[leoqiao18]

Oh awesome. Then i can try to see if I can change the code generations to use this ast instead.

[wonhyukchoi]

Yeah, you can use fromSignalTerm, but you also need to pass in a function that tells you the arity though. You can look here for an example usage

[leoqiao18]

In code generation, I don't have access to anything that provides variable arity. The best way to correctly generate the code is to actually just parse the string into a TSLMT ast directly. Are you currently working on the TSLMT parser @wonhyukchoi ? I can help with that if you are busy with other things.

[wonhyukchoi]

Let's chat offline

[leoqiao18]

Fixed in #43