= Things To Do =


== Release 1.0 ==

Release 1.0 is scheduled for June 1, 2010.  This is the first public release of TASS.  Here is a list of features we expect in the release:

 * the MiniMP front-end we have been using
 * A C front-end, supporting at least a subset of C, with either pragmas or type qualifiers used to provide the meta-information needed by TASS.
 * XML representation of a model, including a model extractor which takes C source and produces a model in XML format, and the ability to read the XML file and construct a model from it
 * convenient binary packaging that bundles everything together and makes installation as easy as possible.   Versions for OS X, Windows, and linux (32- and 64-bit in each case).
 * relatively complete HTML documentation on the TASS web page: background, usage, MiniMP language reference, TASS Intermediate Representation (including XML)
 * bigger, more complex examples (e.g., laplace)
 * complete javadocs

== General To-Do Items ==

 * change names of MiniMP to TASS throughout project
   * for example, in the URL for test data, in the name of the package edu.udel.cis.vsl.minimp, and so on.  The name "MiniMP" should only be used for the language.
 * add good Javadocs for all public methods, classes, and packages
 * achieve much better statement and branch coverage in JUnit tests
 * create separate test tree which mirrors the source tree but contains only JUnit tests

== Symbolic Module ==

Consider re-designing the symbolic module based on lessons learned.

First, is the assumption argument necessary?   Is it ever used for anything?  How about removing it?

Then we can separate entirely the code for manipulating symbolic expressions from the code responsible for proving things and simplifying expressions based on an assumption.

How about multiple layers for the symbolic package:

 1.  Layer 0: Herbrand arithmetic.   No simplifications of anything.  This just produces new symbolic expressions based on the given arguments.  Straightforward factory; operator, arguments type of thing.
 1.  Layer 1: Very basic simplifications only, such as  x+0->x, 1*x->x, x+y->y+x.  Integers commutative/associative, etc.  All of which are applicable to IEEE arithmetic.   Place boolean expressions in canonical form, such as CNF?
 1.  Layer 2: rational canonical form for real expressions.  Valid for real arithmetic but does not necessarily preserve IEEE arithmetic.

Each layer could implement the same interface, SymbolicUniverseIF.  

Add: a SymbolicSimplifierIF interface and a TheoremProverIF interface.

So, the following are the items exported by the symbolic module:

 * {{{SymbolicUniverseIF}}}
   * methods for creating and manipulating symbolic expressions
   * {{{SymbolicExpressionIF}}} and all kinds of subtypes, operators, and so on
 * {{{SymbolicSimplifierIF}}}
   * see the simplifier class currently in the value package
 * {{{TheoremProverIF}}}
   * {{{boolean valid(BooleanSymbolicExpressionIF assumption, BooleanSymbolicExpressionIF predicate);}}}

Other simplifications to symbolic module:

  * get rid of >, >=.  Just use <,<=.
  * get rid of NEQ?  Just use NOT(EQUAL).



== Examples ==

 * Diffusion
    * What does the distribution strategy do if the number of cells is less than the number of procs?  Does it necessarily place two consecutive cells on two consecutive procs?  If it does not, then how can the ghost cell exchange work?   The exchange routine assumes that the neighboring cells will be on neighboring procs.   Check this out.
    * Interestingly, the parallel version is not necessarily correct when the number of cells is less than the number of processes.   It is possible for there to be a process  "gap" between two consecutive cells.  But you need at least 5 procs in order to see this.   Added {{{Diffusion_5_2_5_Test.java}}} to demonstrate this.  The fix: just change the way the neighbor ranks are computed (left/right, upper/lower).  These should be computed using the {{{owner}}} function to find out the rank of the process that owns the row next to you, instead of just assuming this will be your rank +/- 1.

== Parameters ==

I added support for parameters by simply giving the user the ability to specify a concrete value for any input variable in the initial state. At the command line, this is done by
{{{
-inputX=V
}}}
where X is the name of the variable and V its value. In a {{{RunConfiguration}}}, this is done using the method {{{setInput(String,Object)}}}. Now we don't need multiple versions of a single model which just differ by some bounds. Instead, just make the bound an input. I have applied this to several of the examples
.