Tham khảo tài liệu 'petri net part 2', 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ả | Modelling and Analysis of Real-Time Systems with RTCP-Nets 21 changing the state to another state 2 L J such that . Em p t b u Ew t p b Eiu x y b 0 if x y ị A and i Es t p b Slip 0 I 51 p for p Out t forp e In t - Out t otherwise. 3 In other words if a transition fires it removes one token from each input place adds one token to each output place sets time stamps of input places to 0 and sets time stamps of output places to values specified by time expressions of arcs leading from the transition to the places. If a transition I is enabled in a state in a binding b and a state . is derived from firing of the transition then we write . The binding b will be omitted if it is obvious or redundant. Two transitions Activity and TurnOnLS are enabled in the initial state. The first transition is enabled in three different bindings I the value of the variable n is equal to 5 ll I while the second one is enabled in the binding b a trivial binding . For example the result of firing of the transition TurnOnLS in the initial state is the state where Mx IsOn on on off off active on 4 Si 0 60 0 0 0 0 . A global clock is used to measure time. Every time the clock goes forward all time stamps are decreased by the same value. Definition 6. Let M S be a state and - .a vector with T entries. The state M S is changed into a state M1 S by a passage of time E denoted by iff and the passage of time - is possible . no transition is enabled in any state M S such that und . The result of firing of transitions TurnOnLS and Activity in binding b2 is the state M2 S2 where and I i i1 11 . None transition is enabled in the state but it is possible a passage of time I that leads to the state . . . - where i. . . A timeout occurs in this state. A token in the place Console is 6 seconds old the driver did not response within 6 seconds so the transition TurnOnSS will fire. A firing sequence of an RTCP-net is a sequence of pairs . . . such that bi is a binding of the transition ti .