Bence Graics
The abovementioned mapping has been implemented and the verification works. Now only the scheduling problem has to be solved during back-annotation (which parallelly running component ran/was scheduled).
The back-annotation of the scheduling has been solved in 37fff61d102e9ab2ea7872c8383793e2b369b505.
@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...
Sounds good, I think it is a great idea. If you need any help, let me know.
> > > I think setting up the PATH and the environment variables could be done in separate scripts, because that only needs to be done once, but every time...
The scripts have been working well for everybody that I have had contact with. Is there any specific reason to keep this issue open?
I few thoughts: - I left some programming specific comments. - _"it outputs models with an excessive amount of extra locations and edges, making verification slower"_ is a strong statement....