TAPAALPrior to Download
TAPAAL provides a standalone editor, simulator and verifier (called verifytapn) of timed-arc Petri nets.
UPPAAL Integration. -Optionally, for running an automated translation to timed automata, the user should install UPPAAL. You will need to procure a vesion of UPPAAL from www.uppaal.org. Get the latest version from download section, and follow the instalation instructions. You will need to locate the file verifyta that comes with the UPPAAL distribution and point TAPAAL to its location in the engine selection dialog from the Tools menu.
Download
Before running TAPAAL make sure that JRE 11.0 or higher is installed on your system. Additionally, on Mac OS X remember to allow applications downloaded from anywhere (in System Preferences and Security & Privacy tab or right-click on the application and choose “open”).
Binarier for Windows/Linux/Mac OS X:
- TAPAAL 3.9.5 for Windows Download (64 bit)
- TAPAAL 3.9.5 for Linux Download (64 bit)
- TAPAAL 3.9.5 for Mac Download (64 bit)
Source download:
- Download TAPAAL GUI from Github
- Download Continuous-Time TAPAAL Engine from Github
- Download Discrete-Time TAPAAL Engine Source from Github
- Download Untimed P/T TAPAAL Engine from Github
Please report any bugs that you might discover to our general bug tracker or on the bug tracker for the individual project.
Changelog
See the tapaal changelog.
Installation Guide
To install TAPAAL unpack the files for your platform and follow instructions in README.txt.
License
TAPAAL is licensed under tree licenses:
- The GUI tool is licensed under the Open Source Licence 3.0
- The reduction lib, used for automatic translation of TAPN models into UPPAAL Timed Automata and the discrete verification engine verifydtapn are licensed under the BSD License.
- The continuous-time verification engine verifytapn is licensed under GPL v2 license: https://www.gnu.org/licenses/gpl-2.0.txt
Other Downloads
- beta release of TACPN GUI and unfolding engine (Win64, Linux64) and update synthesis experiments (zip)
- partial-order-experiments.zip - models with timed partial order reduction (blood transfusion, BAwPC, alternating bit protocol, fire alarm, Fischer, Lynch Shavit, MPEG-2, patient monitoring).
- Approximation of Time Intervals - Beta Release 3.0.99 (Win, Linux, Linux64, Mac, Mac64, case studies)
- Timed workflow nets - Beta Release 2.4.99 (Win, Linux, Linux64, Mac, Mac64, workflow case studies)
- NFM’14 case studies
- FHIES’12 Blood Transfusion Case Study and MEMICS’12 experiments
- Patient Monitoring System (PMS) and BAwPC Protocol (TAPAAL nets)
- Experiments in TAPAAL and UPPAAL (Alternating bit protocol, engine workshop, Fischer’s protocol, Lynch-Shavit protocol, medical workflow, MPEG2 encoder)
- Lynch-Shavit Protocol and MPEG-2 Encoding Algorithm (TAPAAL and UPPAAL models)
- UPPAAL version of Alternating Bit Protocold with query (not to be opened in TAPAAL)