When the goal state is reached the $movement$ variable should be set to
$finished$ to be able to specify the CTL specification more easily. Via the
following invariant the goal state is tied to the $movement$ variable:
When the goal state is reached the $movement$ variable should be set to
$finished$ to be able to specify the CTL specification more easily. Via the
following invariant the goal state is tied to the $movement$ variable: