Dynamic Time Petri net extension for Tina

This extension was presented in Time Petri Nets with Dynamic Firing paper submitted to the 12th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'14).

Binaries

These binaries were created to work with an extended version of Timed Transition Systems (TTS) which are required by our Dynamic Time Petri nets (DTPN). So they do not execute with TTS created by frac compiler.

They should be added on your system on top of a running Tina installation.

The usage is exactly the same as tina tool so refer to Tina guide for usage.

Models

To configure our models we use Generic Preprocessor (GPP).

The above archive contains models from our paper:

   SimpleInt simple integrator DTPN version
SimpleInt_step simple integrator discrete version
LandingGear landing gear DTPN
LandingGear_step     landing gear DTPN
Sched preemptive scheduler DTPN
Sched_stw preemptive scheduler with stop-watch
PI proportional-integral (PI) controller DTPN version
PI_step proportional-integral (PI) controller discrete version

Execution of DTPN models

Each model has to be generated then compiled using 

make

This requires that gpp preprocessor and frac compiler are installed on your system.

Then you can explore state space and print state space information using

./tina-dyn gen.tts

Or alternatively type 

./tina-dyn gen.tts gen.ktz
to build the reachability graph in ktz format.

For discrete "_step" models use tina instead.

Most models are parametrable, to modify parameters edit condig.def file.

Printing curves

Disclaimer: this script is ad-hoc for each model and will not work on other models.

Some models provide a Python script that allows to print a curve for the integrated function. This script relies on matplotlib and of course requires Python to be installed on your system.

To print a curve of a model type 

./tina-dyn gen.tts > out.tina
this will copy tina output to file out.tina then type 
python parese.py
this will parse the output and show a curve.