vertics/twina repository overview

⁠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.001

You 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.023s

⁠Reference

⁠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.