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?