Can you write the assertions using the exact code provided and show the code using Alloy

assert Al \{ \} assent A2 \{ \} assent A3 \{ \} assent A4 \{ \} assent A5{ \} / assert A6{ \} Write assertions (A1-A6) to check the following statements. Report the results of assertions using bound 5. For invalid assertions, include a picture of a counter example. (a) (2 points) A1. If state s has no outgoing transition, then every state can simulate s. (b) (2 points) A2. The predicate psmsimulato is reflexive, that is, every FSM can simulate itself. (c) (2 points) A3. The predicate FSMSimulate is symmetric, that is, if FSM f1 can simulate FSM f2, then f2 can also simulate f1. (d) (2 points) A4. The predicate FSMSimulate is transitive, that is, if FSM f1 can simulate FSM f2 and f2 can simulate FSM f3, then f1 can also simulate f3. (e) (2 points) A5. If FSM f1 can simulate FSM f2, then every transition's action occurring in f2 also occurs in f1. (f) (10 points) A6. If FSM f1 simulates some other FSM f2, that implies that f1 has at least as many states as f2. If the implication is not true, then which of the already defined predicates (in the format of p [f : FSM]) on FSMs would have to be imposed on f2 to make the implication hold? Add an assertion to your model that can be used to prove your claim. You may add a helper predicate