ProTL is free for academic use only. Any other use requires a license of ProTL. As academic use, we consider only work performed by researchers or students at institutions delivering academic degrees. In addition, the work or the worker may not be contracted by any non-academic institution. Note that, any use at companies, private use, use at national research agencies, or any other non-academic use requires a license of ProTL.
ProTL 3.1
ProTL 3.0
ProTL 2.0
ProTL 1.0
ProTL is available for three types of operating systems: Windows, Mac and Linux.
For Windows, the installation of ProTL can be completed by simply following the installation instructions: (1) selecting the installation directory and (2) clicking “next” button until the installation is finished. Note that if ProTL is installed in Disk C, “Run as administrator” option is required when launching the ProTL to do the verification/simulation.
For Mac OS, users should save the downloaded ProTL package in “Application” directory. ProTL can be launched by opening the package directly in both Mac and Linux OS.
This version history documents the devlopements in ProTL since the first beta release of ProTL 1.0 in Nov 19th, 2018.
New features of ProTL version 3.1 compared to ProTL version 3.1 includes:
1. Support specifications of relations among multiple clocks, called n-ary relations;
2. Support translation of n-ary relations into STA;
3. Generate counter-example for violated n-ary clock relations;
New features of ProTL version 3.0 compared to ProTL version 2.0 includes:
1. Support for analysis of clock action, probabilistic clock action and interval-based delayFor operator;
2. Allowing users to edit/embed C code in the input PrCCSL* specifications;
3. Refining the translation pattern of ITE expression;
4. Support for comment block.
New features of this version compared to ProTL 1.0 includes: