DNAY
Newbie
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
1. 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´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
1. 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 ))