این دستور lbt است که می تواند در ارائه دهنده هاست رایگان OnWorks با استفاده از یکی از چندین ایستگاه کاری آنلاین رایگان ما مانند Ubuntu Online، Fedora Online، شبیه ساز آنلاین ویندوز یا شبیه ساز آنلاین MAC OS اجرا شود.
برنامه:
نام
lbt - مترجم LTL به Büchi
خلاصه
lbt < formula.txt > automaton.txt
lbt2dot < automaton.txt > automaton.dot
شرح
این صفحه راهنما به اختصار مستندات lbt و lbt2dot دستورات این صفحه راهنما بود
برای توزیع گنو/لینوکس دبیان نوشته شده است زیرا برنامه اصلی دارای a نیست
صفحه دستی در عوض، دارای اسناد در قالب HTML است. زیر را ببینید.
lbt فیلتری است که یک فرمول منطق زمانی خطی (LTL) را به یک فرمول متناظر ترجمه می کند
اتومات بوچی تعمیم یافته. ترجمه بر اساس الگوریتم Gerth, Peled است
و واردی در PSTV'95 ارائه شد، ساده در پرواز اتوماتیک تایید of خطی
زمانی منطق. به ندرت هیچ بهینه سازی اجرا شده است، و خودکار تولید شده است
اغلب بزرگتر از حد لازم اما از طرف دیگر، همیشه باید صحیح باشد.
فیلتر lbt2dot می توان برای ترجمه خودکار بوچی از lbt فرمت خروجی به
فرمت GraphViz برای تجسم.
مثال
از دست G p0 | lbt | lbt2dot | دلگیر -
با استفاده از خدمات onworks.net از lbt به صورت آنلاین استفاده کنید
