چهار نوع جستجو
بررسی هر یافته را به چهار نوع دسته‌بندی می‌کند و تنها نوع اول ثابت می‌کند که FET نمی‌تواند برنامه زمانی را بسازد.
اکثر ابزارهای بررسی، یافته‌های خود را بر اساس میزان جدی بودنشان مرتب می‌کنند. این ابزار آنها را بر اساس آنچه می‌تواند اثبات کند، مرتب می‌کند. گزارش چهار نوع را نشان می‌دهد که همیشه به همین ترتیب هستند.
هر نوع یک برگه با شمارش مخصوص به خود است. نوعی که چیزی پیدا نکرد، برگه‌ای ندارد، بنابراین یک برگه خالی نخواهید دید.
اثبات شده غیرممکن
روی صفحه: محاسبات، نه حدس.
بررسی به هر یافته در اینجا با شمارش می‌رسد. ساعات اختصاص‌یافته را با بازه‌های زمانی آزاد مقایسه می‌کند. زمان‌های شروع قانونی یک کلاس را به هیچ کاهش می‌دهد. دو کلاس را پیدا می‌کند که باید همزمان اجرا شوند و یک استاد مشترک دارند.
می‌توانید بر اساس این یافته‌ها بدون اینکه خودتان آنها را بررسی کنید، عمل کنید. اگر گزارش می‌گوید یک کلاس زمان شروع قانونی ندارد، حل‌کننده نیز نمی‌تواند یکی پیدا کند.
این قرارداد ابزار است. بررسی هرگز یافته‌ای را در اینجا گزارش نمی‌کند که نتواند اثبات کند. ابزاری که یک هشدار غلط می‌دهد، ابزاری است که دیگر به آن اعتماد نمی‌کنید.
اشتباهات
روی صفحه: چیزی در اینجا احتمالاً آن چیزی نیست که شما منظور داشتید.
این یافته‌ها حل را متوقف نمی‌کنند. آنها نشان می‌دهند که قوانین شما چیزی را می‌گویند که احتمالاً قصد آن را نداشتید.
- یک قانون به چیزی اشاره می‌کند که دیگر وجود ندارد.
- یک قانون یک کلاس را هدف قرار می‌دهد که شما آن را خاموش کرده‌اید.
- دو قانون دقیقاً یک چیز را می‌گویند.
- یک ترجیح نرم هرگز نمی‌تواند اعمال شود، بنابراین FET آن را نادیده می‌گیرد.
هیچ یک از اینها یک برنامه را غیرممکن نمی‌کند. قوانینی که هیچ کس نمی‌فهمد، باعث معمای ترم بعدی می‌شوند.
چه چیزی این فایل را دشوار می‌کند
روی صفحه: این یک مشکل نیست. این کاری است که حل‌کننده باید انجام دهد.
هیچ چیز در اینجا اشتباه نیست. این نوع فشار موجود در فایل شما را توصیف می‌کند. کلاس‌هایی را نام می‌برد که تقریباً هیچ فضای خالی ندارند. بخش‌هایی از هفته را نام می‌برد که فشرده هستند.
⚠ این نوع را قبل از اینکه هفته را فشرده‌تر کنید، بخوانید.
عنوان برای یک فایل حل‌شده تغییر می‌کند. سپس می‌خواند چه چیزی این فایل را دشوار کرد، زیرا کار کامل شده است.
چه چیزی روی این فایل اجرا شد
روی صفحه: انواع قوانینی که فهرست و شمارش می‌کنیم، هرگز قضاوت نمی‌کنیم.
این نوع آرام است، و به جای فایل شما، در مورد خود بررسی گزارش می‌دهد. انواع قوانینی را که شمارش کرده است، فهرست می‌کند. به شما می‌گوید چه زمانی حالت حل‌کننده شما یک بررسی را از اجرا متوقف می‌کند. به شما می‌گوید چه زمانی بررسی در یک فایل بسیار بزرگ زودتر متوقف شد.
این نوع را زمانی بخوانید که گزارش خالی‌تر از حد انتظار شما به نظر می‌رسد. معمولاً دلیل آن را توضیح می‌دهد.
یک برگه گم‌شده تضمین نیست
بررسی آنچه را که می‌تواند اثبات کند، گزارش می‌دهد. از این نتیجه نمی‌شود که هر چیز دیگری صحیح است.
عدم وجود برگه "اثبات شده غیرممکن" به این معنی است که "هیچ چیز غیرممکن اثبات نشد". به این معنی نیست که "این حل خواهد شد".
⚠ این مهمترین جمله در صفحه است، و صفحه باعث می‌شود به راحتی نادیده گرفته شود: برگه به سادگی غایب است، بنابراین چیزی برای خواندن و کلیک کردن وجود ندارد. غیبت نتیجه خوب است، نه نتیجه کامل.
یک برنامه می‌تواند از نظر محاسباتی ممکن باشد و همچنان زمان زیادی از FET بگیرد. ممکن است همچنان نیاز به کاهش محدودیت‌ها قبل از نهایی شدن داشته باشد. به آنچه نمی‌تواند به شما بگوید مراجعه کنید.