The following releases are available for free for non-profit applications. Please notice that UPPAAL CORA requires Java 5.
- UPPAAL CORA
The latest version of UPPAAL CORA for Linux, Solaris, and Windows.
- UPPAAL CORA (Mac OS X)
The latest version of UPPAAL CORA for Mac OS X (Universal).
UPPAAL CORA has a number of limitations. These limitations are not fundamental, but are a result of using new internal data structures with a currently limited feature set. Over time, these limitations will be resolved.
- No extrapolation, hence termination is not guaranteed unless you
guarantee that either:
- The system is acyclic.
- All clocks are bound by invariants.
- Simple reachability only:
- No liveness check
- No deadlock check
- Limited use of guiding:
- Support for (cost + remaining) sorting is implemented (best first search)
- Support for heuristic variable is implemented, but the expression cannot refer to the cost variable.
- 20060910: Fixes bug 346 and a bug in concrete trace generation. Models of the air craft landing problem and the vehicle routing problem with timed windows have been added to the demo directory. The engine in this release is based on the latest development version of UPPAAL. The GUI is identical to that of UPPAAL 4.0.2.
- 20060808 (PTA): This release fixes a serious memory leak. The engine is based on the latest development version of UPPAAL. The GUI is identical to that of UPPAAL 4.0.2.
- 20060626 (PTA): This release is based on UPPAAL 4.0.1 (the GUI is identical to UPPAAL 4.0.1). No new CORA specific end user functionality was added compared to the previous UPPAAL CORA release. Universal binaries for Mac OS X are now available.
- 20060206 (PTA): This release is based on UPPAAL 3.6 Alpha 4. Besides all the bug fixes in UPPAAL, at least one CORA related bug (bug 243) that caused the verifier to go into an infinite loop was fixed. Notice that the 3.6 syntax is now enabled by default in verifyta. The -N option is no longer needed.
- 20051027 (PTA): This release is based on the soon to be released UPPAAL 3.6 Alpha 1. Since the last release in June 2005 approximately 50 bugs and enhancement requests have been closed and numerous minor problems have been fixed. There are no new CORA specific features in this release, however a number of critical bugs specific to CORA have been fixed. A number of those relate to trace generation.
- 20050621 (PTA): This release is based on UPPAAL 3.5.7. The previous release was rather buggy and I hope most issues are fixed by this release. In particular the use of a heuristic variable for defining the search order was broken.
- 20050531 (PTA): This release is based on UPPAAL 3.5.6. There are lots of changes since the last release: Bug fixes, performance improvements, and new features. The most notable fix is probably that the simulator now works (in the previous release it worked for most simple models, but failed for more complicated models). Also traces can now be loaded reliably from the model checker into the GUI. The most notable new feature is probably the concrete trace generator for priced time automata. This trace generator produces optimal concrete traces. It is only available from the command line (verifyta), though.
- 20041109 (PTA): First release under the new CORA name and first publicly announced release. UPPAAL CORA is now packaged with a GUI (an unmodified version of the latest development version from main line UPPAAL) and ships with the Linux and Windows version in one package. If a Solaris version is needed, please email us and we will add it. Other changes in this release: bug fixes in the parser, active clock reduction added, several optimisations in successor computation. Addition of best depth first search order.
- 20040819 (PTA): New release of PTA version. This release contains all the changes from the 20040625 UPTA version (record-types and UCode support). It also contains support for incrementing the cost on edges using the += operator. Finally, it contains bug fixes and performance improvements.
- 20040625: New release of UPTA version. This release fixes bugs in how meta variables are handled. It also contains basic support for record-types and UCode (support for functions).
- 20040519 (PTA): Merged bug fixes from 3.4 branch.
- 20040518 (PTA): First release of PTA version.
This is the first release of UPPAAL PTA.
- 20040106: Bug fixes.
Fixed some memory leaks and a problem with how meta variables are handled. Also changed the default syntax back to 3.4. Use the -N to enable the extended 4.x syntax with support for the UPTA extensions. Notice however that this option is not listed in the synopsis of verifyta.
- 20031217: Ported UTAP support to the 3.4 series of
Notice that the syntax has changed. Please read the documentation before upgrading. Your old models will not work with this version! The old version is still available here:
- 20021218: Wrong estimate detection.
Added warning message when a goal state is reached and the estimate of the remaining cost is non-zero.
- 20021212: Added support for remaining cost estimation.
An extra implicit variable called remaining was added. This variable can be assigned to on the transitions or using a global assignment right before the global heur assignment. The value of this variable should be set to a lower bound on the remaining cost to reach the goal from the current state. Pruning is done with respect to cost + remaining. If you want to find the best solution, use heur := cost + remaining as your global heur assignment and use the -o and -E option.
- 20021210: Added -R option.
This option randomises the ordering between states with equal heur value (only relevant with -o and -O).
- 20021201: Initial release