TPAL is a tool for the verification and simulation of concurrent systems, which are modeled by using a Timed and
Probabilistic Process Algebra. The main advantage of TPAL is that we may write the specifications directly by using
an algebraic language, and some alternative representation can automatically generated. The current version of
TPAL has the following features:
Full support for the creation and edition of specifications and projects in TPAL. Syntax and semantic analysis of
TPAL specifications. Generation of Probabilistic-Dynamic State Graphs for TPAL specifications. Simple reduction
of the generated graphs. Graph browser, and simulation by using the graphs. Generation of Timed-Arc Petri Nets.
Timed-Arc Petri Nets browser, and simulation by using the nets. Translation of Dynamic State Graphs into Time Automata
for UPPAAL tool. Configuration of some parameters (graph browser and simulation.)
You can obtain the current linux version
HERE.
