XSTS: support choice-else operations

[arminzavada]

I propose the extension of the XSTS language with a choice-else branch.

The else branch on a choice would behave as a last resort default branch, that is only executed iff all other branches are disallowed (because of failing assume operations).

Doing so would allow the simple representation of a frequent pattern in Gamma and Semantifyr. Currently, choice-else is supported using a model rewrite logic, which is difficult to verify and produces unreadable XSTS code.

If the choice-else could be mapped to an efficient solver formula, then it would be worth implementing on the Theta side. Otherwise, it may or may not have any benefit, considering that the choice-else rewrite logic already exists in OXSTS.

Example:

choice {
    assume (x < 5);
    y := 1
} or {
    assume (x > 10);
    y := 2
} else {
    y := 3 // 5 <= x <= 10
}

Is rewritten into:

choice {
    assume (x < 5);
    y := 1
} or {
    assume (x > 10);
    y := 2
} or {
    assume (! (x < 5) || (x > 10));
    y := 3 // 5 <= x <= 10
}

[mondokm]

I think this would be challenging to introduce to Theta, because in a Theta choice statement, assumptions can appear in arbitrary places (inside very complicated control structures), not just the beginning.

Consider the following choice for example:

choice {
    if (x > 0) {
        for i from 1 to y do {
            assume(z < 3);
        }
    }
} else {
    ...
}

[arminzavada]

I think this would be challenging to introduce to Theta, because in a Theta choice statement, assumptions can appear in arbitrary places (inside very complicated control structures), not just the beginning.

Consider the following choice for example:

choice {
    if (x > 0) {
        for i from 1 to y do {
            assume(z < 3);
        }
    }
} else {
    ...
}

Yes, that is one of the strongest motivations for this proposal. In OXSTS, assumptions can also appear anywhere in a choice, which is mostly handled correctly, except in some edge cases.

I remember a conversation about possibly mapping a choice-else into logical formulae that could be interpreted by the solver. Was this proven to be impossible? I tried to implement something similar in my fork, but I was not able to complete it alone:

https://github.com/arminzavada/theta/blob/524052dd63664d39acfdaa3103d1b0857a499ade/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtToExprTransformer.java#L163-L190

[arminzavada]

After a brief discussion, we arrived at the following conclusion.

Choice-else operations can not be efficiently mapped to SMT formulae because they require a not exist quantifier since the else branch must only be allowed if the other branches can not be satisfied. This introduces a significant computational complexity that most solvers can not solve efficiently.

Solving this requires further constraints on assumptions, which could possibly require the introduction of more high-level language constructs - such as switch operations - whose guard assumptions may only appear at fixed places in the model.

It has not yet been decided whether these language features would be implemented on the Theta side or the Gamma/Semantifyr side.