Localizing strategy continued

Last week Walid, Michal and Jan began working on a top-level strategy for the enclosure interpreter. Jan's original idea of reusing the constraint solver developed for the event detection and invariant intersection algorithms turned out not be suitable in its naive form. The problem with the idea is that it would not be able to ignore any events, and therefore not be able to localize the first event effectively. The solution is instead to use a subdivision-based approach that separately localizes the left and right endpoints of a segment of time that may contain the next event following. The segment is analyzed to determine if an event has with certainty been located and if continued sub-division is likely to localize the event further. Currently, an implementation is being finalized and integrated with the Acumen IDE. 

Scala course at Chalmers

During the past week Adam has attended an intensive Scala course at Chalmers, brilliantly presented by David Raymond Christiansen of ITU. The course introduced several aspects of advanced Scala programming, focusing on how its type system can be used with various approaches to embedding DSLs in Scala. Particular weight was given to Scala's implicit conversions mechanism, which e.g. makes it possible to emulate Haskell's type classes (with some additional flexibility) in Scala and can make interoperation with Java libraries smoother. The material of the course built up to the topic covered during the last day, a technique and framework called Lightweight Modular Staging (LMS). Adam found it easier to grasp after having understood the polymorphic DSL embedding technique, covered earlier in the week, of which LMS is an instance. In brief, this technique is based on defining the DSL as operations on an abstract data type. A program in the DSL is a nested call to these operations, and interpreters for the DSL are defined as implementations of the abstract operations which make up the program.

Progression of Zeno systems

During the past week Adam has been implementing a series of models developed by Walid, Jan and Adam, evaluating the enclosure semantics' performance on Zeno systems. An example of such a model is the following, inspired by a formulation of Zeno's paradox:

class Main(simulator)

  private

    d := 1; d' := -1;

    s := 1/2;

    mode := "q"; 

  end

  switch mode assume s <= abs(d)

    case "q"

      if s == d 

        s := s/2; 

        mode := "q" 

      end;

      d' = -1;

  end;

end

Adding a mode invariant (using the assume keyword) enables the interpreter to prune enclosures of impossible solutions, yielding a better overall enclosure. Though, at first glance, s <= d seems to be a suitable invariant for this system, this invariant does not hold after d crosses zero – changing this to s <= abs(d) ensures that the invariant holds for the entire simulation time. 

Adam will spend the coming week participating in a one-week Scala course given at Chalmers, learning about things such as implicit conversions, API design, polymorphic embedding of DSLs, scala-virtualized and LMS.

Towards a localizing strategy

Last week Jan integrated the new atomic step with the enclosure interpreter and started working on the top-level strategy. The idea has been to use the same constraint propagation technique employed to intersect enclosures with mode invariants and event guards during event handling. By composing event guards with the enclosures computed for the free variables in the guard and contracting the domain of the resulting predicate it should be possible to contract time segments around sub-segements where an event may occur. The advantage with this approach is that much of the necessary infrastructure is already in place, but a disadvantage is that it generally cannot show that an event has happened with certainty.