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?