Haftalardır Stabileo’daki her doğrusal statik analiz bir sertifikadan geçiyor; bu sertifika elde edildiğinde, K·u = f denklem sisteminin hangi hatayla çözüldüğüne dair makine tarafından kontrol edilmiş bir sınır verir. Ancak bu sistemi hesap motorunun kendisi kurar. Kurulumda bir hata olsaydı, örneğin bir dönüşümde yanlış bir işaret, eksik bir Timoshenko terimi ya da yanlış bir ankastrelik uç kuvveti, sertifika yanlış sistemin doğru çözüldüğünü tam bir titizlikle kanıtlamış olurdu.
Uçtan uca sertifikalar, 2B ve 3B çerçeveler ile kafes kirişler için bu boşluğu kapatır: sonuç, hesap motorunun kurduğu matrislere karşı değil, yazıldığı haliyle modele karşı kontrol edilir.
İkinci, bağımsız bir kurulum
Ayrı olarak yazılmış bir denetleyici, hesap motorunun eleman veya kurulum fonksiyonlarından hiçbirini çağırmadan, rijitliği ve yükleri model verilerinden yeniden kurar. Kendi formüllerini ve serbestlik derecelerinin kendi numaralandırmasını kullanır:
- her çubuğun eğilmesi, konsol esnekliğinin tersi alınarak, diğer ucu ise denge ile elde edilir; Timoshenko kayma şekil değiştirmesi dahildir;
- mafsallar statik yoğunlaştırma ile, her seferinde serbest bırakılmış bir dönme olmak üzere ele alınır;
- çubuk yükleri, yüksüz çubuğun tam sehim şekilleri üzerindeki iş olarak, integraller kapalı biçimde hesaplanarak bulunur;
- yerel eksenler, eğik mesnetler, yaylar, rijit bağlantılar, diyaframlar ve çok noktalı bağlar modelin kurallarından türetilir.
Sinüsler ve kosinüsler dahil her şey, kesin sınırlarla aralık aritmetiğinde hesaplanır: modelin her girdisi, yazıldığı ondalık sayı olarak bir aralığın içine alınarak girer. Bir karar, aralığın çözemediği bir eşik değerine bağlı olduğunda denetleyici tahmin yürütmek yerine reddeder.
Sertifikanın söylediği
Bu kesin rijitlikle denetleyici, modelin tek bir çözümü olduğunu kanıtlar ve hesap motorunun döndürdüğü yer değiştirmeler ile bu çözüm arasındaki uzaklığı, modelin belirlediği her serbestlik derecesi üzerinde sınırlar. Hesap motorunun matrislerinin bu ifadede hiçbir rolü yoktur. Onlar ayrıca karşılaştırılır: yeniden kurulan matrislerle 10¹⁰’da bir hassasiyetle uyuşmaları, yer değiştirmelerin de modelin mesnet ve bağlarını 10⁹’da bir hassasiyetle sağlaması gerekir. Sağlamıyorlarsa sonuç, gerekçesiyle birlikte uçtan uca kontrol edilmemiş olarak bildirilir.
Sınırın dayandığı teorem Lean’de kanıtlanmıştır. Uygulamada sonuçlar paneli, yer değiştirme hatasının sınırıyla birlikte “Uçtan uca kontrol edildi” satırını ya da kontrol edilememe gerekçesini gösterir.
Neler buldu
| Küme | Modeller | Sertifikalı |
|---|---|---|
| 2B test modelleri | 82 | 82 |
| 3B test modelleri | 32 | 32 |
| Rastgele 2B çerçeveler | 200 | 200 |
| Rastgele 3B çerçeveler | 150 | 150 |
Tüm test modelleri ve rastgele üretilmiş yüzlerce çerçeve uyuşuyor ve sertifikalanıyor; hesap motoruna bilerek yerleştirilen kurulum hataları ise kontrolün başarısız olmasına yol açıyor. Kontrol gerçek sorunlar da buldu:
- XZ düzlemindeki bir 3B diyafram, düğümleri yanlış işaretli dönmeyle bağlıyordu;
- 2B’de, birleşen tüm çubukların mafsallı olduğu bir düğüme etkiyen moment yapay bir yay tarafından yutuluyordu ve modelin çözümü olmamasına rağmen kurulan sistemin sertifikası bunu geçiriyordu;
- böyle bir düğümden çıkan rijit bir bağlantı gerçek bir mekanizmayı gizliyordu.
İlk ikisi düzeltildi: diyafram rijit cisim dönmesini izliyor ve bu moment çözümden önce reddediliyor. Ayrıca hesap motoru bir diyaframın anlamını, tüm döşeme tek bir cisim gibi dönecek şekilde değiştirdiğinde denetleyici yanlış hiçbir şeyi geçirmedi: kuralları güncellenene kadar, işe yaramayan sınırlar vererek dürüst kaldı. Bağımsız bir kontrol tam olarak bunun içindir.
Dışarıda bıraktıkları
- Kabuklar, katı elemanlar, bağlayıcılar, eğrisel kirişler ve çarpılmalı burulma henüz yeniden kurulmuyor: bunlar hiçbir zaman kontrol edilmiş olarak değil, kapsam dışı olarak bildirilir.
- Denetleyicinin formülleri modelin mekaniğini kodlar. Hesap motorundan ayrı yazılmışlardır ve onunla karşılaştırılırlar, ancak kanıtlanmış değildirler.
- Her sertifikada olduğu gibi, Rust uygulamasının Lean algoritmasına denk olduğu kanıtlanmış değildir.
- Bir sertifika sonucun modele ait olduğunu söyler. Modelin yapıyı iyi temsil ettiğini söylemez: bu, mühendisin işi olmaya devam eder.