Generator of Acumen models comprising multiple classes

In order to support the development of Acumen source code transformations, Adam has implemented a basic generator of Acumen models (instances of the Prog type) comprising multiple Acumen classes (ClassDefs). On a high level, the algorithm works as follows:

1. Generate list of leaf classes (containing no constructor calls or object field references) and add these to an environment (list of ClassDefs).
2. A small, random number of times, repeat the following: generate a list of classes based on the environment, and add these to the environment.
3. Generate a main class based on the environment and wrap it in a Prog.

Certain limitations apply to models generated by the algorithm. Significantly, constructors are only called in the private section of classes, and the right-hand sides of continuous assignments are always linear combinations of state variables (effectively making an Acumen program correspond to a system of linear ODEs at each continuous step).

Revision to reference semantics of continuous assingments

Adam and Kevin have been working on a revision of the reference semantics for Acumen. The revision ensures that the order in which continuous assignment statements occur in (a particular scope of) an Acumen model does not affect the simulation results. This was achieved by delaying updates to the state until after all evaluations for a particular continuous step have been performed. A consequence of this change is that the method used to solve ODEs (in particular, the transformation from higher-order ODEs to systems of first-order ODEs) introduces delays in the solutions which did not occur in the previous formulation of the reference semantics.

Not for free

Since last week Jan has extended the Boolean expression language supported by the Acumen enclosure interpreter to include disjunction (||) and logical negation (not). The main difficulty with the former was to extend the constraint solver used to narrow initial condition boxes while performing piecewise IVP solving, and the domains of guard and invariant predicates during event detection and handling. In particular, the intersection operation used by the event tree algorithm (EVT semantics option) relies on domain narrowing to reduce information loss errors while evaluating predicates. The issue with the latter, i.e. supporting negation in the enclosure semantics, was that narrowing cannot be effectively implemented directly on negated predicates. Instead, negations are pushed through the predicate using standard logical identities and into the relations, where e.g. not(x <= 1) becomes x > 1. The main remining issue is that of reducing the effects due to inefficient narrowing over disjunction. The method that Jan believes is easiest to implement is the one used in e.g. the RealPaver constraint solver. There, disjunctive constraints are translated into nonpositivity constraints on minimum expressions, e.g. x > y || x <= 0 becomes min(y-x,x) <= 0.

Summer school on testing

During the past week, Adam attended the Third Halmstad Summer School on Testing. Topics covered both theoretical aspects of testing and applied tool-based sessions and included both testing and formal verification. Generator-driven testing was a common theme to most of the courses. Adam found ProofPad, the tool used in the ACL2 course, to be a surprisingly pleasant to use. It makes the interaction with the logic system comparatively easy and combines testing and verification in one streamlined workflow.

The course on ScalaCheck, given by its creator Rickard Nilsson (and author of the soon-to-be-released ScalaCheck: The Definitive Guide), gave a good overview of the generators that power the testing library.

Finding Zeno :-)

Remember the story about Zeno's paradox, with Achilles and the tortoise?  Well, now we know how to do a computer simulation of that story :-)

Last week our first paper on enclosures and hybrid systems (entitled, "Enclosing the Behavior of a Hybrid System up to and Beyond a Zeno Point") was accepted for publication at the First IEEE Conference of Cyber-Physical Systems, Networks, and Applications (CPSNA 2013).

The figure on the right, taken from the paper, illustrates the basic idea of the new method on another example of Zeno behavior, namely, a bouncing ball.  The approach presented in the paper is to compute an "enclosure" (illustrated in grey in the diagram).  Using enclosures makes it possible simulate the system past the Zeno point without going into an infinite loop.

Code transformation experiments aimed at extending the syntax supported by the enclosure interpreter

During the past week Adam, Kevin and Jan have been working on extending the syntax supported by Acumen's enclosure semantics. The overall approach is to do this by transforming the source program into a form compatible with the enclosure interpreter. Two approaches have been pursued. The first is based on Acumen to Acumen code transformation, whereby incompatible constructs are translated into compatible ones. The other approach first computes the control flow graph of the source program and then performs reductions on this graph in order to arrive at a hybrid automaton corresponding to the source program. Initial manual experiments indicate that both approaches are able to handle simple models (expressed using a restricted but larger subset of the full Acumen syntax than is currently supported) but it remains to be shown how general they are. An illustration of the graph transformation based approach is included below, showing the reduction steps for a simple single-mode bouncing ball model:

Table based interval sine and cosine

Last week Jan implemented lookup table based interval sine and cosine functions. The table is computed as a piecewise enclosure for cosine over [0,π/2] and symmetry and periodicity then give approximations over [0,2π]. Evenness and shifting of the argument interval into [0,2π] gives an approximation for the interval cosine function. Sine is obtained from it by shifting the argument by π/2. The two interval functions are lifted to enclosure functions by taking the range of the argument enclosure and wrapping the result interval in a constant enclosure. Because there is wrapping both of the input and output enclosures, the approach suffers from excessive information loss, but can be improved by using the interval functions to implement a fully enclosure based one. Below is a plot of Acumen using the sine implementation to compute a solution for x' = -sin(x) with x(0) = 1 over [0,4].