16
G. Fey and R. Drechsler
LTL proves this behavior referring to explanations only:
G( ((expPower[3:0]=strong ∨ expPower[3:0]=medium) ∧
X(expPower[3:0]=low)) →
F(expMain[19:16]=pb ∨ expMain[19:16]=ls) )
Using a more expressive language like SVA, properties may be formulated in an
even nicer way, e.g., using expressions over bit vectors. The underlying concepts for
explanation remain the same.
1.4.4 Module “Main” Is Self-explaining
We briefly explain how to show that the module “main” of the robot is selfexplaining according to the definitions given in Sect. 1.3.
The output vector “exp” of module main encodes the explanations as described
in Sect. 1.4.1. As discussed in Sect. 1.3.3 we proceed in the following three steps:
1. Check whether the set of observable actions is complete (see Definition 1.4).
2. Check whether the explanations are well-formed (see Definition 1.3).
3. Check whether the explanations are complete (see Definition 1.5).
Check 1 We have four actions stored in “exp[23:20],” namely “straight,” “forward
left,” “forward right,” or “turn.” By making a case split we show that these actions
partition the output space using the following properties (where the initial AX) skips
the initial state with uninitialized state values):
AX(AG( exp[23:20]=turn ∨ exp[23:20]=straight ∨
exp[23:20]=fwd_right ∨ exp[23:20]=fwd_left ) )
Each of the four actions is related to certain output assignments:
AG( exp[23:20] =straight →
( speed_left[7:0]=255 ∧ speed_right[7:0]=255
∧ direction_right=fwd ∧ direction_left=fwd) )
AG( exp[23:20]=turn →
( ( ( direction_right=bwd ∧ direction_left=fwd )
∨ ( direction_right=fwd ∧ direction_left=bwd ))
∧ speed_left[7:0]=5 ∧ speed_right[7:0]=5 ))
AG( exp[23:20]=fwd_left →
( direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=245 ∧ speed_right[7:0]=255 ))
AG( exp[23:20]=fwd_right →
( direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=255 ∧ speed_right[7:0]=245 ))
G. Fey and R. Drechsler
LTL proves this behavior referring to explanations only:
G( ((expPower[3:0]=strong ∨ expPower[3:0]=medium) ∧
X(expPower[3:0]=low)) →
F(expMain[19:16]=pb ∨ expMain[19:16]=ls) )
Using a more expressive language like SVA, properties may be formulated in an
even nicer way, e.g., using expressions over bit vectors. The underlying concepts for
explanation remain the same.
1.4.4 Module “Main” Is Self-explaining
We briefly explain how to show that the module “main” of the robot is selfexplaining according to the definitions given in Sect. 1.3.
The output vector “exp” of module main encodes the explanations as described
in Sect. 1.4.1. As discussed in Sect. 1.3.3 we proceed in the following three steps:
1. Check whether the set of observable actions is complete (see Definition 1.4).
2. Check whether the explanations are well-formed (see Definition 1.3).
3. Check whether the explanations are complete (see Definition 1.5).
Check 1 We have four actions stored in “exp[23:20],” namely “straight,” “forward
left,” “forward right,” or “turn.” By making a case split we show that these actions
partition the output space using the following properties (where the initial AX) skips
the initial state with uninitialized state values):
AX(AG( exp[23:20]=turn ∨ exp[23:20]=straight ∨
exp[23:20]=fwd_right ∨ exp[23:20]=fwd_left ) )
Each of the four actions is related to certain output assignments:
AG( exp[23:20] =straight →
( speed_left[7:0]=255 ∧ speed_right[7:0]=255
∧ direction_right=fwd ∧ direction_left=fwd) )
AG( exp[23:20]=turn →
( ( ( direction_right=bwd ∧ direction_left=fwd )
∨ ( direction_right=fwd ∧ direction_left=bwd ))
∧ speed_left[7:0]=5 ∧ speed_right[7:0]=5 ))
AG( exp[23:20]=fwd_left →
( direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=245 ∧ speed_right[7:0]=255 ))
AG( exp[23:20]=fwd_right →
( direction_right=fwd ∧ direction_left=fwd
∧ speed_left[7:0]=255 ∧ speed_right[7:0]=245 ))