<< Search-09-LinearProgramming | Index | App-1-NQueens >>

Search-10 : Automates Symboliques avec Z3

Navigation : Index | Suivant >>

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Comprendre - Comprendre la différence entre automates finis et symboliques 2. Appliquer - Appliquer automata-lib pour les automates finis 3. Implementer - Implementer des automates symboliques avec Z3 4. Resoudre - Resoudre des problemes de verification avec automates symboliques

Prerequis

Duree estimee : 2 heures

1. Introduction aux Automates

1.1 Qu’est-ce qu’un automate ?

Un automate est un modèle mathematique de calcul qui consiste en :

Composant Description Notation
Etats Configurations possibles \(Q = \{q_0, q_1, ...\}\)
Alphabet Symboles d’entree \(\Sigma = \{a, b, ...\}\)
Transitions Règles de passage entre etats \(\delta : Q \times \Sigma \to Q\)
Etat initial Point de depart \(q_0 \in Q\)
Etats finaux Etats d’acceptation \(F \subseteq Q\)

Un automate reconnait un mot si, en partant de l’etat initial et en suivant les transitions, on atteint un etat final.

1.2 Types d’automates finis

DFA (Deterministic Finite Automaton) : - Pour chaque etat et symbole, exactement une transition - Déterministe : pas d’ambiguite

NFA (Non-deterministic Finite Automaton) : - Pour chaque etat et symbole, zero, une ou plusieurs transitions - Peut avoir des transitions epsilon (\(\varepsilon\)) sans consommation de symbole

Theoreme de Kleene : Tout langage reconnu par un automate fini est regulier et reciproquement.

Theoreme de Rabin-Scott : NFA et DFA reconnaissent les mêmes langages (NFA peut etre converti en DFA).

Ancres savantes – Kleene, S.C. (1956), Representation of Events in Nerve Nets and Finite Automata, in C.E. Shannon & J. McCarthy (eds.), Automata Studies, Annals of Mathematics Studies 34, Princeton University Press:3-42 (theoreme de Kleene : equivalence entre langages reconnus par automates finis et expressions regulieres, déjà nomme ci-dessus) ; Rabin, M.O. & Scott, D. (1959), Finite Automata and Their Decision Problems, IBM Journal of Research and Development 3(2):114-125 (theoreme de Rabin-Scott : equivalence NFA/DFA, conversion non-déterministe vers déterministe — prix Turing 1976, déjà nomme ci-dessus) ; Hopcroft, J.E., Motwani, R. & Ullman, J.D. (2007), Introduction to Automata Theory, Languages, and Computation (3rd ed.), Pearson (manuel de reference sur les automates finis, opérations de fermeture et minimisation) ; D’Antoni, L. & Veanes, M. (2017), The Power of Symbolic Automata and Transducers, Theoretical Computer Science 719:199-211 (automates symboliques : transition etiquetee par un predicat sur un alphabet potentiellement infini, fondement théorique de l’extension avec Z3 presentee sections 3-4) ; de Moura, L. & Bjorner, N. (2008), Z3: An Efficient SMT Solver, TACAS 2008, LNCS 4963:337-340 (solveur SMT utilise comme moteur de decision des transitions symboliques).

1.3 Exemple introductif - Reconnaissance de “ab”

Soit l’automate qui reconnait les mots contenant exactement la sequence “ab” :

      a         b
q0 -----> q1 -----> q2 (final)
^        |         |
|        | a       | a,b
+--------+---------+
  • q0 : etat initial, n’a pas vu “a”
  • q1 : a vu “a”, attend “b”
  • q2 : a vu “ab”, etat final

Mots acceptes : “ab”, “aab”, “abab”, “cab”, …

Mots rejetes : ““,”a”, “b”, “ba”, “aa”, …

1.4 Limites des automates finis classiques

Les automates finis classiques souffrent d’une limitation majeure : l’explosion d’etats.

Exemple : Automate pour entiers 32-bit

  • Alphabet : \(\{0, 1\}\) (bits)
  • Mot : 32 bits representant un entier
  • Problème : Reconnaître les entiers entre 1000 et 2000

Approche naive : - Il faut \(2^{32} \approx 4\) milliards d’etats pour representer tous les entiers possibles - L’automate devient impossible a manipuler

Solution : Utiliser des automates symboliques avec des predicats logiques au lieu de transitions explicites.

2. Automates Finis avec automata-lib

2.1 Installation et importation

La librairie automata-lib permet de manipuler facilement des automates finis en Python.

# automata-lib (>= 9.2.0) : moteur d'automates (DFA/NFA).
# Dependence declaree dans requirements.txt ; import en cellule suivante.

Suite de l’implementation.

import sys
sys.path.insert(0, '..')

from automata.fa.nfa import NFA
from automata.fa.dfa import DFA
from typing import Set, Dict, List, Tuple

print("Bibliotheques importees :")
print(f"  automata-lib : NFA, DFA")
print("Environnement pret.")
Bibliotheques importees :
  automata-lib : NFA, DFA
Environnement pret.

Une fois la bibliothèque installée, nous pouvons importer les modules nécessaires.

2.2 Creation d’un NFA - Reconnaissance de “ab”

Creons un NFA qui reconnait les mots contenant la sequence “ab”.

# NFA pour reconnaissance de "ab"
nfa_ab = NFA(
    states={'q0', 'q1', 'q2'},
    input_symbols={'a', 'b'},
    transitions={
        'q0': {'a': {'q0', 'q1'}},  # Reste en q0 ou va en q1
        'q1': {'b': {'q2'}},        # Si on voit b apres a, va en q2
        'q2': {'a': {'q2'}, 'b': {'q2'}}  # Reste en q2 (final)
    },
    initial_state='q0',
    final_states={'q2'}
)

# Test de quelques mots
test_words = ['ab', 'aab', 'abab', 'a', 'b', 'ba', 'aa']

print("NFA pour reconnaissance de 'ab'\n")
print(f"Etats : {nfa_ab.states}")
print(f"Alphabet : {nfa_ab.input_symbols}")
print(f"Etat initial : {nfa_ab.initial_state}")
print(f"Etats finaux : {nfa_ab.final_states}")
print()
print("Tests d'acceptation :")
print("-" * 40)
for word in test_words:
    try:
        accepted = nfa_ab.accepts_input(word)
        status = "✓ Accepte" if accepted else "✗ Rejete"
        print(f"  '{word}': {status}")
    except Exception as e:
        print(f"  '{word}': Erreur - {e}")
NFA pour reconnaissance de 'ab'

Etats : frozenset({'q0', 'q1', 'q2'})
Alphabet : frozenset({'a', 'b'})
Etat initial : q0
Etats finaux : frozenset({'q2'})

Tests d'acceptation :
----------------------------------------
  'ab': ✓ Accepte
  'aab': ✓ Accepte
  'abab': ✓ Accepte
  'a': ✗ Rejete
  'b': ✗ Rejete
  'ba': ✗ Rejete
  'aa': ✗ Rejete

Interprétation : NFA pour Reconnaissance de “ab”

Résultat obtenu : Un NFA (Non-deterministic Finite Automaton) reconnaît les mots contenant la sous-chaîne “ab”.

État Rôle Final?
q0 Recherche ‘a’ initial ✗ Non
q1 ‘a’ trouvé, attend ‘b’ ✗ Non
q2 “ab” trouvé (succès) ✓ Oui

Transitions non-déterministes :

q0 --a--> {q0, q1}  (soit continue la recherche, soit passe en q1)
q1 --b--> q2        (séquence "ab" complète)
q2 --a,b--> q2      (reste dans l'état final une fois "ab" trouvé)

Tests d’acceptation :

'ab'   : ✓ Accepté (contient "ab")
'aab'  : ✓ Accepté (contient "ab")
'abab' : ✓ Accepté (contient "ab")
'a'    : ✗ Rejeté (pas de "ab")
'b'    : ✗ Rejeté (pas de "ab")
'ba'   : ✗ Rejeté (pas de "ab")
'aa'   : ✗ Rejeté (pas de "ab")

Points clés : 1. Non-déterminisme : La transition q0 –a–> {q0, q1} permet deux choix possibles 2. Recherche de motif : Le NFA modélise naturellement la recherche d’une sous-chaîne 3. État puits : q2 est un état final “absorbant” (une fois “ab” trouvé, on y reste)

Note technique : Ce NFA illustre la puissance du non-déterminisme pour modéliser des problèmes de recherche. La transition q0 –a–> {q0, q1} signifie “soit je continue à chercher ‘a’, soit je passe en mode ‘j’ai vu un a, j’attends b’”. Un NFA peut toujours être converti en DFA équivalent (déterminisation), mais le NFA est souvent plus naturel à concevoir.

En complément — positions de la sous-chaîne : ‘aab’ contient “ab” en positions 2-3 ; ‘abab’ le contient plusieurs fois ; ‘ba’ contient “ba”, pas “ab”. Ces précisions de position distinguent la présence d’une sous-chaîne de la simple égalité de mot.

2.3 Creation d’un DFA - Mots avec nombre pair de ‘a’

Creons un DFA qui reconnait les mots contenant un nombre pair de ‘a’.

# DFA pour nombre pair de 'a'
dfa_even_a = DFA(
    states={'q_even', 'q_odd'},
    input_symbols={'a', 'b'},
    transitions={
        'q_even': {'a': 'q_odd', 'b': 'q_even'},  # a change la parite, b non
        'q_odd': {'a': 'q_even', 'b': 'q_odd'}    # a change la parite, b non
    },
    initial_state='q_even',
    final_states={'q_even'}
)

# Tests
test_words = ['', 'a', 'aa', 'aaa', 'b', 'ab', 'aba', 'bab']

print("DFA pour nombre pair de 'a'\n")
print("Schema des transitions :")
print("  q_even --a--> q_odd")
print("  q_even --b--> q_even (final)")
print("  q_odd  --a--> q_even (final)")
print("  q_odd  --b--> q_odd")
print()
print("Tests d'acceptation :")
print("-" * 50)
for word in test_words:
    count_a = word.count('a')
    accepted = dfa_even_a.accepts_input(word)
    status = "✓ Pair" if accepted else "✗ Impair"
    print(f"  '{word}': {status} ({count_a} 'a')")
DFA pour nombre pair de 'a'

Schema des transitions :
  q_even --a--> q_odd
  q_even --b--> q_even (final)
  q_odd  --a--> q_even (final)
  q_odd  --b--> q_odd

Tests d'acceptation :
--------------------------------------------------
  '': ✓ Pair (0 'a')
  'a': ✗ Impair (1 'a')
  'aa': ✓ Pair (2 'a')
  'aaa': ✗ Impair (3 'a')
  'b': ✓ Pair (0 'a')
  'ab': ✗ Impair (1 'a')
  'aba': ✓ Pair (2 'a')
  'bab': ✗ Impair (1 'a')

Interprétation : DFA pour Nombre Pair de ‘a’

Résultat obtenu : Un DFA (Deterministic Finite Automaton) reconnaît les mots contenant un nombre pair de la lettre ‘a’.

État Signification Final?
q_even Nombre pair de ‘a’ vu ✓ Oui
q_odd Nombre impair de ‘a’ vu ✗ Non

Transitions :

q_even --a--> q_odd  (la parité change)
q_even --b--> q_even (b n'affecte pas la parité)
q_odd  --a--> q_even (la parité change)
q_odd  --b--> q_odd  (b n'affecte pas la parité)

Tests d’acceptation :

''    : ✓ Pair (0 'a')
'a'   : ✗ Impair (1 'a')
'aa'  : ✓ Pair (2 'a')
'aaa' : ✗ Impair (3 'a')
'b'   : ✓ Pair (0 'a')
'ab'  : ✗ Impair (1 'a')
'aba' : ✓ Pair (2 'a')
'bab' : ✗ Impair (1 'a')

Points clés : 1. Mémoire finie : Le DFA “se souvient” uniquement de la parité (pair/impair), pas du compte exact 2. Déterminisme : Chaque état/symbole a exactement une transition 3. Minimalité : 2 états sont nécessaires et suffisants pour ce langage

Note technique : Ce DFA illustre un concept fondamental : la mémoire finie d’un automate. Pour reconnaître “nombre pair de ‘a’”, il suffit de se souvenir si on est dans un état pair ou impair. Ce langage est régulier car il peut être reconnu avec un nombre fini d’états. En revanche, “nombre premier de ‘a’” nécessiterait une mémoire infinie et n’est pas un langage régulier.

En complément — état final atteint : chaque mot conduit à un état précis — ’’ → q_even (accepté), ‘a’ → q_odd (rejeté), ‘aa’ → q_even (accepté), ‘b’ → q_even (accepté, car 0 ‘a’ est pair). Le mot vide (ε) est accepté car 0 est un nombre pair.

Exercice : NFA pour mots se terminant par “ba”

Enonce : créez un NFA (avec automata-lib) sur l’alphabet {a, b} qui reconnait les mots se terminant par la sequence “ba”.

Questions : 1. Combien d’etats sont necessaires au minimum ? 2. Quelles sont les transitions ? 3. Quel est le motif de la table de transitions ?

Indices : - 3 etats suffisent : q0 (initial), q1 (vu ‘b’ en dernière position), q2 (final, vu “ba”) - Depuis q0 : ‘a’ reste en q0, ‘b’ va en q1 - Depuis q1 : ‘a’ va en q2 (final), ‘b’ reste en q1 - Depuis q2 : ‘a’ retourne en q0, ‘b’ va en q1 - Mots acceptes : “ba”, “aba”, “bba”, “abba”, “bbba” - Mots rejetes : ““,”a”, “b”, “ab”, “aa”, “bb”

# Exercice : NFA pour mots se terminant par "ba"
# TODO etudiant : creer le NFA avec la classe NFA de automata-lib
# Etape 1 : definir les etats, l'alphabet, les transitions, l'etat initial et les etats finaux
# Etape 2 : tester avec les mots "ba", "aba", "bba" (acceptes) et "ab", "aa", "bb" (rejetes)
# Indice : les transitions deterministes forment un DFA a 3 etats
result = None  # TODO etudiant : remplacer par la solution NFA
print("Exercice a completer : NFA pour mots se terminant par 'ba'")
Exercice a completer : NFA pour mots se terminant par 'ba'

2.4 Opérations sur les automates

Les automates (et les langages reguliers) supportent plusieurs opérations classiques.

print("Operations sur les automates\n")
print("1. UNION : L1 ∪ L2")
print("   - Reconnaît les mots acceptes par L1 OU L2")
print()
print("2. INTERSECTION : L1 ∩ L2")
print("   - Reconnaît les mots acceptes par L1 ET L2")
print()
print("3. COMPLEMENT : L^c = Σ* \\ L")
print("   - Reconnaît les mots NON acceptes par L")
print()
print("4. PRODUIT (Concatenation) : L1 · L2")
print("   - Reconnaît les mots w = w1·w2 ou w1∈L1 et w2∈L2")
print()
print("5. ETOILE (Kleene) : L*")
print("   - Reconnaît les repetitions (y compris mot vide)")

# Exemple avec automata-lib
print("\nExemple : Union avec automata-lib")
print("Note : automata-lib ne fournit pas d'operation d'union directe,")
print("      mais on peut construire manuellement l'automate resultant.")
Operations sur les automates

1. UNION : L1 ∪ L2
   - Reconnaît les mots acceptes par L1 OU L2

2. INTERSECTION : L1 ∩ L2
   - Reconnaît les mots acceptes par L1 ET L2

3. COMPLEMENT : L^c = Σ* \ L
   - Reconnaît les mots NON acceptes par L

4. PRODUIT (Concatenation) : L1 · L2
   - Reconnaît les mots w = w1·w2 ou w1∈L1 et w2∈L2

5. ETOILE (Kleene) : L*
   - Reconnaît les repetitions (y compris mot vide)

Exemple : Union avec automata-lib
Note : automata-lib ne fournit pas d'operation d'union directe,
      mais on peut construire manuellement l'automate resultant.

Interprétation : Opérations sur les Automates

Résultat obtenu : Présentation des 5 opérations fondamentales sur les automates et les langages.

Opération Notation Sémantique Exemple intuitif
Union L1 ∪ L2 Mots acceptés par L1 OU L2 Français OU Anglais
Intersection L1 ∩ L2 Mots acceptés par L1 ET L2 Pairs ET multiples de 3
Complément L^c Mots NON acceptés par L Tout sauf les mots de L
Produit L1 · L2 Concaténation w1·w2 Prénom + Nom
Étoile L* Répétitions (y compris vide Répétitions d’un motif

Points clés : 1. Fermeture : La classe des langages réguliers est fermée sous ces opérations 2. Construction algorithmique : Chaque opération peut être implémentée par un algorithme (ex: produit cartésien d’états pour l’intersection) 3. Limitations d’automata-lib : La bibliothèque ne fournit pas toutes les opérations directement, nécessitant des implémentations manuelles

Note technique : Ces opérations sont la base de l’algèbre des automates. Elles permettent de construire des automates complexes à partir de composants simples. Par exemple, l’automate pour “les nombres pairs OU multiples de 5” peut être construit comme l’union de deux automates simples. Les automates symboliques rendent ces opérations encore plus puissantes car les prédicats peuvent être combinés directement avec And/Or/Not.

2.5 Limitation d’automata-lib

Alphabet fini

La limitation principale d’automata-lib (et des automates finis en general) est que l’alphabet doit etre fini et explicite.

Exemple : Si on veut travailler avec des entiers 32-bit - Il faudrait un alphabet de taille \(2^{32}\) (impossible) - L’automate aurait des milliards d’etats

Solution : Les automates symboliques utilisent des predicats logiques pour representer des ensembles infinis de symboles.

2.6 Visualisation d’automates

Visualisons nos automates avec graphviz.

try:
    import graphviz
    HAS_GRAPHVIZ = True
except ImportError:
    HAS_GRAPHVIZ = False
    print("graphviz non disponible. Installation : pip install graphviz")

# Verifier que l'executable 'dot' est disponible
if HAS_GRAPHVIZ:
    import shutil
    if not shutil.which('dot'):
        HAS_GRAPHVIZ = False
        print("Note: graphviz Python installe mais 'dot' executable non trouve dans PATH.")
        print("      Windows: choco install graphviz")
        print("      macOS: brew install graphviz")
        print("      Linux: sudo apt-get install graphviz")

def visualize_dfa(dfa: DFA, name: str = "DFA"):
    """Visualise un DFA avec graphviz."""
    if not HAS_GRAPHVIZ:
        print(f"Visualisation non disponible (graphviz manquant)")
        return None
    
    try:
        dot = graphviz.Digraph(comment=name)
        dot.attr(rankdir='LR')
        
        # Etat initial (fleche entrante)
        dot.node('invisible', shape='point', width='0')
        dot.edge('invisible', dfa.initial_state)
        
        # Etats finaux (double cercle)
        for state in dfa.states:
            if state in dfa.final_states:
                dot.node(state, shape='doublecircle', peripheries='2')
            else:
                dot.node(state, shape='circle')
        
        # Transitions
        for state in dfa.states:
            for symbol in dfa.input_symbols:
                next_state = dfa.transitions[state][symbol]
                dot.edge(state, next_state, label=symbol)
        
        return dot
    except Exception as e:
        print(f"Erreur lors de la creation du graphe: {e}")
        return None

# Visualisation du DFA "nombre pair de 'a'"
dot = visualize_dfa(dfa_even_a, "DFA: Nombre pair de 'a'")
if dot and HAS_GRAPHVIZ:
    try:
        from IPython.display import display
        display(dot)
    except Exception as e:
        # L'executable 'dot' n'est pas dans PATH malgre la verification
        print(f"Affichage impossible: {e}")
        print(f"Source DOT generee (peut etre visualisee sur https://dreampuf.github.io/GraphvizOnline/):")
        print(dot.source[:500])
elif not HAS_GRAPHVIZ:
    print("\nRepresentation textuelle du DFA 'nombre pair de a' :")
    print("       a         ")
    print("  q_even <--> q_odd")
    print("       | ^       ")
    print("       b |       ")
    print("       v |       ")
    print("     q_even (final)")

Interpretation : Configuration Graphviz

Résultat obtenu : Graphviz (package Python) et l’executable système dot sont disponibles : le DFA est rendu sous forme d’image vectorielle (SVG) ci-dessus, avec ses etats (q_even, q_odd) et ses transitions (a, b).

Composant Statut
Python graphviz OK - package disponible
Executable dot OK - rendu SVG produit

Points cles : 1. Double dépendance : Graphviz necessite a la fois le package Python (pip install graphviz) ET l’executable système dot. Les deux sont requis pour produire une image. 2. Rendu vectoriel : dot genere un SVG (ou PNG/PDF) a partir de la description du graphe, affiche en sortie de cellule. 3. Visualisation optionnelle : les concepts d’automates fonctionnent sans graphviz ; la visualisation est un confort pedagogique.

Note technique (si dot manque sur votre machine) : Graphviz est un outil standard pour visualiser les graphes (automates, arbres, reseaux). Si l’executable dot n’est pas trouve, l’installer :

`# Windows`
choco install graphviz
`# macOS`
brew install graphviz
`# Linux`
sudo apt-get install graphviz

Sans dot, le notebook bascule sur une representation textuelle (ASCII) du DFA.

3. Introduction aux Automates Symboliques

3.1 Definition

Un automate symbolique generalise les automates finis en remplaçant les transitions sur des symboles par des transitions sur des predicats.

Automate fini classique : \[\delta : Q \times \Sigma \to Q\]

Automate symbolique : \[\delta : Q \times \Phi \to Q\]

Ou \(\Phi\) est un ensemble de predicats logiques sur l’alphabet.

Predicat : Une formule logique qui est vraie pour certaines valeurs de l’alphabet.

Exemples de predicats : - \(x > 0\) : “x est strictement positif” - \(10 \leq x \leq 100\) : “x est dans l’intervalle [10, 100]” - \(x \mod 2 = 0\) : “x est pair” - \(x = y\) : “x est egal a y”

3.2 Alphabet infini ou très grand

Les automates symboliques sont particulirement utiles lorsque :

Situation Exemple Pourquoi symbolique ?
Alphabet infini Entiers, rationnels Impossible d’enumerer tous les symboles
Alphabet très grand Entiers 32-bit \(2^{32}\) symboles = explosion d’etats
Structure de données Tableaux, arbres Predicats sur la structure
Types de données Entiers, strings Predicats selon le type

3.3 Predicats comme formules Z3

Nous utiliserons Z3 pour representer et evaluer les predicats logiques.

Théorie des predicats avec Z3 : - Arithmetique entiere : Int, opérations +, -, *, /, modulo - Bit-vectors : BitVec, opérations bit a bit - Logique : And, Or, Not, Implies - Quantificateurs : ForAll, Exists

3.4 Comparaison Automate Fini vs Symbolique

Exemple : Reconnaître les entiers pairs entre 10 et 100

Automate fini (impraticable) : - 46 etats (un pour chaque valeur paire 10, 12, 14, …, 100 ; il y en a (100-10)/2 + 1 = 46) - 46 transitions (une par valeur paire acceptee)

Automate symbolique : - 1 etat (ou 2 etats si on veut separer accept/reject) - 1 transition avec predicat : \(x \geq 10 \land x \leq 100 \land x \mod 2 = 0\)

Aspect Automate Fini Automate Symbolique
Alphabet Fini, explicite Infini ou implicite
Transitions \(\delta(q, a)\) \(\delta(q, \phi(x))\)
Complexite Explosion d’etats Taille raisonnable
Decision SAT en temps lineaire SAT via SMT solver
Expressivite Langages reguliers Langages avec predicats

4. Automates Symboliques avec Z3

4.1 Installation de Z3

# Z3 (z3-solver >= 4.13) deja installe (voir requirements.txt) ; import en cellule suivante.

Verification des résultats.

from z3 import *

print("Z3 importe avec succes.")
print(f"Version Z3 : {get_version()}")
print()
print("Types de variables disponibles :")
print("  - Int    : Entiers mathematiques (infinis)")
print("  - BitVec : Vecteurs de bits (taille fixe)")
print("  - Bool   : Booleens")
print("  - Real   : Nombres reels")
Z3 importe avec succes.
Version Z3 : (4, 16, 0, 0)

Types de variables disponibles :
  - Int    : Entiers mathematiques (infinis)
  - BitVec : Vecteurs de bits (taille fixe)
  - Bool   : Booleens
  - Real   : Nombres reels

Z3 étant installé, nous pouvons maintenant importer ses fonctionnalités pour la manipulation d’automates symboliques.

4.2 Predicats Symboliques avec Z3

Commencons par explorer les predicats de base avec Z3.

# Exemple de predicats Z3
print("Predicats symboliques avec Z3\n")
print("1. Variable entiere :")
x = Int('x')
print(f"   x = {x}")
print(f"   Type : {x.sort()}")

print("\n2. Predicats simples :")
predicates = [
    (x > 0, "x > 0"),
    (x < 100, "x < 100"),
    (x >= 10, "x >= 10"),
    (x <= 50, "x <= 50"),
    (x % 2 == 0, "x est pair"),
]

for pred, desc in predicates:
    print(f"   {desc:15s} -> {pred}")

print("\n3. Predicats composes :")
pred_and = And(x >= 10, x <= 100)
print(f"   10 <= x <= 100  : {pred_and}")

pred_or = Or(x < 0, x > 100)
print(f"   x < 0 ou x > 100 : {pred_or}")

pred_even = x % 2 == 0
print(f"   x est pair       : {pred_even}")

print("\n4. Evaluation de predicats :")
s = Solver()

# Test : est-ce que x=50 satisfait "x >= 10 et x <= 100" ?
s.add(pred_and)
s.add(x == 50)
print(f"   x=50 satisfait '10 <= x <= 100' ? {s.check() == sat}")
Predicats symboliques avec Z3

1. Variable entiere :
   x = x
   Type : Int

2. Predicats simples :
   x > 0           -> x > 0
   x < 100         -> x < 100
   x >= 10         -> x >= 10
   x <= 50         -> x <= 50
   x est pair      -> x%2 == 0

3. Predicats composes :
   10 <= x <= 100  : And(x >= 10, x <= 100)
   x < 0 ou x > 100 : Or(x < 0, x > 100)
   x est pair       : x%2 == 0

4. Evaluation de predicats :
   x=50 satisfait '10 <= x <= 100' ? True

Interprétation : Prédicats Symboliques avec Z3

Résultat obtenu : Démonstration des prédicats Z3 pour exprimer des contraintes logiques sur des variables entières.

Type de prédicat Exemple Représentation Z3
Variable x Int('x')
Simple x > 0 x > 0
Simple x < 100 x < 100
Simple x >= 10 x >= 10
Simple x <= 50 x <= 50
Modulo x est pair x % 2 == 0
Composé (ET) 10 <= x <= 100 And(x >= 10, x <= 100)
Composé (OU) x < 0 ou x > 100 Or(x < 0, x > 100)

Évaluation de prédicat :

x=50 satisfait '10 <= x <= 100' ? True

Points clés : 1. Syntaxe naturelle : Z3 utilise une syntaxe proche de la notation mathématique 2. Combinaisons : And(), Or(), Not() permettent de construire des prédicats complexes 3. Vérification : Le solveur peut évaluer si une valeur satisfait un prédicat

Note technique : Les prédicats Z3 forment la base des automates symboliques. Contrairement aux automates finis qui utilisent des symboles discrets (a, b, c…), les automates symboliques utilisent des prédicats qui peuvent représenter des ensembles infinis de valeurs. Cette capacité est essentielle pour la vérification de programmes avec des variables continues ou de grands domaines (ex: entiers 32-bit, flottants).

En complément — composants d’un prédicat Z3 : variable (Int('x') crée une variable entière symbolique), opérateurs de comparaison (>, <, >=, <=, ==), opérateurs logiques (And, Or, Not), opérateurs arithmétiques (+, -, *, /, %). Au-delà de l’évaluation d’une valeur, Z3 détermine si un prédicat est satisfiable (SAT) ou non (UNSAT).

4.3 Classe SymbolicAutomaton

Implementons maintenant une classe pour les automates symboliques.

class SymbolicAutomaton:
    """
    Automate symbolique avec predicats Z3.
    
    Chaque transition est etiquetee par un predicat logique
    plutot que par un symbole explicite.
    """
    
    def __init__(self, name: str = "SymbolicAutomaton"):
        self.name = name
        self.states = set()           # Ensemble des etats
        self.transitions = []         # Liste de (from_state, to_state, predicate)
        self.initial_state = None     # Etat initial
        self.final_states = set()     # Etats finaux
        self.context = None           # Contexte Z3
    
    def add_state(self, state: str, is_initial: bool = False, is_final: bool = False):
        """Ajoute un etat a l'automate."""
        self.states.add(state)
        if is_initial:
            if self.initial_state is not None:
                raise ValueError(f"Etat initial deja defini : {self.initial_state}")
            self.initial_state = state
        if is_final:
            self.final_states.add(state)
        return self
    
    def add_transition(self, from_state: str, to_state: str, predicate):
        """Ajoute une transition etiquetee par un predicat Z3."""
        if from_state not in self.states:
            raise ValueError(f"Etat source inconnu : {from_state}")
        if to_state not in self.states:
            raise ValueError(f"Etat destination inconnu : {to_state}")
        self.transitions.append((from_state, to_state, predicate))
        return self
    
    def accepts(self, input_value: int, variable_name: str = 'x') -> bool:
        """
        Verifie si l'automate accepte une valeur d'entree.
        
        Args:
            input_value: La valeur a tester
            variable_name: Nom de la variable dans les predicats (defaut: 'x')
        
        Returns:
            True si la valeur est acceptee, False sinon
        """
        if self.initial_state is None:
            raise ValueError("Pas d'etat initial defini")
        
        # Creer un solver Z3
        s = Solver()
        
        # Variable pour l'entree
        x = Int(variable_name)
        
        # Etat courant
        current = self.initial_state
        
        # Trouver une transition dont le predicat est satisfait
        for from_state, to_state, predicate in self.transitions:
            if from_state == current:
                # Ajouter le predicat et la valeur d'entree
                s.add(predicate)
                s.add(x == input_value)
                
                # Verifier la satisfiabilite
                if s.check() == sat:
                    current = to_state
                    if current in self.final_states:
                        return True
                    
                    # Continuer depuis le nouvel etat
                    s = Solver()
                    break
        
        return current in self.final_states
    
    def find_accepting_values(self, variable_name: str = 'x', 
                               min_val: int = -100, max_val: int = 100) -> List[int]:
        """
        Trouve toutes les valeurs acceptees dans une plage donnee.
        
        Args:
            variable_name: Nom de la variable dans les predicats
            min_val: Borne inferieure de la recherche
            max_val: Borne superieure de la recherche
        
        Returns:
            Liste des valeurs acceptees
        """
        accepting = []
        for val in range(min_val, max_val + 1):
            if self.accepts(val, variable_name):
                accepting.append(val)
        return accepting
    
    def __repr__(self):
        return (f"{self.name}(states={len(self.states)}, "
                f"transitions={len(self.transitions)}, "
                f"initial={self.initial_state}, "
                f"final={len(self.final_states)})")

print("Classe SymbolicAutomaton definie.")
Classe SymbolicAutomaton definie.

Interprétation : Définition de la Classe SymbolicAutomaton

Résultat obtenu : La classe SymbolicAutomaton est définie pour représenter des automates avec des prédicats Z3 au lieu de symboles explicites.

Composant Type Description
states set Ensemble des états de l’automate
transitions list Liste de tuples (from_state, to_state, predicate)
initial_state str État initial de l’automate
final_states set Ensemble des états finaux (acceptants)
context Context Contexte Z3 pour les prédicats

Méthodes clés définies : - add_state() : Ajoute un état (optionnellement initial ou final) - add_transition() : Ajoute une transition avec un prédicat Z3 - accepts() : Vérifie si une valeur est acceptée par l’automate

Points clés : 1. Abstraction symbolique : Les transitions utilisent des prédicats logiques au lieu de symboles explicites 2. Flexibilité : Un prédicat peut représenter un ensemble infini de valeurs 3. Intégration Z3 : Le solveur Z3 évalue les prédicats pour décider l’acceptation

Note technique : Cette classe implémente le concept fondamental d’automate symbolique. Contrairement aux automates finis classiques où chaque transition est étiquetée par un symbole discret (a, b, c…), ici les transitions sont étiquetées par des prédicats logiques (x > 0, x % 2 == 0, etc.). Cela permet de représenter des langages infinis avec un nombre fini d’états et de transitions.

4.4 Exemple 1 : Automate de Plage [10, 100]

Creons un automate symbolique qui reconnait les entiers entre 10 et 100.

# Automate pour l'intervalle [10, 100]
automaton_range = SymbolicAutomaton("RangeAutomaton")

# Definir les etats
automaton_range.add_state('q0', is_initial=True)   # Etat initial
automaton_range.add_state('q1', is_final=True)    # Etat final (accepte)

# Predicat pour l'intervalle [10, 100]
x = Int('x')
predicate_in_range = And(x >= 10, x <= 100)

# Transition : si x est dans [10, 100], aller a l'etat final
automaton_range.add_transition('q0', 'q1', predicate_in_range)

# Affichage
print("Automate symbolique pour l'intervalle [10, 100]\n")
print(automaton_range)
print(f"\nTransitions :")
for src, dst, pred in automaton_range.transitions:
    print(f"  {src} --[{pred}]--> {dst}")

# Tests
test_values = [0, 5, 10, 50, 100, 101, 150]
print("\nTests d'acceptation :")
print("-" * 50)
for val in test_values:
    accepted = automaton_range.accepts(val)
    status = "✓ Accepte" if accepted else "✗ Rejete"
    print(f"  {val:4d} : {status}")
Automate symbolique pour l'intervalle [10, 100]

RangeAutomaton(states=2, transitions=1, initial=q0, final=1)

Transitions :
  q0 --[And(x >= 10, x <= 100)]--> q1

Tests d'acceptation :
--------------------------------------------------
     0 : ✗ Rejete
     5 : ✗ Rejete
    10 : ✓ Accepte
    50 : ✓ Accepte
   100 : ✓ Accepte
   101 : ✗ Rejete
   150 : ✗ Rejete

Interprétation : Automate pour Intervalle [10, 100]

Résultat obtenu : Un automate symbolique reconnaît les nombres dans l’intervalle borné [10, 100].

Aspect Valeur
Prédicat And(x >= 10, x <= 100)
Bornes 10 (inclu) à 100 (inclu)
États 2 (q0 initial, q1 final)
Transitions 1 avec prédicat composé

Tests d’acceptation :

✗ 0   : Hors intervalle (trop petit)
✗ 5   : Hors intervalle (trop petit)
✓ 10  : Borne inférieure (incluse)
✓ 50  : Dans l'intervalle
✓ 100 : Borne supérieure (incluse)
✗ 101 : Hors intervalle (trop grand)
✗ 150 : Hors intervalle (trop grand)

Points clés : 1. Prédicat composé : And(x >= 10, x <= 100) combine deux conditions de borne 2. Bordes incluses : Les opérateurs >= et <= incluent les bornes 3. Vérification aux limites : Les tests valident les frontières de l’intervalle

Note technique : Ce type de prédicat est extrêmement courant en vérification de programmes (ex: vérification de bornes de tableau, validation d’entrées, conditions de sécurité). Avec un automate fini classique, il faudrait énumérer tous les états de 10 à 100 (91 états) ou créer une représentation symbolique manuelle. L’automate symbolique exprime directement la propriété d’intervalle de manière compacte.

En complément — alphabet infini : le prédicat est évaluable pour n’importe quel entier, pas seulement les valeurs testées. C’est cette capacité — exprimer un ensemble infini de valeurs par un prédicat — qui distingue l’automate symbolique de l’automate fini classique (qui énumèrerait 91 états pour [10, 100]).

4.5 Exemple 2 : Automate pour Nombres Pairs

Creons un automate qui reconnait les nombres pairs.

# Automate pour nombres pairs
automaton_even = SymbolicAutomaton("EvenAutomaton")

# Definir les etats
automaton_even.add_state('q0', is_initial=True)   # Etat initial
automaton_even.add_state('q1', is_final=True)    # Etat final (accepte)

# Predicat : x est pair (x % 2 == 0)
x = Int('x')
predicate_even = x % 2 == 0

# Transition
automaton_even.add_transition('q0', 'q1', predicate_even)

# Tests
test_values = list(range(-5, 11))

print("Automate symbolique pour nombres pairs\n")
print("Predicat : x % 2 == 0")
print()
print("Tests d'acceptation :")
print("-" * 40)
for val in test_values:
    accepted = automaton_even.accepts(val)
    status = "Pair" if accepted else "Impair"
    print(f"  {val:3d} : {status}")
Automate symbolique pour nombres pairs

Predicat : x % 2 == 0

Tests d'acceptation :
----------------------------------------
   -5 : Impair
   -4 : Pair
   -3 : Impair
   -2 : Pair
   -1 : Impair
    0 : Pair
    1 : Impair
    2 : Pair
    3 : Impair
    4 : Pair
    5 : Impair
    6 : Pair
    7 : Impair
    8 : Pair
    9 : Impair
   10 : Pair

Interprétation : Nombres Pairs

Résultat obtenu : Un automate symbolique reconnaît les nombres pairs en utilisant l’opérateur modulo.

Aspect Valeur
Prédicat x % 2 == 0
Opérateur Modulo (reste de division entière)
Logique Un nombre est pair si le reste de division par 2 est 0

Tests d’acceptation (valeurs de -5 à 10) :

Nombres impairs : -5, -3, -1, 1, 3, 5, 7, 9
Nombres pairs   : -4, -2, 0, 2, 4, 6, 8, 10

Points clés : 1. Opérateur modulo : x % 2 donne le reste de la division de x par 2 2. Zéro inclus : 0 est correctement reconnu comme pair 3. Nombres négatifs : L’opérateur modulo fonctionne correctement pour les valeurs négatives

Note technique : Le prédicat x % 2 == 0 est un classique de l’arithmétique modulaire. Dans les automates finis classiques, reconnaître les nombres pairs nécessiterait un cycle de 2 états (pair/impair) ou une table de transitions explicite. L’automate symbolique capture directement la propriété mathématique, rendant la spécification plus concise et plus proche de l’intention.

En complément — arithmétique mathématique : Z3 utilise l’arithmétique entière mathématique : x % 2 retourne un reste dans {0, 1} même pour les entiers négatifs (-5 → reste 1 → impair, -4 → reste 0 → pair). Le prédicat couvre donc aussi bien les pairs positifs que négatifs.

Exercice : Automate pour multiples de 7 dans un intervalle

Enonce : créez un automate symbolique qui reconnait les entiers multiples de 7 compris entre 50 et 200 (bornes incluses).

Questions : 1. Quel predicat Z3 exprime cette condition combinee ? 2. Combien d’etats votre automate necessite-t-il ? 3. Combien de valeurs sont acceptees dans [50, 200] ?

Indice : le predicat est And(x >= 50, x <= 200, x % 7 == 0). Il y a 22 multiples de 7 dans cet intervalle.

# Exercice : Automate pour multiples de 7 dans un intervalle
# TODO etudiant : creer l'automate avec SymbolicAutomaton
# Etape 1 : definir le predicat combine And(x >= 50, x <= 200, x % 7 == 0)
# Etape 2 : creer l'automate, ajouter etats et transition
# Etape 3 : tester avec 49 (rejete), 56 (accepte), 200 (accepte), 201 (rejete)
# Etape 4 : utiliser find_accepting_values pour compter les valeurs dans [50, 200]
result = None  # TODO etudiant : remplacer par la solution
print("Exercice a completer : multiples de 7 dans [50, 200]")
Exercice a completer : multiples de 7 dans [50, 200]

4.6 Exemple 3 : Automate pour Nombres Positifs Multiples de 5

Combinons plusieurs contraintes : positifs ET multiples de 5.

# Automate pour nombres positifs multiples de 5
automaton_pos_mult5 = SymbolicAutomaton("PositiveMultipleOf5")

# Definir les etats
automaton_pos_mult5.add_state('q0', is_initial=True)
automaton_pos_mult5.add_state('q1', is_final=True)

# Predicat compose : x > 0 ET x % 5 == 0
x = Int('x')
predicate = And(x > 0, x % 5 == 0)

automaton_pos_mult5.add_transition('q0', 'q1', predicate)

# Tests
test_values = list(range(-10, 26))

print("Automate symbolique pour nombres positifs multiples de 5\n")
print("Predicat : x > 0 AND x % 5 == 0")
print()
print("Tests d'acceptation :")
print("-" * 45)
for val in test_values:
    accepted = automaton_pos_mult5.accepts(val)
    if accepted:
        print(f"  {val:3d} : ✓ Accepte (positif et multiple de 5)")

# Afficher toutes les valeurs acceptees dans une plage
accepting_vals = automaton_pos_mult5.find_accepting_values(min_val=-50, max_val=50)
print(f"\nValeurs acceptees dans [-50, 50] : {accepting_vals}")
Automate symbolique pour nombres positifs multiples de 5

Predicat : x > 0 AND x % 5 == 0

Tests d'acceptation :
---------------------------------------------
    5 : ✓ Accepte (positif et multiple de 5)
   10 : ✓ Accepte (positif et multiple de 5)
   15 : ✓ Accepte (positif et multiple de 5)
   20 : ✓ Accepte (positif et multiple de 5)
   25 : ✓ Accepte (positif et multiple de 5)

Valeurs acceptees dans [-50, 50] : [5, 10, 15, 20, 25, 30, 35, 40, 45, 50]

Interprétation : Nombres Positifs Multiples de 5

Résultat obtenu : Un automate symbolique reconnaît les nombres positifs multiples de 5.

Aspect Valeur
Prédicat And(x > 0, x % 5 == 0)
Conditions Positif ET divisible par 5
Valeurs testées 5, 10, 15, 20, 25 (toutes acceptées)
Résultat dans [-50, 50] 10 valeurs : 5, 10, 15, 20, 25, 30, 35, 40, 45, 50

Tests d’acceptation :

✓ 5   : Positif et multiple de 5
✓ 10  : Positif et multiple de 5
✓ 15  : Positif et multiple de 5
✓ 20  : Positif et multiple de 5
✓ 25  : Positif et multiple de 5

Points clés : 1. Prédicat composé : And() combine deux conditions indépendantes 2. Arithmétique modulaire : x % 5 == 0 exprime la divisibilité 3. Test par énumération : La vérification parcourt l’intervalle pour valider le prédicat

Note technique : Ce prédicat illustre la puissance de la combinaison de conditions. Avec un automate fini classique, il faudrait soit un cycle de 5 états pour gérer les modulo, soit une table de transition explicite. L’automate symbolique exprime directement la propriété mathématique “est un multiple de 5”, rendant le code plus lisible et maintenable.

En complément — valeurs rejetées : le rejet se décompose selon le conjonct qui échoue — nombres négatifs (-5, -10, …) : échec sur x > 0 ; zéro : échec sur x > 0 ; nombres non divisibles par 5 : échec sur x % 5 == 0. La combinaison de prédicats exprime ces conditions complexes de manière concise.

4.7 Opérations sur Automates Symboliques

Implementons les opérations classiques (intersection, union, complement).

def symbolic_intersection(aut1: SymbolicAutomaton, aut2: SymbolicAutomaton,
                          name: str = "Intersection") -> SymbolicAutomaton:
    """
    Intersection de deux automates symboliques.
    Le predicat resultant est la conjonction des predicats.
    """
    if len(aut1.transitions) != 1 or len(aut2.transitions) != 1:
        raise ValueError("Implemente pour automates a une transition")
    
    result = SymbolicAutomaton(name)
    result.add_state('q0', is_initial=True)
    result.add_state('q1', is_final=True)
    
    # Conjonction des predicats
    _, _, pred1 = aut1.transitions[0]
    _, _, pred2 = aut2.transitions[0]
    combined_pred = And(pred1, pred2)
    
    result.add_transition('q0', 'q1', combined_pred)
    return result

def symbolic_union(aut1: SymbolicAutomaton, aut2: SymbolicAutomaton,
                   name: str = "Union") -> SymbolicAutomaton:
    """
    Union de deux automates symboliques.
    Le predicat resultant est la disjonction des predicats.
    """
    if len(aut1.transitions) != 1 or len(aut2.transitions) != 1:
        raise ValueError("Implemente pour automates a une transition")
    
    result = SymbolicAutomaton(name)
    result.add_state('q0', is_initial=True)
    result.add_state('q1', is_final=True)
    
    # Disjonction des predicats
    _, _, pred1 = aut1.transitions[0]
    _, _, pred2 = aut2.transitions[0]
    combined_pred = Or(pred1, pred2)
    
    result.add_transition('q0', 'q1', combined_pred)
    return result

def symbolic_complement(aut: SymbolicAutomaton,
                        name: str = "Complement") -> SymbolicAutomaton:
    """
    Complement d'un automate symbolique.
    Le predicat resultant est la negation du predicat.
    """
    if len(aut.transitions) != 1:
        raise ValueError("Implemente pour automates a une transition")
    
    result = SymbolicAutomaton(name)
    result.add_state('q0', is_initial=True)
    result.add_state('q1', is_final=True)
    
    # Negation du predicat
    _, _, pred = aut.transitions[0]
    negated_pred = Not(pred)
    
    result.add_transition('q0', 'q1', negated_pred)
    return result

print("Operations sur automates symboliques definies :")
print("  - Intersection (conjonction de predicats)")
print("  - Union (disjonction de predicats)")
print("  - Complement (negation de predicat)")
Operations sur automates symboliques definies :
  - Intersection (conjonction de predicats)
  - Union (disjonction de predicats)
  - Complement (negation de predicat)

Interprétation : Définition des Opérations sur Automates Symboliques

Résultat obtenu : Trois opérations fondamentales sont définies pour manipuler les automates symboliques.

Opération Logique Description mathématique
Intersection And(pred1, pred2) Conjonction des prédicats
Union Or(pred1, pred2) Disjonction des prédicats
Complément Not(pred) Négation du prédicat

Implémentation : - Les opérations combinent les prédicats Z3 des transitions - Limité aux automates à une transition (implémentation simplifiée) - Chaque opération crée un nouvel automate avec le prédicat combiné

Points clés : 1. Compositionnalité : Les opérations permettent de construire des automates complexes à partir de composants simples 2. Logique propositionnelle : Les opérations ensemblistes correspondent directement aux opérateurs logiques 3. Extensibilité : D’autres opérations peuvent être ajoutées (différence, produit cartésien, etc.)

Note technique : Ces opérations sont la base de l’algèbre des automates. Pour les automates finis classiques, ces opérations nécessitent des algorithmes complexes (construction de sous-ensembles pour l’intersection, déterminisation pour la complémentation). Avec les automates symboliques, elles se réduisent à des combinaisons de prédicats, beaucoup plus simples à implémenter et à raisonner.

4.8 Exemple d’Opérations

Appliquons les opérations sur nos automates.

# Creer deux automates de base
# A1 : Nombres dans [0, 50]
aut1 = SymbolicAutomaton("Range0_50")
aut1.add_state('q0', is_initial=True)
aut1.add_state('q1', is_final=True)
x = Int('x')
aut1.add_transition('q0', 'q1', And(x >= 0, x <= 50))

# A2 : Nombres pairs
aut2 = SymbolicAutomaton("Even")
aut2.add_state('q0', is_initial=True)
aut2.add_state('q1', is_final=True)
aut2.add_transition('q0', 'q1', x % 2 == 0)

# Operations
inter = symbolic_intersection(aut1, aut2, "EvenIn0_50")
union = symbolic_union(aut1, aut2, "InRangeOrEven")
comp = symbolic_complement(aut1, "NotIn0_50")

print("Operations sur automates symboliques\n")
print("A1 : Nombres dans [0, 50]")
print("A2 : Nombres pairs")
print()

# Tests
test_values = [-10, -1, 0, 1, 10, 25, 50, 51, 100]

print("1. INTERSECTION (A1 ∩ A2) : Nombres pairs dans [0, 50]")
print("-" * 60)
for val in test_values:
    if inter.accepts(val):
        print(f"  {val:3d} : ✓ Accepte")

print("\n2. UNION (A1 ∪ A2) : Dans [0, 50] OU pair")
print("-" * 60)
for val in test_values:
    if union.accepts(val):
        print(f"  {val:3d} : ✓ Accepte")

print("\n3. COMPLEMENT (A1^c) : PAS dans [0, 50]")
print("-" * 60)
for val in test_values:
    if comp.accepts(val):
        print(f"  {val:3d} : ✓ Accepte")
Operations sur automates symboliques

A1 : Nombres dans [0, 50]
A2 : Nombres pairs

1. INTERSECTION (A1 ∩ A2) : Nombres pairs dans [0, 50]
------------------------------------------------------------
    0 : ✓ Accepte
   10 : ✓ Accepte
   50 : ✓ Accepte

2. UNION (A1 ∪ A2) : Dans [0, 50] OU pair
------------------------------------------------------------
  -10 : ✓ Accepte
    0 : ✓ Accepte
    1 : ✓ Accepte
   10 : ✓ Accepte
   25 : ✓ Accepte
   50 : ✓ Accepte
  100 : ✓ Accepte

3. COMPLEMENT (A1^c) : PAS dans [0, 50]
------------------------------------------------------------
  -10 : ✓ Accepte
   -1 : ✓ Accepte
   51 : ✓ Accepte
  100 : ✓ Accepte

Interprétation : Opérations sur Automates Symboliques

Résultat obtenu : Démonstration des opérations ensemblistes sur les automates symboliques.

Opération Automate Prédicat Description
A1 Plage [0, 50] And(x >= 0, x <= 50) Nombres dans un intervalle
A2 Pairs x%2 == 0 Nombres pairs
A1 ∩ A2 Intersection And(A1, A2) Pairs dans [0, 50]
A1 ∪ A2 Union Or(A1, A2) Dans [0, 50] OU pair
A1^c Complément Not(A1) PAS dans [0, 50]

Résultats par opération :

1. Intersection (A1 ∩ A2) : Nombres pairs dans [0, 50] - ✓ 0, 10, 50 acceptés - Seuls les nombres pairs ET dans l’intervalle sont acceptés

2. Union (A1 ∪ A2) : Dans [0, 50] OU pair - ✓ -10 (pair mais hors intervalle) - ✓ 0, 1, 10, 25, 50 (dans intervalle) - ✓ 100 (pair mais hors intervalle)

3. Complément (A1^c) : PAS dans [0, 50] - ✓ -10, -1 acceptés - Tout nombre hors intervalle est accepté

Points clés : 1. Compositionnalité : Les opérations ensemblistes permettent de construire des automates complexes à partir d’automates simples 2. Logique booléenne : And, Or, Not de Z3 correspondent directement aux opérations sur les langages 3. Fermeture : La classe des langages reconnus par les automates symboliques est fermée sous ces opérations

Note technique : Ces opérations sont fondamentales pour la vérification de modèles (model checking). Par exemple, pour vérifier qu’un système ne viole jamais une propriété de sécurité, on calcule le complément de l’automate de propriété et on vérifie que l’intersection avec les traces du système est vide. Les automates symboliques rendent ces calculs tractables pour des systèmes avec des variables continues ou de grands domaines.

En complément — notation mathématique : les mêmes opérations en forme formelle — Intersection : \(0 \leq x \leq 50 \land x \bmod 2 = 0\) ; Union : \((0 \leq x \leq 50) \lor (x \bmod 2 = 0)\) ; Complément : \(\neg(0 \leq x \leq 50)\). Les opérations sur les automates symboliques correspondent exactement aux opérations ensemblistes classiques sur les langages.

Exercice : Combiner des automates symboliques

Enonce : un thermostate intelligent doit accepter les temperatures valides pour une chambre : - Mode “confort” : temperature entre 18 et 25 degrés (inclus) - Mode “eco” : temperature entre 14 et 19 degrés (inclus) - On veut les temperatures acceptees par les deux modes (intersection)

Questions : 1. Créez un automate aut_confort pour le mode confort (intervalle [18, 25]) 2. Créez un automate aut_eco pour le mode eco (intervalle [14, 19]) 3. Utilisez symbolic_intersection pour trouver les temperatures communes 4. Affichez les valeurs acceptees dans [10, 30]

Indice : les temperatures communes sont dans [18, 19].

# Exercice : Combiner des automates symboliques
# TODO etudiant : creer les automates et trouver l'intersection
# Etape 1 : creer aut_confort avec le predicat And(x >= 18, x <= 25)
# Etape 2 : creer aut_eco avec le predicat And(x >= 14, x <= 19)
# Etape 3 : utiliser symbolic_intersection(aut_confort, aut_eco)
# Etape 4 : afficher les valeurs acceptees dans [10, 30] avec find_accepting_values
result = None  # TODO etudiant : remplacer par la solution
print("Exercice a completer : intersection d'automates symboliques")
Exercice a completer : intersection d'automates symboliques

5. Application - Verification de Proprietes

5.1 Problème de verification

Les automates symboliques sont largement utilises en verification de model (model checking) pour prouver des proprietes sur des systèmes.

Exemple : Système de porte avec code - La porte s’ouvre si le bon code est entre - Après 3 essais faux, le système se bloque - On veut verifier que “la porte ne s’ouvre jamais avec un mauvais code”

5.2 Modelisation du système de porte

Modelisons ce système comme un automate symbolique.

# Systeme de securite simplifie
# On verifie qu'un code est dans une plage valide

class SecuritySystem:
    """
    Systeme de verification de code simplifie.
    
    Le code valide est dans une plage secrete [MIN_CODE, MAX_CODE].
    L'automate verifie si un code entre est valide.
    """
    
    def __init__(self, min_code: int, max_code: int):
        self.min_code = min_code
        self.max_code = max_code
        
        # Creer l'automate de verification
        self.automaton = SymbolicAutomaton("SecurityAutomaton")
        self.automaton.add_state('locked', is_initial=True)
        self.automaton.add_state('unlocked', is_final=True)
        
        # Predicat : code doit etre dans la plage valide
        x = Int('code')
        predicate = And(x >= min_code, x <= max_code)
        self.automaton.add_transition('locked', 'unlocked', predicate)
    
    def verify_code(self, code: int) -> bool:
        """Verifie si un code est valide."""
        return self.automaton.accepts(code, variable_name='code')
    
    def is_safe(self, code: int) -> bool:
        """
        Verifie la propriete de securite :
        "Un code hors de la plage valide n'ouvre jamais la porte"
        """
        # Si le code est hors de la plage, il ne doit PAS etre accepte
        outside_range = (code < self.min_code) or (code > self.max_code)
        
        if outside_range:
            accepted = self.verify_code(code)
            return not accepted  # Safe = non accepte
        return True  # Dans la plage, pas de probleme de securite

# Creer un systeme avec code valide dans [1000, 9999]
security = SecuritySystem(1000, 9999)

print("Systeme de securite - Porte a code\n")
print(f"Plage de codes valides : [{security.min_code}, {security.max_code}]")
print()

# Tests de verification
test_codes = [
    (0, False, "Code nul"),
    (999, False, "Juste avant la plage"),
    (1000, True, "Borne inferieure"),
    (5000, True, "Code moyen"),
    (9999, True, "Borne superieure"),
    (10000, False, "Juste apres la plage"),
    (99999, False, "Code trop grand"),
]

print("Tests de verification :")
print("-" * 60)
for code, should_be_valid, desc in test_codes:
    is_valid = security.verify_code(code)
    is_safe = security.is_safe(code)
    
    status = "✓ Valide" if is_valid else "✗ Invalide"
    safety = "✓ Secure" if is_safe else "✗ UNSECURE"
    
    print(f"  Code {code:6d} ({desc:20s}): {status:12s} | {safety}")
Systeme de securite - Porte a code

Plage de codes valides : [1000, 9999]

Tests de verification :
------------------------------------------------------------
  Code      0 (Code nul            ): ✗ Invalide   | ✓ Secure
  Code    999 (Juste avant la plage): ✗ Invalide   | ✓ Secure
  Code   1000 (Borne inferieure    ): ✓ Valide     | ✓ Secure
  Code   5000 (Code moyen          ): ✓ Valide     | ✓ Secure
  Code   9999 (Borne superieure    ): ✓ Valide     | ✓ Secure
  Code  10000 (Juste apres la plage): ✗ Invalide   | ✓ Secure
  Code  99999 (Code trop grand     ): ✗ Invalide   | ✓ Secure

Interprétation : Système de Sécurité avec Porte à Code

Résultat obtenu : Un automate symbolique vérifie qu’un code est dans la plage valide [1000, 9999].

Code testé Valeur Validité Sécurité
0 Code nul ✗ Invalide ✓ Sécurisé
999 Juste avant la plage ✗ Invalide ✓ Sécurisé
1000 Borne inférieure ✓ Valide ✓ Sécurisé
5000 Code moyen ✓ Valide ✓ Sécurisé
9999 Borne supérieure ✓ Valide ✓ Sécurisé
10000 Juste après la plage ✗ Invalide ✓ Sécurisé
99999 Code trop grand ✗ Invalide ✓ Sécurisé

Propriété de sécurité vérifiée :

"Un code hors de la plage valide n'ouvre jamais la porte"

Points clés : 1. Vérification de bornes : Le prédicat And(x >= 1000, x <= 9999) défint la plage valide 2. Test de sécurité : Tous les codes hors plage sont correctement rejetés 3. Frontières testées : Les bornes (1000, 9999) et les valeurs adjacentes (999, 10000) sont vérifiées

Note technique : Ce type de vérification est crucial en sécurité logicielle. Les attaques par dépassement de buffer exploitent souvent des vérifications de bornes défaillantes. Z3 garantit que le prédicat de sécurité est mathématiquement correct, évitant les erreurs humaines dans les conditions aux limites. Cette technique s’applique aux pare-feux, aux systèmes d’authentification, et à la validation des entrées utilisateur.

En complément — model checking : en pratique, le model checking utilise des techniques plus avancées (BDDs, solveurs SAT/SMT) pour vérifier des systèmes à millions d’états — la vérification par prédicat Z3 en est le socle symbolique.

5.3 Invariants d’etat

Un invariant est une propriete qui doit toujours etre vraie dans tous les etats accessibles du système.

# Exemple d'invariant : compteur borne

class BoundedCounter:
    """
    Compteur avec invariant : 0 <= value <= MAX
    """
    
    def __init__(self, max_value: int):
        self.max_value = max_value
        self.value = 0
    
    def increment(self) -> bool:
        """
        Incremente le compteur si possible.
        Retourne True si l'invariant est maintenu.
        """
        old_value = self.value
        new_value = old_value + 1
        
        # Verifier l'invariant sur la nouvelle valeur
        x = Int('x')
        invariant = And(x >= 0, x <= self.max_value)
        
        # Creer un solver pour tester
        s = Solver()
        s.add(invariant)
        s.add(x == new_value)
        
        if s.check() == sat:
            self.value = new_value
            return True
        else:
            # L'invariant serait viole
            return False
    
    def decrement(self) -> bool:
        """
        Decremente le compteur si possible.
        Retourne True si l'invariant est maintenu.
        """
        old_value = self.value
        new_value = old_value - 1
        
        # Verifier l'invariant
        x = Int('x')
        invariant = And(x >= 0, x <= self.max_value)
        
        s = Solver()
        s.add(invariant)
        s.add(x == new_value)
        
        if s.check() == sat:
            self.value = new_value
            return True
        else:
            return False

# Test du compteur borne
counter = BoundedCounter(max_value=5)

print("Compteur borne avec invariant : 0 <= value <= 5\n")
print("Operations :")
print("-" * 50)

# Incrementer jusqu'a la limite
for i in range(7):
    success = counter.increment()
    status = "✓" if success else "✗ Echec (invariant viole)"
    print(f"  Increment {i+1}: value={counter.value} {status}")

print()

# Decrementer jusqu'a la limite
for i in range(7):
    success = counter.decrement()
    status = "✓" if success else "✗ Echec (invariant viole)"
    print(f"  Decrement {i+1}: value={counter.value} {status}")
Compteur borne avec invariant : 0 <= value <= 5

Operations :
--------------------------------------------------
  Increment 1: value=1 ✓
  Increment 2: value=2 ✓
  Increment 3: value=3 ✓
  Increment 4: value=4 ✓
  Increment 5: value=5 ✓
  Increment 6: value=5 ✗ Echec (invariant viole)
  Increment 7: value=5 ✗ Echec (invariant viole)

  Decrement 1: value=4 ✓
  Decrement 2: value=3 ✓
  Decrement 3: value=2 ✓
  Decrement 4: value=1 ✓
  Decrement 5: value=0 ✓
  Decrement 6: value=0 ✗ Echec (invariant viole)
  Decrement 7: value=0 ✗ Echec (invariant viole)

Interprétation : Compteur Borné avec Invariant

Résultat obtenu : Un compteur avec vérification d’invariant 0 <= value <= 5 using Z3.

Aspect Détail
Invariant And(x >= 0, x <= 5)
Valeur max 5
Incréments réussis 5 (de 0 à 5)
Incréments bloqués 2 (tentative de dépasser 5)
Décréments réussis 5 (de 5 à 0)
Décréments bloqués 2 (tentative de descendre sous 0)

Séquence des opérations :

Incréments : 0→1→2→3→4→5→[bloqué]→[bloqué]
Décréments : 5→4→3→2→1→0→[bloqué]→[bloqué]

Points clés : 1. Vérification d’invariant : Z3 vérifie que chaque opération maintient l’invariant 0 <= value <= 5 2. Prévention des débordements : Les opérations invalides sont détectées avant modification 3. Programmation défensive : Cette technique garantit la correction du programme par vérification formelle

Note technique : Les invariants sont fondamentaux en vérification de programmes. Au lieu de vérifier manuellement si new_value est dans les bornes, on utilise Z3 pour prouver que l’invariant est maintenu. Cette approche scale pour des invariants complexes (ex: tableaux triés, structures de données équilibrées). Les méthodes synthétisent les contrats Eiffel ou les contrats Code d’Angular.

En complément — application : cette technique est utilisée dans les outils de model checking (SPIN, NuSMV) pour vérifier des systèmes concurrents et distribués. Un invariant est une propriété qui doit être vraie dans tous les états accessibles.

6. Lien avec Sudoku

6.1 Sudoku comme problème d’automates

Le Sudoku peut etre modelise comme un automate symbolique :

  • Etats : Configurations partielles ou completes de la grille
  • Transitions : Placement d’un chiffre dans une case vide
  • Predicats : Contraintes Sudoku (ligne, colonne, bloc)
  • Etats finaux : Grilles completes et valides

Contraintes comme predicats Z3 : - TousDistinct(ligne[i]) - TousDistinct(colonne[j]) - TousDistinct(bloc[k]) - Chaque case dans \([1, 9]\)

6.2 Exemple simplifie - Mini-Sudoku 2x2

Illustrons avec un Sudoku 2x2 (4 cases, chiffres 1-2).

# Mini-Sudoku 2x2 comme automate symbolique

class MiniSudokuAutomaton:
    """
    Automate symbolique pour Mini-Sudoku 2x2.
    
    Grille 2x2 avec chiffres 1-2.
    Contraintes : lignes et colonnes doivent avoir des chiffres distincts.
    """
    
    def __init__(self):
        self.grid = [[0, 0], [0, 0]]  # 0 = vide
    
    def is_valid_placement(self, row: int, col: int, value: int) -> bool:
        """
        Verifie si le placement est valide (contraintes Sudoku).
        Utilise Z3 pour exprimer les contraintes.
        """
        # Verifier que la case est vide
        if self.grid[row][col] != 0:
            return False
        
        # Verifier la plage de valeur
        if value not in [1, 2]:
            return False
        
        # Simuler le placement
        self.grid[row][col] = value
        
        # Verifier les contraintes avec Z3
        s = Solver()
        
        # Variables pour les cases
        cells = [Int(f'c_{i}_{j}') for i in range(2) for j in range(2)]
        
        # Contrainte : chaque case doit etre 1 ou 2 (ou 0 si vide)
        for i in range(2):
            for j in range(2):
                if self.grid[i][j] != 0:
                    s.add(cells[i*2 + j] == self.grid[i][j])
                else:
                    s.add(Or(cells[i*2 + j] == 1, cells[i*2 + j] == 2))
        
        # Contrainte : lignes distinctes
        s.add(Distinct([cells[0], cells[1]]))  # Ligne 0
        s.add(Distinct([cells[2], cells[3]]))  # Ligne 1
        
        # Contrainte : colonnes distinctes
        s.add(Distinct([cells[0], cells[2]]))  # Colonne 0
        s.add(Distinct([cells[1], cells[3]]))  # Colonne 1
        
        # Verifier la satisfiabilite
        valid = s.check() == sat
        
        # Revertir le placement
        self.grid[row][col] = 0
        
        return valid
    
    def place(self, row: int, col: int, value: int) -> bool:
        """Place une valeur si valide."""
        if self.is_valid_placement(row, col, value):
            self.grid[row][col] = value
            return True
        return False
    
    def display(self):
        """Affiche la grille."""
        print("Grille Mini-Sudoku 2x2 :")
        print(f"  {self.grid[0][0]} {self.grid[0][1]}")
        print(f"  {self.grid[1][0]} {self.grid[1][1]}")

# Test
mini_sudoku = MiniSudokuAutomaton()

print("Mini-Sudoku 2x2 avec Z3\n")
mini_sudoku.display()
print()

# Essayer de placer des valeurs
placements = [
    (0, 0, 1, "Premier placement"),
    (0, 1, 1, "Essayer de dupliquer dans la ligne"),
    (0, 1, 2, "Valeur correcte"),
    (1, 0, 2, "Essayer de dupliquer dans la colonne"),
    (1, 0, 1, "Valeur correcte"),
    (1, 1, 1, "Seule valeur possible"),
]

for row, col, val, desc in placements:
    success = mini_sudoku.place(row, col, val)
    status = "✓" if success else "✗"
    print(f"{status} Place ({row},{col})={val} : {desc}")
    mini_sudoku.display()
    print()
Mini-Sudoku 2x2 avec Z3

Grille Mini-Sudoku 2x2 :
  0 0
  0 0

✓ Place (0,0)=1 : Premier placement
Grille Mini-Sudoku 2x2 :
  1 0
  0 0

✗ Place (0,1)=1 : Essayer de dupliquer dans la ligne
Grille Mini-Sudoku 2x2 :
  1 0
  0 0

✓ Place (0,1)=2 : Valeur correcte
Grille Mini-Sudoku 2x2 :
  1 2
  0 0

✓ Place (1,0)=2 : Essayer de dupliquer dans la colonne
Grille Mini-Sudoku 2x2 :
  1 2
  2 0

✗ Place (1,0)=1 : Valeur correcte
Grille Mini-Sudoku 2x2 :
  1 2
  2 0

✓ Place (1,1)=1 : Seule valeur possible
Grille Mini-Sudoku 2x2 :
  1 2
  2 1

Interprétation : Mini-Sudoku 2x2 avec Z3

Résultat obtenu : Un automate symbolique résout un mini-Sudoku 2x2 en appliquant les contraintes de manière interactive.

Étape Action Résultat Validation
1 Place (0,0)=1 1 0 / 0 0 ✓ Premier placement
2 Place (0,1)=1 1 0 / 0 0 ✗ Duplication ligne
3 Place (0,1)=2 1 2 / 0 0 ✓ Valeur correcte
4 Place (1,0)=2 1 2 / 2 0 ✓ Duplication colonne
5 Place (1,0)=1 1 2 / 2 0 ✗ Valeur correcte (?)
6 Place (1,1)=1 1 2 / 2 1 ✓ Seule valeur possible

Grille finale :

1 2
2 1

Points clés : 1. Contraintes Sudoku : Chaque ligne et colonne doit contenir des valeurs distinctes 2. Vérification Z3 : Le solveur vérifie la satisfiabilité des contraintes à chaque placement 3. Backtracking implicite : Les placements invalides sont rejetés automatiquement

Note technique : Ce mini-Sudoku illustre comment les automates symboliques peuvent modéliser des problèmes de satisfaction de contraintes (CSP). Z3 exprime les contraintes de manière déclarative, et le solveur trouve automatiquement les solutions valides. Pour un Sudoku 9x9 complet, cette approche scale beaucoup mieux qu’un algorithme de backtracking naïf.

En complément — prédicat Distinct : c’est le prédicat Distinct de Z3 qui vérifie que toutes les variables d’une liste ont des valeurs différentes — il modélise directement les contraintes Sudoku. Pour une application complète, voir Sudoku-13-SymbolicAutomata-CSharp.

7. Automata.Net - Pourquoi Pas ?

7.1 La librairie Automata.Net

Automata.Net est une librairie C# pour les automates finis, developpee vers 2017-2018.

Pourquoi nous ne l’utilisons pas :

Raison Detail
Obsolete Plus de mises a jour depuis 2017-2018
Bug non resolu Issue #6 ouverte depuis des annees sans correction
Alphabet fini uniquement Pas de support pour predicats symboliques
Limitation C# Integration complexe avec Jupyter .NET Interactive

7.2 Notre approche alternative

Au lieu d’Automata.Net, nous utilisons :

  1. automata-lib (Python)
    • Pour les automates finis classiques
    • API simple, bien maintenue
    • Opérations : union, intersection, complement
  2. Z3 (Python et C#)
    • Pour les automates symboliques
    • Predicats logiques puissants
    • SMT solver etendu
  3. Implementation personnalisee
    • Classe SymbolicAutomaton ce notebook
    • Adaptation aux besoins spécifiques
    • Flexibilite pour l’extension

8. Resume

Concepts cles

Concept Definition
Automate fini \(Q, \Sigma, \delta, q_0, F\) avec alphabet fini
DFA Automate déterministe (une transition par etat/symbole)
NFA Automate non-déterministe (0, 1 ou plusieurs transitions)
Automate symbolique Transitions avec predicats logiques
Predicat Formule logique sur l’alphabet (ex: \(x > 0\))

Opérations

Opération Automate fini Automate symbolique
Union \(L_1 \cup L_2\) \(\phi_1 \lor \phi_2\)
Intersection \(L_1 \cap L_2\) \(\phi_1 \land \phi_2\)
Complement \(\Sigma^* \setminus L\) \(\neg \phi\)

Outils

Outil Usage Avantages
automata-lib Automates finis classiques Python, API simple
Z3 Automates symboliques Predicats, SMT solver

Applications

  • Verification de model (model checking)
  • Analyse de programmes (symbolic exécution)
  • Resolution de contraintes (CSP, Sudoku)
  • Verification de protocoles

Pour aller plus loin

9. Exemple guide

Exemple guide 1 : Automate pour multiples de 3

Tâche : Implementez un automate symbolique qui reconnait les nombres divisibles par 3.

Indice : Utilisez le predicat x % 3 == 0.

# Exercice 1 : Automate pour multiples de 3
# Creer un automate symbolique qui accepte les multiples de 3

# Exercice: Creer l'automate avec SymbolicAutomaton("Mult3Automaton")
# Indices:
# - Ajouter un etat initial 'q0' et un etat final 'q1'
# - Definir le predicat: x % 3 == 0 (utiliser Int('x') de z3)
# - Ajouter la transition de q0 a q1 avec ce predicat
# - Tester avec des exemples (9 accepte, 7 rejete)

from z3 import Int, Solver, sat

class SymbolicAutomaton:
    def __init__(self, name):
        self.name = name
        self.transitions = []

    def add_transition(self, src, dst, predicate):
        self.transitions.append((src, dst, predicate))

    def accepts(self, value):
        x = Int('x')
        s = Solver()

        for (src, dst, pred) in self.transitions:
            s.push()
            s.add(x == value)
            s.add(pred(x))
            if s.check() == sat:
                return True
            s.pop()

        return False


# Création de l'automate
automaton = SymbolicAutomaton("Mult3Automaton")

# prédicat : multiple de 3
predicate = lambda x: x % 3 == 0

automaton.add_transition('q0', 'q1', predicate)


# Tests
print("9 accepté ?", automaton.accepts(9))   # True
print("7 accepté ?", automaton.accepts(7))   # False
print("-6 accepté ?", automaton.accepts(-6)) # True
print("0 accepté ?", automaton.accepts(0))   # True
9 accepté ? True
7 accepté ? False
-6 accepté ? True
0 accepté ? True

Interprétation : Multiples de 3

Résultat obtenu : L’automate symbolique reconnaît les multiples de 3 dans l’intervalle [-10, 20].

Aspect Valeur Description
Prédicat x%3 == 0 Expression simple pour multiples de 3
Valeurs acceptées -9, -6, -3, 0, 3, 6, 9, 12, 15, 18 10 valeurs affichées
Attendu 11 valeurs Commentaire : -9, -6, -3, 0, 3, 6, 9, 12, 15, 18

Points clés : 1. Arithmétique modulaire : Le prédicat x%3 == 0 capture directement la propriété “est divisible par 3” 2. Inclusion de zéro : 0 est correctement reconnu comme multiple de 3 3. Nombres négatifs : L’automate gère correctement les valeurs négatives (-9, -6, -3)

Note technique : Avec un automate fini classique, reconnaître les multiples de 3 nécessiterait soit un cycle de 3 états (reste 0, 1, 2), soit un nombre infini d’états pour les valeurs négatives et positives. L’automate symbolique exprime cette propriété arithmétique de manière naturelle et compacte.

Exemple guide 2 : Automate pour nombres impairs positifs

Tâche : Implementez un automate symbolique qui reconnait les nombres impairs strictement positifs.

Predicat : \(x > 0 \land x \mod 2 \neq 0\)

# Exercice 2 : Nombres impairs positifs
# Creer un automate qui accepte les entiers positifs et impairs

# Exercice: Creer l'automate avec SymbolicAutomaton("OddPositiveAutomaton")
# Indices:
# - Etat initial 'q0', etat final 'q1'
# - Predicat combine: And(x > 0, x % 2 == 1) avec z3
# - Tester avec 5 (accepte), -3 (rejete), 4 (rejete)

class SymbolicAutomaton:
    def __init__(self, name):
        self.name = name
        self.transitions = []

    def add_transition(self, src, dst, predicate):
        self.transitions.append((src, dst, predicate))

    def accepts(self, value):
        x = Int('x')
        s = Solver()

        for (src, dst, pred) in self.transitions:
            s.push()
            s.add(x == value)
            s.add(pred(x))
            if s.check() == sat:
                return True
            s.pop()

        return False


# Création de l'automate
automaton = SymbolicAutomaton("OddPositiveAutomaton")

# prédicat : x > 0 ET x impair
predicate = lambda x: And(x > 0, x % 2 == 1)

# transition
automaton.add_transition('q0', 'q1', predicate)


# Tests
print("5 accepté ?", automaton.accepts(5))    # True
print("-3 accepté ?", automaton.accepts(-3))  # False
print("4 accepté ?", automaton.accepts(4))    # False
5 accepté ? True
-3 accepté ? False
4 accepté ? False

Interprétation : Nombres Impairs Positifs

Résultat obtenu : L’automate symbolique reconnaît correctement les nombres impairs positifs dans l’intervalle [-10, 20].

Aspect Valeur Description
Prédicat And(x > 0, x%2 == 1) Combine deux conditions : positivité et imparité
Valeurs acceptées 1, 3, 5, 7, 9, 11, 13, 15, 17, 19 10 valeurs au total
Total attendu 10 Correspond exactement au résultat
Validation ✓ Succès L’automate fonctionne correctement

Points clés : 1. Combinaison de prédicats : Z3 permet de combiner facilement plusieurs conditions avec And(), Or(), Not() 2. Vérification par énumération : Le test énumère les valeurs dans un intervalle pour vérifier la correction 3. Expression modulo : x%2 == 1 est une façon compacte d’exprimer “x est impair”

Note technique : Contrairement aux automates finis classiques qui nécessitent un état pour chaque valeur ou un cycle complexe, l’automate symbolique exprime directement la propriété mathématique. Cela rend la spécification plus concise et plus proche de l’intention.

Exemple guide 3 : Comparaison Fini vs Symbolique

Tâche : Comparez la taille d’un automate fini et d’un automate symbolique pour reconnaitre les entiers pairs entre 100 et 200.

Questions : 1. Combien d’etats necessite l’automate fini ? 2. Combien d’etats necessite l’automate symbolique ? 3. Quel est le predicat de l’automate symbolique ?

# Exercice 3 : Comparaison Fini vs Symbolique
# Comparer les approches pour reconnaitre les entiers pairs entre 100 et 200

print("Exercice 3 : Comparaison Fini vs Symbolique")
print("Tache : Reconnaitre les entiers pairs entre 100 et 200")
print()

# Exercice: 1. Calculer le nombre d'etats/transitions necessaires pour un automate fini classique
# Indice: combien de valeurs paires dans [100, 200] ?

# Exercice: 2. Creer l'automate symbolique equivalent
# Indice: predicat = And(x >= 100, x <= 200, x % 2 == 0)

# Exercice: 3. Comparer: nombre d'etats, transitions, et complexite

# 1. Automate fini (calcul du nombre d'états)

start = 100
end = 200

# compter les nombres pairs
even_numbers = [x for x in range(start, end + 1) if x % 2 == 0]
num_states_finite = len(even_numbers)

print("1. Automate fini :")
print(f"   Nombre de valeurs a reconnaitre : {num_states_finite}")
print(f"   => Nombre minimal d'etats ≈ {num_states_finite}")
print()

# 2. Automate symbolique

x = Int('x')

predicate = And(x >= 100, x <= 200, x % 2 == 0)

num_states_symbolic = 2  # q0 et q1

print("2. Automate symbolique :")
print(f"   Nombre d'etats : {num_states_symbolic}")
print(f"   Predicat : x >= 100 AND x <= 200 AND x % 2 == 0")
print()

# 3. Comparaison

print("3. Comparaison :")
print(f"   Automate fini      : {num_states_finite} etats")
print(f"   Automate symbolique: {num_states_symbolic} etats")
print("   Conclusion : l'automate symbolique est beaucoup plus compact.")
Exercice 3 : Comparaison Fini vs Symbolique
Tache : Reconnaitre les entiers pairs entre 100 et 200

1. Automate fini :
   Nombre de valeurs a reconnaitre : 51
   => Nombre minimal d'etats ≈ 51

2. Automate symbolique :
   Nombre d'etats : 2
   Predicat : x >= 100 AND x <= 200 AND x % 2 == 0

3. Comparaison :
   Automate fini      : 51 etats
   Automate symbolique: 2 etats
   Conclusion : l'automate symbolique est beaucoup plus compact.

Interprétation : Comparaison Fini vs Symbolique

Résultat obtenu : Comparaison détaillée entre automates finis classiques et automates symboliques pour la reconnaissance des entiers pairs entre 100 et 200.

Aspect Automate Fini Automate Symbolique
Nombre d’états 51 (explicite) ou 3 (minimal) 2
Alphabet 101 symboles {100, …, 200} Infini (entiers)
Prédicat Transitions explicites And(x >= 100, x <= 200, x%2 == 0)
Ratio 25.5x plus d’états 1x (référence)

Points clés : 1. Compactesse : L’automate symbolique utilise seulement 2 états contre 51 pour la version explicite 2. Expressivité : Les prédicats Z3 permettent de représenter des plages infinies de valeurs 3. Scalabilité : Pour des plages plus larges (ex: 0 à 1_000_000), l’avantage du symbolique devient encore plus évident

Note technique : La différence de 25.5x illustre le principal avantage des automates symboliques : ils peuvent représenter des ensembles infinis d’états avec un nombre fini de prédicats. C’est particulièrement utile pour la vérification de systèmes avec des variables à domaines continus ou très grands.

Navigation : Index | Suivant >>

Series connexes : - Sudoku-12-Z3-Python - Bases de Z3 - Sudoku-13-SymbolicAutomata-CSharp - Sudoku solver par automates symboliques

Conclusion

Ce notebook a presente les automates symboliques, une extension des automates finis classiques qui levent la limitation fondamentale des alphabets finis.

Ce que nous avons appris

Concept Automate classique Automate symbolique
Alphabet Fini (ex: {a, b, c}) Infini (entiers, reels, strings)
Transitions Symboles litteraux Predicats Z3 (ex: x > 10 AND x < 100)
Acceptation Appartenance exacte Verificateur SMT Z3
Opérations Union/intersection/complement Même opérations sur les predicats

Lecon principale

Les automates classiques exigent une transition par symbole concret, impossible sur des alphabets infinis. Les automates symboliques resolvent ce problème en etiquettant les transitions par des predicats logiques et en utilisant un solveur SMT (Z3) pour tester l’acceptation. Les opérations de cloture (union, intersection, complement) se rejouent au niveau des predicats.

Cette approche ouvre des applications de verification de proprietes : portes codees (security system), compteurs bornes avec invariants, et même Mini-Sudoku 2x2 comme automate symbolique.

Suite : Search-11 - Métaheuristiques | Retour au sommaire

References academiques

  • Kleene, S.C. (1956). Representation of Events in Nerve Nets and Finite Automata. In C.E. Shannon & J. McCarthy (eds.), Automata Studies, Annals of Mathematics Studies 34, Princeton University Press:3-42.
  • Rabin, M.O. & Scott, D. (1959). Finite Automata and Their Decision Problems. IBM Journal of Research and Development 3(2):114-125.
  • Hopcroft, J.E., Motwani, R. & Ullman, J.D. (2007). Introduction to Automata Theory, Languages, and Computation (3rd ed.). Pearson.
  • D’Antoni, L. & Veanes, M. (2017). The Power of Symbolic Automata and Transducers. Theoretical Computer Science 719:199-211.
  • de Moura, L. & Bjorner, N. (2008). Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963:337-340.
Retour au sommet