Guida agli automi visti a lezione

Questa pagina raccoglie gli automi comparsi negli appunti e li mette a confronto per uso pratico: definizione, condizione di accettazione, risultati dimostrativi essenziali e criterio per scegliere un modello invece di un altro.

Le fonti principali sono i capitoli gia' estratti nella knowledge base, raw/notes.pdf, e le anteprime OCR di raw/Riassunti si o.pdf. In particolare, nel riassunto manoscritto ho usato le pagine 42-48 per Büchi e chiusure, 67-75 per DBA/Muller/WS1S, 78-84 per learning automata, 85 per transduttori sequenziali e 88-96 per alberi/tree automata/Rabin.

Mappa rapida

Come scegliere l'automa

Se l'input e' una parola finita, parti da DFA/NFA/epsilon-NFA. Il DFA e' la scelta migliore quando devi complementare, decidere equivalenza o avere una sola computazione. L'NFA e' migliore quando stai costruendo automi a blocchi, perche' il non determinismo rende naturali unione, scelta e composizione. L'epsilon-NFA e' ancora piu' comodo nelle dimostrazioni da regex ad automi, perche' una epsilon-mossa collega componenti senza consumare input.

Se il sistema non termina e devi leggere parole infinite, il DFA/NFA finito non basta: non c'e' un "ultimo stato" su cui decidere. Qui entrano gli automi di Büchi. Un NBA e' il modello standard per omega-regolari, LTL e model checking automata-theoretic. Un DBA e' piu' facile da eseguire, ma e' meno espressivo: usarlo solo quando la proprieta' ha la forma "infiniti prefissi appartengono a un certo regolare $W$".

Se hai piu' obblighi "da vedere infinitamente spesso", usa GNBA come passaggio intermedio: e' esattamente l'oggetto giusto per l'intersezione di automi Büchi. Poi, se serve, lo riconverti in NBA con un contatore finito.

Se vuoi determinismo pieno su parole infinite, non affidarti ai DBA: passa a condizioni piu' ricche, come Muller, Rabin o parity. Nei tuoi appunti Muller serve a recuperare determinismo e chiusura booleana; Rabin serve soprattutto per alberi infiniti e S2S.

Se devi rappresentare un controllore o una strategia, non vuoi solo accettare/rifiutare parole: vuoi produrre azioni. Usa Mealy o un transduttore sequenziale. Se invece il sistema e' black-box e vuoi ricostruirne un modello, usa apprendimento di automi: l'output dell'algoritmo L* e' un DFA ipotesi.

Automi finiti deterministici (DFA)

Un DFA e' una tupla:

$$ \mathcal{A}=(Q,\Sigma,\delta,q_0,F) $$

dove $Q$ e' finito, $\Sigma$ e' l'alfabeto, $\delta:Q\times\Sigma\to Q$ e' la funzione di transizione, $q_0$ e' lo stato iniziale e $F\subseteq Q$ sono gli stati finali. La parola $w$ e' accettata se:

$$ \hat{\delta}(q_0,w)\in F. $$

Il punto centrale e' l'unicita' della run: fissati stato e simbolo, il prossimo stato e' determinato.

Perche' si usa

Il DFA e' lo strumento piu' pulito per decidere problemi su linguaggi regolari finiti. La determinazione rende semplice il complemento: prima completi la funzione di transizione, poi scambi finali e non finali. Rende anche chiara l'equivalenza tra linguaggi: puoi costruire prodotti e cercare stati che distinguono i due automi.

Perche' usarlo rispetto a NFA

Usa DFA quando ti serve una risposta operativa deterministica o quando vuoi complementare. Usa NFA quando ti serve una costruzione compatta. La differenza non e' nel potere espressivo, perche' su parole finite DFA e NFA riconoscono esattamente i linguaggi regolari; la differenza e' nel costo e nella comodita' delle costruzioni.

Automi finiti non deterministici (NFA)

Un NFA ha la stessa struttura del DFA, ma la transizione e':

$$ \Delta:Q\times\Sigma\to 2^Q. $$

Una parola e' accettata se esiste almeno una run che, dopo aver letto tutta la parola, termina in uno stato finale:

$$ \hat{\Delta}(q_0,w)\cap F\neq\emptyset. $$

Dimostrazione: subset construction

Per ogni NFA $\mathcal{N}=(Q,\Sigma,\Delta,q_0,F)$ costruisci un DFA:

$$ \mathcal{D}=(2^Q,\Sigma,\delta^D,\{q_0\},F^D) $$

con:

$$ \begin{aligned} \delta^D(S,a)&=\bigcup_{q\in S}\Delta(q,a),\\ F^D&=\{S\subseteq Q\mid S\cap F\neq\emptyset\}. \end{aligned} $$

L'invariante e': dopo aver letto $w$, lo stato-sottoinsieme del DFA e' esattamente l'insieme degli stati raggiungibili dall'NFA leggendo $w$. Si dimostra per induzione su $|w|$. Da questo segue che il DFA accetta $w$ se e solo se l'NFA ha almeno una run accettante su $w$.

Perche' si usa

L'NFA rende naturali le costruzioni esistenziali. Per l'unione basta scegliere quale automa simulare; per costruire automi da espressioni regolari e' molto piu' semplice passare da NFA/epsilon-NFA che forzare subito una macchina deterministica.

Costo della scelta

La subset construction puo' produrre fino a $2^{|Q|}$ stati. Quindi l'NFA puo' essere molto piu' compatto, ma se ti serve determinismo devi pagare una possibile esplosione esponenziale.

Epsilon-NFA

Un epsilon-NFA permette transizioni che non consumano simboli:

$$ \Delta:Q\times(\Sigma\cup\{\varepsilon\})\to 2^Q. $$

La nozione chiave e' l'epsilon-closure $E(S)$: tutti gli stati raggiungibili da $S$ usando solo mosse $\varepsilon$.

Dimostrazione: eliminare le epsilon-mosse

Dato un epsilon-NFA, costruisci un NFA senza epsilon-mosse usando:

$$ \Delta'(q,a)=E\left(\bigcup_{p\in E(q)}\Delta(p,a)\right). $$

Questa transizione comprime in un solo passo il blocco:

$$ \varepsilon^\ast a\varepsilon^\ast. $$

Gli stati finali diventano:

$$ F'=\{q\in Q\mid E(q)\cap F\neq\emptyset\}. $$

Quindi una parola accettata tramite mosse silenziose prima, durante o dopo la lettura viene accettata anche dal nuovo NFA.

Perche' si usa

L'epsilon-NFA non aggiunge potere espressivo, ma aggiunge modularita'. E' la scelta giusta per dimostrare regex -> automa: unione, concatenazione e stella si costruiscono collegando pezzi con epsilon-mosse.

Espressioni regolari e automi finiti

Le espressioni regolari non sono automi, ma negli appunti sono il linguaggio descrittivo equivalente a DFA/NFA/epsilon-NFA.

Risultato

Per parole finite, queste classi descrivono gli stessi linguaggi:

• DFA;
• NFA;
• epsilon-NFA;
• espressioni regolari ristrette.

Idea della dimostrazione

Regex -> automa: per induzione sulla struttura dell'espressione. I casi base sono $\emptyset$, $\varepsilon$ e una lettera $a$. Unione, concatenazione e stella si implementano con epsilon-mosse.

Automa -> regex: per un DFA con stati $q_1,\ldots,q_n$, definisci $R_{i,j}^k$ come il linguaggio delle parole che portano da $q_i$ a $q_j$ usando solo stati intermedi con indice al massimo $k$. La ricorrenza e':

$$ R_{i,j}^k = R_{i,j}^{k-1} \cup R_{i,k}^{k-1}(R_{k,k}^{k-1})^\ast R_{k,j}^{k-1}. $$

Alla fine:

$$ L(\mathcal{A})=\bigcup_{q_j\in F}R_{1,j}^n. $$

FTS e strutture di Kripke

Un Fair Transition System o una struttura di Kripke non e' un automa di specifica nel senso stretto "accetta/rifiuta una parola". E' il modello del sistema: genera tracce, cammini o computazioni. Negli appunti viene osservato che un FTS puo' essere visto come una forma di automa non deterministico, ma il suo ruolo nel model checking e' diverso: produce comportamenti, mentre l'automa della proprieta' riconosce comportamenti buoni o cattivi.

Perche' si usa

Lo usi quando devi modellare il programma, il protocollo o il sistema reattivo. Poi lo combini con una formula o con un automa della negazione della specifica. L'idea automata-theoretic del model checking e':

$$ \begin{aligned} Lang(S)&\subseteq Lang(\varphi)\\ &\Longleftrightarrow Lang(S)\cap Lang(\neg\varphi)=\emptyset. \end{aligned} $$

Il prodotto con l'automa della violazione trasforma la verifica in un problema di vuotezza.

Automi di Büchi non deterministici (NBA)

Un automa di Büchi legge parole infinite:

$$ \mathcal{A}=(Q,\Sigma,\Delta,q_0,F) $$

con $\Delta\subseteq Q\times\Sigma\times Q$. Una run $\rho$ su una parola infinita $\alpha$ e' accettante se:

$$ Inf(\rho)\cap F\neq\emptyset. $$

Cioe': almeno uno stato finale viene visitato infinitamente spesso. La parola e' accettata se esiste una run accettante.

Perche' si usa

I sistemi reattivi non terminano: server, protocolli, controller e agenti continuano a produrre eventi. Su parole infinite non puoi aspettare "la fine" per decidere. Büchi sostituisce lo stato finale raggiunto alla fine con uno stato finale visto infinite volte.

Gli NBA riconoscono esattamente i linguaggi omega-regolari e sono il ponte standard tra logica temporale, S1S e model checking.

Dimostrazione: emptiness Büchi

Un NBA ha linguaggio non vuoto se e solo se esiste uno stato finale $f\in F$ raggiungibile da $q_0$ e da cui si puo' tornare a $f$ con un cammino non vuoto. In termini di grafo: serve una componente fortemente connessa raggiungibile che contenga un finale.

Se una run accettante esiste, qualche finale compare infinite volte; tra due occorrenze dello stesso finale c'e' un ciclo. Viceversa, se hai un cammino $u$ fino a $f$ e un ciclo $v$ da $f$ a $f$, allora $uv^\omega$ e' accettata.

Chiusure importanti

Se $V\subseteq\Sigma^\ast$ e' regolare, allora $V^\omega$ e' omega-regolare. L'automa di Büchi riconosce un blocco di $V$, torna all'iniziale e ripete infinite volte.

Se $V$ e' regolare e $L$ e' omega-regolare, allora $V\cdot L$ e' omega-regolare: prima simuli l'automa finito per $V$, poi passi all'automa Büchi per $L$.

Unione e intersezione sono chiuse. L'unione usa il non determinismo; l'intersezione richiede piu' attenzione e passa naturalmente da GNBA.

Automi di Büchi generalizzati (GNBA)

Un GNBA ha una famiglia di insiemi di accettazione:

$$ \mathcal{F}=\{F_1,\ldots,F_k\}. $$

Una run e' accettante se visita infinitamente spesso almeno uno stato di ciascun $F_i$.

Perche' si usa

Il GNBA e' lo strumento giusto quando hai piu' obblighi di liveness. Nell'intersezione di due NBA non puoi pretendere che i finali vengano visti nello stesso istante: una run puo' visitare finali del primo automa ai tempi pari e finali del secondo ai tempi dispari. Il GNBA dice invece: visita infinite volte i finali del primo e visita infinite volte i finali del secondo.

Dimostrazione: intersezione di NBA

Dati $\mathcal{A}_1$ e $\mathcal{A}_2$, costruisci il prodotto sincrono sugli stati $Q_1\times Q_2$ e usa:

$$ \mathcal{F}=\{F_1\times Q_2,\; Q_1\times F_2\}. $$

La run prodotto e' accettante se la prima proiezione visita $F_1$ infinite volte e la seconda proiezione visita $F_2$ infinite volte.

Dimostrazione: GNBA -> NBA

Costruisci $k$ copie dell'automa, una per ogni obbligo. Uno stato diventa $(q,i)$, dove $i$ significa "sto aspettando di soddisfare $F_i$". Quando raggiungi uno stato in $F_i$, passi all'obbligo successivo. Se completi il giro $F_1,\ldots,F_k$ infinite volte, allora tutti gli obblighi vengono soddisfatti infinite volte. Il numero di stati cresce di un fattore $k$.

DBA: Büchi deterministici

Un DBA ha la stessa accettazione di Büchi, ma la transizione e' deterministica:

$$ \delta:Q\times\Sigma\to Q. $$

La run su ogni parola infinita e' unica.

Caratterizzazione

Un linguaggio $L\subseteq\Sigma^\omega$ e' riconosciuto da un DBA se e solo se:

$$ L=\overrightarrow{W} $$

per qualche regolare $W\subseteq\Sigma^\ast$, dove:

$$ \overrightarrow{W} = \{\alpha\in\Sigma^\omega\mid \exists^\omega n,\; \alpha(0,n)\in W\}. $$

In parole: una parola infinita e' accettata se ha infiniti prefissi appartenenti a un linguaggio regolare $W$.

Perche' non basta sempre

I DBA sono strettamente meno espressivi degli NBA. Il linguaggio:

$$ \begin{aligned} L_{fin}=\{\alpha\in\{a,b\}^\omega\mid{}& \alpha \text{ contiene}\\ &\text{solo finitemente molte } a\}. \end{aligned} $$

e' riconoscibile da un NBA: l'automa indovina il punto dopo l'ultima $a$ e poi accetta solo se vede soltanto $b$. Un DBA non puo' "indovinare" l'ultima $a$, perche' ha una sola run.

Quando usarlo

Usa DBA quando la proprieta' e' naturalmente deterministica e descrivibile come "infiniti prefissi buoni". Non usarlo come sostituto generale degli NBA: perderesti linguaggi omega-regolari.

Automi di Muller

Un automa di Muller usa l'insieme degli stati visti infinitamente spesso. Nel caso deterministico:

$$ \mathcal{M}=(Q,\Sigma,\delta,q_0,\mathcal{F}) $$

dove $\mathcal{F}\subseteq 2^Q$. Una run $\rho$ accetta se:

$$ Inf(\rho)\in\mathcal{F}. $$

Perche' si usa

Muller e' piu' flessibile di Büchi: non guarda solo "vedo almeno un finale infinite volte", ma esattamente quale insieme di stati ricorre all'infinito. Questo permette agli automi di Muller deterministici di riconoscere tutti gli omega-regolari, cosa che i DBA non fanno.

DBA come caso di Muller

Ogni DBA e' un DMA. Se il DBA ha finali $F$, scegli:

$$ \mathcal{F}=\{P\subseteq Q\mid P\cap F\neq\emptyset\}. $$

Allora $Inf(\rho)\in\mathcal{F}$ se e solo se la run visita qualche stato finale infinite volte.

Complemento semplice, ma solo deterministico

Se $\mathcal{M}=(Q,\Sigma,\delta,q_0,\mathcal{F})$ e' deterministico, il complemento e':

$$ \overline{\mathcal{M}}=(Q,\Sigma,\delta,q_0,2^Q\setminus\mathcal{F}). $$

Funziona perche' la run e' unica. Nel non deterministico l'accettazione e' esistenziale: complementare $\mathcal{F}$ non scambia correttamente "esiste una run accettante" con "tutte le run non accettano".

NMA e NBA

Gli automi di Muller non deterministici hanno lo stesso potere espressivo degli NBA. Una direzione e' immediata usando la famiglia $\mathcal{F}=\{P\mid P\cap F\neq\emptyset\}$. L'altra puo' passare da S1S: si formalizza "gli stati visti infinitamente spesso sono esattamente $P$" con:

$$ Exact_P(Y_0,\ldots,Y_m) = \bigwedge_{q_i\in P}Inf_i(Y_i) \wedge \bigwedge_{q_i\notin P}Fin_i(Y_i), $$

poi si fa la disgiunzione su tutti i $P\in\mathcal{F}$.

Automi di Rabin

Una condizione di Rabin e' una famiglia finita di coppie:

$$ \Omega=\{(L_1,U_1),\ldots,(L_n,U_n)\}. $$

Intuitivamente, per accettare deve esistere una coppia tale che gli stati in $L_i$ compaiano solo finitemente spesso e almeno uno stato in $U_i$ compaia infinitamente spesso:

$$ Inf(\rho)\cap L_i=\emptyset \quad\text{e}\quad Inf(\rho)\cap U_i\neq\emptyset. $$

Negli automi di Rabin su alberi, questa condizione va verificata lungo ogni ramo infinito.

Perche' si usa

Rabin e' utile quando Büchi e' troppo debole, soprattutto sugli alberi infiniti. Un vincolo Büchi dice "vedi $F$ infinitamente spesso"; Rabin puo' dire insieme "da un certo punto in poi evita $L_i$" e "continua a vedere $U_i$". Questa combinazione e' adatta a proprieta' ramificate e al teorema di Rabin per S2S.

Perche' non basta Büchi sugli alberi

Nel riassunto manoscritto compare esplicitamente il punto: per un Rabin automaton non sempre esiste un Büchi automaton equivalente. La ragione concettuale e' che su alberi devi soddisfare la condizione su tutti i rami, e la sola richiesta Büchi puo' non esprimere vincoli "finitamente spesso / infinitamente spesso" abbastanza ricchi.

Tree automata

Un tree automaton legge alberi invece di parole. Per alberi binari una forma tipica e':

$$ \mathcal{A}=(Q,A,\Delta,q_0,\mathcal{C}) $$

con:

$$ \Delta\subseteq Q\times A\times Q\times Q. $$

Se un nodo ha stato $q$ ed etichetta $a$, una transizione assegna stati ai due figli. Una run non e' piu' una sequenza lineare: assegna uno stato a ogni nodo dell'albero.

Alberi finiti

Per alberi finiti, l'emptiness dei tree automata e' decidibile in tempo polinomiale negli appunti. L'automa puo' essere visto top-down: riceve un simbolo e produce due stati per i figli.

Alberi infiniti

Per alberi infiniti ogni ramo e' una parola infinita. Serve quindi una condizione omega lungo i rami: Büchi, Muller, Rabin o parity. Il ruolo principale e' collegare alberi infiniti e logiche ramificate, in particolare S2S.

Quando usarli

Usa tree automata quando devi parlare di tutte le computazioni possibili nello stesso oggetto. Un albero rappresenta naturalmente il non determinismo: la radice e' lo stato iniziale, i rami sono computazioni.

Transduttori sequenziali

Un transduttore sequenziale e' un automa con output:

$$ \mathcal{T}=(\Sigma,\Gamma,Q,q_0,\delta) $$

dove:

$$ \delta:Q\times\Sigma\to Q\times\Gamma^\ast. $$

Non ha stati finali nel senso classico: a ogni transizione produce una porzione di output. Calcola una funzione:

$$ f:\Sigma^\ast\to\Gamma^\ast. $$

Perche' si usa

Serve quando non vuoi riconoscere un linguaggio, ma trasformare input in output. Negli appunti e' collegato anche al learning: invece di imparare una funzione caratteristica $f:\Sigma^\ast\to\{0,1\}$, puoi imparare una funzione su parole.

Limite importante

I transduttori sequenziali calcolano funzioni totali e monotone rispetto al prefisso: se $w$ e' prefisso di $w'$, allora $f(w)$ e' prefisso di $f(w')$. Questo deriva dal fatto che l'output viene prodotto online mentre l'input viene letto.

Automi di Mealy

Un automa di Mealy e' una macchina a stati finiti con output immediato. A ogni passo legge un input dell'ambiente e produce un output del sistema. E' quindi piu' vicino a una strategia che a un riconoscitore.

Perche' si usa

Nel problema di Church e nella sintesi, la soluzione non e' "accetto o rifiuto una parola", ma "dato cio' che fa l'ambiente, quale azione devo produrre?". Se esiste una strategia vincente a memoria finita, la puoi rappresentare come automa di Mealy.

Perche' usarlo rispetto a Büchi/Muller

Büchi e Muller specificano insiemi di comportamenti. Mealy implementa un comportamento: e' un controller. In una pipeline di sintesi, la specifica puo' essere trasformata in un gioco omega-regolare; la strategia vincente estratta diventa una macchina di Mealy.

Apprendimento di automi e algoritmo L*

L'apprendimento di automi non e' una nuova condizione di accettazione. E' un modo per ottenere un DFA che modella un linguaggio regolare sconosciuto.

Nel modello MAT, il Teacher conosce un linguaggio regolare segreto $L_0$, rappresentabile da un DFA. Il Learner puo' fare:

• membership query: "la parola $w$ appartiene a $L_0$?";
• equivalence query: "il mio DFA $\mathcal{A}$ riconosce $L_0$?".

Se l'equivalence query fallisce, il Teacher restituisce un controesempio:

$$ w\in (L_0-L(\mathcal{A}))\cup(L(\mathcal{A})-L_0). $$

Perche' si usa

Serve nella verifica black-box: non conosci la struttura interna del sistema, ma puoi interrogarlo. Costruisci un modello finito appreso e poi applichi tecniche di verifica.

Perche' servono entrambe le query

Solo membership query non bastano a garantire identificazione certa dopo un numero finito di esempi: restano infiniti linguaggi compatibili. Solo equivalence query bastano enumerando tutti gli automi, ma e' brute force. L* combina membership ed equivalence query e sfrutta Myhill-Nerode per arrivare in tempo polinomiale nella dimensione del DFA target, nel modello ideale.

Idea della costruzione

La tabella di osservazione usa prefissi $S$ e suffissi test $T$. Ogni riga rappresenta il comportamento di un prefisso rispetto ai suffissi. Quando la tabella e' chiusa/T-completa e consistente/T-minimale, le righe diventano stati del DFA ipotesi. Il controesempio di una equivalence query raffina $T$ e costringe la tabella a distinguere stati che prima sembravano uguali.

Secondo teorema di Büchi: ponte S1S e automi

Il risultato fondamentale degli appunti e':

$$ \begin{aligned} L\subseteq A^\omega\text{ e' omega-regolare} &\Longleftrightarrow\\ L\text{ e' definibile in S1S}. \end{aligned} $$

Da automa a S1S

Dato un NBA, introduci variabili monadiche $Y_i$ per dire "alla posizione $x$ la run e' nello stato $q_i$". La formula impone:

1. stato iniziale;
2. esattamente uno stato in ogni posizione;
3. rispetto delle transizioni;
4. qualche finale visitato infinitamente spesso.

L'esistenziale sugli insiemi $Y_i$ rappresenta il non determinismo: esiste una run accettante.

Da S1S ad automa

Si procede per induzione sulla formula. Le formule atomiche hanno automi. I connettivi usano chiusure booleane. L'esistenziale $\exists X$ diventa proiezione: l'automa non legge piu' la componente $X$, ma la indovina nondeterministicamente. L'universale si riduce a negazione ed esistenziale.

Perche' e' importante

Questo teorema giustifica il passaggio continuo tra formule logiche e automi. Una formula temporale/logica puo' essere compilata in automa; poi il problema logico diventa un problema su automi, spesso emptiness.

Mini-lista da orale

1. DFA/NFA/epsilon-NFA sono equivalenti su parole finite; la prova chiave e' subset construction ed epsilon-closure.
2. Il complemento di un linguaggio regolare finito si fa facilmente su DFA completi, non direttamente su NFA.
3. Su parole infinite non c'e' stato finale "alla fine"; Büchi richiede finali visitati infinitamente spesso.
4. Per l'intersezione di NBA non basta $F_1\times F_2$; serve GNBA o un contatore.
5. Emptiness Büchi equivale a cercare un finale raggiungibile su un ciclo.
6. Gli NBA sono piu' espressivi dei DBA; "finitamente molte $a$" e' l'esempio da ricordare.
7. Muller deterministico recupera espressivita' omega-regolare e rende il complemento semplice.
8. Rabin serve per condizioni piu' ricche, specialmente su alberi infiniti e S2S.
9. Mealy/transduttori producono output: non sono solo riconoscitori.
10. L* usa Myhill-Nerode in forma algoritmica: le righe della tabella diventano stati del DFA minimo.

Fonti locali usate

• sources/Automi_stati_finiti_parole_finite_Summary.md
• sources/Automi_stati_finiti_parole_infinite_Summary.md
• sources/Learning_Automata_Summary.md
• concepts/Deterministic_Finite_Automata.md
• concepts/Non_Deterministic_Finite_Automata.md
• concepts/Büchi_Automata.md
• concepts/Generalized_Büchi_Automata.md
• concepts/Muller_Automata.md
• concepts/Rabin_Automata.md
• concepts/Tree_Automata.md
• concepts/Sequential_Transducers.md
• concepts/Mealy_Automata.md
• formal_proofs.md
• OCR/anteprime da raw/Riassunti si o.pdf, pagine 42-48, 67-75, 78-85, 88-96.
• Testo estratto da raw/notes.pdf tramite i file work/cap02_notes.txt, work/cap03_notes.txt, work/cap05_notes.txt, work/cap06_notes.txt.