Generating generators

This week Adam started looking at QuickCheck-style property-based testing. He has been focusing on understanding how to create generators "from scratch" as well as how to use combinators to create new generators from existing ones.

One problem which Adam faced was how to create a generator for a nested data structure. Perhaps unsurprisingly, the solution was to use recursion in the comprehension which constructs the generator.

Parametric IVP solver

Building on lazy analytic functions Veronica and Jan have now completed an implementation of a generic solver for initial value problems. The ideas for the solver are borrowed from the work on validated numerics by Davis and Tucker. The solver computes an interval enclosure of the solution and takes the following parameters:
a)  the field as a function of type (A,A) => A for any type A that can be used for endpoints of intervals and as a representation of the real numbers,
b) one such type
c) the initial value of type A
d) the degree for the Taylor expansion used to approximate the solution at each step
e) the step size
Our implementations are in Scala where we could make use parametric polymorphism, overloading and a lazy datastructure in the procedure for automatic differentiation. As a result the taylor coefficients for the sought function needed at the points where the solution is calculated and at intervals are expressed as a mutually recursive definition using the field and the initial value in the lazy data structure. We have performed some experiments with both constructive reals (a Java implementation by Boehm) and BigDecimals (a Java library). 

The following graph summarizes one experiment with the IVP given by x'(t) = -x(t)^3 with x(0)=1up to t = 4. In the graph below we show the execution time and the width of the enclosing interval at time = 4 for  constructive reals and big decimals with precision 10. 

Future work includes a) completing the library for using big decimals as endpoints, b) completing the library for intervals and c) using these libraries in an implementation of a Picard solver. We will also start writing about the program, the experiments and how to use the solver in the context of the parametric version of Acumen.

Interval endpoints should be rounded

Continuing their work on parametrised safe numerics in Scala, Veronica and Jan now have an implementation of intervals parameterized on the type for the endpoints. This type is required  to have numeric operations in 2 versions: for rounding up  and for rounding down. These operations can then be used to define interval extensions of numeric operations that are safe, in the sense that they enclose the result.

Consider the example of addition of intervals [a,b] + [c,d] = [a+c,b+d] when a,b,c and d belong to a type A in which the sum of two values is not necessarily in A. To make the resulting operation safe we need to use a lower bound plusL(a,c) on a+c and an upper bound plusU(b,d) on b+d as the endpoints of the result. Making this a special case of a generic scheme we define plus[Interval[A]]([a,b],[c,d]) as [plusL[A](a,c),plus[A]U(b,d)].

Veronica and Jan have tested the scheme with  BigDecimal as an  instance of the the type of endpoints. The size of the mantissa can be provided as an argument to the instance.  Coming work will focus on a) adding to the set of operations supported by the BigDecimal instance, b) completing the numeric operations for intervals (trigonometric functions) and c) implementing a validated IVP solver using Taylor expansions and intervals of constructive reals.

Lost in transition

As described in Adam's paragraph from last week, the initial implementation of the Three point masses hybrid system, based on a DFA version of the Three point masses NDFA (see reproduction of original NDFA figure below, based on Figure 2.2 on page 15 of Languages and tools for hybrid systems design) manifested incorrect behavior during simulation.

Specifically, after the system made the first transition with label F2 (making the middle mass m2 fall from the table) the rightmost mass m3 subsequently fell through the floor instead of bouncing. The reason for this behavior is a missing transition (with label B3) in the m2bounce state of the original NDFA. Without this transition, when the automaton is in the m2bounce state, the bounce event for m3 is not detected. The STATEFLOW hierarchical automaton part of the SIMULINK implementation of the Three point masses hybrid system presented in the monograph (see Figure 3.3 on page 30) does include corresponding transitions for every state in which a bounce event can occur. Adam thinks that this will make it exhibit the correct behavior and will proceed to implement this hierarchical DFA in Acumen in order to verify his hypothesis.

A Core Language for Executable Models of Cyber Physical Systems (Preliminary Report)

Various members of the group worked to finalize the preliminary report on core Acumen that will appear in the proceedings of the Second International Workshop on Cyber-Physical Networks (CPNS'12).  Featured in this report is a description of the Ping Pong model that was developed by Yingfu Zeng and used in this year's CPS course at Halmstad University.  The report will be presented in Macau by Yingfu, who is currently finishing his Masters thesis at Halmstad University.  This fall, Yingfu is will start his PhD studies at Rice University.

Code Coverage

Anil worked with code coverage analysis for the examples in the tutorial of Accurate Programming 
The image below shows the overall result.  More detailed results
The instructions for the SCCT plugin setup for SBT can be found in his Blog .

Three point masses

This week Adam continued reading the monograph Languages and tools for hybrid systems design by Carloni, Passerone, Pinto and Sangiovanni-Vincentelli. To gain a better understanding of the first of two running examples used throughout this book – a hybrid system modeling three point masses (see page 13) – Adam set out to implement the system in Acumen. The implementation approach was to use the finite automaton describing the system (page 15) as a specification, in order to get an implementation as close as possible to those presented in the remainder of the monograph. Given that the automaton is non-deterministic, it was necessary to first convert it to the following deterministic finite automaton (DFA) to make it possible to simulate it.

The initial Acumen implementation of this DFA turned out to have surprising behavior. When the green mass (m2) starts falling (corresponding to transition F1 in the DFA above), the blue mass (m3) also begins to fall. Click here for a video of this simulation.

Reducing this automaton to one with a single mode made the simulation exhibit the expected behavior. Click here for a video of this simulation (please note that different initial conditions were used here).

Adam is currently studying the related discussion and implementations in the monograph in order to understand the causes of this behavior.

Lazy analytic functions in Scala

During last week Jan and Veronica continued to explore Scala programs that use intervals and automatic differentiation, following ideas explored in the masters thesis of A. Danis (supervised by  W. Tucker). We now have scala programs that can enclose a function with the Taylor expansion (coefficients calculated using automatic differentiation) on intervals. The Lagrange error term is calculated on the whole interval. Here we see the function f(x) = (x^2+1)/(x^3-1) on the interval [3,4] enclosed with Taylor polynomials around 3 of degrees 1 (left figure) and  5 (right figure).

We also found out that due to the fact that we use a lazy datastructure to collect the derivatives of a function when doing automatic differentiation in Scala, we can turn an  initial value problem into the Taylor expansion of both the sought function and the field around the initial value.  This can be combined with tests to decide whether there is a solution around the initial point to approximate the solution in the next point.

Parametrising Safe Numerics

Veronica and Jan have been working on parametrising safe numeric computation in Scala by real types. Extending the previous work on Parametric Acumen they included intervals with exact rationals and BigDecimal endpoints and tested them with Forward Euler. They are currently working on a parametrisation of the type of endpoints. For the moment the IVPs that can be handled with intervals are limited by the lack of support for elementary functions. Adding these functions will be the focus of their work over the near future. 

Learning about CPS modeling languages

This week Adam started reading the monograph Languages and tools for hybrid systems design by Carloni, Passerone, Pinto and Sangiovanni-Vincentelli. It is a survey of various approaches to modeling and simulation of hybrid systems including verification tools, programming languages and modeling environments. These disparate software applications are compared to each other and illustrated using two example models.