Open benedekh opened 3 years ago
@vincemolnar and I have consulted about the issue and we have concluded that the transformation of such select
expressions to havoc
expressions in the XSTS model can lead to non-deterministic behavior in choice actions
due to the else branch. This could be addressed by for example introducing if-else actions
in the XSTS language in the future.
See the introduction of havoc actions in 4a0c205.
SelectExpression exptects an Expression as
operand
from which it chooses a value. At the moment IntegerRangeLiteral and ArrayListLiteral expressions are supported. However, it would be useful if we could select any Integer, Boolean, Real, etc. values not only from a range./cc @vincemolnar