Ir al contenido
learn
Menú global

Redes de Petri — Misión

Por qué estoy aprendiendo esto

Sección titulada «Por qué estoy aprendiendo esto»

Sé dibujar una máquina de estados. He escrito varias en C# con un enum y un switch, y en Java con un patrón estado, y funcionan mientras el sistema hace una cosa a la vez. Luego ocurren dos cosas al mismo tiempo. Dos hilos toman dos cerrojos en dos órdenes. Un Channel<T> se llena y el productor se bloquea para siempre. Un flujo de trabajo tiene tres ramas y nadie sabe decir si todas pueden terminar.

Una máquina de estados no puede decir nada de eso, porque tiene un estado actual, y lo que estoy modelando tiene varios. Lo que quiero es un modelo cuyo estado sea una distribución: tantas peticiones en la cola, tantos trabajadores ocupados, un cerrojo tomado. Una red de Petri es exactamente eso, y viene con un pequeño cuerpo de matemáticas que responde preguntas que hoy respondo con pruebas de carga y esperanza:

  • ¿puede desbordarse esta cola? No «se desbordó el martes pasado» — puede, alguna vez, bajo cualquier entrelazado;
  • ¿puede este sistema interbloquearse? Y si puede, cuál es la secuencia más corta que llega allí;
  • ¿va a terminar este flujo de trabajo? Desde todos los estados en los que puede acabar, no solo el camino feliz.

Esas tres preguntas las decide un programa en este curso, sobre redes que modelan cosas reales: un búfer acotado, una exclusión mutua, dos cerrojos tomados en órdenes opuestos.

Para quién es este curso

Sección titulada «Para quién es este curso»

Eres desarrollador de C# o de Java. Has escrito código concurrente y modelado procesos con máquinas de estados. No necesitas más matemáticas que sumar vectores y multiplicar una matriz por uno; el curso introduce lo que usa, y la primera matriz aparece en la lección 2 solo porque hace más fácil algo concreto.

Las lecciones sobre concurrencia se apoyan en lo que ya sabes. La lección 7 toma la contrapresión de las lecciones 6 a 9 del curso de C# avanzado — channels, TPL Dataflow, Rx — y la modela en lugar de medirla. La lección 14 inicia el dogfooding del repositorio con un ciclo de vida C# acotado y un bloqueo de lanes de agentes; RabbitMQ y Kubernetes quedan como experimentos posteriores explícitos.

El ejemplo conductor

Sección titulada «El ejemplo conductor»

Un productor, un consumidor y un búfer de dos huecos. Tres plazas contienen el estado del productor, del consumidor y del búfer; cuatro transiciones son los eventos. Nada es un «estado actual»: el marcado dice dónde está cada marca, todas a la vez.

flowchart LR
    ready(("ready<br/>●"))
    produced(("produced"))
    free(("free<br/>● ●"))
    full(("full"))
    waiting(("waiting<br/>●"))
    taken(("taken"))
    produce["produce"]
    deposit["deposit"]
    take["take"]
    consume["consume"]
    ready --> produce
    produce --> produced
    produced --> deposit
    free --> deposit
    deposit --> full
    deposit --> ready
    full --> take
    waiting --> take
    take --> taken
    take --> free
    taken --> consume
    consume --> waiting

Los nombres de las plazas y de las transiciones se quedan en inglés en los tres idiomas: forman parte de la salida del programa, comparada por check.sh, y traducirlos haría que los listados dejaran de coincidir.

Esta red tiene doce marcados alcanzables, nunca se interbloquea, y la plaza free es toda la razón por la que el búfer no puede desbordarse — quítala y el conjunto de marcados alcanzables se vuelve infinito. Las lecciones 1 a 4 demuestran las tres afirmaciones, y la lección 5 demuestra la primera otra vez sin mirar ni un solo marcado.

Al terminar este curso podré

Sección titulada «Al terminar este curso podré»
  • leer y dibujar una red de Petri, y decir qué significa su marcado en el sistema que modela;
  • escribir la matriz de incidencia de una red, y saber qué decide y qué no decide la ecuación de estado;
  • construir un grafo de alcanzabilidad, y un árbol de cobertura cuando el grafo es infinito;
  • decidir acotación, seguridad, vivacidad, ausencia de interbloqueo, reversibilidad y persistencia, y decir cuáles de ellas exige realmente un sistema dado;
  • calcular invariantes de plazas y de transiciones, y usar uno como una prueba válida para todos los marcados alcanzables;
  • reconocer máquinas de estados, grafos marcados y redes de libre elección, y usar los teoremas que vienen con esas clases;
  • modelar exclusión mutua, productor-consumidor, lectores-escritores y los filósofos comensales, y comparar los modelos con las construcciones de C# y de Java que representan;
  • usar redes coloreadas, temporizadas y estocásticas, y saber qué cuesta cada extensión al análisis;
  • comprobar la soundness de un flujo de trabajo, y traducir entre BPMN y redes de flujo de trabajo;
  • intercambiar redes con TINA, LoLA, CPN Tools, GreatSPN y TAPAAL mediante PNML;
  • modelar partes de los sistemas de este repositorio, y decir con honestidad qué encontró el modelo y qué se le escapó;
  • saber dónde se detiene el formalismo: qué es indecidible, qué es decidible pero desesperado, y a qué recurrir en su lugar.

Plan

Sección titulada «Plan»
# Lección Lo que quizá ya conoces
1 Por qué las redes de Petri las máquinas de estados, enum más switch, una cola acotada
2 La definición formal y la matriz de incidencia los vectores, un producto de matrices
3 El grafo de alcanzabilidad un recorrido en anchura, la explosión de una matriz de pruebas
4 Propiedades interbloqueo, inanición, livelock
5 Invariantes un invariante de bucle, una cantidad conservada
6 Clases estructurales: máquinas de estados, grafos marcados, redes de libre elección
7 Modelar la concurrencia: exclusión mutua, productor-consumidor, lectores-escritores, filósofos lock, SemaphoreSlim, Channel<T>, synchronized, ReentrantLock
8 Redes coloreadas los genéricos, un mensaje tipado
9 Tiempo y probabilidad: redes temporizadas, estocásticas, GSPN los percentiles, un modelo de colas
10 Flujos de trabajo: redes de flujo de trabajo, soundness, BPMN, process mining BPMN, un motor de flujos de trabajo
11 Herramientas e interoperabilidad: PNML, TINA, LoLA, Snoopy, PIPE, CPN Tools, GreatSPN, TAPAAL un formato de intercambio en XML
12 Aplicaciones industriales: talleres flexibles, protocolos, hardware, bioquímica, seguridad un banco de pruebas público, un espacio de estados
13 Frente a otros formalismos: TLA+, statecharts, álgebras de procesos, autómatas temporizados un segundo espacio de estados, calculado en otra parte
14 En nuestros sistemas: pipelines C# y lanes de agentes C# avanzado; RabbitMQ y Kubernetes son experimentos posteriores
15 Límites y qué viene después: indecidibilidad, desplegados, reducción de orden parcial, extensiones una respuesta falsa de un algoritmo correcto
16 Interoperabilidad: preservar el comportamiento, no solo el dibujo una prueba de ida y vuelta, un fichero que valida y aun así pierde datos

Diario: lo que intenté, lo que me sorprendió, lo que me queda por verificar.

Recursos

Sección titulada «Recursos»