ZLive Release Notes
Release 1.0 – July 2007
| Type | Changes | By |
|---|---|---|
| The calculation of free/bound variables now handles tmpNNN variables as normal variables, so that they are scoped correctly. This was necessary to avoid errors in the mode calculations, such as for sets whose results contained tmpNNN variables. | open | |
| Implemented a FlatPred implementation of function/relation types, like in Jaza. That is, an implementation of A --> B, for all the kinds of functions/relations/sequences that Z supports. (Use flags to keep track of each property such as one-to-one, total, onto etc.) | open | |
| Separated the FlatPred hierarchy from the evaluated results that it returns (see the net.sourceforge.czt.animation.eval.result package). For example, FlatPowerSet now returns a PowerSet object each time it is evaluated. This is more flexible, and was necessary to handle examples like {a:1..10 @ \power(0..a)}. | MarkU, Petra | |
| Implemented a better mode algorithm to reorder lists of FlatPreds, based on the estimated number of solutions for each mode. Initially, just repeatedly choose the predicate with the smallest number of expected solutions. In the future, more sophisticated path-finding algorithms may be used, such as best-first or A* path-finding algorithms. | Petra, MarkU |
Release 0.5 – July 6, 2006
| Type | Changes | By |
|---|---|---|
| Fix flatpred/FlatForall.java so that simple bounded forall predicates work. For example: (\forall x:\{1,3,5\} @ x = 3) should be false, but currently gives a "Cannot find mode" error. | Mark | |
| Design and implement a bounds analysis feature for numeric variables, so that x<=10 and x>=y are combined into the (finite) constraint x \in y..10. This could be done in at least three ways: (1) associate a static lower and upper bound constant with each variable; (2) associate a set of lower/upper bound expressions with each variable; (3) merge several complementary FlatPred constraints into single FlatPred constraint which is more efficient. The first or third approaches seem more in keeping with the ZLive philosophy of static analysis/transformation. | MarkU | |
| Change the test-and-compare framework so that a single directory is used for the results (and these change with time). This is a more CVS-friendly way of recording our progress. | MarkU | |
| Implement set union as a new FlatPred subclass. This should give us more flexibility to choose different algorithms than just unfolding the definition of union, which is a set comprehension with a disjunction. Intersection and difference might be okay done via unfolding. | MarkU | |
| Unfold definitions and rewrite some complex constructs into simpler constructs. This will be done via CZT rules. | MarkU | |
| Change the FlatSetComp implementation of sets so that members are generated lazily, on demand. This will allow us to evaluate schemas that have an infinite number of solutions, when we only want to explore the first few solutions. | MarkU | |
| Design and implement a 'FlatOr' class to handle disjunctions. All branches of the disjunct must have the same mode. Other complex predicates should probably be unfolded into disjunctions. | MarkU | |
| Implemented a simple textual user interface which provides eval Expr and evalp Pred commands. | MarkU |
Release 0.1 – unreleased
| Type | Changes | By |
|---|---|---|
| Better reporting from the usertests. Each animate*.tex file is a separate JUnit test suite so that we can see which groups of tests are mostly passing/failing. It shows line numbers for each test that fails and records previous test runs in subdirectories and shows when new tests pass or old tests start failing. | Rohit | |
| Implemented all basic arithmetic operators, tuples and several implementations of sets. | MarkU, Rohit | |
| Designed the EvalSet interface. Rohit wrote the first implementation of it (RangeSet for a..b sets), plus the FlatMember predicate which uses it. | MarkU, Rohit | |
| Designed basic architecture of ZLive (unfolding, flattening, mode analysis, reordering, then evaluation), and the FlatPred interface (abstract class actually). With Rohit, developed several FlatPred implementations for plus, times, negate etc. plus a basic left-to-right, deterministic-only evaluation engine. | MarkU | |
| Translated the 500+ Jaza tests into standard Z conjectures and wrote a JUnit harness which calls evalPred on each one (but conjectures of the form E=undefnum pass E to evalExpr and expect an exception to be raised). The resulting 'usertests' give a good measure of how much progress we are making towards a useful animator. | MarkU, Rohit |