LTL Specification

[Dnay]

Hello, 

I´m trying to formalize some specification for defined problem using Linear temporal logic and i dont know why it is still not realizable. i´ve already performed so much modification but i dont get a good result.

I put here the 3 different way i´ve already tried

Once A is raised, it must remain high until A && B

G(F( A -> (A U (A && B))) && (G (A && B) -> (X(!A && !B))))

G(F( A -> (A U B)))

arvalid starts as false: !arvalid

arvalid becomes true, it remains true until B becomes true: G((A -> F B)

While arvalid is true arready is false until B becomes true:G (A -> !B U B)

After arready BECOMES TRUE arvalid becomes false: G ( B -> X !A ))

Combined LTL Formula

!A ∧ G((A -> F B) ∧ (A -> !B U B) ∧( B -> X !A ))

I put here the 3 different way i´ve already tried