Ce simulateur comprend un

• format de fichier simple pour spécifier les états et transitions du système
• Tous les opérateurs (AG AF AU AW AX, EG EF EU EW EX) de CTL sont implémentés et testés
• Capacités de visualisation des résultats des requêtes sur le graphe. Pour l'instant, la seule visualisation disponible est l'output de la FSM au complet avec les états résultats en couleur

Dans le futur il y aura de la visualisation pour :

• contre exemples
• visualisation du calcul récursif dans le graphe
• autres possibilités

(Pas encore implémenté) Parser de formule CTL.

Pour l'instant les requêtes CTL se font avec l'appel direct des fonctions.

Vitesse/Benchmark. Aucun test de vitesse n'a été fait pour l'instant. Les fonctions récursives sont néanmoins toutes optimisées avec la mémoisation lorsque c'est possible