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.

Bouncing ball

During the past week Jan has been working on an implementation of event handling for the enclosure-based hybrid ODE IVP solver. There is an initial version and a first simulation of the bouncing ball hybrid system was performed. The algorithm was capable of improving the produced enclosures when the step size was reduced as can be seen from the figures below.

Simulation done with step size 0.01.

Simulation done with step size 0.01.

Next, Jan will be testing the implementation looking for bugs that cause the solver to sometimes stall and eventually run out of memory.

Switched converters, average values and publication

Anita has moved on from simple electronic circuits to pulse width modulation for power converters. She has implemented models of switched converters in Acumen, Simulink and Matlab.

Anita and Veronica also implemented a class in Acumen that calculates the average of any given signal over a specified period of time.
---------------------------------------------------
class CalculateAverage(signal, startTime, endTime)
private
t=0; t'=0; adder=0; counter=0; average=0;
end
t'[=]1;
if t>=startTime && t<=endTime
counter [=] counter + 1;
adder[=]signal+adder;
average[=]adder/counter;
end
end
---------------------------------------------------

Anita and Yingfu have started structuring a paper about Acumen3D. The contributions of this work will include:
- Using abstractions => user needs to specify only a few key parameters.
- Taking full advantage of the information already in the simulation model (e.g. position of a object)
- Automatically generating virtual scenes
- Integrating visualization file with modeling file


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

WG 2.11 in Halmstad

Last week Halmstad University hosted the 9th meeting of the International Federation on Information Processing (IFIP) Working Group on Program Generation (WG 2.11).  The group comprises international research leaders in the area of program generation.  Over the last twenty years, there has been an increasing awareness of the role of program generation in enabling drastically better utilization of computing resources.  The working group meetings have a deliberately relaxed structure where speakers volunteer to talk about and discuss recent and ongoing work.

The local organizers for this meeting were Walid Taha and Eva Nestius.  The Office of the President kindly offered the University Board meeting room for the working group to use.  Many of the attendees indicated that they very much enjoyed visiting Halmstad and the university.  Photos of the event taken by several participants can be found here.

Cleaner name bindings

Adam has continued working on the symbolic differentiation implementation. The main change is the way in which unique names are bound to expressions. Previously, this was done during hash-consing. This was helpful for debugging, as the toString methods of the expression types could use the names from the expression binding context to output reduced expressions. However, this caused gaps in the indices of the names when printing the expression binding context for a given expression (showing only those bindings which are used in the expression). The solution was to move the process of binding names to expressions to the pretty-printing phase. Aside from resolving the problem of gaps in the expression names, this also gave a better separation of the differentiation algorithm from the pretty-printing logic.