Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2021-08-03 10:06:41
- jllang
- Member
- From: Finland
- Registered: 2021-05-05
- Posts: 29
The precedence between LTL operators and Boolean connectives
I'm working on a PROMELA parser. I have a simple question: Do LTL operators take precedence over Boolean connectives, or is it the other way around? What about the precedence between LTL operators? I read these manual pages, but they don't seem to give an answer: https://spinroot.com/spin/Man/operators.html https://spinroot.com/spin/Man/ltl.html
Offline
#2 2022-03-01 19:05:08
Re: The precedence between LTL operators and Boolean connectives
the temporal operators have lower precedence than the arithmetic operators, but higher than logical or or and
X is highest, then U then [] and <>
you can see this in the grammar description in spin.y
(sorry for the slow response!)
Offline