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.
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 2:
E⟦z⟧(σ) |
= |
z |
||||
E⟦A⟧(σ) |
= |
σ0(A) |
||||
E⟦ig(ie1,…,ien)⟧(σ) |
= |
ig(E⟦ie1⟧(σ),…, E⟦ien⟧(σ)) |
||||
E⟦ A⟧(σ) |
= |
|
||||
E⟦fin A⟧(σ) |
= |
σ|σ|(A) |
||||
E⟦b⟧(σ) |
= |
b |
||||
E⟦Q⟧(σ) |
= |
σ0(Q) |
||||
E⟦bg(be1,…,ben)⟧(σ) |
= |
bg(E⟦be1⟧(σ),…, E⟦ben⟧(σ)) |
||||
E⟦ Q⟧(σ) |
= |
|
||||
E⟦fin Q⟧(σ) | = | σ|σ|(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⟦f1⟧(σ) = 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)
| ||||||
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)
| ||||||