None
EN
Demonstrating SPARK with a Mars Rover (Part 4): Formalizing Safety
['Tony Aiello']
Home | Electronic Design
If both left and right are too close (closer than 50 units), turn around.
For example, what if it doesn't turn far enough to the left or the right?
that it will end up pointed in a direction with an obstacle more than 40 units away.
What if motor power drops during the turn and it doesn't turn as far as expected?
Here, it’s met entirely because “Find_New_Direction” always leaves the Rover in a state in which it’s not moving straight forward.