Timeline
08/25/09:
- 22:41 Ticket #41 (change the JUnit test) created by
- Because the constructor of the ExecConfig class in the util package …
- 22:41 Ticket #39 (format of examples) closed by
- fixed: I think these are all fixed, along with other formatting issues. One …
- 22:39 Ticket #27 (send-recv deadlock) closed by
- fixed: Changed.
- 21:46 Ticket #37 (Command line option to specify buffer bound) closed by
- fixed: Option added.
- 16:00 Ticket #35 (if-then-else) closed by
- fixed: Expression added.
- 15:59 Ticket #38 (Need ifThenElse symbolic expression) closed by
- fixed: Expression added.
- 14:49 Ticket #36 (Flag to control simplify) closed by
- fixed: Flags added as "-simplify".
- 12:15 Ticket #40 (change name of Minimp to MiniMP) created by
- Make sure to change all occurences of Minimp to MiniMP. The Java …
- 08:38 Ticket #39 (format of examples) created by
- 1. Examples should have meaningful names based on name of containing …
08/24/09:
- 23:46 Ticket #38 (Need ifThenElse symbolic expression) created by
- I need symbolic universe to provide the following method: …
- 12:49 Ticket #37 (Command line option to specify buffer bound) created by
- Need a command line option for this. It currently is just set to 10.
- 12:05 Ticket #36 (Flag to control simplify) created by
- We want a command line flag to turn simplify (through CVC3) on and off.
- 12:04 Ticket #35 (if-then-else) created by
- Add if-then-else expression.
- 11:24 Ticket #34 (Add for loop support to front end) created by
- 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
- 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
- fixed: This has been corrected. Also, arrayloop is now called …
08/22/09:
08/21/09:
- 18:14 Ticket #32 (casting between ints and reals) created by
- The symbolic package needs to support some way to cast between ints …
- 17:53 Ticket #23 (printing of symbolic expressions needs improvement) closed by
- fixed: Fixed. Parenthesis added.
- 17:52 Ticket #30 (improve model names) closed by
- fixed: Fixed.
- 17:41 Ticket #31 (deprecated "\O" notation occurs in diffusion example) created by
- The following assertion occurs in diffusion_seq.mmp: […] See my …
- 15:26 Ticket #30 (improve model names) created by
- In compare mode, the models are named "Spec" and "Impl". I think it …
- 15:21 Ticket #29 (matrix multiplication tiling is incorrect) created by
- In the matrix multiplication example, tass correctly points out that …
- 15:19 Ticket #25 (SyntaxException when verifying matmat-seq.mmp) closed by
- fixed
- 15:16 Ticket #28 (improvements to model printing with source) created by
- 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
- fixed: Fixed.
- 23:09 Ticket #26 (Error in front-end on factorial example) closed by
- fixed: Fixed the bug in TreeParser.
- 19:52 Ticket #27 (send-recv deadlock) created by
- 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
- […]
- 17:29 Ticket #24 (symbolic arrayWrite method giving incorrect results) closed by
- fixed: Fixed. The CVC3 will simplify the representation of an array when …
- 12:55 Ticket #25 (SyntaxException when verifying matmat-seq.mmp) created by
- 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
- Here is an example of incorrect result (from arrayLoop): Setting …
- 17:55 Ticket #7 (white space in text) closed by
- 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
- fixed: Fixed. The theorem prover will take care of the type issue.
- 16:23 Ticket #23 (printing of symbolic expressions needs improvement) created by
- The symbolic expressions, when printed, do not contain parentheses, so …
- 16:16 Ticket #22 (automatic email) created by
- There should be a way to automatically email people whenever a ticket …
- 16:08 Ticket #7 (white space in text) reopened by
- Still seeing white space there. For example, in arrayloop_2 example: …
- 16:06 Ticket #21 (improvements to user interface) created by
- 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
- In arrayloopImpl (maybe spec too?), the output variable C is read in …
08/16/09:
- 22:53 Ticket #19 (JUnit test cases) created by
- JUnit test classes should be set up to run tests on each of the …
- 10:08 Ticket #18 (examples) created by
- All of the examples need to be brought up to date so that they work …
- 10:03 Ticket #17 (implement verify.loop) created by
- The transition system for verifying unbounded loops has to be …
- 09:59 Ticket #16 (symbolic exception: arrayloop_2) created by
- frederic:arrayloop siegel$ tass compare arrayloopSpec_2.mmp …
08/15/09:
- 01:56 Ticket #12 (Execution exception in Evaluator) closed by
- fixed: Fixed by correcting other bugs.
- 01:55 Ticket #14 (flaw in simplify routine?) closed by
- fixed: Fixed.
- 01:55 Ticket #13 (erratic behavior in symbolic package) closed by
- 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
- 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
- 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
- The following code occurs in SymUniverse.java, method andExpression. …
- 23:38 Ticket #13 (erratic behavior in symbolic package) created by
- Using revision 952, I am getting wrong answers from symbolic package. …
08/12/09:
- 17:38 Ticket #12 (Execution exception in Evaluator) created by
- 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
- 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
- fixed: Fixed. The front end can accept these new options now.
- 16:05 Ticket #7 (white space in text) closed by
- fixed: Fixed.
- 15:35 Ticket #6 (text associated to branch statements) closed by
- fixed: Fixed. The branch statements now associate with correct source program …
- 12:59 Ticket #11 (improve handling of counterexamples) created by
- A lot of violations are dealt with by throwing exceptions. It would …
- 12:56 Ticket #10 (command line interface additions) created by
- Several options need to be added to the commandline interface: …
- 12:49 Ticket #9 (multiple bugs in Urgent) created by
- 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
- It seems like the symbolic expressions are not being transformed into …
- 11:32 Ticket #5 (command line interface corrections) closed by
- fixed: Fixed. The front end will reject any unrecognized options and throw an …
- 11:14 Ticket #7 (white space in text) created by
- Sometimes the text associated to a statement includes white space at …
- 11:11 Ticket #6 (text associated to branch statements) created by
- For branch statements (if (expr) S1 else S2) the text associated to …
- 00:43 Ticket #4 (ugly output in verbose mode) closed by
- fixed: Fixed.
08/10/09:
- 21:40 Ticket #5 (command line interface corrections) created by
- The commandline syntax should be tass verify [options] foo tass …
- 21:37 Ticket #4 (ugly output in verbose mode) created by
- In verbose mode, there is still extra junk printed when the models are …
- 21:35 Ticket #3 (Execution exception in InnerPredicate) closed by
- fixed: Bug fixed in revision 946----input variables were not getting …
- 16:16 Ticket #3 (Execution exception in InnerPredicate) created by
- Revision 945, tile example: CVC3 prover invoked with query: (LET …
08/09/09:
- 20:02 Ticket #2 (null pointer exception in Evaluator) closed by
- 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
- Revision 943, tile example: java.lang.NullPointerException …
- 17:15 Ticket #1 (null corresponding variable: tile example) closed by
- fixed
08/07/09:
- 21:21 Ticket #1 (null corresponding variable: tile example) created by
- Using revision 942. Running compare on tile example yields following …
Note:
See TracTimeline
for information about the timeline view.
