- Partial order reduction to the verifydtapn engine and GUI support.
- Support for timed-safety-games to the engine (no GUI support yet).
- Refactoring of verifydtapn engine and all around for performance improvement (including new successor generator).
- Numerous improvements for the untimed verifypn engine (including structural reductions for CTL and advanced query simplification algorithms).
- new CTL query creation dialog when modelling untimed nets
- new CTL untimed verification engine verifypn
- rapid drawing of nets - when holding down ctlr/cmd while creating a place/transition, continue clicking and the GUI will alternate in creating places and transitions while connecting them by arcs
- the view menu now has the option to display tokens as dots when they are of age 0
- numerous bug fixes and minor GUI improvements
- 64 bit engines for windows users.
- numerous bug fixes in the GUI
- improved implementation of the verifypn engine (includes CTL engine too but with no GUI support for now).
- the possibility to hide/show place and transition names,
- creation of shared places and transitions directly from the context menu,
- improved simulator that allows to setup time delays using a slider,
- new memory compression technique (PTrie) in the engine for workflow analysis,
- possibility to import XML queries for untimed nets from MCC-15 competition, and
- numerous bug fixes.
- bug fixes in the workflow analysis and query creating dialog,
- allows to execute 0 time unit delays in the simulator, and
- improves compatibility with the most recent UPPAAL verification engine.
- bug fixes in the untimed and discrete verification engines
- small GUI improvements in the simulator
- fixes a bug in the query dialog that allowed to use darts in cases where it should be disabled
- improved export/import of traces in a new XML format
- bug fixes in the untimed and discrete verification engines
- small bug fixes in the GUI
- PNML loading for nets with fractional x/y-coordinates
- overrride of queries in batch processing for deadlock check
- displays place-bound statistics for the discrete engine verifydtapn.
- PNML import/export is now available within TAPAAL GUI.
- Over-/under-approximation of the intervals in the net.
- Optimized workflow engine, in particular for strong soundness check.
- New untimed structural reductions in verifyPN engine.
- Possibility to define general arithmetic queries over the number of tokens in places (in the manual edit mode).
- Fastes trace option added to the query dialog for the discrete-time engine.
- Place-bound statistics of a search added for the untimed verifyPN engine.
- Improved export of the net as a latex (tikz) file.
- GUI and verification support for timed workflow analysis (available under Tool/Workflow analysis) that allow to check for soundness and strong soundness of workflow nets and computing the shortest and longest execution times.
- An untimed verification engine verifypn.
- A new optimized broadcast translation to UPPAAL timed automata, supporting all the new features like weighted arcs and urgent transitions, and providing performace optimizations for nets containing untimed places.
- Fix in the engine verifydtapn that now corrently generates loop-traces for EG/AF queries even with Time Darts turned on.
- explanation for verification results in batch processing and correction of PTrie and Dart options for the verifydtapn engine
- editor improvements for urgent transitions and shared places/transitions
- problem with UPPAAL translations for models with zero tokens and zero extra tokens
- deadlock reporting problem in simulator
- loading invalid XML files
- problem with removing orphan transitions that have inhibitor arcs
- "some trace" option is now remembered
- undo/redo of urgency flag
- fix for boundedness check with verifydtapn engine
- a few other bug fixes.
- a problem with loading verifyta.exe file (UPPAAL engine) on some windows installations running Java 6,
- a bug in simulator when used with urgent transitions,
- corrects the interpretation of verification results as some are actually valid also for the continuous semantics, and
- propertly terminates processes run via the batch processing dialog.
- adds the possibility to model urgent transitions (enabled urgent transition disables time passing),
- adds deadlock as one of a possible propositions in the query dialog (a marking is a deadlock if after any delay no transition gets ever enabled),
- improves the simulator by adding a random automated simulator and allowing to export/import traces,
- fixes a number of bugs and contains some GUI improvements, and
- makes performance improvements in the discrete-time engine verifydtapn.
- supports Java 7 (and Java 6),
- a considerably improved discrete verification engine verifydtapn 2.0 which includes semi-symbolic optimization called timed-darts and memory optimization option PTrie,
- a brand new simulator that shows the currently enabled transitions (red ones) and future-enabled transitions (blue ones),
- supports native file open/save dialogs,
- contains numerous GUI improvements (constant highlight, deadlock information in trace simulation),
- and fixes a number of bugs.
- A number of bug fixes in the discrete verification engine verifydtapn.
- A major upgrade of the tool featuring a new open source engine for closed timed-arc Petri nets. The main new features are
- a new TAPAAL engine called verifydtapn for discrete verification of closed nets
- updated TAPAAL engine verifytapn transition statistics that shows how many times transitions were enabled during the search
- support for weighted arcs in the editor, simulator and the new engine
- fully adjustable workspace that can be saved in preferences new shortcuts, namely the arrows that can be used both in editor and simulator (e.g. in editor arrows left/right can increase/decrease constant values when highlighted and ctrl-M runs the verification of the currently selected query)
- number of other GUI improvements and bug-fixes.
- A maintenance release fixing some minor problems in the editor when multiple objects were selected and when deleting places.
- It also fixes a problem in a simulator where arrows used in the delay field affected also the current position in the trace.
- A maintenance release fixing a few smaller bugs in the GUI
- as well as the interpretation of the verification answers for EG and AF queries.
- A maintenance release fixing several bugs and
- improving the speed of loading large models and moving/sorting in the component list,
- introducing a new update notification dialog,
- fixing a rare memory leak in the TAPAAL engine verifytapn,
- possibility to change the values of constants using the arrows left/right,
- user preferences are now relative to the version of TAPAAL,
- tool tips can be disabled,
- query dialog allows to create any query and suggests automatically the most suitable verification engine, and
- it is now possible to move in the error trace using the arrows up/down while the arrows left/right change the currently displayed component.
- A major release with several new features and GUI improvements.
- A new version of TAPAAL engine that allows to use discrete inclusion technique even for queries that are now upward closed.
- Numerous GUI improvements including a fully resizable panels, possibility for different workspace configurations for showing/hiding the interval [0,inf), and more.
- During the verification process there is now displayed a timer.
- Simulator now displays a clickable list of enabled transitions in all active components.
- New engine selection dialog provides an overview of the configured engines and the settings are remembered in preferences.
- Improved batch processing dialog with a better layout and the possibility to individually select verification engines.
- Sorting of components shared places/transitions, queries and constants in the editor panels.
- Improved query dialog with simplified/advanced view.
- New net statistics tool.
- New hot key assignments including command-modification for Mac users.
- When a transition is select in the editor window, it can be now rotated using the mouse wheel; if a place is selected the wheel changes the number of tokens in the place.
- Improved installation options, including an .exe launcher for windows users.
- Several bug fixes.
- A maintenance release that fixes a number of bugs, one of them connected to slow verification in case of the presence of orphan transitions (no input and no output arcs) and it fixes some rare issues during the saving of a net. The release also improves the layout of the query dialog and several other dialogs and a new example of train level crossing has been added to File/Example net.
- Several bugfixes introduced in 2.0.0, one of them related to boundedness checking problem in the TAPAAL engine. Highly recommended update for all TAPAAL users.
- TAPAAL engine (both 32 and 64 bit version) with symmetry reduction, concrete trace generation, discrete inclusion, heuristic search
- Component-based design editor with shared places and transitions
- Flexible batch processing dialog
- Numerous GUI improvements (view/hide of panels, updated query editor, improved verification statistics, ...)
- Fixes bugs (#769875, #769881, #781502)
- Fixes bugs with boundness checking (#737485, #750190)
- Bug fix release, fixes a number of bugs introduced in the 1.4 release
- New feature: timed inhibitor arcs
- Completely new query creation dialog
- New features: option to model and verify untimed Petri nets (mainly for educational purposes)
- Several visual improvements
- Bug fixes
- Deals with the new licensing policy of UPPAAL
- New features: parameterized nets, better GUI for query and constant editting, optimization of the number of extra tokens in case the net is bounded, automatic update notification, export to tikz.
- A new example of a web-server.
- A number of bux fixes.
- Included demo net
- Multiple bugfixes
- Boundedness checking
- Visualization of untimed traces for the verification of liveness properties.
- Added query to sidebar
- Restructured simulation to sidebar
- Multiple bugfixes
- First Public Release
- Graphical Query Designer