ARCH-COMP 2019

[schillic]

This is a meta issue for collecting tasks and cross-references for ARCH-COMP 2019.

AFF

• add benchmark script to run all benchmarks (#93 - Benchmark scripts for AFF #94)
• adapt axis ranges in plots to suggestions in report (ARCH-COMP benchmark fixes #118)
• double-check discrete-time time steps (Adapt discrete time steps for ARCH-COMP 2019 #120)
• add dashed lines to plots for property (ARCH-COMP benchmark fixes #118)
• ISS
  • add plot creation (Plots for ISS model #96)
  • resolve regression
• Spacecraft rendezvous
  • add benchmark script (#93 - Benchmark scripts for AFF #94)
  • add plot creation (#93 - Benchmark scripts for AFF #94)
  • investigate "aborting" scenario (no behavior after switching to the "aborting" location) (Fix inputs for Spacecraft Rendezvous benchmark #103)
  • update model to recently proposed changes (New scenarios for Spacecraft Rendezvous model #105)
  • make new versions work
  • investigate which specification is most efficient to check (BadStatesProperty or SafeStatesProperty, box given as constraints or as BallInf)
• Powertrain
  • add model (Add parametric powertrain model (ARCH2018 AFF) #41, Add parametric powertrain model (ARCH2018 AFF) #41, Powertrain #112)
  • make it work
  • add script for benchmarking and plot creation
• Building (Building benchmark #89)
  • add plot creation (Plots for Building model #95)
• Platooning
  • add benchmark script (#93 - Benchmark scripts for AFF #94)
  • add plot creation (#93 - Benchmark scripts for AFF #94)
  • add unbounded-time setting (Use proper unbounded setting in Platooning model #101)
  • make BND30 setting work
• Gearbox
  • make it work (Make Gearbox benchmark succeed #86)
  • add script for benchmarking and plot creation

NLN

• add benchmark script to run all benchmarks and create plots (Add ARCH COMP NLN script #121)
• add TMJets to Reachability (Reachability#537)
• Van der Pol (Van der Pol benchmark #84)
  • add scenario μ = 2 with evolution time = 8 seconds
  • show both results in one plot (range of the plot: [-2.5,2.5]x[-4, 4])
• Laub-Loomis (Laub-Loomis benchmark using TMJets #83)
  • add W=0.05 as an additional width
  • show both results in one plot
  • output width of x4 in the final set
• Quadrotor (Quadrotor benchmark #97)
  • update and add issue with bench results and plot (Add quad TMJets #98)
• Spacecraft rendezvous (Spacecraft rendezvous benchmark #59)
  • add model (#59 - Spacecraft Rendezvous model with TMJets #122)
  • make it work

[schillic]

Current results:

AFF

ISS
("ISU01", "dense") => TrialEstimate(1.103 s)
("ISS02", "discrete") => TrialEstimate(267.215 ms)
("ISU01", "discrete") => TrialEstimate(8.328 s)
("ISS01", "discrete") => TrialEstimate(1.906 s)
("ISU02", "discrete") => TrialEstimate(142.628 ms)
("ISS02", "dense") => TrialEstimate(515.296 ms)
("ISU02", "dense") => TrialEstimate(394.097 ms)
("ISS01", "dense") => TrialEstimate(2.625 s)

rendezvous
("SRNA01-SR01", "dense") => TrialEstimate(711.522 ms)
("SRNA01-SR01", "discrete") => TrialEstimate(339.373 ms)
("SRA01-SR02", "discrete") => TrialEstimate(550.754 ms)
("SRA01-SR02", "dense") => TrialEstimate(1.240 s)

building
("BLDF01-BDS01", "dense") => TrialEstimate(230.333 ms)
("BLDC01-BDS01", "dense") => TrialEstimate(157.276 ms)
("BLDF01-BDS01", "discrete") => TrialEstimate(136.422 ms)
("BLDC01-BDS01", "discrete") => TrialEstimate(133.928 ms)

platooning
("PLAD01_BND42", "discrete") => TrialEstimate(188.199 ms)
("PLAN01_UNB50", "discrete") => TrialEstimate(7.339 s)
("PLAD01_BND42", "dense") => TrialEstimate(600.418 ms)
("PLAN01_UNB50", "dense") => TrialEstimate(9.370 s)

[lbenet]

For NLN I think we should also add a point related to the Van der Pol system with a different parameter.

[schillic]

You can just edit above if you want.

[mforets]

You can just edit above if you want.

I added the open task, thanks for the reminder Luis ;)
It has been communicated that we should experiment with different values of mu. This parameter governs non linearity and for increasing values the limit cycle becomes "sharper".