Seit Wochen durchläuft jede lineare statische Berechnung in Stabileo ein Zertifikat, das, wenn es zustande kommt, eine maschinell geprüfte Schranke für den Fehler liefert, mit dem das Gleichungssystem K·u = f gelöst wurde. Dieses System stellt der Rechenkern aber selbst auf. Enthielte die Assemblierung einen Fehler, ein falsches Vorzeichen in einer Transformation, einen fehlenden Timoshenko-Term, eine falsche Volleinspannkraft, dann würde das Zertifikat mit voller Strenge beweisen, dass das falsche System korrekt gelöst wurde.
Durchgängige Zertifikate schließen diese Lücke für Rahmen und Fachwerke in 2D und 3D: Das Ergebnis wird gegen das Modell geprüft, wie es eingegeben wurde, nicht gegen die Matrizen, die der Rechenkern aufgestellt hat.
Eine zweite, unabhängige Assemblierung
Ein separat geschriebener Prüfer baut Steifigkeit und Lasten aus den Modelldaten neu auf, ohne eine einzige Element- oder Assemblierungsfunktion des Rechenkerns aufzurufen. Er verwendet eigene Formeln und eine eigene Nummerierung der Freiheitsgrade:
- die Biegung jedes Stabs aus der Nachgiebigkeit des Kragarms, invertiert, und das andere Ende über das Gleichgewicht, mit Timoshenko-Schubverformung;
- Gelenke durch statische Kondensation, jeweils eine freigegebene Verdrehung nach der anderen;
- Stablasten als Arbeit an den exakten Biegelinien des unbelasteten Stabs, mit den Integralen in geschlossener Form;
- lokale Achsen, schräge Auflager, Federn, starre Kopplungen, Scheiben und Mehrpunktbindungen, abgeleitet aus den Konventionen des Modells.
Alles wird in Intervallarithmetik berechnet, Sinus und Kosinus eingeschlossen, mit strengen Schranken: Jede Modelleingabe geht als die Dezimalzahl ein, als die sie eingegeben wurde, eingeschlossen in ein Intervall. Hängt eine Entscheidung von einem Schwellenwert ab, den das Intervall nicht klären kann, verweigert der Prüfer das Ergebnis, statt zu raten.
Was das Zertifikat aussagt
Mit dieser exakten Steifigkeit beweist der Prüfer, dass das Modell eine eindeutige Lösung hat, und schränkt den Abstand zwischen den vom Rechenkern gelieferten Verschiebungen und dieser Lösung ein, und zwar über alle Freiheitsgrade, die das Modell bestimmt. Die Matrizen des Rechenkerns spielen für diese Aussage keine Rolle. Sie werden getrennt verglichen: Sie müssen mit den neu aufgebauten bis auf einen Teil in 10¹⁰ übereinstimmen, und die Verschiebungen müssen die Auflager und Bindungen des Modells bis auf einen Teil in 10⁹ erfüllen. Ist das nicht der Fall, wird das Ergebnis als nicht durchgängig geprüft gemeldet, mit Angabe des Grundes.
Der Satz hinter der Schranke ist in Lean bewiesen. In der App zeigt das Ergebnisfenster die Zeile „Durchgängig geprüft“ mit der Schranke für den Verschiebungsfehler oder den Grund, warum nicht geprüft werden konnte.
Was gefunden wurde
| Satz | Modelle | Zertifiziert |
|---|---|---|
| 2D-Testmodelle | 82 | 82 |
| 3D-Testmodelle | 32 | 32 |
| Zufällige 2D-Rahmen | 200 | 200 |
| Zufällige 3D-Rahmen | 150 | 150 |
Alle Testmodelle und Hunderte zufällig erzeugter Rahmen stimmen überein und sind zertifiziert, und absichtlich in den Rechenkern eingebaute Assemblierungsfehler lassen die Prüfung scheitern. Sie hat auch echte Probleme gefunden:
- eine 3D-Scheibe in der XZ-Ebene koppelte die Knoten mit einer Verdrehung des falschen Vorzeichens;
- in 2D wurde ein Moment auf einem Knoten, an dem alle Stäbe gelenkig angeschlossen sind, von einer künstlichen Feder aufgenommen, und das Zertifikat des aufgestellten Systems ließ es durchgehen, obwohl das Modell keine Lösung hat;
- eine starre Kopplung, die von einem solchen Knoten ausging, verdeckte einen echten Mechanismus.
Die ersten beiden sind behoben: Die Scheibe folgt der Starrkörperdrehung, und dieses Moment wird vor der Berechnung abgewiesen. Und als der Rechenkern änderte, was eine Scheibe bedeutet, sodass sich die ganze Decke als ein Körper dreht, ließ der Prüfer nichts Falsches durch: Er blieb ehrlich, mit nutzlosen Schranken, bis seine Konventionen angepasst waren. Genau dafür ist eine unabhängige Prüfung da.
Was außen vor bleibt
- Schalen, Volumenelemente, Verbindungselemente, gekrümmte Balken und Wölbkrafttorsion werden noch nicht neu aufgebaut: Sie werden als außerhalb des Geltungsbereichs gemeldet, nie als geprüft.
- Die Formeln des Prüfers bilden die Mechanik des Modells ab. Sie sind getrennt vom Rechenkern geschrieben und werden mit ihm verglichen, aber sie sind nicht bewiesen.
- Wie bei jedem Zertifikat ist nicht bewiesen, dass die Rust-Implementierung dem Lean-Algorithmus entspricht.
- Ein Zertifikat sagt, dass das Ergebnis zum Modell gehört. Es sagt nicht, dass das Modell das Tragwerk gut abbildet: Das bleibt Aufgabe des Ingenieurs.