Yet another adaptive cruise controller
I was able to run the files you provided. Running with 2 vehicles was fairly quick, whereas 6 vehicles took a long time with SpaceEx/Phaver (I stopped it after 8 minutes). What are the expected runtimes for these models? Also, which instance do you recommend that is difficult enough to be interesting, but not too difficult that tools won't be able to handle the model?
I have a very similar case which I will post in the HBMC category. I think the intersting point of this model is that it is scalable, you can introduce arbitrary number of cars into the system to increase the size, number of variables and locations, of the model. Therefore, this case is suitable to measure the scalability of the tool.
Please find attached the ACC SpaceEx models for 7 and 8 cars.
Note: for the unsafe models (ACCU*) we adopted a much shorter encoding
for the forbidden region; I would appreciate if someone can confirm that
it is going to be equivalent to those encoded for the models having fewer cars.
Enea.