Prior 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 Java 11 or higher is installed on your system. You can use Adoptium to obtain Java for 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”). On windows, it is important that during the installation you select “JavaSoft (Oracle) registry keys”, otherwise TAPAAL may not find your Java and fail with “This application requires a Java Runtime Environment 11.0-21.0” even if Java is already installed.

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)
  

Older Releases

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)