# Embedding differential equations into types

**URL:** <https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737>\
**Category:** Google Group\
**Created:** [May 7, 2016, 7:50pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737 "2016-05-07T19:50:21Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 7, 2016, 7:50pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/1 "2016-05-07T19:50:21Z")

</div>

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/)  
[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_anim.html)  
[http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 11, 2016, 11:54pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/2 "2016-05-11T23:54:58Z")

</div>

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/)  
[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_anim.html)  
[http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_anim.htmlOn](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/)
> 
> [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_anim.html)
> 
> [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![steinwaywhw](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/steinwaywhw/32/2_2.png) [@steinwaywhw](https://discourse.ats-lang.org/u/steinwaywhw)\
**Post date:** [July 17, 2016, 12:48pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/3 "2016-07-17T12:48:30Z")

</div>

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](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/)
> > > > > > 
> > > > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.html](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/)
> > > > > > > 
> > > > > > > [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_anim.html)
> > > > > > > 
> > > > > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > > > > > > > 
> > > > > > > > [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_anim.html)
> > > > > > > > 
> > > > > > > > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 13, 2016, 10:08pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/4 "2016-06-13T22:08:12Z")

</div>

The directory is renamed as follows:

[http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/CPS/DREACH/SCRATCH/bouncing\_ball](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/)
> > > 
> > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.html](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/)
> > > > 
> > > > [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_anim.html)
> > > > 
> > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > > > > 
> > > > > [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_anim.html)
> > > > > 
> > > > > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 12, 2016, 3:39am UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/5 "2016-05-12T03:39:09Z")

</div>

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/)
> > 
> > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.html](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/)
> > > 
> > > [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_anim.html)
> > > 
> > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > > > 
> > > > [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_anim.html)
> > > > 
> > > > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![Raoul\_Duke](https://avatars.discourse-cdn.com/v4/letter/r/bbe5ce/32.png) [@Raoul\_Duke](https://discourse.ats-lang.org/u/Raoul_Duke)\
**Post date:** [May 7, 2016, 9:41pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/6 "2016-05-07T21:41:05Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 7, 2016, 9:49pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/7 "2016-05-07T21:49:21Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Artyom\_Shalkhakov](https://avatars.discourse-cdn.com/v4/letter/a/6bbea6/32.png) [@Artyom\_Shalkhakov](https://discourse.ats-lang.org/u/Artyom_Shalkhakov)\
**Post date:** [May 12, 2016, 3:36am UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/8 "2016-05-12T03:36:34Z")

</div>

> 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/)
> 
> [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.html](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/)
> > 
> > [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_anim.html)
> > 
> > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > > 
> > > [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_anim.html)
> > > 
> > > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [July 17, 2016, 3:58am UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/9 "2016-07-17T03:58:43Z")

</div>

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](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/)
> > > > > 
> > > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.html](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/)
> > > > > > 
> > > > > > [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_anim.html)
> > > > > > 
> > > > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > > > > > > 
> > > > > > > [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_anim.html)
> > > > > > > 
> > > > > > > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![steinwaywhw](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/steinwaywhw/32/2_2.png) [@steinwaywhw](https://discourse.ats-lang.org/u/steinwaywhw)\
**Post date:** [July 17, 2016, 3:53am UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/10 "2016-07-17T03:53:41Z")

</div>

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](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/)
> > > > 
> > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.html](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/)
> > > > > 
> > > > > [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_anim.html)
> > > > > 
> > > > > [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > > > > > 
> > > > > > [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_anim.html)
> > > > > > 
> > > > > > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 11, 2016, 11:56pm UTC](https://discourse.ats-lang.org/t/embedding-differential-equations-into-types/737/11 "2016-05-11T23:56:56Z")

</div>

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/)  
[http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator\_2d\_anim.htmlOn](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/)
> 
> [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_anim.html)
> 
> [http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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/)
> > 
> > [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_anim.html)
> > 
> > [http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing\_ball/bouncing\_ball\_with\_drag\_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!