• 沒有找到結果。

Transformation of Places and Transitions

CHAPTER 3 MODEL CHECKING WITH PETRI NET

3.2 T RANSFORMATION FROM FSM INTO P ETRI N ET

3.2.1 Transformation of Places and Transitions

To transform a FSM into a Petri net, we need to know the relation between a FSM and a Petri net. A FSM is composed of the following five parts:

z Q : States

z Σ: Input alphabet z Δ: Output alphabet

z δ: Q × Σ→Q next-state function z Γ: Q → Δ output function

17

A Petri net is a four-tuple (P, T, I, O). As a FSM (Q,Σ,Δ,δ,Γ) we define a Petri net (P, T, I, O) by

z P = Q∪Σ∪Δ

z T = {tq,σ| q∈Q andσ∈Σ}

z I(tq,σ) = {q ,σ}

z O(tq,σ) = {Γ( q )}

According to the illustration above, we could know that all states, inputs, and outputs in a finite state machine are represented with places in a Petri net and all events (arrows) in a state machine are represented by transitions in a Petri net [1]. The rules of transferring a FSM into a Petri net are:

1. Inputs, outputs, and states → places 2. Events (arrows) → transitions 3. Preconditions → input places 4. Post-conditions → output places

The arrows determine the state transitions in a FSM as well as the transitions in a Petri net, so an arrow in a FSM would be transferred into a transition in a Petri net. The input places and output places of the transition are the preconditions and post conditions of the arrow in the FSM respectively.

After discussing the transformation rules of FSMs and Petri nets, the following are some examples to show the transformation in different situations.

Figure 3-2 FSM 1 Figure 3-3 Petri net of Figure 3-2

Figure 3-3 is the Petri net transferred from the state machine in Figure 3-2. In Figure 3-2, there are three states (State 0, State 1, and State 2) and three signals (A, B, C). According to the transformation rule 1, there should be three places represent the states and another three places represent the control signals in the corresponding Petri net. There are three arrows in the state machine to determine the state transitions. According to the transformation rule 2, the Petri net needs to have three transitions to represent the three arrows, there are t0, t1, and t2. Finally we connect the places and transitions bottom on the transformation rule 3 and 4 then the Petri net is built.

In the above example, we told about the state machine which changes states when control signals are 1(i.e. there is only one value being used for each signal).

So there is only one place needs to be built to represent each signal in Petri net. In some state machines, states may change when the control signal is 0 and 1 both. In this kind of situation, we should generate two places to represent the two values of the signal. It is illustrated in the following example.

19

Figure 3-4 FSM 2 Figure 3-5 Petri net for Figure 3-4

In the FSM in Figure 3-4, State 0 may change to State 1 when A = 0 and may change to State 2 when A = 1. To transfer the FSM into a Petri net in this situation we should create two places to represent the two values of the signal A. The corresponding Petri net is shown in Figure 3-5. The transition t0 controls the state transition from State 0 to State 1, and t1 controls the state transition from State 0 to State 2.

In some cases, we could ignore to transfer some arrows and some values of signals into transitions and places. It is that when a value of a signal which does not control any state transitions, we could ignore the transformation of the value and the arrow. For example, in Figure 3-6, State 0 has a self-loop when A = 0. Assume the initial state is State 0, and A = 0, the state is still at State 0 until A = 1. This FSM could have the same behavior even if we ignore the transformation of the arrow controlled by signal A = 0. Because A = 0 does not determine any state transitions.

Figure 3-6 FSM 4

But in some other case, we still generate transitions and places even if the arrows and signals do not determine any state transitions. An example is shown in section 5.2.

From the three examples above, we can observe that in some situations we transfer one signal into one place, but in other situations we transfer one signal into two places. Theoretically speaking, we should always transfer a signal in a FSM into places based on its values. In other words, when a signal A can be 0 and 1, we should generate two places to represent A = 0 and A = 1. But some values of signals do not control any state transitions. For example, the value 0 of the signal A in Figure 3-2 do not control any state changes in the FSM, we don’t need to generate a place to represent A = 0 and the transition controlled by A = 0 either. It is no effect that we do not generate the place A = 0 and the transition in the corresponding Petri net. Summarily speaking, when there are any arrows which do not determine state transitions, we could ignore the transformations of the arrows. We only transfer the signals and arrows which are used into places and transitions respectively. By doing this, we could make the corresponding Petri net more concise and the transition matrix of the Petri net smaller.

There is a special kind of transitions which do not have input places. The transitions are firable all the time and usually connected in front of inputs to provide the input places tokens. When we meet a situation that we don’t know how many tokens we have to assign to an input signal (e.g. clk), we put an input transition in front of the place to generate tokens to the signal.

21

Figure 3-7 Petri net 1

In Figure 3-7, t3 to t5 are input transitions, they provide tokens to the inputs A, B and C respectively.

相關文件