Twina Docker image
This image is based on the Ubuntu (bionic) image and contains binaries from several tools developed in the Vertics group:
- twina: a tool for analyzing the “product” of two Time Petri nets with inhibitor and read arcs.
- sift: a specialized version of tina supporting on the fly verification of reachability properties for Time Petri nets. Sift offers less options than tina but is typically faster and requires considerably less space.
- ktzio: a conversion tool for transition systems that can generates ktz files from the output of twina.
- selt: a State/Event-LTL model checker.
This image also contains script files and models that can be used to reproduce results from our benchmarks.
The download size of this image is:
Usage Example
This image is intended to be used for testing Twina; you can find instructions
on how to install the tool here. To
reproduce the results in our [Formats19] paper on example
jdeds.net you can simply run the following command:
$ docker run --rm vertics/twina ./twinaluate.sh jdeds f
jdeds,plain,LSCG,21,42,0.001,SSCG,28,45,0.002
jdeds,twin,LSCG,489,1144,0.004,SSCG,706,1432,0.011
jdeds,obs,LSCG,49,103,0.001,SSCG,64,115,0.001You can also start an interactive bash session to try the tools, for instance by reproducing the experiments with the diagnosability of patterns described in this post.
$ docker run --rm -it vertics/twina bash
root@55c69b04edf3:~# twina transport.tpn
904 classe(s), 820 marking(s), 142 domain(s), 1947 transition(s)
0.023sReference
[Formats19] Lubat É, Dal Zilio S, Le Botlan D, Pencolé Y, Subias A. A State Class Construction for Computing the Intersection of Time Petri Nets Languages. In 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS) 2019, LNCS Vol. 11750. Springer. (hal-02263832))
Dependencies
The vertics/twina image contains a copy of the LTL2BA software written by Denis Oddoux and modified by Paul Gastin. This program is used by selt.