  Developing algorithms for distributed systems is an error-prone task. Formal
models like Petri nets with transits and Petri games can prevent errors when
developing such algorithms. Petri nets with transits allow us to follow the
data flow between components in a distributed system. They can be model checked
against specifications in LTL on both the local data flow and the global
behavior. Petri games allow the synthesis of local controllers for distributed
systems from safety specifications. Modeling problems in these formalisms
requires defining extended Petri nets which can be cumbersome when performed
textually.
  In this paper, we present a web interface that allows an intuitive, visual
definition of Petri nets with transits and Petri games. The corresponding model
checking and synthesis problems are solved directly on a server. In the
interface, implementations, counterexamples, and all intermediate steps can be
analyzed and simulated. Stepwise simulations and interactive state space
generation support the user in detecting modeling errors.
