$($i$)$ Express the following two properties as LTL formulas and explain how they work. Do not use Next $()$ operators.

L$1$: There$$s exactly one contiguous period during which a property P holds.

L$\backslash$infty : P holds and fails to hold infinitely many times.

$($ii$)$ Write

$1.$ a Promela model M$1$ that satisfies L$1$ but not L$\backslash$infty and

$2.$ a Promela model M$\backslash$infty that satisfies L$\backslash$infty but not L$1,$

and verify them $($note: $4$ combinations$)$ using Spin.$$

Note: The choice of a property P and models M and M is up to you. Different solutions to $($i$)$ are especially welcome.