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.