Timeline



08/28/09:

17:54 Ticket #71 (laplace example: inputs) created by Stephen Siegel
The laplace example is looking good. But instead of initializing the …
17:32 Ticket #70 (Add abstract functions to frontend) created by zirkel
An abstract function is a subclass of a function. It has a return …
17:25 Ticket #69 (skewFactor: EmptyStackException) closed by ywei
fixed
17:12 Ticket #69 (skewFactor: EmptyStackException) created by zirkel
Running skewFactor currently generates an EmptyStackException
17:10 Ticket #68 (-loop option) created by zirkel
Loop verifier shouldn't execute unless -loop is specified.
14:21 Ticket #65 (JUnit test problem with SimpleMP) closed by zirkel
fixed: ExecConfig had the write number, but the wrong option was being passed …
12:30 Ticket #67 (text associated to expressions has extra token) created by Stephen Siegel
The text associated to an expression extends one token beyond what it …
12:26 Ticket #66 (error in simpleMPImpl) created by Stephen Siegel
MiniMP has correctly found an error in simpleMPImpl. It points out …
12:18 Ticket #65 (JUnit test problem with SimpleMP) created by Stephen Siegel
When I run tass verify simpleMPSpec.mmp -np 2 from commandline, …
12:10 Ticket #62 (infinite loop when verifying simpleMPSpec) closed by Stephen Siegel
fixed: The logic in the proceedToNext method had a bug. If numProcs>0 and …
12:02 Ticket #22 (automatic email) closed by zirkel
fixed: Seems to work.
11:15 Ticket #31 (deprecated "\O" notation occurs in diffusion example) closed by zirkel
fixed: Changed.
09:34 Ticket #64 (error due to integer division in mean example) closed by Stephen Siegel
fixed: I put in the 1.0 as suggested, and the test passed.
09:31 Ticket #64 (error due to integer division in mean example) created by Stephen Siegel
The impl version of the mean example was getting the wrong answer. …
02:39 Ticket #32 (casting between ints and reals) closed by ywei
fixed: Fixed. The SymInteger now is a subtype of SymRational.
02:38 Ticket #54 (translate <= as lessThanOrEquals) closed by ywei
fixed: Feature added.
01:27 Ticket #56 (mean: null pointer exception) closed by ywei
fixed
01:27 Ticket #59 (skewFactor: Null pointer exception) closed by ywei
fixed: Fixed.
00:58 Ticket #63 (errors in matmat-par_2_2_2.mmp) created by ywei
For the bcast, the workers are sending, when they should be receiving; …
00:55 Ticket #62 (infinite loop when verifying simpleMPSpec) created by ywei
command: tass verify -verbose simpleMPSpec.mmp -np 2 The infinite loop …
00:52 Ticket #61 (null pointer exception in simpleMPSpec) closed by ywei
fixed: Fixed.
00:26 Ticket #61 (null pointer exception in simpleMPSpec) created by Stephen Siegel
[…]
00:23 Ticket #60 (ArrayStoreException in simpleMP) closed by Stephen Siegel
fixed: Problem was I had an array of Frame[] and I tried to stick into it a …

08/27/09:

23:48 Ticket #51 (add front end support for ++ and --) closed by ywei
fixed: Feature added.
23:47 Ticket #60 (ArrayStoreException in simpleMP) created by ywei
command is: tass verify -verbose simpleMPSpec.mmp -np 2 Exception in …
23:43 Ticket #58 (simpleMP: Null pointer exception from parse) closed by ywei
fixed: Fixed.
23:42 Ticket #43 (matmat: send stmt parse exception) closed by ywei
fixed: Fixed. But since the language doesn't support the notion of null …
18:51 Ticket #57 (nestedLoops: RuntimeException: Undefined value found.) closed by Stephen Siegel
fixed: Steve & Yi fixed: problem was that k had undefined value. Modified …
15:15 Ticket #59 (skewFactor: Null pointer exception) created by zirkel
Exception when running verify on skewFactorImpl.mmp. Possibly related …
15:10 Ticket #58 (simpleMP: Null pointer exception from parse) created by zirkel
Error while parsing: Exception in thread "main" …
15:07 Ticket #57 (nestedLoops: RuntimeException: Undefined value found.) created by zirkel
Running compare on nestedLoopsSpec_2.mmp and nestedLoopsImpl_2.mmp …
15:02 Ticket #56 (mean: null pointer exception) created by zirkel
Running verify on meanImpl_2.mmp gives the following: Exception in …
13:20 Ticket #19 (JUnit test cases) closed by zirkel
fixed: The remainder of this task is part of another ticket.
11:35 Ticket #41 (change the JUnit test) closed by zirkel
fixed: This has been fixed.
09:38 Ticket #55 (enhance JUnit tests) created by Stephen Siegel
Add additional test methods to try different options, such as …
09:28 Ticket #54 (translate <= as lessThanOrEquals) created by Stephen Siegel
There is now support for the <= expression (lessThanOrEquals) in the …
09:26 Ticket #53 (Add <= operator to model) closed by Stephen Siegel
fixed
09:13 Ticket #53 (Add <= operator to model) created by Stephen Siegel
Add expression <=. We already have <.
00:08 Ticket #52 (matrixMultiplication compare returns false) created by zirkel
Compare on the matrixMultiplication returns false. The problems are: …

08/26/09:

23:45 Ticket #51 (add front end support for ++ and --) created by Stephen Siegel
Add to grammar statements of the form expr++. This is just …
22:38 Ticket #46 (add front end support for if-then-else) closed by ywei
fixed: Feature added.
21:58 Ticket #50 (add front end support for initialization expressions) created by Stephen Siegel
Certain scalar variables can now have initialization expressions, …
21:52 Ticket #45 (add support for initial values of scalar variables to model) closed by Stephen Siegel
fixed
20:00 Ticket #49 (add primitive MPI-like communication operations to model) created by Stephen Siegel
Refer to how this was done for Mover.
19:59 Ticket #48 (add pointer types, values to model) created by Stephen Siegel
Refer to how this was done for Mover. Need pointers to variables, …
19:57 Ticket #47 (add record types to model) created by Stephen Siegel
A record is what is a called a struct in C. Need to add RecordTypeIF, …
19:54 Ticket #46 (add front end support for if-then-else) created by Stephen Siegel
An if the else expression has the following syntax: […] Just as …
19:30 Ticket #29 (matrix multiplication tiling is incorrect) closed by zirkel
fixed: The out of bounds error is corrected.
18:38 Ticket #45 (add support for initial values of scalar variables to model) created by Stephen Siegel
The language should support initial values for any scalar variable, as …
18:34 Ticket #44 (Add for loop functionality to model) created by Stephen Siegel
Add a ForLoopLocationIF which extends LoopLocationIF. Ditto for the …
18:11 Ticket #43 (matmat: send stmt parse exception) created by Stephen Siegel
There is a problem parsing the statement {{{send(a[count], count + 1, …
14:24 Ticket #42 (CVC3 prover problems) created by zirkel
Two problems: 1) For the factorial example, CVC3 prover returns …
14:16 Ticket #18 (examples) closed by zirkel
fixed: Examples have been updated.

08/25/09:

22:41 Ticket #41 (change the JUnit test) created by ywei
Because the constructor of the ExecConfig class in the util package …
22:41 Ticket #39 (format of examples) closed by zirkel
fixed: I think these are all fixed, along with other formatting issues. One …
22:39 Ticket #27 (send-recv deadlock) closed by zirkel
fixed: Changed.
21:46 Ticket #37 (Command line option to specify buffer bound) closed by ywei
fixed: Option added.
16:00 Ticket #35 (if-then-else) closed by ywei
fixed: Expression added.
15:59 Ticket #38 (Need ifThenElse symbolic expression) closed by ywei
fixed: Expression added.
14:49 Ticket #36 (Flag to control simplify) closed by ywei
fixed: Flags added as "-simplify".
12:15 Ticket #40 (change name of Minimp to MiniMP) created by Stephen Siegel
Make sure to change all occurences of Minimp to MiniMP. The Java …
08:38 Ticket #39 (format of examples) created by Stephen Siegel
1. Examples should have meaningful names based on name of containing …

08/24/09:

23:46 Ticket #38 (Need ifThenElse symbolic expression) created by Stephen Siegel
I need symbolic universe to provide the following method: …
12:49 Ticket #37 (Command line option to specify buffer bound) created by zirkel
Need a command line option for this. It currently is just set to 10.
12:05 Ticket #36 (Flag to control simplify) created by zirkel
We want a command line flag to turn simplify (through CVC3) on and off.
12:04 Ticket #35 (if-then-else) created by zirkel
Add if-then-else expression.
11:24 Ticket #34 (Add for loop support to front end) created by zirkel
Add for loop support to the front end. A related ticket has been …
00:27 Ticket #33 (illegal use of output variable in matmat) closed by zirkel
fixed: Now uses a temporary variable, which is later copied to the output …

08/23/09:

22:58 Ticket #20 (illegal reading of output variable) closed by zirkel
fixed: This has been corrected. Also, arrayloop is now called …

08/22/09:

11:22 Ticket #33 (illegal use of output variable in matmat) created by Stephen Siegel
[…]

08/21/09:

18:14 Ticket #32 (casting between ints and reals) created by Stephen Siegel
The symbolic package needs to support some way to cast between ints …
17:53 Ticket #23 (printing of symbolic expressions needs improvement) closed by ywei
fixed: Fixed. Parenthesis added.
17:52 Ticket #30 (improve model names) closed by ywei
fixed: Fixed.
17:41 Ticket #31 (deprecated "\O" notation occurs in diffusion example) created by Stephen Siegel
The following assertion occurs in diffusion_seq.mmp: […] See my …
15:26 Ticket #30 (improve model names) created by Stephen Siegel
In compare mode, the models are named "Spec" and "Impl". I think it …
15:21 Ticket #29 (matrix multiplication tiling is incorrect) created by Stephen Siegel
In the matrix multiplication example, tass correctly points out that …
15:19 Ticket #25 (SyntaxException when verifying matmat-seq.mmp) closed by Stephen Siegel
fixed
15:16 Ticket #28 (improvements to model printing with source) created by Stephen Siegel
The format for including source code in the model print out could be …

08/20/09:

23:57 Ticket #21 (improvements to user interface) closed by ywei
fixed: Fixed.
23:09 Ticket #26 (Error in front-end on factorial example) closed by ywei
fixed: Fixed the bug in TreeParser.
19:52 Ticket #27 (send-recv deadlock) created by Stephen Siegel
To do a message-passing data exchange, you need to send first, receive …
18:12 Ticket #26 (Error in front-end on factorial example) created by Stephen Siegel
[…]
17:29 Ticket #24 (symbolic arrayWrite method giving incorrect results) closed by ywei
fixed: Fixed. The CVC3 will simplify the representation of an array when …
12:55 Ticket #25 (SyntaxException when verifying matmat-seq.mmp) created by zirkel
When running verify on examples/matmat/matmat-seq.mmp, a …

08/19/09:

23:41 Ticket #24 (symbolic arrayWrite method giving incorrect results) created by Stephen Siegel
Here is an example of incorrect result (from arrayLoop): Setting …
17:55 Ticket #7 (white space in text) closed by ywei
fixed: Fixed. The source text will not include extra white space and all tabs now.
17:43 Ticket #16 (symbolic exception: arrayloop_2) closed by ywei
fixed: Fixed. The theorem prover will take care of the type issue.
16:23 Ticket #23 (printing of symbolic expressions needs improvement) created by Stephen Siegel
The symbolic expressions, when printed, do not contain parentheses, so …
16:16 Ticket #22 (automatic email) created by Stephen Siegel
There should be a way to automatically email people whenever a ticket …
16:08 Ticket #7 (white space in text) reopened by Stephen Siegel
Still seeing white space there. For example, in arrayloop_2 example: …
16:06 Ticket #21 (improvements to user interface) created by Stephen Siegel
At the end of a verification run, the system just prints "true" of …

08/18/09:

12:00 Ticket #20 (illegal reading of output variable) created by Stephen Siegel
In arrayloopImpl (maybe spec too?), the output variable C is read in …

08/16/09:

22:53 Ticket #19 (JUnit test cases) created by Stephen Siegel
JUnit test classes should be set up to run tests on each of the …
10:08 Ticket #18 (examples) created by Stephen Siegel
All of the examples need to be brought up to date so that they work …
10:03 Ticket #17 (implement verify.loop) created by Stephen Siegel
The transition system for verifying unbounded loops has to be …
09:59 Ticket #16 (symbolic exception: arrayloop_2) created by Stephen Siegel
frederic:arrayloop siegel$ tass compare arrayloopSpec_2.mmp …

08/15/09:

01:56 Ticket #12 (Execution exception in Evaluator) closed by ywei
fixed: Fixed by correcting other bugs.
01:55 Ticket #14 (flaw in simplify routine?) closed by ywei
fixed: Fixed.
01:55 Ticket #13 (erratic behavior in symbolic package) closed by ywei
fixed: Fixed. It turned out that the real source of this bug is in …
01:01 Ticket #15 (prover debugging output should print result) closed by ywei
fixed: Fixed. The prover will print Valid or Invalid under verbose mode.

08/14/09:

10:45 Ticket #15 (prover debugging output should print result) created by Stephen Siegel
In verbose mode, the prover class prints out the theorem that the …

08/13/09:

23:51 Ticket #14 (flaw in simplify routine?) created by Stephen Siegel
The following code occurs in SymUniverse.java, method andExpression. …
23:38 Ticket #13 (erratic behavior in symbolic package) created by Stephen Siegel
Using revision 952, I am getting wrong answers from symbolic package. …

08/12/09:

17:38 Ticket #12 (Execution exception in Evaluator) created by ywei
Revision 952, tile compare example: Step 4: State 3 -> spec.mmp line …
17:34 Ticket #8 (symbolic expressions not being transformed into canonical form) closed by ywei
fixed: Fixed. The symbolic universe will try to simplify each expression by …

08/11/09:

16:29 Ticket #10 (command line interface additions) closed by ywei
fixed: Fixed. The front end can accept these new options now.
16:05 Ticket #7 (white space in text) closed by ywei
fixed: Fixed.
15:35 Ticket #6 (text associated to branch statements) closed by ywei
fixed: Fixed. The branch statements now associate with correct source program …
12:59 Ticket #11 (improve handling of counterexamples) created by Stephen Siegel
A lot of violations are dealt with by throwing exceptions. It would …
12:56 Ticket #10 (command line interface additions) created by Stephen Siegel
Several options need to be added to the commandline interface: …
12:49 Ticket #9 (multiple bugs in Urgent) created by Stephen Siegel
There are several bugs in urgent package that parallel the bugs that …
11:33 Ticket #8 (symbolic expressions not being transformed into canonical form) created by Stephen Siegel
It seems like the symbolic expressions are not being transformed into …
11:32 Ticket #5 (command line interface corrections) closed by ywei
fixed: Fixed. The front end will reject any unrecognized options and throw an …
11:14 Ticket #7 (white space in text) created by Stephen Siegel
Sometimes the text associated to a statement includes white space at …
11:11 Ticket #6 (text associated to branch statements) created by Stephen Siegel
For branch statements (if (expr) S1 else S2) the text associated to …
00:43 Ticket #4 (ugly output in verbose mode) closed by ywei
fixed: Fixed.

08/10/09:

21:40 Ticket #5 (command line interface corrections) created by Stephen Siegel
The commandline syntax should be tass verify [options] foo tass …
21:37 Ticket #4 (ugly output in verbose mode) created by Stephen Siegel
In verbose mode, there is still extra junk printed when the models are …
21:35 Ticket #3 (Execution exception in InnerPredicate) closed by Stephen Siegel
fixed: Bug fixed in revision 946----input variables were not getting …
16:16 Ticket #3 (Execution exception in InnerPredicate) created by ywei
Revision 945, tile example: CVC3 prover invoked with query: (LET …

08/09/09:

20:02 Ticket #2 (null pointer exception in Evaluator) closed by Stephen Siegel
fixed: Fixed. There were some inputs variables in second model that were not …

08/08/09:

17:20 Ticket #2 (null pointer exception in Evaluator) created by ywei
Revision 943, tile example: java.lang.NullPointerException
17:15 Ticket #1 (null corresponding variable: tile example) closed by ywei
fixed

08/07/09:

21:21 Ticket #1 (null corresponding variable: tile example) created by Stephen Siegel
Using revision 942. Running compare on tile example yields following …
Note: See TracTimeline for information about the timeline view.