Spinroot

A forum for Spin users

You are not logged in.

#1 2021-08-03 10:06:41

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

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

Board footer

Powered by FluxBB