Each state σi is the union of the mapping from the set of integer variables IntVar to the set of integer values ℤ and the mapping from propositional variables PropVar to set of Boolean values {tt, ff}.
Each interval has at least one state. The length |σ| of an interval σ0…σn is equal to n, one less than the number of states in the interval (this has always been a convention in ITL), i.e., a one state interval has length 0. Let σ = σ0σ1σ2… be an interval then
The informal semantics of the most interesting constructs are as follows:
Let Σ+ denote the set of all finite intervals and Σω denotes the set of all infinite intervals.
Let Expressions denote the set of (integer or Boolean) expressions.
Let Val denote the set of integer or Boolean values (ℤ ∪ Bool).
Let E⟦…⟧( ) denote the meaning function from Expressions × (Σ+ ∪ Σω) to Val.
Let Formulae denote the set of ITL formulae.
Let M⟦…⟧( ) denote the meaning function from Formulae × (Σ+ ∪ Σω) to Bool (set of Boolean
values, {tt, ff}).
Let σ = σ0σ1… denote an interval.
We write σ ∼V σ′ if the intervals σ and σ′ are identical with the possible exception of their mappings for
the variable V .
Let choose-any-from(Val) denote the choice function that selects an arbitrary value from Val.
The formal semantics is listed in Table 10:
E⟦z⟧(σ) |
= |
z |
||||
E⟦A⟧(σ) |
= |
σ0(A) |
||||
E⟦ig(ie1,…,ien)⟧(σ) |
= |
ig(E⟦ie1⟧(σ),…, E⟦ien⟧(σ)) |
||||
E⟦ A⟧(σ) |
= |
|
||||
E⟦fin A⟧(σ) |
= |
|
||||
E⟦b⟧(σ) |
= |
b |
||||
E⟦Q⟧(σ) |
= |
σ0(Q) |
||||
E⟦bg(be1,…,ben)⟧(σ) |
= |
bg(E⟦be1⟧(σ),…, E⟦ben⟧(σ)) |
||||
E⟦ Q⟧(σ) |
= |
|
||||
E⟦fin Q⟧(σ) |
= |
|
||||
M⟦true⟧(σ) |
= |
tt |
||||
M⟦h(e1,…,en)⟧(σ) = tt |
iff |
h(E⟦e1⟧(σ),…, E⟦en⟧(σ)) |
||||
M⟦¬f⟧(σ) = tt | iff | not (M⟦f⟧(σ) = tt) |
||||
M⟦f1 ∧ f2⟧(σ) = tt | iff | (M⟦f
1⟧(σ) = tt) and (M⟦f2⟧(σ) = tt) |
||||
M⟦skip⟧(σ) = tt |
iff |
|σ| = 1 |
||||
M⟦∀V f⟧(σ) = tt |
iff |
(for all σ′ s.t. σ ∼V σ′, M⟦f⟧(σ′) = tt) |
||||
M⟦f1 ; f2⟧(σ) = tt |
iff |
|||||
(exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt)
| ||||||
or (σ is infinite and M⟦f1⟧(σ) = tt)
| ||||||
M⟦f∗⟧(σ) = tt |
iff |
|||||
if σ is finite then
| ||||||
(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)
| ||||||
else
| ||||||
(exist l0,…,ln s.t. l0 = 0 and
| ||||||
M⟦f⟧(σln…σ|σ|) = tt and
| ||||||
for all 0 ≤ i < n,li < li+1 and M⟦f⟧(σli…σli+1) = tt)
| ||||||
or
| ||||||
(exist an infinite number of li s.t. l0 = 0 and
| ||||||
for all 0 ≤ i,li < li+1 and M⟦f⟧(σli…σli+1) = tt)
| ||||||