Let M⟦…⟧(…) be the “meaning” function from PITL × Σ+ to {tt,ff} and let σ be an interval (σ ∈ Σ+) then
M⟦true⟧(σ) |
≜ |
tt |
M⟦Q⟧(σ) |
≜ |
σ0(Q) |
M⟦¬f⟧(σ) | ≜ | not (M⟦f⟧(σ)) |
M⟦f1 ∧ f2⟧(σ) |
≜ |
M⟦f1⟧(σ) and M⟦f2⟧(σ) |
M⟦skip⟧(σ) |
≜ |
(|σ| = 1) |
The semantics of ‘chop’ is as follows M⟦f1 ; f2⟧(σ) = tt iff
(exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt) |
||||||||||||||||
|
Interval σ is a fusion of two intervals σ0…σk (satisfies f1) and σk…σ|σ| (satisfies f2). State σk is shared by both.
Let σ be an interval σ0σ1σ2σ3 (4 states).
We evaluate
M⟦skip ; (Q ∧skip2)⟧(σ)
(exists k, s.t. M⟦skip⟧(σ0…σk) = tt and |
M⟦Q ∧skip2⟧(σk…σ3) = tt) |
As M⟦skip⟧(σ0…σk) = tt means that |σ0…σk| = 1.
We know that an interval of length 1 has two states, i.e., k can only be 1.
We now evaluate M⟦Q ∧skip2⟧(σ1…σ3)
(M⟦Q ∧skip2⟧(σ
1…σ3) = tt) iff |
M⟦Q⟧(σ1…σ3) = tt and M⟦skip2⟧(σ1…σ3) = tt |
Evaluate M⟦Q⟧(σ1…σ3)
M⟦Q⟧(σ1…σ3) = tt iff σ1(Q) = tt
Note, the definition states that we evaluate Q in the first state of the interval σ1…σ3, i.e., state σ1.
Finally we evaluate M⟦skip2⟧(σ1…σ3)
M⟦skip2⟧(σ1…σ3) = tt iff |σ1…σ3| = 2
An interval of length 2 means σ1…σ3 has 3 states and it certainly does.
The semantics of ‘chopstar’ is as follows M⟦f∗⟧(σ) = tt iff
(exist l0,…,ln s.t. l0 = 0 and ln = |σ|and |
||||||||||||||||||||||||||||||||||
for all 0 ≤ i < n,li ≤ li+1 and M⟦f⟧(σli…σli+1) = tt) |
||||||||||||||||||||||||||||||||||
|
Finite interval σ is the fusion of a finite number of finite sub-intervals each satisfying f.