Bouncing better

During last week Jan implemented two improvements of the basic enclosure-based hybrid IVP solver. Both are based on a reduction of the set of potential states that the system may exist in, based on knowledge deduced from the hybrid IVP specification. The first one uses an explicit encoding of the states that are permissible while a particular ODE describes the dynamics of the system. The second uses the knowledge that the state immediately following a transition must satisfy the guard of the transition. 

The improvements in enclosure quality can be significant, as may be observed in the plots below. The first one shows the solution to the bouncing ball problem described previously, now simulated correctly but without using the additions:

 

The second one shows the plot resulting from simulating the same model but with the new additions:

Tests using a model of two tanks being filled and alternatively filled have indicated that the implementation may not be bug free and Jan will be concentrating on resolving this issue. Time permitting he will also address another possible addition to the solver based on dependency analysis of the ODE fields in a model.

Summing things up

This week Adam wrote a summary of his reading of the monograph "Languages and Tools for Hybrid System Simulation" and related work studying a common pathology of hybrid system simulation tools which he has done for the group. He has now begun a literature review of parallel programming, and will start by learning about deterministic parallelism.

Tales from the world of testing

This week Adam held an invited talk about automated testing of XSL Transformations at ETSE2012. The workshop covered a wide range of topics, ranging from analysis of performance requirement fulfillment in concurrent embedded systems, fully automatic tests of GUIs, to automatic derivation of formal test cases from natural language specifications. The workshop concluded with a fascinating talk by Mark Grechanik about moving from "linear" tests to adaptive tests which function like feedback control systems.

The ETSE workshop was co-located with ISSTA 2012, and Adam got the chance to attend some very interesting talks at this conference as well. Particular highlights were the keynotes by Martin Rinard (thought-provoking and controversial about program transformations which sacrifice correctness for accuracy and bug-freedom) and Rance Cleaveland (insightful about the interplay of research/fun and industry/profit), as well as Yannis Smaragdakis' talk on Residual Investigation, which presented a recipe for deriving a dynamic analysis from a given conservative static analysis.

Simpler and also correct

During last week Jan updated the hybrid IVP solver so that it implements the core of a recently developed and significantly simplified version of the algorithm. In a previous post it was possible to see that the solver was not correctly enclosing events in time. This may be observed by "flipping between" the two plots included in the post. The current version no longer exhibits this problem. Coming work will complete the implementation of the algorithm.

More operators and a Taylor expansion property

This week Yingfu and Adam continued working on the symbolic differentiation implementation in Scala.  The expression type was extended with exponentiation, the power operation and logarithms.  A memoized version of the evaluation function was also added.  More smart constructors were added along with a new differential function which computes higher order derivatives.  A new property-based test based on Taylor expansion was introduced.  It checks the difference between a function's value and the generated polynomial's value in a certain point.  This test was so far applied to unary functions and binary operators.

New hybrid solver specification

Last week Michal, Walid, Aaron, Veronica and Jan worked on the latest version of the hybrid IVP solver. The result is a much simplified algorithm that Jan feels he understands much better. He also started to update the Scala implementation to fit more closely with the new specification. In the coming week Jan plans to finish the update and start benchmarking the solver to get a better understanding of the current bottlenecks.

First steps in property-based testing of symbolic differentiation

This week Adam and Yingfu continued working on the symbolic differentiation implementation in Scala. The focus of the work was to get a property-based test up and running. The starting point was to implement a simple property - that the derivative of a monotonically increasing function (in one variable) is non-negative. The approximation of this property that was implemented uses a generator of polynomials which produces terms of odd degree and with non-negative coefficients. An issue with the current implementation is that the generator generally produces very large terms, which in turn makes the failure reports difficult to read. Future work in this direction will therefore target implementing shrinking of terms, as well as implementing additional operators which could be used to further reduce the size of the terms.