Solve the following puzzle using SAL:
Exercise 0:
Model the Collatz conjecture in SAL (3n+1 problem).
Write temporal properties that check bounds in a sequence starting from a given interval.
Exercise 1:
You are camping, and have an 8-liter bowl which is full of fresh water.
You need exactly 1 liter for cooking.
But you only have two empty bowls: a 5-liter and a 3-liter bowl.
Find a way to separate out 1 liter in as short a time as possible.
Exercise 2:
You are camping, and have an 8-liter bowl which is full of fresh water.
You need to share this water fairly into exactly two portions (4 + 4 liters).
But you only have two empty bowls: a 5-liter and a 3-liter bowl.
Divide the 8 liters in half in as short a time as possible.
Exercise 3:
HybridSAL: Model the following to verify safety.
A robot moves in 2-d. We can apply force to it in NE direction, or NW direction.
When force is applied in NE direction:
dv_x/dt = 1 - v_x
dv_y/dt = 1 - v_y
When force is applied in NW direction:
dv_x/dt = -1 - v_x
dv_y/dt = 1 - v_y
where v_x = dx/dt and v_y = dy/dt are the velocity in the x- and y-directions.
Initially, the robot starts in region -1 <= x <= 1, y = 0, v_x = 0, v_y = 0
The region -3 <= x <= 3 is the SAFE region, and I want the robot to remain safe always.
I design the following switching controller.
(1) if the current mode is NE,
and if x >= 1, but before x + v_x > 2, the controller switches to NW mode
(2) if the current mode is NW,
and if x <= -1, but before x + v_x < -2, the controller switches to NE mode
Does this controller guarantee safety?
Exercise 4:
Add a new mode, N (North):
dv_x/dt = 0 - v_x
dv_y/dt = 1 - v_y
Extend the controller to optionally switch to N, whenever it switches
from NE to NW, or from NW to NE.
that is; NE -> (NW | N) and NW -> (NE | N) under the same condition as before
Does the new controller guarantee safety?