HPWA Problem: Drivedrain
This benchmark is taken from
M. Althoff and B. H. Krogh. Avoiding geometric intersection operations in reachability analysis of hybrid systems. In Hybrid Systems: Computation and Control, pages 45-54, 2012
The model files were taken from the attachments to
"Rigorous Simulation-Based Analysis of Linear Hybrid Systems", S. Bak, P. Duggirala, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017)
available at http://stanleybak.com/.
There are two instances:
1) theta1_100percent refers to the initial states as given in the TACAS 2017 paper above.
2) theta1_5percent has the initial states with the same center, but shrunken in diameter to 5%.
SpaceEx is able to handle case (2), but not case (1).
| Attachment | Size |
|---|---|
| bytes |
Do we want to consider other cases, like (single-point), 1%, 10%, 50%?
Also, I think the FORMATS version we had the formal spec that the system passes through the deadzone completely without going back, so going from deadzone -> first mode is an error as well as last mode -> deadzone. Should we use this as the formal spec as well?
There's also a neat video of the reachability of this model made with Hylaa: https://www.youtube.com/watch?v=dxMN9szGIrk
Here's a plot using Hylaa that meet the above-mentioned spec and the script used to create it:
Dear Stan,
I have prepared several versions of the drivetrain example in the report. Could you check the report and let us know if you like to make modifications?
-Matthias
It looks pretty good. I would suggest also adding versions with very small initial sets to try to get more tools to analyze the model. For example, we could remove the theta=12 case, and a version with an initial set that is 1% of the original one.
Hyst has a built-in model generator for this system. This means you can create the model internally and output to any tool supported by Hyst (Hylaa, SpaceEx, Flow*). The command line you want to use is:
java -jar Hyst.jar -gen drivetrain '-theta 22 -init_scale 0.3 -reverse_errors' -passes sub_constants '' simplify -p -o hylaa_output.py -tool hylaa ''
In this case, I generate the version with theta=22 and the initial set is 30% of the original one (this is case DTN06 from the overleaf report). The '-reverse_errors' flag will add error modes on reverse transitions that ensures the spec is met if the tool classifies the systems as safe. The two transformation passes "sub_constants" and "simplify" are needed to make the dynamics be simplified linear ones. Finally, in this case I was outputting to hylaa, so you can change that part to whatever output you want.
If you're even more ambitious, you can use hyst in combination with hypy to generate the models and automatically run the tool on them. Then you can do all 6 cases from one script. I attached what I used for hylaa.
for the spec for this one, I would also want to add the condition that you can't go from z2 back to z1. Something like:
(z1 U z2 U z3) = G(z3)
In the github repository in the src folder there is a compiled Hyst.jar that you can directly use in the future. You might need to go through the readme to setup some environment variables first for the pythonbridge part, though. Compiling is also not too hard, we use ant which is the equivalent of make for java (I think the readme has details).
The command for spaceex would be: java -jar Hyst.jar -gen drivetrain '-theta 22 -init_scale 0.3 -reverse_errors' -passes sub_constants '' simplify -p -o drivetrain_out.xml -tool spaceex ''
Anyways, I've attached the models as well.
Dear all,
Can we use a box initial set? since the current API of Flow* does not support zonotope initial sets.
thanks,
Xin
Dear Xin,
the current initial set has been chosen by the following consideration: Based on the range of initial angular velocities, the other initial states are chosen as the steady state solution for an external load of 300 [Nm], resulting in the current initial set.
However, I am open to using a box initial set, but it has to be carefully chosen since this could cause many oscillations. Do you have a suggestion for a box initial set?
Is it ok for you if in at least one instance we keep the zonotopic initial set?
Hi Matthias,
Thanks! I just added a new function in the Flow* API last weekend to handle zonotope initial set. It works very well now, I just need some time to find potential bugs.
thanks,
Xin
Hi Stan,
It's really great that you made the model generator. Thanks for the work! I tried to use your command line on the Hyst that's for download at http://verivital.com/hyst/hyst1.17.zip. It says that the options (gen...) are unknown. I also downloaded the latest version of Hyst from Github, but I wasn't able to compile it (I have zero skills with Java).
Any chance you could directly post the models for -- ahem, ahem -- SpaceEx?
Cheers,
Goran