DIPOT Implements interface between SPOT and DIVINE Features Create a C format of transition based Buchi automaton, from LTL formula, that is accepted by DIVINE.