scungao
commented
9 years ago Thanks Stanley. Yes we've been too lazy on updating the webpage. In fact what we wanted is to put a nonlinear model there.
There's no easy way for encoding x' = x ± 1 yet. Ideally we can do that when the flow can be analytically represented, but in the general case nondeterministic flow requires second-order quantification. For something like x'=[2,3], we could say x'=a where a is used as a constant in [2,3]. But this is mostly cheating, as it wouldn't allow a to change during the flow. Again, we can do it when the flow can be expressed explicitly as a function over time; so in this case it's easy but we still need to do it.
We need to update the webpage soon. Thank you very much for the careful correction.
On Wed, Jan 28, 2015 at 1:47 PM, Stanley Bak notifications@github.com wrote:
On the dreach homepage (http://dreal.github.io/dReach/), for the input format description, there is a bouncing ball model. Under that, there are descriptions of various parts of the model.
1.
For the dynamics, it says "v' =−g±(D×v)" which does not match the model file that is given. The actual dynamics in the model are "v' = -g + (-D×v)". 2.
As an aside, is there a way to include ± within flows? For example, can I have x' = x ± 1? or x' = [2, 3]? Or is the only way to introduce a new variable with that range, use that in the derivative, and set its derivative to 0? 3.
Later on in the description, for the guard it says the reset is "v′=K×v", whereas in the model it is "v′=-K×v". The same mismatch also appears before the model in the sentence "The ball is partially elastic. Whenever it hits the wall, it loses its velocity (v'=K×v)."
— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/74.
stanleybak
On the dreach homepage (http://dreal.github.io/dReach/), for the input format description, there is a bouncing ball model. Under that, there are descriptions of various parts of the model.