dreach homepage explanations do not match sample model file

[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.

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 ranges within flows? For example, can I have x' = x + [0,1], or x' = [x, x^2]? Or is the only way to introduce a new variable for constant ranges, 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)."

[scungao]

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 [email protected]
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.

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
#74.

[stanleybak]

Makes sense, thanks Sean.