Outil dédié à la génération automatique de modèles PRISM pour des systèmes de production industrielle. Il permet de créer des fichiers DTMC (Discrete-Time Markov Chains) basés sur des politiques de service spécifiques, comme le blocage après service. Les modèles générés facilitent l'analyse et l'optimisation des performances des lignes de production en exploitant des configurations paramétrables pour différents types de systèmes (1-slot ou 2-slot).