Embedding differential equations into types


#1

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!


#2

Renaming Github to GitHub:

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.htmlOn Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#3

I see. Thanks!On Saturday, July 16, 2016 at 11:58:44 PM UTC-4, gmhwxi wrote:

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.

On Saturday, July 16, 2016 at 11:53:42 PM UTC-4, Steinway Wu wrote:

I’m a little confused. This is solved using z3, not using dReal, right?
So what’s the relation with dReal/dReach here?

On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:

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.

On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote:

I skipped the constraint-solving part, which needs to be exported to Z3.

On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:

On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:

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

What’s this for?

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

Is it asserting falsity?

On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#4

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.On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote:

I skipped the constraint-solving part, which needs to be exported to Z3.

On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:

On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:

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

What’s this for?

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

Is it asserting falsity?

On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#5

I skipped the constraint-solving part, which needs to be exported to Z3.On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:

On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:

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

What’s this for?

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

Is it asserting falsity?

On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#6

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?


#7

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


#8

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

What’s this for?

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

Is it asserting falsity?On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#9

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.On Saturday, July 16, 2016 at 11:53:42 PM UTC-4, Steinway Wu wrote:

I’m a little confused. This is solved using z3, not using dReal, right? So
what’s the relation with dReal/dReach here?

On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:

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.

On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote:

I skipped the constraint-solving part, which needs to be exported to Z3.

On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:

On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:

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

What’s this for?

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

Is it asserting falsity?

On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#10

I’m a little confused. This is solved using z3, not using dReal, right? So
what’s the relation with dReal/dReach here?On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:

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.

On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote:

I skipped the constraint-solving part, which needs to be exported to Z3.

On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:

On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:

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

What’s this for?

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

Is it asserting falsity?

On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!


#11

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.htmlOn Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:

Renaming Github to GitHub:

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

On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:

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!