Diario

Progreso

• Lección 1 — Por qué las redes de Petri
• Lección 2 — La definición formal y la matriz de incidencia
• Lección 3 — El grafo de alcanzabilidad
• Lección 4 — Propiedades
• Lección 5 — Invariantes
• Lección 6 — Clases estructurales
• Lección 7 — Modelar la concurrencia
• Lección 8 — Redes coloreadas
• Lección 9 — Tiempo y probabilidad
• Lección 10 — Flujos de trabajo
• Lección 11 — Herramientas e interoperabilidad
• Lección 12 — Aplicaciones industriales
• Lección 13 — Frente a otros formalismos
• Lección 14 — Sobre nuestros propios sistemas
• Lección 15 — Límites y qué viene después
• Lección 16 — Interoperabilidad: preservar el comportamiento, no solo el dibujo (su parte con TINA es una receta pendiente)

QA

Este curso enseña un formalismo y se ejecuta sobre un analizador que escribí yo, así que no hay ningún producto de terceros contra el que abrir incidencias. Lo que la tabla contiene en su lugar es lo que encontró el recalcular: dos defectos en el analizador, y toda afirmación que resultó estar mal cuando se le preguntó al programa. Los números de línea apuntan a los archivos de code/petri-nets.

Esperado	Lo que pasa	Dónde	Medición	Estado
La declaración del PNML indica la codificación que el archivo tiene	XmlWriter.Create(StringBuilder, settings) escribe encoding="utf-16" diga lo que diga XmlWriterSettings.Encoding, porque la codificación viene del TextWriter; los bytes eran UTF-8	Pnml.cs	Los ocho archivos del lote 1 declaraban una codificación que no tenían	Arreglado con una subclase de StringWriter de tres líneas que redefine Encoding (2026-09-15)
El árbol de cobertura se imprime como un árbol	El primer impresor recorría los nodos en orden de creación y los indentaba por profundidad, así que los hijos aparecían bajo hermanos sin relación	Report.cs, Tree	El árbol de 17 nodos de unbounded-producer se leía como un sinsentido; estuve a punto de escribir una lección alrededor	Arreglado: el impresor recorre el árbol en profundidad desde la raíz (2026-09-15)
El marcado más lejano del productor/consumidor está a 6 disparos de M0	Está a 8	Borrador de la lección 3	PathTo(11) devuelve ocho nombres de transición	Corregido antes de publicar (2026-09-15)
handshake tiene 8 marcados alcanzables	Tiene 1, y ese está muerto	Borrador de la lección 2	ReachabilityGraph.Build devuelve un único estado	Corregido antes de publicar (2026-09-15)
Una trampa sin marcas es lo que hace espuria a una solución	Es un sifón. Una trampa que está marcada sigue marcada; un sifón que está vacío se queda vacío	Borrador de la lección 2	Las dos definiciones son duales y el borrador las tenía al revés	Corregido antes de publicar (2026-09-15)
handshake tiene el invariante de transiciones (1, 1)	No tiene ninguno: receive deja caer una marca en served que nada retira, así que ningún multiconjunto de disparos se cancela	Invariants.cs	Invariants.Transitions(handshake).Count es 0, y también para handshake-started	Corregido antes de publicar; la lección 5 usa ahora ese cero como resultado propio (2026-09-17)
mutual-exclusion queda fuera de la clase de elección asimétrica	Queda dentro: idle1• e idle2• están cada uno contenidos en mutex•	Structure.cs	Una prueba unitaria que afirmaba lo contrario falló; los filósofos son la red que sí cae fuera de la clase	Prueba corregida a la respuesta medida (2026-09-17)
{x, y} sigue siendo un sifón minimal cuando los dos hilos toman x primero	Ya no es minimal: {y} sola pasa a ser un sifón, y x queda en {a_has_x, b_has_x, x}	Lección 6, ejercicio 1	two-locks-ordered tiene 4 sifones minimales, todos con una trampa marcada	Corregido antes de publicar, y la predicción equivocada se publica junto a la respuesta correcta (2026-09-17)
El sifón sin trampa de un cerrojo que nunca se suelta es {critical1, critical2, mutex}	Hay dos, {idle1} y {critical2, mutex}; {critical1} resulta ser una trampa	Lección 7, ejercicio 2	Report.Siphons(mutual-exclusion-leaky)	Corregido antes de publicar (2026-09-17)
El árbol de cobertura de una red pequeña y acotada es calculable	CoverabilityTree.Build(Nets.Kanban(1)), una red con 160 marcados alcanzables, no vuelve: limitado a 2 GiB lanza OutOfMemoryException a los 15,5 s, sin límite llegó a 35,7 GB y doce minutos de CPU	CoverabilityTree.cs	160 marcados, ningún resultado; el árbol nunca fusiona dos ramas que llegan al mismo marcado, así que su tamaño sigue al número de caminos	Ni un defecto ni arreglable: la lección 12 imprime dos columnas de cotas en vez de tres, y dice por qué (2026-09-22)
Un verificador de modelos dice cuándo no comprobó nada	TLC con una restricción de estado que excluye el marcado inicial imprime Model checking completed. No error has been found. y 0 distinct states found, sin ninguna línea que lo distinga de una ejecución completa	tla2tools.jar 2.19, herramientas TLA+	queue_5.tla con Cap == 2 frente a un marcado inicial de 5 marcas: 1 estado generado, 0 distintos, salida 0	Reproducido el 2026-09-22; no comunicado aguas arriba — comunicarlo necesita el visto bueno del autor. La lección deduce el tope de los invariantes de plaza en su lugar (2026-09-22)
El árbol de cobertura aproxima, y se equivoca del lado seguro	En una red con un arco inhibidor responde omega para una plaza que nunca lleva dos marcas. La aceleración de Karp y Miller supone que la secuencia que alcanza un marcado que cubre puede repetirse, y un arco inhibidor lo rompe	CoverabilityTree.cs, Inhibitor.cs	self-inhibited: el árbol dice no acotada, el conjunto alcanzable son 2 marcados con p <= 1	Ni un defecto ni arreglable — la acotación es indecidible para estas redes. InhibitorNet viene sin contrapartida de cobertura, e InhibitorTests conserva la contradicción para que nadie añada una (2026-09-22)
Un arco PNML que el lector P/T no modela se rechaza	Un arco marcado <type value="inhibitor"/> se leía como un arco ordinario que consume: la red de admisión de la lección 16 se volvía una red que no admite a nadie, sin error. Tras esa corrección, la revisión encontró el mismo silencio para <type><text>inhibitor</text></type>, un hijo <arctype> y un <type/> vacío	Pnml.cs:68-73; pruebas PetriNetTests.cs:626, PetriNetTests.cs:644	l16 antes de la corrección: READ: 3 states, muerta con los dos jobs probados. PnmlTests: fallaba 1 de 5, luego 5 de 5; tras la revisión, fallaban 4 casos nuevos, luego 12 de 12	Reproducido, corregido localmente para un hijo <type> o <arctype>, como atributo o etiqueta; un tipo anotado en <toolspecific> sigue sin reconocerse (2026-09-27); no verificado de forma independiente
Un marcado rechazado nombra su plaza	FormatException: The input string 'two' was not in a correct format., el mensaje de int.Parse	Pnml.cs:50	l16, E3	Observado, sin corregir (2026-09-27)
El viaje de ida y vuelta de la lección 16 señala cada línea que cambia	Las dos listas se emparejaban con Zip, que se detiene en la más corta. En la lista de E1, un marcado muerto añadido o perdido se seguía viendo, porque la línea de cotas va después, pero contaba una vez y nunca se imprimía; una última línea perdida daba same meaning: yes	Report.cs:321, Program.cs:1130; prueba PetriNetTests.cs:663	Encontrado en la revisión, no en una ejecución. La prueba fallaba con Zip y pasa después. Repetido sobre las 8 líneas de E1: 1 diferencia en vez de 2 para una línea muerta añadida o perdida, 0 en vez de 1 para una última línea perdida	Corregido localmente (2026-09-27); no verificado de forma independiente

Experimentos

Una advertencia antes de la tabla: a diferencia del laboratorio GA, este curso no commitea sus hipótesis a un archivo antes de medir. Las predicciones de abajo se escribieron en mis notas mientras construía cada red y luego se contrastaron con el programa; esa disciplina es más débil, y donde una predicción falló fue el analizador quien lo detectó, no un revisor.

Pregunta	Hipótesis, escrita antes de medir	Resultado	Veredicto
¿Dan los invariantes de plazas las mismas cotas que el grafo de alcanzabilidad?	Dan los mismos seis números sobre el productor y el consumidor	Idénticos, plaza por plaza, y ahora una prueba unitaria falla si divergen: 0 marcados enumerados de un lado, 12 del otro	Confirmada (2026-09-17)
¿La plaza que crece no tiene invariante?	Quitar free quita el invariante que acotaba full	unbounded-producer tiene 2 invariantes de plazas en vez de 3, y a full no lo cubre ninguno	Confirmada, con la salvedad que enuncia la lección: no estar cubierta es una prueba que falta, no una prueba de no acotación (2026-09-17)
¿Pueden los invariantes de plazas excluir una solución espuria?	No — son consecuencias de la ecuación de estado	Las dos soluciones espurias de handshake, (0, 0, 1) y (0, 0, 2), satisfacen todos los invariantes de plazas	Confirmada (2026-09-17)
¿Coincide la condición de Commoner con el grafo de alcanzabilidad?	En todas las redes de libre elección del curso	Coincidencia en las cuatro — producer-consumer viva, start-once y handshake no, connection viva — y una prueba unitaria lo afirma	Confirmada, solo sobre cuatro redes; el teorema en sí está tomado de fuentes secundarias (2026-09-17)
¿Son los circuitos de un grafo marcado los mismos conjuntos que sus invariantes de plazas?	Sí, con las mismas constantes	Los tres circuitos de producer-consumer son {ready, produced} 1, {free, full} 2, {waiting, taken} 1 — los tres invariantes de la lección 5	Confirmada (2026-09-17)
¿Cuántos invariantes de transiciones tiene la red handshake?	(1, 1): receive y luego reply devuelve la marca	Cero, y el prefijo de 500 marcados de handshake-started no contiene ningún marcado alcanzable dos veces	Refutada, y se convirtió en el mejor resultado: una red sin T-invariante nunca puede volver a un marcado que haya dejado (2026-09-17)
¿Cuánto cuesta tomar los tenedores de uno en uno?	Un interbloqueo, y más marcados	Exactamente un marcado muerto a cada tamaño de 2 a 6 filósofos, y 6, 14, 34, 82, 198 marcados frente a 3, 4, 7, 11, 18 de la versión atómica	Confirmada, y la constante 1 fue una sorpresa (2026-09-17)
¿Qué le hace a la estructura invertir un filósofo?	Quita el interbloqueo	Quita un sifón: tres filósofos tienen 7 sifones minimales, uno de ellos — {eating1, fork1, eating2, fork2, eating3, fork3} — sin trampa marcada; invertido, 6 sifones y ninguno sin ella	Confirmada, y es el enunciado estructural de «ordena tus cerrojos» (2026-09-17)
¿Está una transición viva a salvo de la inanición?	No	start_write es L4 en lectores y escritores, y el grafo contiene un ciclo de dos marcados, start_read y luego stop_read, que no la dispara nunca	Confirmada: la vivacidad es «siempre posible», nunca «acaba ocurriendo» (2026-09-17)
¿Encoge el color el espacio de estados?	No — solo pliega el modelo	4 plazas y 4 transiciones a cualquier límite de intentos; el despliegue y el número de marcados alcanzables crecen los dos linealmente, 8, 10, 14, 24, 44 marcados para los límites 2, 3, 5, 10, 20	Confirmada, y es el argumento central de la lección 8 (2026-09-17)
¿Coincide la cadena construida a partir de la red con la fórmula M/M/1/K?	Hasta unos 1e-12, ya que la red es esa cola	La mayor diferencia sobre los seis estados es 5,6e-17, cinco órdenes de magnitud por debajo del 1e-12 que afirma la comprobación	Confirmada, y es la única comprobación independiente que tiene el solucionador estocástico (2026-09-22)
¿Dónde se sitúa una cola finita cuando las llegadas igualan exactamente al servicio?	En algún punto intermedio, con los extremos menos probables	Uniforme: cada longitud de 0 a 5 tiene probabilidad 0,1667, vacía tan a menudo como llena	Refutada, y se convirtió en el resultado más útil: con carga 1 no hay tendencia alguna (2026-09-22)
¿Coincide la solidez con que el cortocircuito sea vivo y acotado?	En las cuatro redes de flujo de trabajo, porque lo dice el teorema	Coincidencia en las cuatro, y una prueba parametrizada falla ahora si se rompe	Confirmada (2026-09-22)
¿Está acotado pero no vivo el cortocircuito de la red bifurcación-Y/convergencia-O?	Acotado: nada se acumula en un proceso 1-seguro	No acotado: la marca sobrante de cada caso se acumula a través de t-star sin límite	Refutada, y es lo que hizo la lección: una marca dejada atrás y un cortocircuito no acotado son el mismo defecto (2026-09-22)
¿Cuántos marcados añade un paso de facturación tras la convergencia?	Dos, uno por rama de la elección	Uno: el marcado en que la marca está en la nueva plaza	Refutada; un paso en secuencia añade un estado venga lo que venga antes, solo la concurrencia multiplica (2026-09-22)
¿Sabe el lector leer un fichero PNML escrito por otra herramienta?	Sí para los P/T; las trampas del ejemplo de la ISO están todas tratadas	2 de 16 leídos, 14 rechazados correctamente por el tipo — y el nombre, que está en la página y no en la red, se perdía	Refutada en parte, y es el único defecto que once lecciones de salida autocomprobada no habían encontrado (2026-09-22)
¿Coincide este analizador con herramientas escritas por otra gente?	Sí en las instancias pequeñas; un desacuerdo en algún punto intermedio no me sorprendería	21 instancias del Model Checking Contest, cuatro números cada una, todas idénticas, más cuatro mayores coincidiendo cifra a cifra	Confirmada, y es la primera comprobación externa que ha tenido este curso (2026-09-22)
¿Da una red Kanban reconstruida desde su descripción publicada la respuesta del concurso?	Sí si el modelado es correcto; es una prueba más dura que leer el fichero del concurso	2 546 432 marcados y 24 460 016 arcos con cinco tarjetas, exactamente los números publicados	Confirmada: se valida el modelado, no solo el lector de PNML (2026-09-22)
¿Cuántos invariantes de plaza tiene la red Kanban?	Cuatro, uno por celda	Seis: las celdas 2 y 3 están sincronizadas, así que también se conservan dos sumas cruzadas, y los invariantes de soporte mínimo no son una base de espacio vectorial	Refutada, y el ejercicio pide al lector derivar los dos de más (2026-09-22)
¿Dónde se detiene la enumeración explícita, y qué la detiene?	Hacia diez millones de marcados, y son los marcados	Son los arcos: 3,4 M de marcados con 13,6 M de arcos caben, 11,5 M de marcados con 1 200 millones de arcos lanzan OutOfMemoryException con un montículo de 8 GiB a los 158 s	Refutada en su causa; tedd hace la misma instancia en 2,3 s porque un diagrama de decisión no almacena arcos (2026-09-22)
¿Encuentra los mismos espacios de estados un verificador escrito por otra gente?	Sí en las redes pequeñas; un desajuste de etiquetado en algún punto no me sorprendería	22 redes con espacio de estados finito, tres números cada una, todos idénticos: los estados distintos, estados generados y profundidad de TLC igualan los marcados, los arcos + 1 y el camino más corto más largo + 1	Confirmada, sobre una traducción cuyo generador no contiene lógica (2026-09-22)
¿Rompe estados generados = arcos + 1 el único marcado alcanzado por dos transiciones distintas?	Sí: la relación de transición de TLA+ es un conjunto de estados, así que order-sound debería imprimir 7 donde el analizador tiene 8 arcos	Imprime 8. TLC cuenta un estado generado por disyunto evaluado, no por sucesor conservado	Refutada, y la razón es la diferencia entre un grafo etiquetado y una relación de transición (2026-09-22)
¿Anuncia una restricción de estado elegida a mano lo que recortó?	Al menos informa de un espacio de estados más pequeño	Nada en absoluto: un tope por debajo del marcado inicial da 0 distinct states found bajo No error has been found	Refutada; por eso el tope de la lección viene de Invariants.PlaceBounds (2026-09-22)
¿Son las redes que los invariantes de plaza no acotan las que no tienen espacio de estados finito?	Sí, para eso sirve un invariante	No: handshake no tiene ningún invariante sobre todas sus plazas y tiene exactamente un marcado, porque está muerta de entrada	Refutada antes de publicarse por TlaTests; un invariante de plaza demuestra la acotación y nunca la refuta (2026-09-22)
¿Cómo crece el coste de la enumeración al añadir componentes?	Como los marcados, que es lo que todo el mundo cita	Como los arcos por marcado: de 1,3 a 3,9 en seis filósofos, de 3,9 a 8,8 en cuatro tarjetas Kanban, porque cada componente multiplica las maneras de abandonar cada estado existente	Confirmada como forma, y se aplana: la razón es un grado de salida medio y no puede superar el número de transiciones (2026-09-22)
¿Qué cuesta la atomicidad en espacio de estados?	Un factor constante	Filósofos tomando los dos tenedores de golpe: 29 marcados con siete. Un tenedor cada vez: 198 con seis. La diferencia es entrelazado, y es lo que quitan los desplegados	Medida; ni desplegado ni reducción de orden parcial está implementado aquí, y la lección lo dice (2026-09-22)
¿Sigue siendo el árbol de cobertura una aproximación segura cuando la red gana un arco inhibidor?	Sí — sobreaproxima por construcción, así que debería responder omega demasiado a menudo, nunca equivocadamente	Responde omega para una plaza que nunca lleva dos marcas. self-inhibited tiene 2 marcados alcanzables y el árbol dice no acotada	Refutada. La premisa de la aceleración falla, y falla porque la acotación es indecidible aquí, así que no hay nada que arreglar (2026-09-22)
¿Conserva una red PNML escrita a mano su comportamiento a través de una lectura, una escritura y una relectura?	Sí: mismos identificadores, marcado, pesos y transiciones habilitadas, 9 marcados, un marcado muerto, running<=1; las posiciones descartadas	Exactamente eso, y la segunda escritura es idéntica byte a byte a la primera; 9 posiciones de entrada, 0 de salida	Confirmado, prerregistrado en un fichero (2026-09-27)
¿Qué hace olvidar la liberación?	7 marcados, y un marcado muerto con un job probado y nunca admitido, a 4 disparos	waiting=0 tested=1 capacity=0 running=0 done=1 tras test test admit finish	Confirmado (2026-09-27)
¿Se rechazan los ficheros mal formados?	Los dos: un arco hacia un nodo inexistente, y un marcado escrito two	Rechazados, con ArgumentException y FormatException	Confirmado (2026-09-27)
¿Se rechaza un tipo de arco que el lector no modela?	No: según la lectura de Pnml.Parse, un arco inhibidor se lee como uno ordinario, lo que da 3 marcados	READ: 3 states, muerta con tested=2	Confirmado, y era un defecto: los arcos marcados con un hijo <type> o <arctype> ahora se rechazan (2026-09-27)

2026-09-15 — Lecciones 1 a 4, y el analizador sobre el que se ejecutan

Por qué escribir un analizador. Existen herramientas maduras — TINA, LoLA, CPN Tools, GreatSPN, TAPAAL — y la lección 11 las usará. Aun así escribí uno pequeño, por tres razones. Un curso cuyas salidas compara la CI necesita un programa cuya salida yo controle hasta el orden. Un lector que tiene la regla de disparo delante en C# la entiende más rápido que uno que tiene una captura de pantalla de una interfaz gráfica. Y el analizador es la única forma honesta de escribir estas lecciones: los doce marcados, los diecisiete nodos del árbol y las dos soluciones espurias los imprime él, no los recuerdo yo.

Son unas 1 400 líneas repartidas en diez archivos de code/petri-nets/PetriNets: la red y la regla de disparo, PNML de lectura y de escritura, el grafo de alcanzabilidad, el árbol de cobertura de Karp–Miller, los invariantes de plazas y de transiciones por eliminación de Farkas, la ecuación de estado y un impresor. El SDK de .NET de esta máquina es el 10.0.112, sobre .NET 10.0.12; global.json fija la banda 10.0.1xx con rollForward: latestFeature, de modo que la versión preliminar 11.0.100, también instalada, no se elige.

El determinismo fue la restricción que dio forma al código. Todo lo que una lección cita tiene que salir igual en Windows, Linux y macOS, y las colecciones basadas en hash no lo prometen. Por eso el grafo de alcanzabilidad se construye en anchura y numera sus estados en orden de descubrimiento; los disparos se ordenan por estado origen y luego por transición antes de devolverlos; los invariantes se normalizan por su máximo común divisor y se ordenan; el escritor de PNML emite finales de línea LF y una indentación fija. check.sh compara cuatro salidas de lección y ocho archivos PNML, así que un cambio que reordene algo falla de inmediato en vez de dejar una lección equivocada en silencio.

Sorpresas:

• El búfer sin freno está a una plaza de distancia. Quitar free y sus dos arcos del productor/consumidor convierte una red de doce marcados en una cuyo conjunto alcanzable es infinito. Nada en la imagen avisa; lo hace la ausencia de una plaza. Ahora leo «qué plaza detiene esta transición» como la primera pregunta que hacerle a una red.
• Los números de Lucas. El grafo de alcanzabilidad de n filósofos tiene 3, 4, 7, 11, 18, 29, 47, 76, 123 marcados para n = 2 … 10. Esperaba algo como 2ⁿ y obtuve una sucesión donde cada término es la suma de los dos anteriores. Tiene sentido en cuanto ves que un marcado es una elección de qué filósofos comen, sin que dos sean vecinos — los conjuntos independientes de un ciclo, contados por los números de Lucas. Un recordatorio agradable de que el espacio de estados tiene estructura, que es justo lo que explotan las técnicas de reducción de la lección 15.
• El árbol de cobertura es mayor que el grafo al que sustituye. Para el productor/consumidor acotado: 56 nodos de árbol para 12 marcados. Un árbol no comparte nada, así que cada marcado se repite una vez por cada camino que llega a él. El árbol solo sale a cuenta cuando el grafo no existe en absoluto.
• Las soluciones espurias son más difíciles de construir que de describir. Quería un marcado que satisficiera M = M0 + C x sin ser alcanzable, y mis cuatro primeros intentos fallaron por la misma razón: en esas redes todo ciclo llevaba una marca, así que la ecuación de estado y la regla de disparo coincidían. La que funciona es la red handshake, donde receive y reply se pasan una sola marca y nadie envía nunca la primera petición — la ecuación deja que receive tome prestada la marca que reply solo produciría después. En vez de fiarme de la construcción, el analizador ahora enumera todos los marcados hasta un presupuesto de marcas e informa de los que la ecuación acepta y el grafo no contiene; encuentra (0, 0, 1) y (0, 0, 2). Una prueba comprueba además lo contrario para el productor/consumidor, que no tiene ninguna.

Dos errores míos, los dos de impresión más que de matemáticas:

• Un PNML que mentía sobre su codificación. XmlWriter.Create(StringBuilder, settings) escribe encoding="utf-16" en la declaración diga lo que diga XmlWriterSettings.Encoding, porque la codificación se toma del TextWriter. Los archivos se escribían en UTF-8, así que cada uno declaraba una codificación que no tenía — inofensivo para mi propio lector, una trampa para cualquier herramienta que crea la declaración. Arreglado con una subclase de StringWriter de tres líneas que redefine Encoding.
• Un árbol de cobertura impreso en el orden equivocado. La primera versión imprimía los nodos en orden de creación y los indentaba por profundidad, lo que parece un árbol sin serlo: los hijos de un nodo creado más tarde aparecían bajo un hermano sin relación. La salida no tenía sentido y estuve a punto de escribir una lección alrededor. El impresor ahora recorre el árbol en profundidad desde la raíz.

Lo que no he podido verificar, y he marcado como tal:

• El artículo de síntesis de Murata está tras el muro de pago de la IEEE, e IEEE Xplore rechazó la petición sin más. El registro bibliográfico está confirmado a través de Crossref — Proceedings of the IEEE 77(4), abril de 1989, páginas 541–580, doi:10.1109/5.24143 — y las definiciones que le atribuyo son las estándar, pero no he leído el artículo en sí. Donde tendría que apoyarme en él para una afirmación que no puedo comprobar de otro modo — que la ecuación de estado es necesaria y suficiente para las redes acíclicas — la lección 2 dice por verificar en lugar de afirmarlo.
• El informe técnico de Yale de Lipton, 1976, para la cota inferior EXPSPACE de la cobertura, está citado a partir de fuentes secundarias. La cota superior correspondiente de Rackoff sí está confirmada: Theoretical Computer Science 6(2), 1978, páginas 223–231.
• Todo lo relativo a la complejidad de la alcanzabilidad está anclado a artículos cuyos registros comprobé en Crossref: decidibilidad por Mayr (STOC 1981) y Kosaraju (STOC 1982), cota superior ackermanniana por Leroux y Schmitz (LICS 2019), y cota inferior correspondiente por Czerwiński y Orlikowski y, de forma independiente, Leroux, ambos en FOCS 2021. Quería el estado actual de esa cuestión en vez del «decidible, complejidad abierta» de los manuales más antiguos, y 2021 la cerró.
• ISO/IEC 15909 tiene tres partes, y las comprobé las tres en iso.org: la parte 1 (2019, conceptos), la parte 2 (2011, el formato de intercambio que escribe este curso, confirmada por última vez en 2024) y la parte 3 (2021, extensiones). La norma en sí cuesta 227 CHF y no la he leído; el PNML que escribe el analizador sigue la gramática pública de pnml.org y da la vuelta completa por su propio lector, que es todo lo que este curso afirma.

Queda por hacer:

• El flujo de trabajo de CI .github/workflows/petri-nets-examples.yml está escrito pero no confirmado: el token disponible aquí no tiene el alcance workflow. Nada en las lecciones afirma tener una CI en verde mientras no se haya ejecutado.
• El dogfooding de la lección 14 — una tubería Channel<T> de Guitar Alchemist, una topología de RabbitMQ, una actualización progresiva de Kubernetes, una tubería de agentes — no ha empezado. El lote 1 solo modela sistemas de manual, y lo dice.

2026-09-15 — Traducciones

Las versiones francesa y española de la misión, de las lecciones 1 a 4 y de este diario se produjeron a partir del commit en inglés, copiando los bloques de código con un script y traduciendo solo la prosa, los comentarios del código y las etiquetas de Mermaid. Los nombres de las plazas y de las transiciones dentro de las redes forman parte de la salida del programa: se quedan en inglés en los tres idiomas, porque traducirlos haría que los listados dejaran de coincidir con expected/.

2026-09-17 — Lecciones 5 a 8, y las cuatro cosas que el analizador me dijo que tenía mal

La cuestión de la CI del lote 1 está zanjada: .github/workflows/petri-nets-examples.yml se commiteó y está en verde en Ubuntu, Windows y macOS desde el 2026-09-16, en 53ceefc. Ahora ejecuta ocho lecciones en vez de cuatro.

Lo que creció el analizador. 672 líneas en tres archivos nuevos, más añadidos a cuatro existentes:

• Structure.cs — las clases (máquina de estados, grafo marcado, libre elección, libre elección extendida, elección asimétrica, ordinaria, pura, fuertemente conexa), los circuitos elementales, los sifones y las trampas por fuerza bruta sobre los subconjuntos de plazas, y la mayor trampa dentro de un conjunto por el punto fijo de siempre.
• Coloured.cs — conjuntos de colores, guardas, expresiones de arco, una regla de disparo sobre marcados coloreados, y Unfold() hacia una red P/T ordinaria.
• En Invariants.cs, la cota que cada plaza obtiene solo de los invariantes, y el rango de C por eliminación entera exacta.
• En ReachabilityGraph.cs, CycleAvoiding(t): un ciclo alcanzable desde M0 que nunca dispara t. Dos docenas de líneas, y es lo que convierte «esta transición es viva» en «y aquí está la ejecución en la que no ocurre nunca».

Se añadieron siete redes a las que exporta el lote 1 — connection, handshake-started, readers-writers, counting-semaphore, los filósofos tomando un tenedor cada vez con y sin un orden impuesto, y el despliegue de la red coloreada de reintentos — y una octava, el cerrojo que nunca se suelta, existe solo para romperse en el ejercicio de la lección 7 y no se exporta. Toda red exportada se regenera y se compara con check.sh. Las pruebas unitarias pasaron de 30 a 52.

El resultado que no esperaba, y que me quedé. La lección 5 iba a terminar en «existe un invariante de transiciones pero no puede dispararse», con la red handshake como ejemplo. La red handshake no tiene ningún invariante de transiciones. receive mete una marca en served y nada la saca nunca, así que ningún multiconjunto no vacío de disparos se cancela; y en cuanto eso es cierto, la red nunca puede volver a un marcado que haya dejado. La lección dice ahora eso, que es un hecho mejor, y two-locks lleva el argumento original — tiene dos T-invariantes y un marcado desde el que ninguno puede empezar.

Otras tres predicciones que el programa rechazó, todas en la tabla de QA de arriba: mutual-exclusion sí es una red de elección asimétrica (una prueba unitaria que afirmaba lo contrario falló), {x, y} deja de ser un sifón minimal en cuanto los dos hilos toman x primero, y el cerrojo que nunca se suelta tiene dos sifones sin trampa en vez del único que yo nombré. La lección 6 publica la predicción equivocada junto a la respuesta correcta, porque la forma del error — suponer que un conjunto sigue siendo minimal cuando la estructura a su alrededor cambia — es más útil que la respuesta.

Sorpresas que merece la pena conservar:

• Los filósofos se interbloquean exactamente una vez. De dos a seis filósofos, un tenedor cada vez: 1 marcado muerto siempre, de 6, 14, 34, 82, 198. Esperaba que el número creciera con el anillo. No crece, porque la única forma de perder es que todo el mundo tenga un tenedor, y hay un solo marcado así.
• La inanición mide dos marcados. La red de lectores y escritores es viva, y la ejecución en la que el escritor nunca entra es start_read, stop_read, repetido. Encontrarla costó una búsqueda en profundidad sobre el grafo con una transición borrada, y verla impresa hizo concreta la diferencia entre vivacidad y equidad de una forma que las definiciones nunca lograron.
• El color no compra nada en el análisis. La red de reintentos conserva cuatro plazas y cuatro transiciones tanto si el límite de intentos es 2 como si es 20; el despliegue pasa de 8 plazas a 44 y los marcados alcanzables de 8 a 44. Sabía que la teoría decía esto; ver las columnas de la izquierda quietas mientras las de la derecha trepan es lo que lo hace calar.
• La condición de Commoner se gana el sueldo en handshake-started. El grafo de alcanzabilidad de esa red es infinito — el analizador se rinde a los 500 marcados — y el árbol de cobertura solo puede informar de que no está acotada y de que ninguna transición está muerta. La condición de sifones y trampas responde viva de todos modos, en lo que se tarda en enumerar los subconjuntos de tres plazas. Es el primer sitio de este curso donde el método estructural hace algo que la enumeración no puede hacer en absoluto.

Lo que no he podido verificar, y he marcado como tal:

• Hack 1972 es donde está enunciado el teorema de vivacidad de Commoner para las redes de libre elección. El registro está confirmado en DSpace@MIT — Analysis of production schemata by Petri nets, MIT-LCS-TR-094, febrero de 1972, handle 1721.1/149406 — y el PDF es de acceso abierto, pero la descarga está tras una comprobación antibots que rechazó todas mis peticiones, así que no lo he leído. La redacción del teorema en la lección 6 viene de fuentes secundarias. Lo que la lección afirma con su propia evidencia es más estrecho y está comprobado: la condición y el grafo de alcanzabilidad coinciden en las cuatro redes de libre elección de este curso, y una prueba unitaria falla si dejan de coincidir.
• Commoner, Holt, Even y Pnueli 1971 para los teoremas de los grafos marcados: registro confirmado a través de Crossref (JCSS 5(5), páginas 511–523, doi:10.1016/S0022-0000(71)80013-2), artículo tras el muro de pago de Elsevier, no leído.
• Desel y Esparza 1995, Free Choice Petri Nets: registro confirmado en Cambridge Core, doi:10.1017/CBO9780511526558, no leído.
• Jensen y Kristensen 2009 para las redes coloreadas: registro confirmado a través de Crossref, doi:10.1007/b95112, no leído. ISO/IEC 15909-1:2019, donde se define la subclase de las redes simétricas, sigue costando 227 CHF y sigue sin leerse.
• Dijkstra 1971 para los filósofos y el orden de los recursos: registro confirmado a través de Crossref, doi:10.1007/BF00289519, no leído.
• El ejercicio 3 de la lección 7 — los filósofos con un tiempo de espera — está argumentado, no construido. Está marcado por verificar en la propia lección.

Una cosa que es honestamente más débil de lo que parece. Toda afirmación de «ningún marcado enumerado» de las lecciones 5 y 6 es cierta del método, y el mismo programa construye luego el grafo de alcanzabilidad de todas formas para comprobar el método. Ese es el orden correcto para un curso, y significa que ninguna de estas lecciones demuestra el método sobre una red donde la enumeración fallaría de verdad — salvo handshake-started, que es la única red de aquí cuyo grafo no existe.

2026-09-21 — Primer oráculo ejecutable del ciclo de vida C#

La lección 14 conecta ahora el modelo formal con las formas de fallo medidas en las lecciones 6 y 9 de C# avanzado. Añadí un pipeline finito de una plaza con lugares explícitos succeeded, failed y cancelled. Su grafo completo tiene ocho marcados y tres marcados muertos; todos son terminales intencionales, así que no hay marcados muertos no terminales. Cinco pruebas enfocadas preservan esa clasificación y el invariante de capacidad free + queued = 1, y el fixture PNML se regenera con el resto del curso.

La corrección importante fue semántica: DeadStates significa que ninguna transición está habilitada, por lo que el final correcto de un workflow finito también está muerto. «Sin interbloqueo» es el oráculo equivocado para un pipeline que termina. El contrato ejecutable es, en cambio, un grafo completo cuyos marcados muertos contienen exactamente una marca terminal con nombre. La página también etiqueta honestamente los ejemplos Channel con forma de GA como reproducciones del mecanismo, no como pruebas de regresión de los binarios actuales. RabbitMQ, Redis y Kubernetes siguen siendo experimentos posteriores.

2026-09-22 — Lección 9, y una cola resuelta dos veces

La lección 9 convierte el grafo de alcanzabilidad en una cadena de Markov de tiempo continuo. Stochastic.cs construye la matriz de tasas a partir del grafo, elimina los estados evanescentes que crea una transición inmediata, y resuelve piQ = 0 por eliminación de Gauss con pivoteo parcial. La pregunta abierta del 2026-09-17 la zanja la propia lección: el curso enseña primero el formalismo estocástico, porque es aquel cuya semántica se sigue de la red no temporizada sin una nueva regla de disparo, y los retardos deterministas de Merlin y de Ramchandani quedan nombrados como la teoría más difícil que son.

La decisión de diseño que merece anotarse es la de la comprobación. Una cola con una transición de llegada, una de servicio y retardos exponenciales es una cola M/M/1/K, así que la misma distribución puede calcularse dos veces por caminos que no comparten código: la cadena construida a partir de la red, y la forma cerrada calculada a partir de rho. Las seis probabilidades coinciden con unos 1e-16. Esa coincidencia es la única razón para fiarse del analizador en las redes cuya respuesta no se conoce en forma cerrada — es decir, todas, después de esta lección.

Dos cosas salieron de escribirla que no había previsto. Primero, la comprobación de la lección imprime un veredicto en lugar de la diferencia: las cifras de la diferencia dependen del orden en que la máquina sumó los números en coma flotante, así que imprimirla haría fallar check.sh en uno de los tres sistemas operativos por un motivo ajeno a las redes de Petri. Segundo, el caso de carga 1 es más interesante que el de carga 0,75 — la cola no se concentra en el medio, es uniforme sobre todas las longitudes, lo que dice sobre «dimensionado exactamente a capacidad» algo que ninguna media diría.

La ley de Little se usa como una tercera comprobación independiente y no como resultado: vale para todo sistema estable sin hipótesis, así que si la cadena la violara, la equivocada sería la cadena.

check.sh ejecuta ahora l9 y lo compara con expected/l9.txt. Pasan 57 pruebas, y l1 a l9, l14, music, chat y nets coinciden todos.

2026-09-22 — Lección 10, y la solidez decidida dos veces

La lección 10 añade Workflow.cs: la comprobación estructural de la red de flujo de trabajo, las tres condiciones de solidez, y el cortocircuito del teorema de van der Aalst. Es el teorema lo que hace que la lección merezca escribirse — la solidez se decide una vez sobre sus propias condiciones y otra como «la red cortocircuitada es viva y acotada», con código de la lección 4 que no sabe nada de procesos, y una prueba parametrizada falla si alguna vez dejan de coincidir en las cuatro redes de ejemplo.

Dos cosas que no esperaba, ambas ya en la lección.

La primera: order-and-xor — la bifurcación Y convergida por una O exclusiva, el error más común de los procesos dibujados — no se atasca solo a veces. Su marcado final es inalcanzable desde cualquier sitio: el estado final correcto no existe en la red en absoluto. Toda tarea puede ejecutarse todavía, así que una batería de pruebas que ejercite cada tarea pasa sobre un proceso que nunca puede terminar correctamente. El informe se cambió para decir eso en una línea en vez de listar los diez marcados como «atascados», lo que era cierto e inútil.

La segunda: su cortocircuito no está acotado. Yo esperaba «acotado pero no vivo». La marca sobrante de cada caso se acumula a través de t-star sin límite, lo que significa que «la terminación limpia falla» y «el cortocircuito no está acotado» son el mismo defecto contado una vez por caso o contado para siempre. La red espejo, order-xor-and, está acotada y no es viva — así que cada mitad del teorema la necesita uno de los dos fallos de ejemplo, lo que es mejor demostración que la que tenía planeada.

También me equivoqué en un ejercicio antes de comprobarlo. Al añadir un paso de facturación tras la convergencia, predije que el número de marcados pasaría de 6 a 8; el analizador dijo 7. Un paso en secuencia añade un marcado venga lo que venga antes, porque solo la concurrencia multiplica. La predicción equivocada se publica con la respuesta correcta, y el motivo se ha convertido en el argumento del ejercicio.

check.sh ejecuta l10; pasan 66 pruebas y l1 a l10, l14, music, chat y nets coinciden todos.

2026-09-22 — Lección 11, y el primer fichero que este repositorio no escribió

Diez lecciones se habían comprobado contra un analizador que escribí yo, sobre redes que escribí yo. La lección 11 rompe ese círculo: descarga los dieciséis ejemplos PNML que acompañan a ePNK, la implementación de referencia del metamodelo de la norma, y se los entrega al lector.

Catorce fueron rechazados correctamente — diez redes de alto nivel, tres redes simétricas, y una que merece su propia frase. simple-dot-net.pnml es una red P/T corriente escrita en la gramática de alto nivel sobre el conjunto de colores de un solo valor dot: el mismo comportamiento que todas las redes de este curso, otro lenguaje, ilegible. «PNML» nombra una sintaxis más una URI de tipo, no un formato.

Los dos ficheros aceptados encontraron el defecto que esperaba. El ejemplo de la propia norma, tal como lo escribe ePNK, pone el nombre de la red en la <page> y no en el <net>, no le da nombre alguno a la transición, y mete un bloque <toolspecific> dentro de <initialMarking> antes de su <text>. El lector sobrevivió a tres de esas trampas y perdió el nombre: el fichero volvía llamándose n1, su identificador. Tres líneas en Pnml.cs lo arreglaron, y una prueba unitaria lleva ahora toda la forma incómoda como cadena, de modo que la corrección no puede regresar sin la descarga de ePNK.

Ese es todo el argumento de la lección, y costó tres minutos: diez lecciones de salida coherente consigo misma no habían encontrado nada, y el primer fichero ajeno encontró algo.

Dos cosas que no pude hacer. La gramática P/T no está entre los .rng publicados en pnml.org — pnmlcoremodel.rng, anyElement.rng, conventions.rng y las que no dependen del tipo sí están, ptnet.rng devuelve un 404 — así que la salida del analizador sigue sin haberse validado nunca contra un esquema. Y los ejemplos de ePNK están bajo EPL-1.0, así que no se incluyen: check.sh ejecuta l11 sin ellos e imprime un aviso, y el listado ajeno de la lección está marcado como procedente de una ejecución manual fechada, no de la comparación.

check.sh ejecuta l11; pasan 67 pruebas y l1 a l11, l14, music, chat y nets coinciden todos.

2026-09-22 — Lección 12, y la primera vez que había una respuesta de otros

Once lecciones comprobaron este analizador contra sí mismo. La lección 12 lo comprueba contra el Model Checking Contest, que publica tanto una colección pública de modelos industriales como las respuestas que sus participantes calcularon sobre ellos.

El examen StateSpace pide cuatro números por instancia — marcados, arcos, marcas máximas en una plaza, marcas máximas en un marcado — y raw-result-analysis.csv lleva una columna estimated result con el valor en el que coincide una mayoría de herramientas, ponderada por la confianza. Eso es un oráculo. Tomé las veintiuna instancias P/T cuyos cuatro números se publican enteros — taller flexible, protocolos, memoria compartida, bioquímica, y un modelo de seguridad — y ejecuté el analizador sobre todas.

Veintiuna instancias, ochenta y cuatro números, ni un desacuerdo. Luego cuatro más por encima de la línea de lo «publicado entero» — FMS-PT-00005, Kanban-PT-00005, Peterson-PT-3, Dekker-PT-010 — usando las cifras que varias herramientas imprimieron idénticas. Sigue sin haber desacuerdo. Es la primera validación externa que ha tenido este curso, y estuvo disponible todo el tiempo.

La red Kanban está reconstruida aquí en vez de leída del fichero del concurso, a partir de la imagen y los nombres de plazas de la propia ficha del concurso. Da 2 546 432 marcados y 24 460 016 arcos con cinco tarjetas, que es lo que el concurso publica, así que el modelado es correcto y no solo el lector. check.sh la ejecuta con tres tarjetas para seguir siendo rápido.

Dos cosas en las que me equivoqué, ambas publicadas en la lección con la respuesta medida. Esperaba cuatro invariantes de plaza, uno por celda; hay seis, porque las celdas 2 y 3 están sincronizadas y la base de soporte mínimo no es una base de espacio vectorial. Y esperaba que el muro fuera el número de marcados; es el número de arcos. Peterson-PT-3 tiene 3,4 M de marcados y 13,6 M de arcos y cabe; Dekker-PT-020 tiene 11,5 M de marcados y 1 200 millones de arcos y lanza OutOfMemoryException con un montículo de 8 GiB a los 158 s. tedd hace esa misma instancia en 2,3 s y 1,2 GB, porque un diagrama de decisión nunca almacena un arco.

Y una cosa que la lección encontró en el código de este repositorio: CoverabilityTree.Build no termina de forma útil con kanban-1, una red con 160 marcados alcanzables. Limitado a 2 GiB lanza a los 15,5 s; sin límite llegó a 35,7 GB y doce minutos de CPU sin volver. No es un error — el árbol nunca fusiona ramas, así que su tamaño sigue al número de caminos — pero significa que la herramienta de la lección 3 es inutilizable en cualquier cosa industrial, y la lección lo dice en vez de imprimir una tercera columna.

2026-09-22 — Lección 13, y un espacio de estados calculado dos veces

La lección 12 tomó prestadas las respuestas de otros. La lección 13 toma prestado su motor: las 25 redes se escriben como módulos TLA+ y se le entregan a TLC, que enumera los mismos espacios de estados desde el otro lado.

La traducción resultó caber en una frase. Haz que la única variable TLA+ sea una función de las plazas a los naturales y un estado es un marcado; la regla de disparo cabe entonces en seis líneas, escritas una vez a mano en tla/PetriNet.tla, y Tla.cs genera solo la red. Nada del generador contiene lógica, y esa es la única razón por la que su salida merece compararse.

TLC termina con tres números. Antes de ejecutar ninguno anoté lo que cada uno debía valer: estados distintos = marcados, estados generados = arcos + 1, profundidad = el más largo de los caminos más cortos + 1. Veintidós redes con espacio de estados finito, sesenta y seis números, ni un desacuerdo.

Dos de las tres apuestas acertaron por la razón equivocada, y la lección conserva ambas.

order-sound es la única red donde dos transiciones llevan de un marcado al mismo marcado — ship y cancel. El grafo de una red de Petri está etiquetado y el de TLA+ no, así que ese paso debería haber desaparecido del recuento de TLC: 8 frente a 7. Es 8 frente a 8, porque TLC cuenta un estado generado por disyunto evaluado, no por sucesor conservado. La regla sobrevive a la colisión por accidente, y el accidente es la diferencia entre los formalismos: pregunta qué puede pasar a continuación y TLA+ responde con estados, pregunta qué puede pasar y una red responde con transiciones.

La primera ejecución se detuvo pronto en retry — tres marcados de ocho — y en pipeline-lifecycle. No era un fallo de traducción: TLC llama interbloqueo a un estado sin sucesor y se para, porque una especificación TLA+ describe algo que funciona para siempre. El marcado final de una red de flujo de trabajo es ese estado, y la lección 10 se pasa entera definiendo la solidez como alcanzarlo. CHECK_DEADLOCK FALSE es el punto donde los dos formalismos no coinciden en si los sistemas terminan.

Luego el número que debería inquietar a cualquiera que haya elegido una cota a mano. Pon el tope de queue-5 en 2 — su marcado inicial lleva cinco marcas — y TLC descarta el estado inicial, no comprueba nada, e imprime Model checking completed. No error has been found. con 0 distinct states found. No hay ninguna línea en esa salida que la distinga de una ejecución completa. Por eso el tope de esta lección es Invariants.PlaceBounds, y por eso la lección imprime cuáles de las cuatro redes recibieron uno que no supo demostrar.

Y una afirmación mía que las pruebas refutaron antes de publicarla: había escrito que las cuatro redes que los invariantes no acotan son las cuatro sin grafo de alcanzabilidad finito. handshake no tiene ningún invariante sobre todas sus plazas y tiene exactamente un marcado, porque está muerta de entrada. Un invariante de plaza demuestra la acotación y nunca la refuta.

Statecharts, álgebras de procesos y autómatas temporizados se comparan en prosa y se marcan como no ejecutados. Lo único que vale la pena llevarse es el canje que todos hacen: un álgebra de procesos compone, P | Q es un término, y puedes razonar sobre P solo — mientras que una red debe existir entera antes de que un sifón, una trampa o un invariante signifiquen algo. Es precisamente por eso que la red Kanban de la lección 12 tuvo que reconstruirse entera en vez de ensamblarse con cuatro copias de una celda.

2026-09-22 — Lección 15, y un algoritmo correcto que aun así se equivoca

La última lección del plan pregunta qué no sabe hacer el analizador. Tres de las respuestas son mediciones en vez de argumentos.

El crecimiento tiene forma. La lección 12 encontró que el muro de memoria es de arcos. Esta lección ve subir los arcos por marcado a medida que se añaden componentes: 1,3 → 3,9 en seis filósofos, 3,9 → 7,6 en tres tarjetas Kanban, 8,8 con cuatro tarjetas (454 475 marcados, 3 979 850 arcos — la extrapolación lineal anunciaba 8,9 y se pasó, como debe, porque la razón es un grado de salida medio y Nets.Kanban tiene dieciséis transiciones con cualquier número de tarjetas). Cada componente añadido no solo trae sus propios estados; multiplica las maneras de abandonar cada estado existente.

El entrelazado se ve. Filósofos tomando los dos tenedores de golpe: 29 marcados con siete. Un tenedor cada vez: 198 con seis. Mismo formalismo, misma máquina. La diferencia es exactamente lo que los desplegados y la reducción de orden parcial existen para quitar, y ninguno de los dos está implementado aquí — la lección lo dice en vez de dar a entender lo contrario.

Y el hallazgo sobre el que se construye la lección. PetriNets/Inhibitor.cs añade los arcos inhibidores: una transición que solo se dispara mientras una plaza está vacía. flush(n) dice entonces cuando todos los artículos se hayan movido, terminar en n + 2 marcados, donde la red ordinaria dice en algún momento, terminar en 2(n + 1). Los marcados de más no son complejidad, son respuestas falsas.

El coste llega de inmediato. self-inhibited es una plaza, una transición, y un arco de la plaza a la transición que la llena. El árbol de Karp y Miller, ejecutado sobre la red ordinaria subyacente, responde ω. El conjunto alcanzable es de dos marcados y la plaza nunca lleva más de una marca. La aceleración supone que la secuencia entre un marcado y el ancestro que cubre puede repetirse; aquí la marca que apareció es lo que ahora bloquea la transición que la produjo. El árbol no es lento, es falso — y tiene que serlo, porque la comprobación a cero convierte dos plazas en los contadores de una máquina de dos contadores y hace indecidible la acotación. InhibitorNet tiene por eso un constructor de conjunto alcanzable con un límite y ninguna contrapartida de cobertura: incompleto significa «no dentro del límite», nunca «no acotada».

Esa es también la respuesta a por qué todas las demás redes de este repositorio son redes plaza/transición ordinarias. No es conservadurismo. Es la línea más allá de la cual los veredictos del analizador dejan de significar nada.

2026-09-27 — Lección 16, y un fichero que se leía y significaba otra cosa

La pregunta vino de fuera del curso: ¿conserva una red su comportamiento de una herramienta a otra, y no solo su dibujo? Todo se ejecutó en e3cb4be, solo con el analizador de este curso. TINA, pm4py y Graphviz no están instalados en esta máquina, así que la parte de la lección con TINA es una receta, y lo dice.

Por una vez, las predicciones fueron a un fichero antes de la primera ejecución: interop/preregistration.md, con hash tomado a las 10:54:11 EDT (SHA-256 44fd0d02…). Cuatro experimentos, cada uno con sus números escritos primero:

• E1, la ida y vuelta de una red de admisión escrita a mano. Reproducido como se predijo:
  • 9 marcados, y un marcado muerto, que es el final previsto;
  • running<=1;
  • el mismo significado tras escribir la red y releerla;
  • 9 posiciones descartadas.
• E2, la liberación olvidada. Reproducido: 7 marcados, y un marcado muerto tras 4 disparos, test test admit finish.
• E3, dos ficheros mal formados: un arco hacia un nodo inexistente, y un marcado escrito two.
  • Los dos se rechazan. Reproducido.
  • El segundo rechazo es el mensaje de int.Parse, que no nombra la plaza. Observado, se deja así.
• E4, un arco inhibidor marcado <type value="inhibitor"/>.
  • Se predijo, leyendo Pnml.Parse, que se leería como un arco ordinario. Así fue: READ: 3 states, una red que no admite a nadie. Reproducido.
  • Luego corregido localmente: el lector ahora rechaza cualquier tipo de arco que no sea normal.
  • La prueba unitaria falló primero (1 de las 5 pruebas PNML) y pasó tras la corrección (5 de 5). check.sh pasa 92 pruebas y 19 salidas comparadas, l16 incluida.

Tiempos: el build de Examples tardó 5 s, cada ejecución de l16 menos de un segundo, y el check.sh completo 47 s.

Límites: es el espacio de estados de una red de 9 marcados. No es una ejecución de jobs reales, ni una prueba de equidad. Nada de esto está aún verificado de forma independiente ni publicado.

2026-09-27 — Lección 16 tras la revisión

Codex revisó la PR #28 en 3c1ff61 y pidió tres reparaciones. Las tres están hechas en 3242df6, con las pruebas escritas antes de las correcciones:

• La comparación del viaje de ida y vuelta truncaba. Emparejaba las dos listas con Zip, que se detiene en la más corta. En la lista de E1 eso no ocultaba del todo un cambio, porque la línea de cotas va al final, pero una última línea perdida habría impreso same meaning: yes. Report.LineDifferences empareja ahora cada línea.
• La guarda sobre el tipo de arco leía una sola codificación, <type value="…"/>. Ahora también rechaza una etiqueta <type>, un hijo <arctype> en sus dos formas y un <type/> vacío. Un tipo anotado en un bloque <toolspecific> sigue sin reconocerse, y la lección 16 ahora lo dice.
• Las filas de QA enlazaban blob/main. Ahora apuntan a líneas de 3242df6.

Antes de las correcciones fallaban 5 de las 12 PnmlTests: los 4 casos de tipo de arco y la comparación. Después pasan las 12. check.sh pasa 99 pruebas y 19 salidas comparadas, y expected/ no cambió. El sitio se construye (1231 páginas) y su comprobación de enlaces no encuentra ningún enlace roto. Nada de esto está aún verificado de forma independiente.

Por verificar

• La lección 15 nombra los desplegados, la reducción de orden parcial y los diagramas de decisión y no implementa ninguno de los tres. La afirmación de que un desplegado es exponencialmente más pequeño para la familia de los filósofos es el resultado publicado, no una medición de este repositorio; los artículos de Karp y Miller y de Araki y Kasami están confirmados por Crossref pero tras un muro de pago y sin leer.
• Nada de las secciones de statecharts, álgebras de procesos y autómatas temporizados de la lección 13 se ejecutó. No se construyó ningún modelo UPPAAL ni se calculó ningún grafo de clases de estados de TINA; las referencias de Harel y Milner están confirmadas por Crossref pero están tras un muro de pago y sin leer.
• La literatura sobre FMS da muchos menos estados que el concurso para el mismo modelo, porque los recuentos publicados son los marcados tangibles de una red estocástica generalizada mientras que FMS-PT-* es una red P/T corriente. Las cifras concretas están citadas de memoria en mis notas y no aparecen en ninguna lección hasta que se lea una fuente.
• La gramática de las redes P/T no está entre los ficheros RELAX NG publicados en pnml.org, así que el PNML del analizador nunca se ha validado contra un esquema. pnmlcoremodel.rng está y comprobaría la estructura; las particularidades P/T se cuelan por su regla anyElement.
• Hack 1972, la fuente del teorema de Commoner, es de acceso abierto e ilegible para una descarga automatizada. Leerlo en un navegador permitiría que la lección 6 citara el teorema en vez de parafrasear una paráfrasis.
• Murata 1989 sigue tras muro de pago y sin leer; toda atribución a él en las lecciones 1 a 8 está marcada en la página.
• Lección 7, ejercicio 3: construir los filósofos con un tiempo de espera y comprobar que la red está libre de interbloqueo y tiene una ejecución infinita en la que nadie come.
• La afirmación de que la enumeración de sifones minimales es NP-difícil se enuncia en la lección 6 a partir de conocimiento general y no está anclada a ningún artículo.
• La parte de la lección 16 con TINA. tina -R interop/admission.pnml debería dar 9 marcados y un marcado muerto; TINA no está instalado aquí. Lo mismo para inhibitor-arc.pnml, que TINA sí modela, con y sin -inh.
• Qué herramientas escriben el tipo de un arco como <type value="…"/> en PNML no está respaldado por ninguna fuente. La lección 16 dice «las herramientas que modelan más que redes P/T» y no nombra ninguna. Las formas de etiqueta y <arctype> que ahora rechaza vienen de la revisión, no de un fichero visto en otro lugar.
• Un registro XES de ejecuciones simuladas de la red de admisión, contrastado con el modelo, y una exportación DOT. Ni pm4py ni Graphviz están instalados aquí.

Preguntas abiertas

• La lección 13 le entrega a TLC solo el espacio de estados: el .cfg generado tiene una línea INVARIANT y ninguna línea PROPERTY, así que no se ha comprobado ninguna fórmula temporal bajo equidad. []<>Enabled(t) => []<>t es lo que pregunta la cuestión de la inanición de la lección 7, y TLC la respondería. Si generar condiciones de equidad por red, o escribir un módulo a mano para la única red donde la inanición es el tema, está sin decidir.
• La fuerza bruta sobre los subconjuntos de plazas limita el analizador a veinte plazas. Seis filósofos tomando un tenedor cada vez tienen veinticuatro, así que el veredicto estructural no se puede calcular para la mayor red de la propia tabla de la lección 7. Una formulación con un resolutor de restricciones lo arreglaría y haría que el curso dependiera de un resolutor.
• Las redes coloreadas de la lección 8 enlazan una variable por transición. Una transición que une dos mensajes necesita una tupla, y el despliegue crecería como un producto. La lección 12 esquivó la cuestión — el concurso entrega cada modelo ya desplegado a P/T — así que sigue abierta, y la lección 15 es el último sitio donde responderla.
• La lección 9 enseñó el formalismo estocástico, lo que deja abierto el determinista: una red de Petri temporal en el sentido de Merlin, donde una transición lleva un intervalo en vez de una tasa, no tiene detrás una cadena de Markov y necesita una construcción por clases de estados que el analizador no tiene. Si la lección 13 construye una o le entrega el modelo a TINA, que hace exactamente eso, está sin decidir.