Desde hace semanas, cada análisis estático lineal de Stabileo pasa por un certificado que, cuando se obtiene, da una cota verificada por la máquina del error con que se resolvió el sistema de ecuaciones K·u = f. Pero ese sistema lo arma el propio motor. Si el armado tuviera un error, un signo equivocado en una transformación, un término de Timoshenko que falta, una fuerza de empotramiento mal calculada, el certificado probaría con todo rigor que se resolvió bien el sistema equivocado.
Los certificados de punta a punta cierran ese hueco para pórticos y reticulados, en 2D y en 3D: el resultado se verifica contra el modelo tal como fue escrito, no contra las matrices que armó el motor.
Un segundo armado, independiente
Un verificador escrito aparte reconstruye la rigidez y las cargas a partir de los datos del modelo, sin llamar a ninguna función de elementos ni de ensamblado del motor. Usa sus propias fórmulas y su propia numeración de grados de libertad:
- la flexión de cada barra desde la flexibilidad de la ménsula, invertida, y el otro extremo por equilibrio, con la deformación por corte de Timoshenko;
- las articulaciones por condensación estática, una rotación liberada por vez;
- las cargas sobre barras como el trabajo sobre las deformadas exactas de la barra descargada, con las integrales resueltas en forma cerrada;
- los ejes locales, los apoyos inclinados, los resortes, los vínculos rígidos, los diafragmas y las restricciones multipunto, derivados de las convenciones del modelo.
Todo se calcula en aritmética de intervalos, incluidos senos y cosenos con cotas rigurosas: cada dato del modelo entra como el decimal que se escribió, encerrado en un intervalo. Si una decisión depende de un umbral que el intervalo no permite resolver, el verificador se niega en lugar de adivinar.
Qué afirma el certificado
Con esa rigidez exacta, el verificador demuestra que el modelo tiene una única solución y acota la distancia entre los desplazamientos que dio el motor y esa solución, en todos los grados de libertad que el modelo determina. Las matrices del motor no participan de esa afirmación. Se comparan aparte: deben coincidir con las reconstruidas hasta una parte en 10¹⁰, y los desplazamientos deben cumplir las condiciones de apoyo y de vínculo del modelo hasta una parte en 10⁹. Si no, el resultado se informa como no verificado de punta a punta, con el motivo.
El teorema que sostiene la cota está demostrado en Lean. En la aplicación, el panel de resultados muestra la línea «Verificado de punta a punta» con la cota del error de desplazamientos, o el motivo por el que no se pudo verificar.
Qué encontró
| Conjunto | Modelos | Certificados |
|---|---|---|
| Modelos de prueba 2D | 82 | 82 |
| Modelos de prueba 3D | 32 | 32 |
| Pórticos 2D generados al azar | 200 | 200 |
| Pórticos 3D generados al azar | 150 | 150 |
Todos los modelos de prueba y cientos de pórticos generados al azar coinciden y quedan certificados, y los errores de armado plantados a propósito en el motor hacen fallar el control. Además encontró problemas reales:
- un diafragma 3D en el plano XZ vinculaba los nudos con el giro de signo invertido;
- en 2D, un momento aplicado en un nudo donde todas las barras están articuladas lo absorbía un resorte artificial, y el certificado del sistema armado lo aprobaba aunque el modelo no tiene solución;
- un vínculo rígido desde un nudo así escondía un mecanismo real.
Los dos primeros están corregidos: el diafragma sigue el giro de cuerpo rígido, y ese momento se rechaza antes de resolver. Y cuando el motor cambió el significado de un diafragma para que todo el piso gire como un cuerpo, el verificador no aprobó nada falso: siguió siendo honesto, pero con cotas inútiles, hasta que se actualizaron sus convenciones. Es exactamente lo que se espera de un control independiente.
Qué queda fuera
- Láminas, sólidos, conectores, vigas curvas y torsión con alabeo todavía no se reconstruyen: se informan fuera de alcance, nunca como verificados.
- Las fórmulas del verificador codifican la mecánica del modelo. Están escritas aparte del motor y se contrastan con él, pero no están demostradas.
- La implementación en Rust no está demostrada equivalente al algoritmo de Lean, como ocurre con todos los certificados.
- Un certificado dice que el resultado corresponde al modelo. No dice que el modelo represente bien la estructura: eso sigue siendo trabajo del ingeniero.