Dear Petri Netters, (and Other Models of Concurrency)-ers
We are happy to announce a new release of ITS-tools, a user friendly and powerful symbolic model-checker. We offer support for reachability, CTL and LTL model-checking of Petri nets and some of their extensions (time Petri nets, Colored nets, inhibitor arcs,...) and their compositions. ITS-tools are efficient; while we lost Gold for state space (after holding it for a long time) in 2017, we still ranked on the podium in every single category of the Model-Checking contest at ICATPN'17. Our main feature is a general purpose and easy to use pivot language : GAL, Guarded Action Language. With C like textual syntax, simple Petri style interleaving semantics (any enabled transition can fire, leading to a new state), but high expressivity, GAL is ideal as a target language for verification of diverse DSL. Showcasing this, we offer support for model checking of a variety of formalisms, ranging from Promela and Divine for description of concurrent process, to timed automata Upaal style. With new features such as a textual syntax to express model composition, parametric modeling, embedded properties, one click install into eclipse or command line interaction, ITS-tools could be the model-checker *you* were looking for. (Isn't everybody looking for a good model-checker ?) So please visit our new homepage on GitHub, and give the tool a trial : https://lip6.github.io/ITSTools-web Best Regards Yann Thierry-Mieg ITS-tools developer Maitre de Conférences, HDR LIP6, UPMC Sorbonne Universités ---- [[ Petri Nets World: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies: ]] [[ [email protected] ]]
