Petri Net Part 8

Tham khảo tài liệu 'petri net part 8', kỹ thuật - công nghệ, cơ khí - chế tạo máy phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả | Model Checking of Time Petri Nets 201 The verification of p proceeds as follows During the generation of the SCG of N I Alarm if is satisfied in a state class a m f transition ta is enabled in a to capture the event corresponding to the beginning of time interval Ir. ta is enabled by changing the marking m in a such that place Pa would contain one token and replacing f with f A ta a. These two actions correspond to artificially putting a token in place Pa of Alarm. Since a 0 and transition ta has the highest priority it is fired before all others. When ta is fired which means that time has come to start looking for Ộ2 tb gets enabled in the resulting state class a m f to capture the event corresponding to the end of interval Ir. If tb is fired during the exploration p is declared invalid and the exploration stops. If before firing tb ộ2is satisfied in a state class a m f transition tb is disabled in a by changing the marking m such that place Pb would contain zero tokens and eliminating variable tb from f . These two actions correspond to artificially removing the token in place Pb. After a is modified p is checked again starting from a . Note that in this technique the fact of knowing a state class and the transition that led to it is sufficient to know which action to take9. This means that there is no need to keep track of execution paths during the exploration and hence the exploration strategy of the SCG depth first breadth first . is irrelevant. This in turn solves the problem of dealing with cycles and infinite execution paths for bounded TPN models. Let a m f be a state class and t the transition that led to it. The different cases that might arise during the exploration are given in what follows 1. The case where ta tb Ể En m and tế ta tb corresponds to a situation where we are looking for In case Ộị is satisfied in a we enable ta in a 2. The case where tbe En m corresponds to a situation where we are looking for 02. If Ộ2is satisfied in a then we disable

Không thể tạo bản xem trước, hãy bấm tải xuống
TÀI LIỆU LIÊN QUAN
TỪ KHÓA LIÊN QUAN
TÀI LIỆU MỚI ĐĂNG
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.