LTS задачи
Описание файла
PDF-файл из архива "LTS задачи", который расположен в категории "". Всё это находится в предмете "верификация программ на моделях" из 8 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
После события 'it_b' и до наступления события 'it_e' верно: всегда выполняется 'p'[]((it_b) -> ((ps U it_e) || []ps))После наступления события 'it_e' верно: никогда не выполняется 'da'[] (it_e -> ( []!da ))После наступления события 'it_p' верно: после события 'pu' рано или позднонаступит событие 'pl'[] (it_b -> ( [](pu -> <>pl) ))После события 'it_b' и до наступления события 'it_e' верно: после события 'p'рано или позднонаступит событие 'q'[](it_b -> ((p -> (!it_e U (q && !it_e))) U it_e) || ([](p -> <>q)))Между событиями 'it_b' и 'it_e' верно: если наступило событие 'p', то до негобыло событие 'q'[]((it_b && !it_e && <>it_e) -> (!p U (q || it_e)))После наступления события 'it_b' верно: событие p наступает ровно один раз[](it_b -> (p -> ([]p || (p U []!p))))После события it_b и до наступления события 'it_e' верно: после события 'p'рано или поздно наступит событие 'q'[](it_b -> ((p -> (!it_e U (q && !it_e))) U it_e) || ([](p -> <>q)))Между событиями 'it_b' и 'it_e' верно: если наступило событие 'p', то до негобыло событие 'q'[]((it_b && !it_e && <>it_e) -> (!p U (q || it_e)))После наступления события 'it_b' верно: событие 'p' наступает ровно один раз[](it_b -> (p -> ([]p || (p U []!p))))Задача 2Между событиями 'процесс p находится на метке iter_begin' и 'процесс pнаходится на метке iter_end' верно: если наступило событие 'значениеглобальной переменной x равно 3', то до него было событие 'значениеглобальной переменной y равно 5'#define it_b p@iter_begin#define it_e p@iter_end#define p (x == 3)#define q (y == 5)[]((it_b && !it_e && <>it_e) -> (!p U (q || it_e)))Задача 3После наступления события 'процесс p находится на метке iter_begin' верно:событие 'значение глобальной переменной state равно locked' наступает ровноодин раз#define it_b p@iter_begin#define p (state == locked)[](it_b -> (p -> ([]p || (p U []!p))))Задача 1После события 'процесс p находится на метке iter_begin' и до наступлениясобытия 'процесс p находится на метке iter_end' верно: после события'значение глобальной переменной x равно 3' рано или поздно наступит событие'значение глобальной переменной y равно 5'#define it_b p@iter_begin#define it_e p@iter_end#define p (x == 3)#define q (y == 5)[](it_b -> ((p -> (!it_e U (q && !it_e))) U it_e) || ([](p -> <>q)))Задача 2Между событиями 'процесс p находится на метке iter_begin' и 'процесс pнаходится на метке iter_end' верно: если наступило событие 'значениеглобальной переменной x равно 3', то до него было событие 'значениеглобальной переменной y равно 5'#define it_b p@iter_begin#define it_e p@iter_end#define p (x == 3)#define q (y == 5)[]((it_b && !it_e && <>it_e) -> (!p U (q || it_e)))Задача 3После наступления события 'процесс p находится на метке iter_begin' верно:событие 'значение глобальной переменной state равно locked' наступает ровноодин раз#define it_b p@iter_begin#define p (state == locked)[](it_b -> (p -> ([]p || (p U []!p)))) .