10 — Générer un témoin depuis A & ~B (fork Automata vivant)

<< 06 — Meal Planner hiérarchique | Sudoku-13 — Automates symboliques >>

---

Le problème : reconnaître ne suffit pas, il faut produire

Un moteur comme RE# (System.Text.RegularExpressions) répond à « cette chaîne appartient-elle au langage ? » — c’est de la reconnaissance. Mais beaucoup de tâches réelles demandent l’inverse : « donne-moi une chaîne qui appartient au langage » — c’est la génération de témoin (witness generation). Exemples :

• générer un mot de passe conforme à une politique mais évitant les motifs faibles connus ;
• fabriquer une entrée de test qui satisfait une contrainte et en viole une autre ;
• produire un identifiant valide mais pas encore utilisé.

Toutes ces tâches s’écrivent A & ~B : « dans le langage A, mais pas dans le langage B ».

Ce notebook

On consomme le fork MyIntelligenceAgency/Automata (modernisation net8.0 de Microsoft.Automata, dit AutomataDotNet, gelé vers 2020). Le fork ajoute deux choses que ni RE# ni le paquet public ne savent faire :

1. les opérateurs de surface & (intersection) et ~ (complément) directement dans la syntaxe regex ;
2. la génération de témoin sans le plafond historique de ~21 caractères (issue #6).

Objectifs

1. Manipuler l’algèbre CharSetSolver (BDD sur 128 caractères ASCII).
2. Écrire A & ~B en surface et générer un témoin via RexEngine.
3. Émettre la formule SMT-LIB correspondante (re.inter / re.comp) et la résoudre avec Z3 pour en extraire un témoin.
4. Comprendre honnêtement la portée : le fork lève le mur du témoin, pas l’explosion d’automate à grande échelle — voir le Sudoku-13 pour le verdict mesuré.

Non-but (issue #2979) : ce patch ne remplace pas RE# pour la reconnaissance et ne réveille pas Z3.LinqBinding. Il ajoute ce que RE# ne fait pas : un témoin depuis la syntaxe &/~.

// Le fork est déployé en submodule sibling (Windows/PowerShell : scripts/environment/automata-build-deploy.ps1 ;
// Linux/macOS : scripts/environment/automata-build-deploy.sh — jumeau cross-platform, mêmes commandes dotnet).
// .deploy/ contient Microsoft.Automata.dll (pure-managed, fork net8.0) + sa dépendance System.CodeDom.
#r "../Automata/.deploy/System.CodeDom.dll"
#r "../Automata/.deploy/Microsoft.Automata.dll"

using System;
using System.Linq;
using System.Diagnostics;
using System.Text.RegularExpressions;
using Microsoft.Automata;
using Microsoft.Automata.Rex;

Console.WriteLine("Imports OK — fork Automata (surface &/~ + témoin non-capé) chargé.");

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

Imports OK — fork Automata (surface &/~ + témoin non-capé) chargé.

1. Reconnaître vs produire — trois outils, trois rôles

Outil	Question répondue	Direction
RE# (Regex.IsMatch)	« s appartient-il à L ? »	reconnaissance
RexEngine (ce notebook)	« donne-moi un s de L »	génération de témoin
Z3 (notebooks 01–09)	« existe-t-il un s satisfaisant ces contraintes ? »	résolution SMT générale

Les trois sont complémentaires. RexEngine occupe la case que RE# laisse vide : il fabrique un mot du langage, et — grâce au fork — depuis un langage décrit avec & et ~.

2. L’algèbre CharSetSolver — des BDD sur l’alphabet

Sous le capot, un langage régulier est un automate dont les transitions sont étiquetées par des ensembles de caractères. Ces ensembles ne sont pas stockés en clair mais comme BDD (Binary Decision Diagrams) — une représentation compacte et canonique des prédicats booléens sur les bits d’un caractère.

CharSetSolver(BitWidth.BV7) travaille sur 7 bits = 128 caractères ASCII. C’est l’algèbre partagée par tout le pipeline : convertir une regex en automate, intersecter, complémenter, tester l’appartenance. Retenez ce mot — « algèbre partagée » — il reviendra au §6.

// Construire un automate depuis une regex, puis tester l'appartenance.
// API correcte : solver.Accepts(automate, chaine)  (et NON automate.Accepts).
var solver = new CharSetSolver(BitWidth.BV7);

// "^[a-z]$" = exactement une lettre minuscule.
var uneMinuscule = solver.Convert("^[a-z]$", RegexOptions.None)
                         .RemoveEpsilons().Determinize().Minimize();

foreach (var s in new[] { "a", "Z", "5", "ab" })
    Console.WriteLine($"  Accepts(\"{s}\") = {solver.Accepts(uneMinuscule, s)}");

  Accepts("a") = True
  Accepts("Z") = False
  Accepts("5") = False
  Accepts("ab") = False

3. L’opérateur de surface & — intersection dans la syntaxe

Le fork branche & en tête du parser regex : A&B est analysé comme l’intersection des deux langages, et câblé sur Automaton.Intersect. Pas de manipulation manuelle d’automates : on l’écrit, c’est tout.

Exemple canonique : ^[ab]$ & ^[bc]$. Un caractère unique qui est (a ou b) et (b ou c) ne peut être que b — l’intersection est le singleton {b}.

Pourquoi les ancres ^…$ ? Une regex .NET non ancrée signifie « la chaîne contient un tel caractère » : [ab] ≡ .*[ab].*. Sans ancres, [ab]&[bc] accepterait "ac" (contient a et c). Les ancres bornent la longueur et donnent un témoin propre et lisible.

Pourquoi & et ~ marchent — la fermeture des langages réguliers

Écrire A & ~B revient à combiner des langages par intersection (&) et complément (~). Cela n’a de sens que parce que les langages réguliers possèdent une propriété fondamentale : ils sont fermés sous ces opérations (théorème de Kleene). Concrètement, l’union (∪), l’intersection (∩) et le complément (¬) de langages réguliers sont encore des langages réguliers — on dit que les langages réguliers forment une algèbre de Boole.

C’est ce fondement qui garantit que A & ~B reste un langage régulier, donc représentable par un automate fini et manipulable par les opérations Automaton.Intersect et Automaton.Complement sur lesquelles le fork câble & et ~. Sans cette fermeture, intersecter ou compléter des langages pourrait produire un objet hors de portée d’un automate (impossible à représenter, donc à résoudre). Le motif vedette de ce notebook — « dans A, mais pas dans B » — doit donc toute son existence à ce théorème.

Les briques d’automates appelées en code. Dans les cellules, on voit souvent .RemoveEpsilons().Determinize().Minimize() après Convert. Ce sont les trois étapes standard de la théorie des automates : - Determinize — passer d’un automate non-déterministe (NFA) à l’automate déterministe (DFA) équivalent (la construction des parties) ; - Minimize — calculer le DFA minimal (les états équivalents fusionnés) ; - RemoveEpsilons — supprimer les transitions « epsilon » (vides).

Ces opérations rendent l’intersection et le complément effectivement calculables : on ne se contente pas de savoir que le résultat existe (fermeture), on le construit en pratique. Les détails algorithmiques relèvent d’un cours d’automates ; ici on consomme le résultat.

Pipeline du motif A & ~B — vue d’ensemble

Le diagramme ci-dessous illustre comment deux expressions régulières se combinent pour produire un témoin via l’intersection et le complément :

flowchart TB
    subgraph G1 ["Construction des automates"]
        A["Regex A"] --> DFA_A["DFA(A)"]
        B["Regex B"] --> DFA_B["DFA(B)"]
        DFA_B --> COMP["~DFA(B) — Complément"]
    end
    subgraph G2 ["Opération A & ~B"]
        DFA_A --> INT["DFA(A) ∩ ~DFA(B)"]
        COMP --> INT
    end
    INT --> W["Témoin w ← GenerateMember"]
    W --> V["Vérifié par RE#"]  
    %% color: explicite -- sans lui, libelle clair sur fond clair en mode sombre GitHub (#15022) ; ton parfois plus fonce que le stroke (le stroke en couleur de texte rendrait infer illisible) : ne pas harmoniser
    style W fill:#c8f7c5,color:#1b5e20
    style V fill:#c8f7c5,color:#1b5e20

Pourquoi ça fonctionne : les langages réguliers sont fermés sous l’intersection (&) et le complément (~). Le résultat A & ~B est donc lui-même régulier — un automate fini existe pour le représenter, et GenerateMember peut en extraire un mot accepté (le témoin).

// "[ab] & [bc]" ancré = le singleton {b}. On construit via le solveur et on vérifie.
var inter = solver.Convert("^[ab]$&^[bc]$", RegexOptions.None)
                  .RemoveEpsilons().Determinize().Minimize();

foreach (var s in new[] { "a", "b", "c" })
    Console.WriteLine($"  Accepts(\"{s}\") = {solver.Accepts(inter, s)}");

// Génération du témoin : engine.CreateFromRegexes partage l'algèbre interne du moteur.
var engine = new RexEngine(BitWidth.BV7);
var interAut = engine.CreateFromRegexes("^[ab]$&^[bc]$");
string temoinInter = engine.GenerateMember(interAut);
Console.WriteLine($"  Témoin de (^[ab]$ & ^[bc]$) = \"{temoinInter}\"");

  Accepts("a") = False
  Accepts("b") = True
  Accepts("c") = False
  Témoin de (^[ab]$ & ^[bc]$) = "b"

4. L’opérateur de surface ~ — complément, et le motif A & ~B

~A est le complément de A : tout ce qui n’est pas dans A. Combiné à &, on obtient le motif vedette A & ~B : « dans A, mais pas dans B ».

Exemple : ^[a-z]$ & ~[aeiou] = une lettre minuscule qui n’est pas une voyelle = une consonne.

Précédence de ~ — un piège à connaître. ~ se lie à l’atome qui suit immédiatement (une classe […], une ancre, ou un groupe (…)). Pour complémenter une séquence, il faut parenthéser : ~(.*motif.*) et non ~.*motif.* (ce dernier ne complémente que le . et laisse passer le motif). On exploitera cette règle au §8.

// A & ~B : une minuscule (A) qui n'est pas une voyelle (~B) = une consonne.
var consonne = engine.CreateFromRegexes("^[a-z]$&~[aeiou]");

foreach (var s in new[] { "a", "e", "t", "z" })
    Console.WriteLine($"  Accepts(\"{s}\") = {engine.Solver.Accepts(consonne, s)}");

string temoinConsonne = engine.GenerateMember(consonne);
Console.WriteLine($"  Témoin de (^[a-z]$ & ~[aeiou]) = \"{temoinConsonne}\" (une consonne)");

  Accepts("a") = False
  Accepts("e") = False
  Accepts("t") = True
  Accepts("z") = True
  Témoin de (^[a-z]$ & ~[aeiou]) = "z" (une consonne)

5. Le moteur de témoin — le chemin sûr

RexEngine.GenerateMember(automate) effectue une marche aléatoire sur l’automate déterministe et renvoie un mot accepté. Deux règles d’usage :

• Construire l’automate via engine.CreateFromRegexes(...) (ou engine.Solver), pour qu’il partage l’algèbre du moteur (cf §2). Le §6 montre ce qui se passe sinon.
• Utiliser GenerateMember (marche aléatoire) et non GenerateMemberUniformly : ce dernier exige un automate fini et lève une exception sur un langage infini/bouclant.

Le chemin est toujours le même :

var engine = new RexEngine(BitWidth.BV7);
var aut    = engine.CreateFromRegexes("...&~...");  // surface &/~
string w   = engine.GenerateMember(aut);            // témoin
bool ok    = engine.Solver.Accepts(aut, w);         // vérification

// Vérification systématique : tout témoin généré doit être accepté par son propre automate.
string CheckTemoin(RexEngine eng, string regex)
{
    var aut = eng.CreateFromRegexes(regex);
    string w = eng.GenerateMember(aut);
    bool ok = eng.Solver.Accepts(aut, w);
    return $"  regex={regex,-22} témoin=\"{w}\" accepté={ok}";
}

Console.WriteLine(CheckTemoin(engine, "^[ab]$&^[bc]$"));
Console.WriteLine(CheckTemoin(engine, "^[a-z]$&~[aeiou]"));
Console.WriteLine(CheckTemoin(engine, "^[0-9]{4}$&~(.*0.*)"));  // 4 chiffres sans aucun zéro

  regex=^[ab]$&^[bc]$          témoin="b" accepté=True
  regex=^[a-z]$&~[aeiou]       témoin="s" accepté=True
  regex=^[0-9]{4}$&~(.*0.*)    témoin="8411" accepté=True

6. Le piège du solveur croisé — une leçon sur l’identité d’algèbre

Que se passe-t-il si on construit l’automate avec un CharSetSolver puis qu’on demande le témoin à un RexEngine qui en possède un autre ? Les BDD des deux solveurs ne partagent aucune identité de terminal : la descente dans l’algèbre échouerait.

Le fork (#2979, étape 4) transforme cette situation en ArgumentException claire et actionnable — au lieu de l’historique NullReferenceException cryptique au fond de BDDAlgebra.Choose. Ce n’est pas un bug, c’est une garde : le message vous dit exactement quoi faire.

On enveloppe la démonstration dans un try/catch : le notebook s’exécute de bout en bout (la garde est attendue, pas une panne).

// MAUVAIS chemin : automate bâti avec un solveur externe, témoin demandé à un autre moteur.
var solveurExterne = new CharSetSolver(BitWidth.BV7);
var moteur = new RexEngine(BitWidth.BV7);   // possède un solveur DIFFÉRENT
var autExterne = solveurExterne.Convert("[ab]+", RegexOptions.None)
                               .RemoveEpsilons().Determinize().Minimize();

try
{
    string w = moteur.GenerateMember(autExterne);   // déclenche la garde
    Console.WriteLine($"(inattendu) témoin = {w}");
}
catch (ArgumentException ex)
{
    Console.WriteLine("ArgumentException attendue (garde du fork) :");
    Console.WriteLine("  " + ex.Message.Split('\n')[0]);
}

// BON chemin : construire via le moteur lui-même.
var autSafe = moteur.CreateFromRegexes("[ab]+");
Console.WriteLine($"  Correction → CreateFromRegexes : témoin = \"{moteur.GenerateMember(autSafe)}\"");

ArgumentException attendue (garde du fork) :
  RexEngine.GenerateMember: the automaton was built with a different CharSetSolver than this engine. BDD descent requires a shared algebra. Build the automaton via engine.CreateFromRegexes(...) or engine.Solver, or construct the engine via the RexEngine(CharSetSolver) ctor. (Parameter 'fa')
  Correction → CreateFromRegexes : témoin = "[as}g"

7. Émettre la formule SMT-LIB — re.inter / re.comp

Le même motif A & ~B se traduit en théorie des chaînes SMT-LIB, le langage des solveurs comme Z3. Le fork expose RegexToSMTConverter (rendu public pour ce notebook, #2979 étape 6) : il convertit une regex de surface en expression SMT, où & devient re.inter et ~ devient re.comp.

C’est le pont entre les deux mondes du cours : la syntaxe regex d’ici et la contrainte SMT des notebooks Z3 01–09.

var conv = new RegexToSMTConverter(BitWidth.BV7);

foreach (var regex in new[] { "[ab]&~[bc]", "[a-z]&~[aeiou]" })
{
    Console.WriteLine($"regex   : {regex}");
    Console.WriteLine($"SMT-LIB : {conv.ConvertRegex(regex)}");
    Console.WriteLine();
}

regex   : [ab]&~[bc]
SMT-LIB : (re.inter (re.range "a" "b") (re.comp (re.range "b" "c")))

regex   : [a-z]&~[aeiou]
SMT-LIB : (re.inter (re.range "a" "z") (re.comp (re.union (str.to_re "a")(re.union (str.to_re "e")(re.union (str.to_re "i")(re.union (str.to_re "o") (str.to_re "u")))))))

7b. Fermer la boucle — résoudre le SMT-LIB avec Z3

Le §7 émet la formule ; mais une formule SMT-LIB n’a de valeur que si un solveur la résout. C’est exactement ce que font les notebooks 01–09 : on referme ici la boucle émettre → résoudre en injectant la sortie du convertisseur dans Z3 (ParseSMTLIB2String), puis en extrayant un témoin.

Le convertisseur émet la théorie des chaînes SMT-LIB 2.6 (str.to_re, re.range, re.inter, re.comp, (_ re.loop m n)) — le dialecte que Z3 consomme réellement. La requête de témoin est (str.in_re w R) : « trouve un mot complet w du langage R ». Chaque témoin est ensuite re-vérifié indépendamment par RE# (Regex.IsMatch), comme au §8.

Deux moteurs, un même langage. Le §5 produit le témoin par marche aléatoire sur l’automate (chemin DFA) ; ici Z3 le produit par résolution de contraintes (chemin SMT). Les deux acceptent la même description A & ~B — et Z3, comme le fork, n’a pas le plafond historique de ~21 caractères (cf §9).

// Émettre ne suffit pas : on **résout** réellement le SMT-LIB produit au §7.
// Le convertisseur (modernisé, #2979) émet la théorie des chaînes SMT-LIB 2.6 que Z3
// consomme directement. On injecte sa sortie dans Z3 via ParseSMTLIB2String et on
// extrait un témoin — le pendant Z3 (sans plafond) du moteur DFA des §5–§9.
#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
using Microsoft.Z3;

string ResoudreSMT(Context ctx, string regexSMT)
{
    // (str.in_re w R) = « w est un mot complet du langage R » (appartenance = match ancré).
    string script =
        "(declare-const w String)\n" +
        $"(assert (str.in_re w {regexSMT}))\n" +
        "(check-sat)";
    BoolExpr[] contraintes = ctx.ParseSMTLIB2String(script);
    var solver = ctx.MkSolver();
    solver.Assert(contraintes);
    if (solver.Check() != Status.SATISFIABLE) return null;
    var w = (SeqExpr)ctx.MkConst("w", ctx.StringSort);
    return solver.Model.Eval(w, true).ToString().Trim('"');
}

using (var ctx = new Context())
{
    Console.WriteLine($"{Microsoft.Z3.Version.FullVersion} — résolution du SMT-LIB émis par le fork :\n");

    // (surface, vérif positive RE#, vérif négative RE#) — re-vérification indépendante.
    var demos = new (string surface, string pos, string neg)[]
    {
        ("[ab]&~[bc]",     "^[ab]$",   "^[bc]$"),
        ("[a-z]&~[aeiou]", "^[a-z]$",  "^[aeiou]$"),
    };

    foreach (var (surface, pos, neg) in demos)
    {
        string smt = conv.ConvertRegex(surface);     // la sortie réelle du §7
        string temoin = ResoudreSMT(ctx, smt);
        bool ok = temoin != null && Regex.IsMatch(temoin, pos) && !Regex.IsMatch(temoin, neg);
        Console.WriteLine($"  {surface,-16} → témoin Z3 = \"{temoin}\"  re-vérifié(RE#)={ok}");
    }

    // Et ça passe à l'échelle SANS le plafond ~21 : [a-z]{30} résolu par Z3.
    string smt30 = conv.ConvertRegex("[a-z]{30}");
    string t30 = ResoudreSMT(ctx, smt30);
    Console.WriteLine($"  [a-z]{{30}}        → témoin Z3 (len={t30?.Length}) re-vérifié(RE#)={Regex.IsMatch(t30, "^[a-z]{30}$")}");
}

Z3 4.12.2.0 — résolution du SMT-LIB émis par le fork :

  [ab]&~[bc]       → témoin Z3 = "a"  re-vérifié(RE#)=True
  [a-z]&~[aeiou]   → témoin Z3 = "d"  re-vérifié(RE#)=True
  [a-z]{30}        → témoin Z3 (len=30) re-vérifié(RE#)=True

7c. Quand re.inter tient l’echelle - la decomposition monadique

Le 7b resout A & ~B sur de petits langages (un caractère, une trentaine). Mais re.inter materialise l’espace croise des langages intersectes, et cet espace explose quand les contraintes se chevauchent. Le notebook Sudoku-13 le mesure : l’intersection 10-way d’une ligne, emise en re.inter fondu, fait unknown ; la même contrainte eclatee en str.contains par chiffre atterrit la grille 9x9.

La théorie qui tranche est la decomposition monadique de Veanes (Monadic Decomposition, CAV 2014). Une formule a plusieurs variables est monadiquement decomposable si elle equivaut a une combinaison booleenne de predicats a une seule variable. Quand elle l’est, on remplace le produit (re.inter) par une conjonction de tests independants - sans jamais construire l’automate croise.

Forme emise	Ce que fait le solveur	Echelle
re.inter (intersection fondue)	materialise le produit des langages	sature des que les contraintes se chevauchent
conjonction de predicats monadiques (str.contains)	tests independants, pas de produit	atterrit

La lecon, des deux cotes. Ce notebook montre A & ~B la ou re.inter est rapide (peu de chevauchement) ; Sudoku-13 montre l’echelle ou il faut decomposer. Le bon critere n’est pas ” Z3 sait-il faire ? ” mais ” la conjonction est-elle monadiquement decomposable ? “. Veanes donne le verdict exact : un tous-distincts l’est (eclatable par chiffre), un ordre x < y ne l’est pas (aucune decomposition finie).

8. Le payoff — générer un mot de passe politique & ~faibles

Voici le motif A & ~B à pleine puissance, sur un cas réel : fabriquer un mot de passe conforme à une politique tout en évitant les motifs faibles connus.

• A = ^[A-Za-z0-9]{8}$ — exactement 8 caractères alphanumériques ;
• ~B₁ = ~(.*password.*) — ne contient pas la sous-chaîne password ;
• ~B₂ = ~(^[0-9].*$) — ne commence pas par un chiffre.

On note l’usage des parenthèses sur ~(…) (cf §4) : on complémente bien des séquences, pas un seul atome. Le moteur produit des témoins variés (marche aléatoire) — chacun est un mot de passe valide selon la politique, vérifié contre les trois conditions.

// A & ~B1 & ~B2 : 8 alphanumériques, sans "password", ne commençant pas par un chiffre.
string politique = "^[A-Za-z0-9]{8}$&~(.*password.*)&~(^[0-9].*$)";
var motDePasse = engine.CreateFromRegexes(politique);

// Vérificateurs indépendants (RE#) pour prouver l'honnêteté de chaque témoin.
bool SansPassword(string s) => !s.Contains("password");
bool SansChiffreInitial(string s) => s.Length > 0 && !char.IsDigit(s[0]);

Console.WriteLine("Témoins générés (chacun re-vérifié indépendamment) :");
for (int i = 0; i < 5; i++)
{
    string w = engine.GenerateMember(motDePasse);
    bool len8 = w.Length == 8;
    Console.WriteLine($"  \"{w}\"  len8={len8}  sansPassword={SansPassword(w)}  sansChiffreInitial={SansChiffreInitial(w)}");
}

Témoins générés (chacun re-vérifié indépendamment) :
  "Wppaipak"  len8=True  sansPassword=True  sansChiffreInitial=True
  "pVP9TpGp"  len8=True  sansPassword=True  sansChiffreInitial=True
  "phpPO6pq"  len8=True  sansPassword=True  sansChiffreInitial=True
  "ppapaspa"  len8=True  sansPassword=True  sansChiffreInitial=True
  "TApapGpp"  len8=True  sansPassword=True  sansChiffreInitial=True

9. Le plafond de 21 caractères est levé (issue #6)

La machinerie de témoin historique d’AutomataDotNet plafonnait en pratique vers ~21 caractères pour les automates non triviaux (au-delà, elle explosait ou bouclait). Le fork sous net8.0 lève ce plafond : on génère ici un témoin de 30 caractères sans difficulté.

Honnêteté — la portée exacte. Le fork lève le mur du témoin (longueur). Il ne lève pas le mur de l’explosion d’automate : intersecter des dizaines de contraintes (p. ex. les 81 cases d’un Sudoku) fait exploser le produit cartésien des états. Pour le Sudoku à l’échelle, Z3 Distinct reste le résolveur de production (~27 ms). Le verdict mesuré est au §6b du Sudoku-13. Le vrai payoff de ce notebook est la génération de témoin générale A & ~B, pas le Sudoku.

// [a-z]{30} : plus long que l'ancien plafond ~21. Mesure du temps.
var long30 = engine.CreateFromRegexes("^[a-z]{30}$");
var sw = Stopwatch.StartNew();
string temoinLong = engine.GenerateMember(long30);
sw.Stop();

Console.WriteLine($"  témoin     = \"{temoinLong}\"");
Console.WriteLine($"  longueur   = {temoinLong.Length}  (ancien plafond ~21)");
Console.WriteLine($"  accepté    = {engine.Solver.Accepts(long30, temoinLong)}");
Console.WriteLine($"  temps      = {sw.Elapsed.TotalMilliseconds:F1} ms");

  témoin     = "pgrsaqshzhoxnmysyerqzxbjlomzsv"
  longueur   = 30  (ancien plafond ~21)
  accepté    = True
  temps      = 0,0 ms

Exercices

Trois exercices pour pratiquer le motif A & ~B et la génération de témoin. Les cellules sont des squelettes à compléter : remplacez les // TODO etudiant puis exécutez. Un vérificateur indépendant est fourni à chaque fois.

Exercice 1 — Une adresse e-mail valide mais pas @spam.com

Générez un témoin pour le motif A & ~B où : - A = une adresse e-mail simple, p. ex. ^[a-z]+@[a-z]+\.[a-z]+$ ; - ~B = qui ne se termine pas par @spam.com → ~(.*@spam\.com$).

# Indice : pensez à parenthéser le ~(…) (cf §4). # Étape 1 : construisez l’automate via engine.CreateFromRegexes. # Étape 2 : générez et vérifiez le témoin.

// Exercice 1 : e-mail valide, mais pas @spam.com.
// Etape 1 : composez le motif A & ~B (A = email simple, ~B = pas @spam.com).
string motifEmail = null;  // TODO etudiant : "^[a-z]+@[a-z]+\\.[a-z]+$&~(.*@spam\\.com$)"

if (motifEmail == null)
{
    Console.WriteLine("Exercice a completer : definir motifEmail (A & ~B).");
}
else
{
    // Etape 2 : construire, generer, verifier.
    var autEmail = engine.CreateFromRegexes(motifEmail);
    string temoin = engine.GenerateMember(autEmail);
    bool pasSpam = !temoin.EndsWith("@spam.com");
    Console.WriteLine($"temoin=\"{temoin}\"  pasSpam={pasSpam}");
}

Exercice a completer : definir motifEmail (A & ~B).

Exercice 2 — Diagnostiquer et corriger le piège du solveur croisé

Le code ci-dessous échoue : il construit l’automate avec un CharSetSolver local puis demande le témoin à un RexEngine distinct (le piège du §6). Diagnostiquez l’exception attendue, puis corrigez en utilisant le chemin sûr.

# Indice : relisez le §6 — l’automate doit partager l’algèbre du moteur. # Étape 1 : remplacez la construction par engine.CreateFromRegexes(...).

// Exercice 2 : corriger le piège du solveur croisé.
var solveurLocal = new CharSetSolver(BitWidth.BV7);
var moteurEx2 = new RexEngine(BitWidth.BV7);

// TODO etudiant : cette construction utilise le MAUVAIS solveur. Corrigez-la.
// Indice : Automaton<BDD> autEx2 = moteurEx2.CreateFromRegexes("^[a-z]{5}$");
Automaton<BDD> autEx2 = null;  // Etape 1 : construire via moteurEx2.CreateFromRegexes(...)

if (autEx2 == null)
{
    Console.WriteLine("Exercice a completer : construire autEx2 via le chemin sur (cf section 6).");
}
else
{
    string temoin = moteurEx2.GenerateMember(autEx2);
    Console.WriteLine($"temoin=\"{temoin}\"  accepte={moteurEx2.Solver.Accepts(autEx2, temoin)}");
}

Exercice a completer : construire autEx2 via le chemin sur (cf section 6).

Exercice 3 — Un numéro de test à 10 chiffres, non déjà utilisé

Classique de la génération de test : produire un identifiant valide mais pas dans une liste déjà utilisée. Motif A & ~B : - A = ^[0-9]{10}$ — dix chiffres ; - ~B = ne commence pas par un préfixe réservé connu, p. ex. ~(^0000.*$).

# Indice : même schéma qu’au §8. # Étape 1 : composez le motif. # Étape 2 : générez plusieurs témoins et vérifiez qu’aucun ne commence par 0000.

// Exercice 3 : numero de test a 10 chiffres, ne commencant pas par 0000.
string motifNumero = null;  // TODO etudiant : "^[0-9]{10}$&~(^0000.*$)"

if (motifNumero == null)
{
    Console.WriteLine("Exercice a completer : definir motifNumero (A & ~B).");
}
else
{
    var autNum = engine.CreateFromRegexes(motifNumero);
    for (int i = 0; i < 3; i++)
    {
        string w = engine.GenerateMember(autNum);
        Console.WriteLine($"numero=\"{w}\"  len10={w.Length == 10}  pasPrefixe0000={!w.StartsWith("0000")}");
    }
}

Exercice a completer : definir motifNumero (A & ~B).

Conclusion

Ce qu’on a vu	Outil du fork
Intersection & en surface	parser → Automaton.Intersect
Complément ~ en surface (avec parenthésage)	parser → Automaton.Complement
Témoin de A & ~B	RexEngine.GenerateMember (chemin partagé)
Garde solveur croisé	ArgumentException claire (#2979 étape 4)
Formule SMT-LIB	RegexToSMTConverter → re.inter / re.comp
Témoin via Z3 (SMT)	ParseSMTLIB2String + str.in_re → Model.Eval
Témoin > 21 caractères	plafond #6 levé sous net8.0

À retenir

• Reconnaître ≠ produire. RexEngine fabrique un témoin là où RE# ne fait que tester.
• A & ~B est le motif universel de génération sous contrainte positive/négative.
• ~ se lie à l’atome suivant : parenthésez ~(…) pour complémenter une séquence.
• Algèbre partagée : construisez l’automate via le moteur (CreateFromRegexes).
• Émettre puis résoudre : le SMT-LIB du fork est le dialecte réel de Z3 — ParseSMTLIB2String ferme la boucle et produit un témoin par résolution de contraintes.
• Portée honnête : le fork lève le mur du témoin, pas l’explosion d’automate. À l’échelle (Sudoku 81), Z3 reste le résolveur de production.
• Décomposition monadique (Veanes, CAV’14) : le critère théorique qui décide si re.inter tient l’échelle. Un tous-distincts est décomposable (éclatable par chiffre, cf 7c) ; un ordre x < y ne l’est pas. C’est la frontière entre ” émettre ” et ” émettre dans la bonne forme ” du Sudoku-13.

Source du programme. Margus Veanes, Symbolic Automata - Dagstuhl Seminar 17142 (2017) : SFA sur algèbre de Boole, minimisation symbolique (POPL’14), logique M2L-str vers SFA (POPL’17), décomposition monadique (CAV’14).

---

<< 06 — Meal Planner hiérarchique | Sudoku-13 — Automates symboliques >>