Embedding differential equations into types

111 views
Skip to first unread message

gmhwxi

unread,
May 7, 2016, 3:50:21 PM5/7/16
to ats-lang-users

I'd like to report an interesting example of using types in ATS.

Here are two animations of bouncing balls:

http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html

The graphics is uninteresting. What is interesting here is that the differential equations governing the movement of the ball are
captured in the ATS types.

Cheers!

Raoul Duke

unread,
May 7, 2016, 5:41:06 PM5/7/16
to ats-lang-users

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 && v>0?

gmhwxi

unread,
May 7, 2016, 5:49:22 PM5/7/16
to ats-lang-users
M1 and M2 come from the corresponding dReach model..

What the ATS code does is to make sure the model is "correctly" implemented.

gmhwxi

unread,
May 11, 2016, 7:54:58 PM5/11/16
to ats-lang-users

gmhwxi

unread,
May 11, 2016, 7:56:56 PM5/11/16
to ats-lang-users
Adding a 2d-oscillator example:

http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/
http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html

Artyom Shalkhakov

unread,
May 11, 2016, 11:36:34 PM5/11/16
to ats-lang-users

What's this for?

prval () =
  $UN.prop_assert{false}()


Is it asserting falsity?

gmhwxi

unread,
May 11, 2016, 11:39:09 PM5/11/16
to ats-lang-users
I skipped the constraint-solving part, which needs to be exported to Z3.

gmhwxi

unread,
Jun 13, 2016, 6:08:13 PM6/13/16
to ats-lang-users
The directory is renamed as follows:

http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/CPS/DREACH/SCRATCH/bouncing_ball

Also, the constraints can now be solved if they are passed to patsolve_z3.

Steinway Wu

unread,
Jul 16, 2016, 11:53:42 PM7/16/16
to ats-lang-users
I'm a little confused. This is solved using z3, not using dReal, right? So what's the relation with dReal/dReach here? 

gmhwxi

unread,
Jul 16, 2016, 11:58:44 PM7/16/16
to ats-lang-users
In this case, the constraints do not involve transcendental functions (sin, cos, exp, etc.).
Once you have transcendental functions (and beyond), there is very little that z3 can do.
The hope is that dReal can be used to solve such constraints effectively in practice.

Steinway Wu

unread,
Jul 17, 2016, 8:48:30 AM7/17/16
to ats-lang-users
I see. Thanks!
Reply all
Reply to author
Forward
0 new messages