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

Search-10 (C#) : Automates Finis Classiques — jumeau .NET (tranche 1)

Navigation : Index | Version Python (automates symboliques Z3)

Ce notebook est le jumeau C# / .NET de Search-10-SymbolicAutomata.ipynb. La version Python couvre l’ensemble du sujet (automates finis + automates symboliques avec Z3). Cette version .NET est livrée en deux tranches :

• Tranche 1 (ce notebook) — Automates finis classiques : DFA, NFA, opérations ensemblistes. Implémentation manuelle en C# (cf. §7 du notebook Python : « Notre approche alternative » — il n’existe pas de librairie .NET équivalente à automata-lib qui soit à la fois maintenue et didactique ; construire les classes DFA/NFA à la main EST l’objectif pédagogique).
• Tranche 2 (livrée : §4 de ce notebook) — Automates symboliques avec Microsoft.Z3 (NuGet) : prédicats sur alphabet infini, intervalles, parité — le cœur « symbolique » du sujet.
• Tranche 3 (#10382, livrée) — Le moteur réel automata-lib (celui du jumeau Python) invoqué via le pont PythonNet 3.1.0 : expériences du jumeau rejouées, déterminisation, minimisation Myhill-Nerode, opérations ensemblistes natives du moteur.

Objectifs d’apprentissage (tranche 1)

À la fin de cette tranche, vous saurez : 1. Comprendre la différence entre automate fini déterministe (DFA) et non déterministe (NFA). 2. Appliquer — implémenter un DFA et un NFA en C# à partir d’une spécification. 3. Analyser — exécuter un automate sur un mot et décider l’acceptation. 4. Créer — combiner des automates via les opérations ensemblistes (union, intersection, complément).

Prérequis

• Bases du C# (classes, génériques, LINQ).
• Notions de théorie des langages (états, alphabet, transitions) — voir §1.
• Pour le pont de la tranche 3 : un CPython où automata-lib est installé (pip install automata-lib). Sans PYTHONNET_PYDLL ni le CPython Windows préconfiguré, la cellule du pont interroge le premier interpréteur (python3, puis python) qui importe automata, et en reprend la bibliothèque et le sys.path, environnement virtuel compris.

Durée estimée : 45 minutes

1. Introduction aux Automates

1.1 Qu’est-ce qu’un automate ?

Un automate est un modèle mathématique de calcul. Il se compose de :

Composant	Description	Notation
États	Configurations possibles	\(Q = \{q_0, q_1, ...\}\)
Alphabet	Symboles d’entrée	\(\Sigma = \{a, b, ...\}\)
Transitions	Règles de passage entre états	\(\delta : Q \times \Sigma \to Q\) (DFA) ou \(\to 2^Q\) (NFA)
État initial	Point de départ	\(q_0 \in Q\)
États finaux	États d’acceptation	\(F \subseteq Q\)

Un mot \(w = a_1 a_2 \dots a_n\) est accepté si, en partant de \(q_0\) et en suivant les transitions, on termine dans un état final.

1.2 DFA vs NFA

• DFA (Déterministe) : pour chaque couple (état, symbole), exactement une transition. \(\delta : Q \times \Sigma \to Q\).
• NFA (Non déterministe) : pour chaque couple (état, symbole), zéro, une ou plusieurs transitions. \(\delta : Q \times \Sigma \to 2^Q\). Un mot est accepté si au moins un chemin mène à un état final.

Les deux formalismes ont la même puissance d’expression (tout NFA est convertible en DFA équivalent), mais le NFA est souvent plus compact pour spécifier un langage.

1.3 Exemple introductif — Reconnaissance de “ab”

Soit le langage \(L = \{ w \in \{a,b\}^* : w \text{ contient le facteur } ab \}\). Construisons un NFA qui le reconnaît :

• \(q_0\) : état initial (on n’a pas encore vu de a candidat).
• \(q_1\) : on vient de voir un a (candidat au facteur ab).
• \(q_2\) : état final — on a vu ab.

Le non-déterminisme apparaît en \(q_0\) : sur a, on peut rester en \(q_0\) (pour chercher un ab plus loin) ou passer en \(q_1\) (tenter le facteur ici). C’est cette liberté qui rend le NFA plus concis que le DFA équivalent.

// Imports + structures communes : classes DFA et NFA ("hand-rolled").
// Conformement a la section 7 du notebook Python ("Notre approche alternative"),
// on construit les automates a la main : c'est l'objectif pedagogique meme.
using System;
using System.Collections.Generic;
using System.Linq;

// NFA : transitions (etat, symbole) -> ensemble d'etats (non-determinisme).
// Un meme (etat, symbole) peut pointer vers plusieurs etats cibles.
public sealed class NFA {
    public ISet<string> States { get; }
    public ISet<char> Alphabet { get; }
    // transitions[(q, a)] = ensemble d'etats cibles ; absent = ensemble vide.
    public IDictionary<(string, char), ISet<string>> Delta { get; }
    public string InitialState { get; }
    public ISet<string> FinalStates { get; }

    public NFA(ISet<string> states, ISet<char> alphabet,
               IDictionary<(string, char), ISet<string>> delta,
               string initial, ISet<string> finals) {
        States = states; Alphabet = alphabet; Delta = delta;
        InitialState = initial; FinalStates = finals;
    }

    // Etat-atteignable apres lecture d'un mot (union de tous les chemins NFA).
    public ISet<string> EpsilonClosureStep(ISet<string> current, char symbol) {
        var next = new HashSet<string>();
        foreach (var q in current) {
            if (Delta.TryGetValue((q, symbol), out var targets))
                next.UnionWith(targets);
        }
        return next;
    }

    // Accepte w ssi au moins un chemin mene a un etat final.
    public bool Accepts(string word) {
        ISet<string> current = new HashSet<string> { InitialState };
        foreach (var sym in word) {
            current = EpsilonClosureStep(current, sym);
            if (current.Count == 0) return false;
        }
        return current.Overlaps(FinalStates);
    }
}

// DFA : transitions (etat, symbole) -> exactement un etat (determinisme).
public sealed class DFA {
    public ISet<string> States { get; }
    public ISet<char> Alphabet { get; }
    public IDictionary<(string, char), string> Delta { get; }
    public string InitialState { get; }
    public ISet<string> FinalStates { get; }

    public DFA(ISet<string> states, ISet<char> alphabet,
               IDictionary<(string, char), string> delta,
               string initial, ISet<string> finals) {
        States = states; Alphabet = alphabet; Delta = delta;
        InitialState = initial; FinalStates = finals;
    }

    public bool Accepts(string word) {
        var current = InitialState;
        foreach (var sym in word) {
            if (!Delta.TryGetValue((current, sym), out var next))
                return false;  // aucune transition : rejet
            current = next;
        }
        return FinalStates.Contains(current);
    }

    // Complement : L^c = Sigma* \ L. On inverse les etats finaux.
    public DFA Complement() {
        var newFinals = new HashSet<string>(States);
        newFinals.ExceptWith(FinalStates);
        return new DFA(States, Alphabet, Delta, InitialState, newFinals);
    }
}

$@"Bibliotheques definies :
  - DFA  : automate deterministe (Delta : (etat, symbole) -> etat)
  - NFA  : automate non deterministe (Delta : (etat, symbole) -> ensemble d'etats)
Environnement pret.".Display();

The below script needs to be able to find the current output cell; this is an easy method to get it.

Bibliotheques definies :
  - DFA  : automate deterministe (Delta : (etat, symbole) -> etat)
  - NFA  : automate non deterministe (Delta : (etat, symbole) -> ensemble d'etats)
Environnement pret.

2. Automates Finis en C

2.2 Création d’un NFA — Reconnaissance de “ab”

Implémentons le NFA de la §1.3. Le non-déterminisme se traduit en C# par un ensemble de cibles pour la transition ('q0', 'a') = {'q0', 'q1'} : sur un a en \(q_0\), l’automate peut soit rester en \(q_0\) soit passer en \(q_1\).

// NFA pour reconnaissance du facteur "ab"
var nfaAb = new NFA(
    states: new HashSet<string> { "q0", "q1", "q2" },
    alphabet: new HashSet<char> { 'a', 'b' },
    delta: new Dictionary<(string, char), ISet<string>> {
        [("q0", 'a')] = new HashSet<string> { "q0", "q1" },  // reste q0 OU va q1
        [("q1", 'b')] = new HashSet<string> { "q2" },         // b apres a -> q2
        [("q2", 'a')] = new HashSet<string> { "q2" },         // puits q2
        [("q2", 'b')] = new HashSet<string> { "q2" },
    },
    initial: "q0",
    finals: new HashSet<string> { "q2" }
);

string[] testWords = { "ab", "aab", "abab", "a", "b", "ba", "aa" };
var sb = new System.Text.StringBuilder();
sb.AppendLine("NFA pour reconnaissance de 'ab'\n");
sb.AppendLine("Alphabet : { a, b }   Etat initial : q0   Etat final : q2\n");
sb.AppendLine($"{"Mot",-8} {"Accepte ?",-12}");
sb.AppendLine(new string('-', 20));
foreach (var w in testWords)
    sb.AppendLine($"{w,-8} {(nfaAb.Accepts(w) ? "OUI" : "non"),-12}");
sb.ToString().Display();

NFA pour reconnaissance de 'ab'

Alphabet : { a, b }   Etat initial : q0   Etat final : q2

Mot      Accepte ?   
--------------------
ab       OUI         
aab      OUI         
abab     OUI         
a        non         
b        non         
ba       non         
aa       non         

Interprétation : NFA pour reconnaissance de “ab”

• ab, aab, abab → acceptés : ils contiennent le facteur ab.
• a, b, ba, aa → rejetés : aucun ne contient ab.

Le non-déterminisme (deux cibles pour ('q0','a')) est résolu par l’exploration simultanée de tous les chemins (EpsilonClosureStep cumule les cibles). Le mot est accepté dès qu’un chemin se termine en \(q_2\).

2.3 Création d’un DFA — Mots avec un nombre pair de ‘a’

Le langage \(L = \{ w \in \{a,b\}^* : w \text{ contient un nombre pair de } a \}\) se code naturellement par un DFA à deux états : \(q_{even}\) (pair, final) et \(q_{odd}\) (impair). Sur a on change de parité, sur b on ne change pas.

// DFA pour nombre pair de 'a'
var dfaEvenA = new DFA(
    states: new HashSet<string> { "q_even", "q_odd" },
    alphabet: new HashSet<char> { 'a', 'b' },
    delta: new Dictionary<(string, char), string> {
        [("q_even", 'a')] = "q_odd",   // a change la parite
        [("q_even", 'b')] = "q_even",  // b non
        [("q_odd", 'a')]  = "q_even",
        [("q_odd", 'b')]  = "q_odd",
    },
    initial: "q_even",
    finals: new HashSet<string> { "q_even" }  // pair = accepte
);

string[] testWordsDfa = { "", "a", "aa", "aaa", "b", "ab", "aba", "bab" };
var sb2 = new System.Text.StringBuilder();
sb2.AppendLine("DFA pour nombre pair de 'a'\n");
sb2.AppendLine($"{"Mot",-8} {"#a",-4} {"Accepte ?",-12}");
sb2.AppendLine(new string('-', 26));
foreach (var w in testWordsDfa) {
    int na = w.Count(c => c == 'a');
    sb2.AppendLine($"{(w == "" ? "(vide)" : w),-8} {na,-4} {(dfaEvenA.Accepts(w) ? "OUI" : "non"),-12}");
}
sb2.ToString().Display();

DFA pour nombre pair de 'a'

Mot      #a   Accepte ?   
--------------------------
(vide)   0    OUI         
a        1    non         
aa       2    OUI         
aaa      3    non         
b        0    OUI         
ab       1    non         
aba      2    OUI         
bab      1    non         

Interprétation : DFA nombre pair de ‘a’

Le mot vide "" est accepté (zéro a, zéro est pair). aaa (3 a) est rejeté, aa (2) accepté. Ce DFA est minimal : deux états suffisent car seule la parité du compte de a importe.

Exercice : NFA pour mots se terminant par “ba”

Construisez un NFA reconnaissant le langage \(L = \{ w \in \{a,b\}^* : w \text{ se termine par } ba \}\).

Indices : - Étape 1 : trois états suffisent — un état “en cours” \(q_0\), un état “on vient de voir b” \(q_1\), et un état final \(q_2\) (“on vient de voir ba”). - Étape 2 : attention — sur b en \(q_1\), où retourner ? (le nouveau b peut être le début du suffixe ba final). - Étape 3 : testez avec ba, aba, bba (acceptés) et ab, aa, bb (rejetés).

// Exercice : NFA pour mots se terminant par "ba"
// TODO etudiant : construire le NFA et le stocker dans 'nfaBa'.
// Etape 1 : definir etats / alphabet / transitions / initial / finals
// Etape 2 : caser le non-determinisme sur 'b' (le b peut etre debut de suffixe OU non)
// Etape 3 : tester ba / aba / bba (acceptes) vs ab / aa / bb (rejetes)
NFA nfaBa = null;  // TODO etudiant : remplacer par la solution NFA
Console.WriteLine("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 langages reconnus par des automates sont clos par les opérations ensemblistes :

Opération	Langage	Construction sur DFA
Union \(L_1 \cup L_2\)	mots acceptés par \(L_1\) ou \(L_2\)	produit cartésien des états
Intersection \(L_1 \cap L_2\)	mots acceptés par \(L_1\) et \(L_2\)	produit cartésien, final = couple final×final
Complément \(\overline{L}\)	mots non acceptés	inverser les états finaux (DFA complet)

Le complément est immédiat sur un DFA complet (toutes les transitions définies) : on inverse simplement l’ensemble des états finaux (méthode DFA.Complement() ci-dessus). L’union et l’intersection passent par le produit cartésien de deux automates.

// Demonstration : complement du DFA "pair de a".
// L_complement = mots a nombre IMPAIR de 'a'.
var dfaOddA = dfaEvenA.Complement();

// Intersection par produit cartesien : (p,q) final ssi p final pour L1 ET q final pour L2.
// Illustration : L1 = "contient ab" (NFA -> on prend l'acceptation NFA directe)
//                L2 = "pair de a"    (DFA)
// On montre ici le complement + un produit cartesien simple : pair de a ET se termine par 'b'.
// (DFA_pair_a x DFA_termine_par_b : deux DFA -> produit direct)
var dfaEndsB = new DFA(
    states: new HashSet<string> { "p0", "p1" },  // p0 = ne termine pas par b (ou vide), p1 = termine par b
    alphabet: new HashSet<char> { 'a', 'b' },
    delta: new Dictionary<(string, char), string> {
        [("p0", 'a')] = "p0",
        [("p0", 'b')] = "p1",
        [("p1", 'a')] = "p0",
        [("p1", 'b')] = "p1",
    },
    initial: "p0",
    finals: new HashSet<string> { "p1" }
);

// Produit cartesien DFA_pair_a x DFA_ends_b : (etat_pair, etat_ends)
var prodStates = new HashSet<string>();
var prodDelta = new Dictionary<(string, char), string>();
foreach (var s1 in dfaEvenA.States)
    foreach (var s2 in dfaEndsB.States) {
        prodStates.Add($"{s1}|{s2}");
        foreach (var sym in dfaEvenA.Alphabet)
            prodDelta[($"{s1}|{s2}", sym)] = $"{dfaEvenA.Delta[(s1, sym)]}|{dfaEndsB.Delta[(s2, sym)]}";
    }
// Final ssi les deux composantes sont finales.
var prodFinals = new HashSet<string>(
    from s1 in dfaEvenA.FinalStates
    from s2 in dfaEndsB.FinalStates
    select $"{s1}|{s2}"
);
var dfaInter = new DFA(prodStates, dfaEvenA.Alphabet, prodDelta, $"q_even|p0", prodFinals);

string[] testWordsOp = { "b", "ab", "bb", "aab", "bab", "aa", "aabab" };
var sb3 = new System.Text.StringBuilder();
sb3.AppendLine("Operations sur les automates\n");
sb3.AppendLine("L1 = 'nombre pair de a'   L2 = 'se termine par b'   L1 n L2\n");
sb3.AppendLine($"{"Mot",-8} {"L1",-5} {"L2",-5} {"L1nL2",-7}");
sb3.AppendLine(new string('-', 28));
foreach (var w in testWordsOp) {
    bool l1 = dfaEvenA.Accepts(w), l2 = dfaEndsB.Accepts(w), lint = dfaInter.Accepts(w);
    sb3.AppendLine($"{(w == "" ? "(vide)" : w),-8} {(l1 ? "OUI" : "non"),-5} {(l2 ? "OUI" : "non"),-5} {(lint ? "OUI" : "non"),-7}");
}
sb3.AppendLine("\nVerification coherence : L1 n L2 == L1 logique AND L2 sur chaque mot.");
bool coherent = testWordsOp.All(w => dfaInter.Accepts(w) == (dfaEvenA.Accepts(w) && dfaEndsB.Accepts(w)));
sb3.AppendLine($"Coherence produit cartesien : {(coherent ? "OK (intersection = AND logique)" : "ECHEC")}");
sb3.ToString().Display();

Operations sur les automates

L1 = 'nombre pair de a'   L2 = 'se termine par b'   L1 n L2

Mot      L1    L2    L1nL2  
----------------------------
b        OUI   OUI   OUI    
ab       non   OUI   non    
bb       OUI   OUI   OUI    
aab      OUI   OUI   OUI    
bab      non   OUI   non    
aa       OUI   non   non    
aabab    non   OUI   non    

Verification coherence : L1 n L2 == L1 logique AND L2 sur chaque mot.
Coherence produit cartesien : OK (intersection = AND logique)

Interprétation : opérations sur les automates

• L’intersection par produit cartésien donne exactement le ET logique mot à mot (vérifié : Coherence OK). C’est la construction standard de fermeture des langages réguliers.
• Le complément (dfaEvenA.Complement() → nombres impairs de a) ne fonctionne que parce que le DFA est complet (toute transition définie). Sur un NFA, il faudrait d’abord déterminiser.
• Ces opérations sont la base de la vérification de propriétés (§5 du notebook Python) : on construit l’automate du système, celui de la propriété, et on teste l’intersection / le complément.

2.5 Limite des automates finis classiques

Un automate fini ne peut pas compter arbitrairement : il ne peut reconnaître ni \(\{a^n b^n : n \geq 0\}\) (comptage imbriqué), ni \(\{w : w \text{ est un carré}\}\). Plus précisément, un DFA à \(k\) états ne peut pas distinguer deux mots qui passent par le même état après un préfixe assez long (pumping lemma). C’est cette limite qui motive les automates symboliques : au lieu d’énumérer des symboles concrets, on manipule des prédicats sur un alphabet potentiellement infini (entiers, par exemple). Ce sera l’objet de la tranche 2 (avec Microsoft.Z3).

---

Tranche 3 (#10382) : le moteur réel automata-lib via le pont PythonNet

La Tranche 1 construit les automates à la main — c’est l’objectif pédagogique (cf. §7 du jumeau Python : il n’existe pas de librairie .NET équivalente à automata-lib qui soit maintenue et didactique). Cette tranche referme la boucle d’une autre façon : le C# invoque le même moteur que le jumeau Python — automata-lib 9.2.0 (DFA/NFA, déterminisation, minimisation, opérations ensemblistes) — via le pont PythonNet 3.1.0 qui héberge CPython dans le processus .NET (même pattern que pyspiel GT-13 et mealpy Sudoku-05).

Une seule cellule de pont, trois mouvements (le bloc GIL vit dans une unique soumission — le pattern éprouvé de Sudoku-05/GT-13) :

1. Rejouer les deux expériences canoniques du jumeau Python (NFA de « ab », DFA du nombre pair de « a ») sur les mêmes vecteurs de tests — les verdicts d’acceptation doivent être identiques aux outputs du jumeau.
2. Le complément par le moteur : dfa.complement() du moteur, vérifié par inversion exacte des verdicts sur les 8 mots du jumeau.
3. Les opérations que la Tranche 1 n’implémente pas : déterminisation from_nfa, minimisation minify (Myhill-Nerode), équivalence par symmetric_difference vide, union/intersection natives — et un contraste mesuré qui précise le langage réellement reconnu par le NFA.

#r "nuget: pythonnet,3.1.0"
using Python.Runtime;
using System.IO;

// === Tranche 3 (#10382) : pont PythonNet -> automata-lib 9.2.0, LE MÊME MOTEUR que le jumeau Python ===
// Pattern de Sudoku-5 / GT-13 : CPython hébergé dans le kernel .NET Interactive, bloc GIL unique,
// tout le calcul côté Python, les résultats reviennent par Get<string>.
string[] dllCandidates =
{
    Environment.GetEnvironmentVariable("PYTHONNET_PYDLL"),
    @"C:\ProgramData\miniconda3\python313.dll",
};
// Repli portable (Linux, macOS, ou Windows sans le CPython ci-dessus) : le premier
// interpreteur (python3, puis python) qui importe le module fournit sa bibliotheque
// partagee, son prefixe et son sys.path, environnement virtuel compris.
static void InitPythonFromInterpreter(string module)
{
    const string probe =
        "import importlib, json, os, sys, sysconfig\n" +
        "importlib.import_module(sys.argv[1])\n" +
        "v = sysconfig.get_config_var; lib = v('LIBDIR') or ''; mm = sys.version_info[:2]\n" +
        "c = [os.path.join(lib, n) for n in (v('INSTSONAME'), v('LDLIBRARY')) if n]\n" +
        "c += [os.path.join(d, 'libpython%d.%d.dylib' % mm) for d in (lib, os.path.join(sys.base_prefix, 'lib'))]\n" +
        "c.append(os.path.join(sys.base_prefix, 'python%d%d.dll' % mm))\n" +
        "dll = next((p for p in c if os.path.isfile(p)), '')\n" +
        "print(json.dumps({'dll': dll, 'home': sys.base_prefix, 'path': [p for p in sys.path if p]}))\n";
    foreach (var exe in new[] { "python3", "python" })
    {
        try
        {
            var psi = new System.Diagnostics.ProcessStartInfo(exe)
            { RedirectStandardOutput = true, RedirectStandardError = true, UseShellExecute = false };
            foreach (var arg in new[] { "-c", probe, module }) psi.ArgumentList.Add(arg);
            using var p = System.Diagnostics.Process.Start(psi);
            var stderr = p.StandardError.ReadToEndAsync();
            string json = p.StandardOutput.ReadToEnd();
            p.WaitForExit();
            if (p.ExitCode != 0) continue;
            var info = System.Text.Json.JsonDocument.Parse(json).RootElement;
            string dll = info.GetProperty("dll").GetString();
            if (string.IsNullOrEmpty(dll)) continue;
            Runtime.PythonDLL = dll;
            PythonEngine.PythonHome = info.GetProperty("home").GetString();
            PythonEngine.Initialize();
            using (Py.GIL())
            {
                var path = info.GetProperty("path").EnumerateArray()
                    .Select(e => (PyObject)new PyString(e.GetString())).ToArray();
                Py.Import("sys").SetAttr("path", new PyList(path));
            }
            return;
        }
        catch (System.ComponentModel.Win32Exception) { }   // interpreteur absent du PATH
    }
    throw new System.IO.FileNotFoundException(
        $"Aucun CPython n'importe {module} : l'installer (pip install), ou definir PYTHONNET_PYDLL.");
}

string pyDll = dllCandidates.FirstOrDefault(File.Exists);
if (pyDll != null)
{
    string pyDir = Path.GetDirectoryName(pyDll);
    Environment.SetEnvironmentVariable(
        "PATH", pyDir + Path.PathSeparator + Environment.GetEnvironmentVariable("PATH"));
    Runtime.PythonDLL = pyDll;
    PythonEngine.Initialize();
}
else InitPythonFromInterpreter("automata");
Console.WriteLine($"Pont PythonNet : CPython {PythonEngine.Version} -> automata-lib (même moteur que le jumeau Python)");
Console.WriteLine();

using (Py.GIL())
{
    dynamic scope = Py.CreateScope();
    scope.Exec(@"
from automata.fa.nfa import NFA
from automata.fa.dfa import DFA

# ---------- Mouvement 1 : l'expérience NFA ""ab"" du jumeau Python, rejouée sur le même moteur ----------
nfa_ab = NFA(
    states={'q0', 'q1', 'q2'}, input_symbols={'a', 'b'},
    transitions={'q0': {'a': {'q0', 'q1'}}, 'q1': {'b': {'q2'}}, 'q2': {'a': {'q2'}, 'b': {'q2'}}},
    initial_state='q0', final_states={'q2'})

words1 = ['ab', 'aab', 'abab', 'a', 'b', 'ba', 'aa']
lines1 = ['Mouvement 1 : NFA de ""ab"" (jumeau Python) rejoué via le moteur']
lines1.append('Vecteur de tests (identique au jumeau) :')
for w in words1:
    lines1.append('  %-6s -> %s' % (repr(w), 'Accepté' if nfa_ab.accepts_input(w) else 'Rejeté'))
import importlib.metadata as md
lines1.append('moteur : automata-lib %s sous CPython' % md.version('automata-lib'))
summary1 = chr(10).join(lines1)

# ---------- Mouvement 2 : DFA nombre pair de a + complément PAR LE MOTEUR ----------
dfa_even_a = DFA(
    states={'q_even', 'q_odd'}, input_symbols={'a', 'b'},
    transitions={'q_even': {'a': 'q_odd', 'b': 'q_even'}, 'q_odd': {'a': 'q_even', 'b': 'q_odd'}},
    initial_state='q_even', final_states={'q_even'})

words2 = ['', 'a', 'aa', 'aaa', 'b', 'ab', 'aba', 'bab']
verdicts = {w: dfa_even_a.accepts_input(w) for w in words2}
comp = dfa_even_a.complement()
inverses = {w: comp.accepts_input(w) for w in words2}
ok = all(verdicts[w] != inverses[w] for w in words2)
lines2 = ['Mouvement 2 : DFA nombre pair de a (jumeau Python) + complement() du moteur']
lines2.append('Vecteur de tests (identique au jumeau) :')
for w in words2:
    lines2.append('  %-6s -> %s' % (repr(w), 'Pair' if verdicts[w] else 'Impair'))
lines2.append('complement() : inversion vérifiée sur les %d mots -> %s' % (len(words2), ok))
summary2 = chr(10).join(lines2)

# ---------- Mouvement 3 : les opérations que la Tranche 1 from-scratch n'implémente pas ----------
det = DFA.from_nfa(nfa_ab)
mini = det.minify()
sd = mini.symmetric_difference(det)
preservation = sd.isempty()

u = dfa_even_a.union(mini)
i_ = dfa_even_a.intersection(mini)
temoins = [('ab', 'pair? non | dans le langage? oui'), ('aa', 'pair? oui | dans le langage? non'), ('ba', 'pair? non | dans le langage? non'), ('a', 'pair? non | dans le langage? non')]

sub = DFA.from_substring(input_symbols={'a','b'}, substring='ab')
sd2 = mini.symmetric_difference(sub)
equiv_contient_ab = sd2.isempty()

lines3 = ['Mouvement 3 : opérations natives du moteur (Prong B)']
lines3.append('from_nfa : NFA %d états -> DFA %d états ; minify -> %d états' % (len(nfa_ab.states), len(det.states), len(mini.states)))
lines3.append('minify préserve le langage (symmetric_difference vide) : %s' % preservation)
lines3.append('')
lines3.append('union / intersection natives (témoins) :')
for w, attendu in temoins:
    lines3.append('  %-4s union=%-5s intersection=%-5s  (%s)' % (repr(w), u.accepts_input(w), i_.accepts_input(w), attendu))
lines3.append('')
lines3.append('contraste mesuré : from_substring(ab) vs le NFA -- langages équivalents = %s' % equiv_contient_ab)
lines3.append('  témoin bab : from_substring accepte=%s, NFA accepte=%s' % (sub.accepts_input('bab'), nfa_ab.accepts_input('bab')))
lines3.append('  -> le NFA exige au moins un a avant le premier b : son langage est a+ . b . (a|b)*, pas contient-ab')
summary3 = chr(10).join(lines3)
summary4 = 'Objets vivants dans le scope moteur : nfa_ab.accepts_input(aab) = %s, accepts_input(bab) = %s' % (nfa_ab.accepts_input('aab'), nfa_ab.accepts_input('bab'))");
    Console.WriteLine(scope.Get<string>("summary1"));
    Console.WriteLine();
    Console.WriteLine(scope.Get<string>("summary2"));
    Console.WriteLine();
    Console.WriteLine(scope.Get<string>("summary3"));
    Console.WriteLine();
    Console.WriteLine(scope.Get<string>("summary4"));
    Console.WriteLine("--> le C# pilote le moteur par l'API du scope (Exec + Get<string>) : le pont est une API, pas un eval aveugle.");
}
PythonEngine.Shutdown();

Installed Packages

• pythonnet, 3.1.0

Pont PythonNet : CPython 3.11.15 (main, Mar  3 2026, 09:26:23) [GCC 13.3.0] -> automata-lib (même moteur que le jumeau Python)

Mouvement 1 : NFA de "ab" (jumeau Python) rejoué via le moteur
Vecteur de tests (identique au jumeau) :
  'ab'   -> Accepté
  'aab'  -> Accepté
  'abab' -> Accepté
  'a'    -> Rejeté
  'b'    -> Rejeté
  'ba'   -> Rejeté
  'aa'   -> Rejeté
moteur : automata-lib 9.2.0 sous CPython

Mouvement 2 : DFA nombre pair de a (jumeau Python) + complement() du moteur
Vecteur de tests (identique au jumeau) :
  ''     -> Pair
  'a'    -> Impair
  'aa'   -> Pair
  'aaa'  -> Impair
  'b'    -> Pair
  'ab'   -> Impair
  'aba'  -> Pair
  'bab'  -> Impair
complement() : inversion vérifiée sur les 8 mots -> True

Mouvement 3 : opérations natives du moteur (Prong B)
from_nfa : NFA 3 états -> DFA 3 états ; minify -> 3 états
minify préserve le langage (symmetric_difference vide) : True

union / intersection natives (témoins) :
  'ab' union=True  intersection=False  (pair? non | dans le langage? oui)
  'aa' union=True  intersection=False  (pair? oui | dans le langage? non)
  'ba' union=False intersection=False  (pair? non | dans le langage? non)
  'a'  union=False intersection=False  (pair? non | dans le langage? non)

contraste mesuré : from_substring(ab) vs le NFA -- langages équivalents = False
  témoin bab : from_substring accepte=True, NFA accepte=False
  -> le NFA exige au moins un a avant le premier b : son langage est a+ . b . (a|b)*, pas contient-ab

Objets vivants dans le scope moteur : nfa_ab.accepts_input(aab) = True, accepts_input(bab) = False
--> le C# pilote le moteur par l'API du scope (Exec + Get<string>) : le pont est une API, pas un eval aveugle.

Interprétation : le moteur sous le pont

• Les deux vecteurs de tests du jumeau Python sont reproduits à l’identique par le même moteur invoqué depuis C# — la preuve de parité croisée vit dans les outputs committés des deux jumeaux.
• complement() du moteur inverse exactement les 8 verdicts du DFA pair — la Tranche 1 implémentait le complément à la main (produit cartésien), ici c’est une méthode du moteur.
• from_nfa (déterminisation par ensemble d’états) puis minify (Myhill-Nerode) ramènent le NFA à 3 états, et le moteur prouve la préservation du langage : symmetric_difference vide.
• Le contraste final est une mesure, pas une intuition : le langage du NFA est a⁺·b·(a|b)* (au moins un a avant le premier b), pas « contient ab » — le témoin bab l’établit.
• Verdict SOTA (Prong A) : SOTA-OK — le vrai moteur (automata-lib 9.2.0, celui du jumeau Python) est installé et invoqué via PythonNet 3.1.0 ; les sorties committées sont ses sorties réelles. La parité de la paire passe de surface à pont-vivant.

---

3. Introduction aux Automates Symboliques

3.1 Définition

Un automate symbolique généralise l’automate fini en remplaçant les symboles concrets des transitions par des prédicats logiques. Au lieu d’étiqueter une transition par 'a' ou 'b', on l’étiquette par une formule du type x >= 10 AND x <= 100 — un prédicat sur une variable d’entrée x.

3.2 Alphabet infini ou très grand

L’intérêt apparaît avec un alphabet infini (les entiers \(\mathbb{Z}\)) ou très grand : énumérer une transition par valeur est impossible. Un automate symbolique manipule directement l’ensemble infini via ses propriétés (parité, intervalle, divisibilité) plutôt que par énumeration.

3.3 Prédicats comme formules

Un prédicat devient une formule logique qu’un solveur SMT (Satisfiability Modulo Théories) peut vérifier. C’est le rôle de Z3 : étant donné un prédicat \(P(x)\) et une valeur \(v\), Z3 décide si \(P(v)\) est vrai (sat) ou faux (unsat). On utilise le solveur comme un « oracle de transition ».

3.4 Comparaison Automate Fini vs Symbolique

Aspect	Automate fini (§2)	Automate symbolique (§4)
Alphabet	fini \(\Sigma = \{a, b, ...\}\)	infini (\(\mathbb{Z}\)) ou très grand
Transitions	symbole concret ('q0','a')	prédicat x >= 10 AND x <= 100
Décision	lookup dans Dictionary	solveur SMT (Z3) : sat/unsat
Cas d’usage	mots sur \(\{a,b\}\)	intervalles, parité, propriétés arithmétiques

4. Automates Symboliques avec Z3

4.1 Installation et importation de Microsoft.Z3

Z3 est le solveur SMT de Microsoft Research. En .NET, on l’obtient via le package NuGet Microsoft.Z3 (version 4.12.2, dernière publiée). La cellule suivante restore le package et importe l’espace de noms.

Sous Linux et sous macOS Apple Silicon, ce package ne contient pas la bibliothèque native de Z3 : la cellule charge alors celle du paquet Python z3-solver, par Z3NativeLoader.cs de la série Z3-API (voir l’en-tête du fichier). Pour utiliser la même version de Z3 que le package NuGet : pip install z3-solver==4.12.2.0.

// Restoration du package NuGet Microsoft.Z3 (solveur SOT de Microsoft Research).
// Version 4.12.2 = derniere publiee sur NuGet (4.13+ n'existe pas encore en package).
#r "nuget: Microsoft.Z3, 4.12.2"
#load "../../SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs"
using Microsoft.Z3;
using System.Text;

// Bibliotheque native de Z3 hors Windows et macOS Intel (voir Z3NativeLoader.cs)
Z3NativeLoader.Register(typeof(Context).Assembly);

var ctx = new Context();
$@"Z3 importe avec succes.
Package NuGet : Microsoft.Z3 4.12.2 (solveur SMT SOTA de Microsoft Research)
Contexte SMT cree.

Types de variables disponibles :
  - IntExpr  : Entiers mathematiques (infinis, via MkIntConst)
  - BitVecExpr : Vecteurs de bits (taille fixe)
  - BoolExpr : Booleens (formules logiques)
  - RealExpr : Nombres reels".Display();

Installed Packages

• Microsoft.Z3, 4.12.2

Z3 importe avec succes.
Package NuGet : Microsoft.Z3 4.12.2 (solveur SMT SOTA de Microsoft Research)
Contexte SMT cree.

Types de variables disponibles :
  - IntExpr  : Entiers mathematiques (infinis, via MkIntConst)
  - BitVecExpr : Vecteurs de bits (taille fixe)
  - BoolExpr : Booleens (formules logiques)
  - RealExpr : Nombres reels

4.2 Prédicats Symboliques avec Z3

Construisons des prédicats sur une variable entière x. Z3 représente chaque prédicat comme un arbre de syntaxe abstraite (BoolExpr) — on peut le composer (MkAnd, MkOr, MkNot) et le vérifier contre une valeur via un solver.

// Predicats symboliques avec Z3 sur une variable entiere x.
var x = ctx.MkIntConst("x");

var preds = new (BoolExpr expr, string desc)[] {
    (ctx.MkGt(x, ctx.MkInt(0)),   "x > 0"),
    (ctx.MkLt(x, ctx.MkInt(100)), "x < 100"),
    (ctx.MkGe(x, ctx.MkInt(10)),  "x >= 10"),
    (ctx.MkLe(x, ctx.MkInt(50)),  "x <= 50"),
    (ctx.MkEq(ctx.MkMod(x, ctx.MkInt(2)), ctx.MkInt(0)), "x est pair (x mod 2 = 0)"),
};

var sbP = new StringBuilder();
sbP.AppendLine("Predicats symboliques avec Z3\n");
sbP.AppendLine($"Variable : {x}  (sort : {x.Sort})\n");
sbP.AppendLine("Predicats simples :");
foreach (var (expr, desc) in preds)
    sbP.AppendLine($"  {desc,-30} -> {expr}");

// Predicats composes
var inRange = ctx.MkAnd(ctx.MkGe(x, ctx.MkInt(10)), ctx.MkLe(x, ctx.MkInt(100)));
var outRange = ctx.MkOr(ctx.MkLt(x, ctx.MkInt(0)), ctx.MkGt(x, ctx.MkInt(100)));
sbP.AppendLine("\nPredicats composes :");
sbP.AppendLine($"  10 <= x <= 100   : {inRange}");
sbP.AppendLine($"  x < 0 ou x > 100 : {outRange}");

// Evaluation d'un predicat contre une valeur : sat = vrai, unsat = faux.
sbP.AppendLine("\nEvaluation de (10 <= x <= 100) sur des valeurs :");
foreach (int v in new[] { -5, 0, 10, 50, 100, 150 }) {
    var solver = ctx.MkSolver();
    solver.Add(inRange);
    solver.Add(ctx.MkEq(x, ctx.MkInt(v)));
    var st = solver.Check();
    sbP.AppendLine($"  x = {v,-4} -> {st}  {(st == Status.SATISFIABLE ? "(accepte)" : "(rejete)")}");
}
sbP.ToString().Display();

Predicats symboliques avec Z3

Variable : x  (sort : Int)

Predicats simples :
  x > 0                          -> (> x 0)
  x < 100                        -> (< x 100)
  x >= 10                        -> (>= x 10)
  x <= 50                        -> (<= x 50)
  x est pair (x mod 2 = 0)       -> (= (mod x 2) 0)

Predicats composes :
  10 <= x <= 100   : (and (>= x 10) (<= x 100))
  x < 0 ou x > 100 : (or (< x 0) (> x 100))

Evaluation de (10 <= x <= 100) sur des valeurs :
  x = -5   -> UNSATISFIABLE  (rejete)
  x = 0    -> UNSATISFIABLE  (rejete)
  x = 10   -> SATISFIABLE  (accepte)
  x = 50   -> SATISFIABLE  (accepte)
  x = 100  -> SATISFIABLE  (accepte)
  x = 150  -> UNSATISFIABLE  (rejete)

Interprétation : Prédicats symboliques avec Z3

Chaque prédicat est un BoolExpr — un arbre, pas un booléen. Pour savoir s’il est vrai pour une valeur donnée, on ajoute au solver le prédicat et la contrainte x == v, puis on appelle solver.Check() : TRUE (sat) = le prédicat est satisfait, FALSE (unsat) = non. C’est exactement le mécanisme qu’un automate symbolique utilisera pour décider les transitions.

4.3 Classe SymbolicAutomaton

Portons la classe SymbolicAutomaton du notebook Python. Chaque transition est étiquetée par un prédicat Z3 (fabriqué à partir du Context et de la variable d’entrée x). La méthode Accepts(input) résout, pour chaque transition sortante de l’état courant, si son prédicat est satisfait par input — si oui, on passe à l’état cible (et on s’arrête si c’est un final).

Choix de conception C# : les prédicats Z3 sont stockés comme des Func<Context, IntExpr, BoolExpr> (des fabriques), reconstruits à chaque appel de Accepts. Cela évite le couplage fragile entre un BoolExpr et son Context d’origine, et permet de réutiliser la même fabrique pour toutes les valeurs testées.

// Automate symbolique : transitions etiquetees par des predicats Z3 (fabriques).
// Une fabrique (Context, x) -> BoolExpr est reconstruite a chaque Accepts, ce qui evite
// le couplage entre un BoolExpr et son Context d'origine (piage classique Z3 .NET).
public sealed class SymbolicAutomaton {
    private readonly Context _ctx;
    public ISet<string> States { get; }
    // transitions : (source, cible, fabrique de predicat)
    public List<(string From, string To, Func<Context, IntExpr, BoolExpr> Pred)> Transitions { get; }
    public string InitialState { get; private set; }
    public ISet<string> FinalStates { get; }

    public SymbolicAutomaton(Context ctx) {
        _ctx = ctx; States = new HashSet<string>(); Transitions = new();
        FinalStates = new HashSet<string>(); InitialState = null;
    }

    public SymbolicAutomaton AddState(string state, bool isInitial = false, bool isFinal = false) {
        States.Add(state);
        if (isInitial) {
            if (InitialState != null) throw new InvalidOperationException($"Etat initial deja defini : {InitialState}");
            InitialState = state;
        }
        if (isFinal) FinalStates.Add(state);
        return this;
    }

    public SymbolicAutomaton AddTransition(string from, string to, Func<Context, IntExpr, BoolExpr> pred) {
        if (!States.Contains(from)) throw new InvalidOperationException($"Etat source inconnu : {from}");
        if (!States.Contains(to)) throw new InvalidOperationException($"Etat destination inconnu : {to}");
        Transitions.Add((from, to, pred));
        return this;
    }

    // Accepte input ssi un chemin d'etats (chaque transition validant input via Z3) atteint un final.
    public bool Accepts(int input, string variableName = "x") {
        if (InitialState == null) throw new InvalidOperationException("Pas d'etat initial defini");
        var current = InitialState;
        // Chemin lineaire : on suit la premiere transition dont le predicat est sat pour input.
        // (Les exemples de la serie sont des automates en chaine ; le cas NFA-symbolique general
        // suivrait tous les chemins comme le NFA de la tranche 1.)
        for (int step = 0; step < Transitions.Count + 1; step++) {
            if (FinalStates.Contains(current)) return true;
            bool advanced = false;
            foreach (var (f, t, pred) in Transitions) {
                if (f != current) continue;
                var xx = _ctx.MkIntConst(variableName);
                var solver = _ctx.MkSolver();
                solver.Add(pred(_ctx, xx));
                solver.Add(_ctx.MkEq(xx, _ctx.MkInt(input)));
                if (solver.Check() == Status.SATISFIABLE) {
                    current = t; advanced = true; break;
                }
            }
            if (!advanced) return false;  // aucune transition sortante valide : bloque
        }
        return FinalStates.Contains(current);
    }
}

"Classe SymbolicAutomaton definie (transitions = predicats Z3, Accepts via solveur SMT).".Display();

Classe SymbolicAutomaton definie (transitions = predicats Z3, Accepts via solveur SMT).

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

Construisons l’automate à 2 états qui accepte les entiers de l’intervalle \([10, 100]\). Transition unique \(q_0 \to q_1\) étiquetée par le prédicat 10 <= x <= 100.

// Automate symbolique pour l'intervalle [10, 100]
var autoRange = new SymbolicAutomaton(ctx)
    .AddState("q0", isInitial: true)
    .AddState("q1", isFinal: true)
    .AddTransition("q0", "q1",
        (c, x) => c.MkAnd(c.MkGe(x, c.MkInt(10)), c.MkLe(x, c.MkInt(100))));

var sbR = new StringBuilder();
sbR.AppendLine("Automate symbolique pour l'intervalle [10, 100]");
sbR.AppendLine("  q0 --[10 <= x <= 100]--> q1 (final)\n");
sbR.AppendLine($"{"Valeur",-8} {"Accepte ?",-12}");
sbR.AppendLine(new string('-', 22));
foreach (int v in new[] { -10, 0, 9, 10, 50, 100, 101, 500 })
    sbR.AppendLine($"{v,-8} {(autoRange.Accepts(v) ? "OUI" : "non"),-12}");
sbR.ToString().Display();

Automate symbolique pour l'intervalle [10, 100]
  q0 --[10 <= x <= 100]--> q1 (final)

Valeur   Accepte ?   
----------------------
-10      non         
0        non         
9        non         
10       OUI         
50       OUI         
100      OUI         
101      non         
500      non         

Interprétation : Automate de Plage

• 10, 50, 100 → acceptés (bornes incluses, <= et >=).
• 9, 101, 0, -10, 500 → rejetés (hors intervalle).

Le solveur Z3 a décidé chaque transition en vérifiant la satisfiabilité de (10 <= x <= 100) AND (x == v) — l’automate n’énumère jamais l’ensemble infini des entiers.

4.5 Exemple 2 : Automate pour Nombres Pairs

L’automate « nombre pair » (\(x \bmod 2 = 0\)) se construit en chaînanant deux prédicats : \(q_0 \to q_1\) sur x >= 0 (positif), puis \(q_1 \to q_2\) sur x mod 2 = 0 (pair). L’état final \(q_2\) exige donc à la fois la positivité et la parité.

// Automate symbolique pour nombres pairs positifs
var autoEven = new SymbolicAutomaton(ctx)
    .AddState("q0", isInitial: true)
    .AddState("q1")
    .AddState("q2", isFinal: true)
    .AddTransition("q0", "q1", (c, x) => c.MkGe(x, c.MkInt(0)))
    .AddTransition("q1", "q2", (c, x) => c.MkEq(c.MkMod(x, c.MkInt(2)), c.MkInt(0)));

var sbE = new StringBuilder();
sbE.AppendLine("Automate symbolique : nombres pairs POSITIFS");
sbE.AppendLine("  q0 --[x >= 0]--> q1 --[x mod 2 = 0]--> q2 (final)\n");
sbE.AppendLine($"{"Valeur",-8} {"Accepte ?",-12}");
sbE.AppendLine(new string('-', 22));
foreach (int v in new[] { -4, -2, 0, 1, 2, 3, 4, 7, 8, 100, 101 })
    sbE.AppendLine($"{v,-8} {(autoEven.Accepts(v) ? "OUI" : "non"),-12}");
sbE.ToString().Display();

Automate symbolique : nombres pairs POSITIFS
  q0 --[x >= 0]--> q1 --[x mod 2 = 0]--> q2 (final)

Valeur   Accepte ?   
----------------------
-4       non         
-2       non         
0        OUI         
1        non         
2        OUI         
3        non         
4        OUI         
7        non         
8        OUI         
100      OUI         
101      non         

Interprétation : Nombres pairs

• 0, 2, 4, 8, 100 → acceptés (positifs et pairs).
• -2, -4 → rejetés : pairs mais négatifs (échouent le premier prédicat x >= 0).
• 1, 3, 7, 101 → rejetés : positifs mais impairs.

Cet exemple montre la composition de prédicats le long d’un chemin — l’équivalent symbolique d’un DFA à plusieurs états, mais où chaque transition exprime une propriété arithmétique.

4.6 Exemple 3 : Automate pour Nombres Positifs Multiples de 5

Même structure, mais le prédicat final est x mod 5 = 0. Démontre que l’automate symbolique gère n’importe quelle propriété décidable par Z3 — pas seulement les intervalles.

// Automate symbolique : multiples de 5 positifs
var autoMult5 = new SymbolicAutomaton(ctx)
    .AddState("q0", isInitial: true)
    .AddState("q1")
    .AddState("q2", isFinal: true)
    .AddTransition("q0", "q1", (c, x) => c.MkGt(x, c.MkInt(0)))  // strictement positif
    .AddTransition("q1", "q2", (c, x) => c.MkEq(c.MkMod(x, c.MkInt(5)), c.MkInt(0)));

var sbM = new StringBuilder();
sbM.AppendLine("Automate symbolique : multiples de 5 STRICTEMENT positifs");
sbM.AppendLine("  q0 --[x > 0]--> q1 --[x mod 5 = 0]--> q2 (final)\n");
sbM.AppendLine($"{"Valeur",-8} {"Accepte ?",-12}");
sbM.AppendLine(new string('-', 22));
foreach (int v in new[] { -10, 0, 3, 5, 10, 12, 15, 20, 23, 100 })
    sbM.AppendLine($"{v,-8} {(autoMult5.Accepts(v) ? "OUI" : "non"),-12}");
sbM.ToString().Display();

Automate symbolique : multiples de 5 STRICTEMENT positifs
  q0 --[x > 0]--> q1 --[x mod 5 = 0]--> q2 (final)

Valeur   Accepte ?   
----------------------
-10      non         
0        non         
3        non         
5        OUI         
10       OUI         
12       non         
15       OUI         
20       OUI         
23       non         
100      OUI         

Exercice : Automate pour multiples de 7 dans un intervalle

Construisez un automate symbolique à 3 états qui accepte les entiers \(x\) tels que \(20 \le x \le 100\) et \(x\) est multiple de 7 (i.e. \(x \bmod 7 = 0\)).

Indices : - Étape 1 : trois états en chaîne — \(q_0\) (initial), \(q_1\) (intermédiaire), \(q_2\) (final). - Étape 2 : transition \(q_0 \to q_1\) sur le prédicat d’intervalle 20 <= x <= 100 (MkAnd(MkGe(x, 20), MkLe(x, 100))). - Étape 3 : transition \(q_1 \to q_2\) sur la divisibilité par 7 (MkEq(MkMod(x, 7), 0)). - Étape 4 : testez — 21, 35, 49, 70, 98 doivent être acceptés ; 14, 20, 25, 105 rejetés.

// Exercice : automate pour multiples de 7 dans [20, 100]
// TODO etudiant : construire l'automate 'autoMult7' avec la classe SymbolicAutomaton.
// Etape 1 : 3 etats en chaine (q0 initial, q1 intermediaire, q2 final)
// Etape 2 : q0 -> q1 sur (20 <= x <= 100)
// Etape 3 : q1 -> q2 sur (x mod 7 = 0)
// Etape 4 : tester 21/35/49/70/98 (acceptes) vs 14/20/25/105 (rejetes)
SymbolicAutomaton autoMult7 = null;  // TODO etudiant : remplacer par la solution
Console.WriteLine("Exercice a completer : automate pour multiples de 7 dans [20, 100]");

Exercice a completer : automate pour multiples de 7 dans [20, 100]

4.7 Opérations sur Automates Symboliques

Comme les automates finis, les automates symboliques sont clos par opérations ensemblistes. La clé : les prédicats Z3 se combinent avec MkAnd (intersection), MkOr (union), MkNot (complément). On peut ainsi construire un automate « multiple de 3 ou multiple de 5 » sans réécrire la logique de divisibilité — juste en combinant les prédicats.

4.8 Exemple d’Opérations

Vérifions par solver qu’un entier satisfait « multiple de 3 ou multiple de 5 » pour quelques valeurs — l’approche symbolique évite d’énumérer les multiples.

// Operations sur predicats : union (OR) de divisibilites.
var xV = ctx.MkIntConst("x");
var mult3 = ctx.MkEq(ctx.MkMod(xV, ctx.MkInt(3)), ctx.MkInt(0));
var mult5 = ctx.MkEq(ctx.MkMod(xV, ctx.MkInt(5)), ctx.MkInt(0));
var mult3or5 = ctx.MkOr(mult3, mult5);   // union
var mult3and5 = ctx.MkAnd(mult3, mult5); // intersection = multiples de 15
var notMult3 = ctx.MkNot(mult3);         // complement

var sbO = new StringBuilder();
sbO.AppendLine("Operations sur predicats symboliques\n");
sbO.AppendLine("Predicats : mult3 = (x mod 3 = 0), mult5 = (x mod 5 = 0)\n");
sbO.AppendLine($"{"Valeur",-8} {"mult3",-7} {"mult5",-7} {"3 OU 5",-8} {"3 ET 5 (15)",-12} {"non-3",-7}");
sbO.AppendLine(new string('-', 50));
foreach (int v in new[] { 1, 3, 5, 7, 9, 10, 15, 20, 30, 23 }) {
    bool Eval(BoolExpr p) {
        var s = ctx.MkSolver(); s.Add(p); s.Add(ctx.MkEq(xV, ctx.MkInt(v))); return s.Check() == Status.SATISFIABLE;
    }
    sbO.AppendLine($"{v,-8} {(Eval(mult3) ? "OUI" : "non"),-7} {(Eval(mult5) ? "OUI" : "non"),-7} " +
                   $"{(Eval(mult3or5) ? "OUI" : "non"),-8} {(Eval(mult3and5) ? "OUI" : "non"),-12} {(Eval(notMult3) ? "OUI" : "non"),-7}");
}
sbO.AppendLine("\nVerification : '3 ET 5' = multiples de 15 uniquement (15, 30). 'non-3' = complement.");
sbO.ToString().Display();

Operations sur predicats symboliques

Predicats : mult3 = (x mod 3 = 0), mult5 = (x mod 5 = 0)

Valeur   mult3   mult5   3 OU 5   3 ET 5 (15)  non-3  
--------------------------------------------------
1        non     non     non      non          OUI    
3        OUI     non     OUI      non          non    
5        non     OUI     OUI      non          OUI    
7        non     non     non      non          OUI    
9        OUI     non     OUI      non          non    
10       non     OUI     OUI      non          OUI    
15       OUI     OUI     OUI      OUI          non    
20       non     OUI     OUI      non          OUI    
30       OUI     OUI     OUI      OUI          non    
23       non     non     non      non          OUI    

Verification : '3 ET 5' = multiples de 15 uniquement (15, 30). 'non-3' = complement.

<null>

Interprétation : Opérations symboliques

• Union (MkOr) : « mult3 OU mult5 » accepte 3, 5, 9, 10, 15, 20, 30 — tout multiple de l’un ou l’autre.
• Intersection (MkAnd) : « mult3 ET mult5 » n’accepte que 15, 30 — les multiples de 15 (ppcm).
• Complément (MkNot) : « non-mult3 » accepte tout ce qui n’est pas divisible par 3.

Ces combinaisons sont exactes et automatiques : Z3 décide chaque cas sans qu’on ait à énumérer ou coder les multiples. C’est la puissance de l’approche symbolique sur l’approche énumérative des automates finis classiques.

---

Note sur la portée : cette tranche 2 couvre les §3-4 du notebook Python (le cœur « automates symboliques avec Z3 »). Les §5 (vérification de propriétés), §6 (lien Sudoku) et §7 (discussion Automata.Net) du notebook Python restent à porter dans une tranche 3 — ils construisent des modèles plus riches (système de porte, mini-Sudoku) au-dessus de la classe SymbolicAutomaton introduite ici.

Exercice (capstone) : Automate symbolique pour nombres premiers avec 30

Cet exercice de synthèse mobilise les opérations sur prédicats de la §4.7 (complément et conjonction). Construisez un automate symbolique à 2 états qui accepte les entiers \(x \ge 1\) premiers avec 30, c’est-à-dire non divisibles par 2, par 3 ni par 5.

Indices : - Étape 1 : deux états — \(q_0\) (initial), \(q_1\) (final). - Étape 2 : définir trois prédicats de divisibilité : \(\mathrm{div2} = (x \bmod 2 = 0)\), \(\mathrm{div3} = (x \bmod 3 = 0)\), \(\mathrm{div5} = (x \bmod 5 = 0)\). - Étape 3 : composer la transition \(q_0 \to q_1\) comme la conjonction de la garde et des compléments : \(x \ge 1 \wedge \neg\,\mathrm{div2} \wedge \neg\,\mathrm{div3} \wedge \neg\,\mathrm{div5}\). - Étape 4 : testez — dans \([1, 30]\) les acceptés sont \(\{1, 7, 11, 13, 17, 19, 23, 29\}\) (fonction d’Euler \(\varphi(30) = 8\)) ; \(2, 3, 5, 6, 10, 15, 30\) doivent être rejetés.

Astuce : la conjonction de compléments \(\neg \mathrm{div2} \wedge \neg \mathrm{div3}\) est équivalente au complément de l’union \(\neg(\mathrm{div2} \vee \mathrm{div3})\) (loi de De Morgan) — les deux formulations donnent le même automate. Utilisez MkNot, MkAnd, MkOr selon votre préférence.

// Exercice (capstone) : automate symbolique pour nombres premiers avec 30 (coprimes a 30)
// TODO etudiant : construire l'automate 'autoCoprime30' avec la classe SymbolicAutomaton.
// Etape 1 : 2 etats (q0 initial, q1 final)
// Etape 2 : predicats div2 = (x mod 2 = 0), div3 = (x mod 3 = 0), div5 = (x mod 5 = 0)
// Etape 3 : q0 -> q1 sur (x >= 1) AND NOT div2 AND NOT div3 AND NOT div5
//           (equivalent : (x >= 1) AND NOT (div2 OR div3 OR div5), loi de De Morgan)
// Etape 4 : tester {1,7,11,13,17,19,23,29} (acceptes) vs {2,3,5,6,10,15,30} (rejetes)
SymbolicAutomaton autoCoprime30 = null;  // TODO etudiant : remplacer par la solution
Console.WriteLine("Exercice a completer : automate pour nombres premiers avec 30");

Exercice a completer : automate pour nombres premiers avec 30

---

Bilan (tranches 1 + 2)

Concepts clés

• Automate fini (§1-2) : DFA (déterministe, Dictionary<(string,char),string>) et NFA (non déterministe, Dictionary<(string,char),HashSet<string>>). Clos par complément, union, intersection (produit cartésien). Limité par le pumping lemma (impossible de compter au-delà du nombre d’états).
• Automate symbolique (§3-4) : transitions étiquetées par des prédicats Z3 sur un alphabet infini (\(\mathbb{Z}\)). Décision via solveur SMT (solver.Check() == Status.TRUE). Clos par MkAnd (intersection), MkOr (union), MkNot (complément) — combinaisons exactes et automatiques.
• Avantage clé : l’automate symbolique manipule des propriétés (parité, intervalle, divisibilité) sur un ensemble infini sans énumération, alors que l’automate fini exige une transition par symbole concret.

Ce qu’apportera la tranche 3 (à suivre)

• §5 : vérification de propriétés (système de porte à code, invariants d’état) — application directe de la classe SymbolicAutomaton à un modèle de système réactif.
• §6 : lien avec Sudoku (mini-Sudoku 2×2 comme problème d’automates / CSP).

Version de référence

Le notebook Python complet (Search-10-SymbolicAutomata.ipynb) couvre l’ensemble (§1-8) avec automata-lib (DFA/NFA) et z3-solver (symbolique). Ce jumeau .NET utilise des classes DFA/NFA hand-rolled (§7 du Python : « Notre approche alternative ») et la vraie librairie SOTA Microsoft.Z3 (NuGet 4.12.2) pour la partie symbolique.

Honnêtement : l’implémentation manuelle des DFA/NFA en C# est un choix pédagogique délibéré (pas de lib .NET maintenue et didactique équivalente à automata-lib). En revanche, la partie symbolique utilise bien la vraie librairie SOTA Microsoft.Z3 — aucun workaround.