M1 and M2 come from the corresponding dReach model..
What the ATS code does is to make sure the model is "correctly" implemented.On Saturday, May 7, 2016 at 5:41:06 PM UTC-4, Raoul Duke wrote:
Keen. Why M1 and M2? Eyeballing it, they seem like they should instead be
testing the sign of v? Also because I think it would be good to be
testing/constraining the sign of v. As in what if / how to disallow X<=0 &&