Joint deployment and schedule synthesis does not work if two tasks have the same name
OBSERVED PROBLEM
On examples where at least two tasks have the same name, joint
deployment and schedule synthesis does not work properly.
How to reproduce the problem:
- In the DSE perspective (Home view) load the enclosed model: ACC-nodepl.af3_23
- Go to Deployment Synthesis
- Select the checkbox: Enable joint schedule synthesis
- Press the button Generate
- The problem appears to be unsolvable (a warning suggests to relax the constraint set)
The example model is just the ACC example, where random WCETs and
periods have been assigned to tasks.
At a first sight, the problem seems to be related to the presence of two
tasks with the same name (Task_<).
By loading the other enclosed model file ACC-nodepl-working.af3_23
(where one of the tasks has been renamed as Task_2<), we get a
solution.
Also related to #3547 : Check/fix identifier names generation in Z3.
(from redmine: issue id 3559, created on 2018-10-24, closed on 2019-07-02)