ticket summary component version milestone type owner status created _changetime _description _reporter 49 add primitive MPI-like communication operations to model model 1.0 enhancement Stephen Siegel new 2009-08-26T20:00:27-04:00 2009-08-26T20:00:27-04:00 Refer to how this was done for Mover. Stephen Siegel 328 Generate Human-Readable Description of XML Schema XML task stachnik new 2011-10-19T15:20:21-04:00 2011-10-19T15:20:21-04:00 The raw schema files are very difficult for a human being to read when looking for the structure of an XML node. It would be easier to read a text file which explicitly listed the children for each node individually. stachnik 331 Finish AST Module Implementation ast task stachnik new 2011-11-02T17:09:09-04:00 2011-11-02T17:09:09-04:00 All the nodes in the AST IF package should be implemented and their factory methods in ASTFactory should be implemented as well. stachnik 275 modify arrays in examples to use new #define input feature examples 1.1 1.1 defect bperry new 2010-09-15T10:52:40-04:00 2010-09-15T10:52:40-04:00 "Several of the examples won't compile because they declare global arrays with extents that are not statically defined. Fix this by using the #define to define the extents, as in {{{ #pragma TASS input { N>0 } int #define N 10 }}} " Stephen Siegel 278 array literal parse problems in TreeParser front 1.1 1.1 defect new 2010-12-18T23:16:03-05:00 2010-12-18T23:16:03-05:00 "Array literals are sometimes parsed incorrectly. See test2 in example literal directory. Literal {{1,2},{3,4},{5,6}} is interpreted as {{5,6},,}. Also, the front end forbids array declarations in which the extent is not specified, e.g. ""int x[];"" However there are cases where this should be allowed, as in ""int x[]={1,2,3};"". See test3 in literal. The front end should just not check for this and leave it to the model layer to throw a syntax exception in the right places." Stephen Siegel 297 expressions are not statements ast 1.1 1.1 defect stachnik assigned 2011-07-01T17:15:20-04:00 2011-07-16T08:51:12-04:00 "In the AST package, we now have ExpressionNodeIF extending StatementNodeIF. However, this does not correspond to the syntax of C or any of the other languages under consideration. According to the C99 Standard, expressions are not statements, but one of the kinds of statements is an ""expression statement"", which wraps an expression. In a statement such as lab: x*(y+1); clearly (y+1) is not a statement. Labels cannot be associated to it. This statement is not a compound statement. There is only one statement there. Let us discuss here the ramifications of the following changes, before doing anything: Proposed Changes: Delete ""implements StatementNodeIF"" from ExpressionNodeIF. In ast/IF, move expression package up one level, outside of the statement package. Add a new statement node: ExpressionStatementNodeIF. It has one child, which is an ExpressionNodeIF. Add factory method to create an ExpressionStatementNodeIF. Implementation classes will have to be modified accordingly. XML and XML parser will have to be changed accordingly. " Stephen Siegel 326 Add source information to pragma nodes and variable declarations clang 1.1 defect tmcclory new 2011-10-06T16:35:58-04:00 2011-10-26T13:19:00-04:00 Source information isn't being added to pragma nodes or global variable declarations. The source information is not being printed in the XML output. zirkel 330 Add structs to XML output clang 1.1 1.1 defect tmcclory new 2011-11-02T14:03:01-04:00 2011-11-02T14:03:01-04:00 struct types need to be printed in XML output in order to parse libmpi.c tmcclory 295 augment continuity options multiple 1.1 1.1 enhancement zirkel new 2011-06-18T12:45:36-04:00 2011-06-20T10:50:58-04:00 "An abstract function has a continuity field associated to it. This is the number of times the function can be differentiated. This must be improved in two ways: 1. Make continuity optional. Some abstract functions do not have any notion of continuity. (They don't have to be functions of real numbers, for examples). In this case, continuity could be ""null"" and the TASS abstract pragma should not have to include continuity. 2. Allow infinitely differentiable functions. So continuity can be a special value, INFINITY. Think of how to represent this in the TASS pragma. \infty? Changes will be need to be made to model level, front end, and perhaps other modules." Stephen Siegel 274 add support for skew factors in collective assertions/invariants multiple 1.1 1.1 task zirkel new 2010-09-15T10:22:08-04:00 2010-09-15T10:22:08-04:00 "Syntax: {{{ #pragma TASS collective assert ID x==PROC[1].y skew N+M; }}}" Stephen Siegel 294 Implement XML representation of TASS AST Administration 1.1 1.1 task stachnik accepted 2011-06-18T12:41:18-04:00 2011-07-03T19:59:04-04:00 "This project involves: 1. creation of an AST module, including interface and implementation 2. creation of XML schema, and functions to go from XML to AST and vice versa " Stephen Siegel 183 Verify derivative example using manual insertion of Taylor theorem examples 1.0 Release 1.0 enhancement zirkel new 2010-04-23T15:16:12-04:00 2010-04-23T15:16:12-04:00 This is an intermediate step to full accuracy support zirkel 211 don't check for deadlocked states when not necessary verify 1.0 Release 1.0 enhancement new 2010-05-27T21:07:52-04:00 2010-05-27T21:07:52-04:00 "No need to check for deadlock at a statement that can't block, like an ""if"" or ""while"". Right now we are checking the "" p || !p "" query at these states." Stephen Siegel 239 store malloc statements in heap multiple 1.0 Release 1.0 enhancement Stephen Siegel accepted 2010-07-05T23:33:34-04:00 2010-07-09T10:18:49-04:00 It would be of great use if the malloc statement used to create a heap variable were stored in the state. For example, when a memory leak occurs, TASS could report what the original malloc was that led to the leak. Also when viewing the state it would help to know where the variable came from. Stephen Siegel 161 Automatic performance analysis Administration 1.0 Release 1.0 task zirkel accepted 2010-02-01T10:36:36-05:00 2010-07-09T12:52:35-04:00 Tim figured out how to use an OS X tool to get performance information from the test suite. It showed the amount of time spent in each method, etc. Is there a way to do this or something like it automatically (perhaps a standard Ant task?). We could then add it to the things we do automatically and put it up on the web page. Stephen Siegel 181 Add derivative support to frontend front 1.0 Release 1.0 task zirkel accepted 2010-04-23T14:48:17-04:00 2010-05-21T11:17:40-04:00 Abstract functions are supported, need analogous changes for derivatives zirkel 202 installation from source Administration 1.0 Release 1.0 task new 2010-05-15T09:44:29-04:00 2010-05-15T09:44:29-04:00 "Can someone summarize for me how to a. install gmp, 64 bit version. Which version do I need? b. install cvc3 with java interface maybe we can also put this info in the README." Stephen Siegel 313 reimplement state as value multiple milestone2 enhancement Stephen Siegel new 2011-07-16T11:44:08-04:00 2011-07-20T08:32:27-04:00 "Re-implement all state components and state as instances of ValueIF. Each can be defined as an array or record, etc. This will allow things like creating a symbolic constant of type ""State""." Stephen Siegel 332 VariableReferenceNode names aren't getting set ast defect stachnik new 2012-01-04T14:48:41-05:00 2012-01-04T14:48:41-05:00 Whenever a {{{VariableReferenceNode}}} is created, the name should be set. This can be done in one of two ways. Either the setName() method can be used, or the appropriate IdentifierNodeIF can be passed as the second argument to the constructor. Right now, sometimes a {{{VariableReferenceNode}}} will have the referent set, but not the name. zirkel 88 compile set of CVC3 problems we want solved Administration task new 2009-10-31T12:40:06-04:00 2009-10-31T12:40:06-04:00 "Cesare is working with a group that is compiling a big collection of SMT problems that can be used as a standard test suite for different SMT tools, e.g., in competitions. He wants us to add some examples from our nonlinear problems that come up in accuracy verification that CVC3 cannot currently solve. They can be in the standard CVC3 input format, but without any ""TRANSFORM""s. Then send these to Cesare." Stephen Siegel 154 create package-level javadocs multiple 1.0 task Stephen Siegel accepted 2010-01-29T12:18:15-05:00 2011-06-18T12:37:41-04:00 For each package, create a file package.html with an overview of that package. This will get sucked into the Javadoc API web page by the javadoc utility. Stephen Siegel 269 move newCollectiveAssertion to ModelFactory model 1.1 1.1 enhancement new 2010-09-04T14:35:32-04:00 2010-09-04T14:35:32-04:00 Seems like newCollectiveAssertion would be better place in ModelFactory (instead of Model) since it may involve several models and does not require any particular knowledge of any one model. Stephen Siegel 232 checkSat multiple 1.0 Release 1.0 enhancement new 2010-06-24T10:42:57-04:00 2010-06-24T10:42:57-04:00 CVC3 has some methods which we are not using but probably should: checkSat. Stephen Siegel