Properties for the solver's foundation

During the past week, Adam was helping Jan develop a suite of properties and generators for the affine enclosure- and interval arithmetic library that underlies the enclosure-based hybrid solver. Adam learned several useful lessons about testing scientific code using generator-driven PBT. In particular, that shrinking can lead to misleading error messages, that run-time assertions help development of generators and properties (and debugging in general) and that generating small values is often much more useful for finding bugs than aiming for a uniform coverage of the algorithm's state space. During the coming week Adam plans to add PBTs for the higher-level parts of the solver's algorithm, set up SCCT to obtain coverage metrics for the solver code and continue familiarising himself with Delite.

Testing enclosure arithmetic

During the past week Adam and Jan worked on improving the quality of the enclosure based hybrid solver by developing a suite of property based tests for the underlying enclosure arithmetic. One observation was that enclosures  may have (surprisingly) weak properties,. They may, for example, not satisfy seemingly obvious monotonicity properties. A concrete example may be observed when using affine Chebyshev approximation (in the sense of Darulova and Kuncak) for quadratic terms to approximate the quadratic term x^2. For x in [0,1] one obtains [x,x-0.25] and for x in [0,0.5] the result is [0.5*x,0.5*x-0.0625]. An illustration of this is provided below:

The latter is everywhere point-wise thinner than the former, however the former does not contain the latter as an enclosure. In the coming days the property based testing of the solver will continue as well as work to extend the arithmetic operations supported in the arithmetic.

Translation from ODE to WHILEdt language

During his two-week visit to the EMG group, Kohei aims at investigating the relation between ODEs and WHILE^dt. WHILE^dt is an imperative language extended with an "infinitesimal" constant. By using this language, one can model hybrid systems in the form of imperative programs. This week Kohei designed a translation from ODE into WHILE^dt, and proved that this translation is correct if the original ODE has a unique solution. In the next week, Kohei plans to investigate ODEs with non-unique solutions.

Weekly meetings resumed

The team at Halmstad resumed weekly meetings on Monday afternoons.  This meeting will replace the weekly lunch that used to take place on Tuesdays.  A standing agenda will be used as a guideline for meetings.  The new and more structured format for the meeting appears to improve the efficiency of the meeting.  Thanks to everyone for making the first meeting a success!

Lattices, properties and smart constructors

During the past week, Adam has finished a first reading of A Lattice-Theoretical Approach to Deterministic Parallelism with Shared State by Lindsey Kuper and Ryan R. Newton which introduces LVars as a novel building block for deterministic parallel programming. LVars are variables which support put operations of monotonically increasing values (with respect to a given domain) and can be thought of as a generalisation of IVars (single-assignment variables). Further, Adam and Jan have been working on adapting the previously constructed symbolic differentiation implementation (more specifically, its "smart constructors") to improve the execution time of a bipedal robot model written in Mathematica and Matlab, with some success – a first attempt which is still missing several optimisations gave a 10% performance improvement. During the coming week Adam plans to focus on creating PBTs of the most critical parts of safesolver, and to begin looking in to the LMS framework Delite.

A Student's Guide to Maxwell's Equations

Since being introduced to Lagrangian modeling by Marcie and Aaron, Walid has been developing a renewed interest in physics.  Last week he started reading Daniel A. Fleisch's very nicely written Student's Guide to Maxwell's Equations, the basic equations of electromagnetics.  The book explains the equations intuitively, and is a pleasurable and easy read.  Interestingly, the book's careful explanation of the equation's notation reveals aspects that a programming languages researcher could take issue with :-)  The key example is being consistent and explicit about binding and usage occurrences of variables.  As a result, the book can also be a sensible starting point for a study into formal aspects of the mathematical notation used in this domain.  Although the book's notation is not universal, and despite the fact that a quick search on the web shows that there are differing notational conventions, the binding/usage issue appears to be pervasive.  Of course, studying math notation and understanding physics are two separate things.  This is still a great book about physics.  

Embedding hybrid automata in Acumen

During last week Jan worked on integrating the enclosure based solver with Acumen. Initially, the aim has been to support a very limited subset of Acumen used to embed hybrid automata that can then be extracted and passed to the solver as specifications of the hybrid system to be simulated. Hybrid state invariants are required by the solver to significantly improve the quality of the solutions and it has been necessary to extend the Acumen language in order to accommodate them. Together with Adam a prototype extractor was implemented, which uses the Acumen parser to generate the input to the solver. The work in the coming week will focus on de-bugging the solver.

Modeling physical communication links

Anita and Muzeyen are working on a paper investigating the key aspects of simulation languages from the point of view of an Engineer instead of a programmer or language designer. The main idea is to look at hybrid system models as a DSL for Engineers. A physical communication link, consisting of a modulator, a demodulator and a non-ideal channel, will be used as an example of a hybrid system. The paper will draw insights from modeling and simulating this system using different simulation tools.

3D visualization in Acumen

Anita and Yingfu continue to work on a paper describing 3D visualization for Acumen, Acumen3D. The problem formulation is along the lines of "what would be a good core language for 3D animation?" The paper will highlight some interesting features of Acumen3D, such as directly linking simulation variables to visualization objects, and dynamically generating objects. Yingfu is currently at Rice University but he and Anita will continue to work together on the paper.

Collaborating with PSU

Anita is planning a visit to Portland State University (PSU) in September to discuss possible collaboration projects. The collaboration between Halmstad University (HU) and PSU started a few years ago with Dan Hammerstrom as a guest researcher at HU. In order to strengthen the ties between both universities, a joint project was formulated. The initial idea was to use Acumen to model electric vehicle and smart grid components in Dan's electric vehicles course at PSU. After Dan moved to DARPA, he suggested Robert Bass be HU's link to PSU. Anita, Veronica, Dan and Robert had a Skype meeting at the beginning of August, and it was decided that Anita would pay a short visit to Robert at PSU to discuss the continuation of the project.

------------------------------
Anita Pinheiro Sant'Anna
------------------------------
Intelligent Systems Lab
Halmstad University
+46 35167849

Unit test for symbolic differentiation

This week Yingfu started developing unit test cases for the symbolic differentiation implementation in Acumen.  Some examples are shown below:

dif("2*x^2","x")  should be (parseExpr("4*x"))

dif("cos(x)","x")  should be (parseExpr("-sin(x)"))

dif("x^2/(x+1)","x") should be (parseExpr("(2*x*(x+1)-x^2)/(x+1)^2"))

dif("x^x","x") should be (parseExpr("x^x*(log(x)+1)"))

Coming work will include the old property-based test cases.  Anita and Yingfu continued working on the paper about Acumen3D and built a comparison table with other simulation tools including LabView, Simulink and Modelica. 

Property-based testing of intervals and interval functions

This week Adam and Jan started developing a property-based test suite for the enclosure-based solver that is under development. The properties aim to meet two goals, first to catch bugs in the implementation, and second to make up an automatically testable specification of the implementation. Pure Scalacheck properties were chosen over properties expressed in a ScalaTest style, because they give more readable output when used in conjunction with SBT, and seem to give a terser formulation of the properties. So far, properties and generators have been written for intervals and interval functions.

Event-variable independence analysis

During last week Jan has been working on an implementation of an event-variable independence analysis for the hybrid solver under development. The analysis determines when it is safe to ignore events when building an enclosure of all possible trajectories for a hybrid IVP over a fixed time segment. The analysis uses equality of IVP fields and reset maps and to facilitate such judgements these functions have been represented essentially as syntax trees. The representation makes it simple to e.g. test when tow fields have the same effect on a given variable, or when a reset map acts as the identity on the variables a given variable depends. Coming work will focus on testing the solver in preparation of integration with the Acumen code base.

Toward symbolic differentiation in Acumen

This week Adam and Yingfu have been working on integrating the
symbolic differentiation implementation with Acumen. This amounted to
adding a code transformation step which applies the previously
developed logic, updated to operate on the Acumen AST types. This
approach was chosen over one where a specialized AST is used, as the
existing types did not add much syntactic overhead. Future work in
this area includes adding support for more language constructs and
improving the handling of singularities.

Yingfu deposits Masters thesis

Yingfu has completed and deposited his masters thesis at Halmstad University.  The title of his thesis is "Lightweight Three-Dimensional Visualization for Hybrid Systems Simulation."  The basic idea behind the thesis is to find an easy way to give engineers access to some of the most basic functionality provided by OpenGL in a way that can help them during the process of modeling and simulation of cyber-physical systems.  In the propose approach, all the user needs to do is to define the value of some special variables, and they are automatically used to generate an 3D animation based on the results of the simulation.  The thesis, defense presentation, and all related Acumen models can be found in online archive available from the group website.  Yingfu and Anita are working on writing up the results as a conference submission.