local model checking confusion

Question

This question solution is a bit confusing, as there are no brackets in question, So If i split on a, !b or c, and diamond x then this does not hold, but just like given solution, If i interpret it as a&!b | diamond x then it holds..... are both ways correct or not?     Also even if i take second way why right branch is evaluated when left branch has already satisfied it?

Answer 1

Of course, you cannot choose this. The syntax is unambiguous since we defined precedence rules and associativities of operators: On page 5 of VRS-02-PropLogic, you can find the following precedence rules:

The binary temporal operators always use brackets and the unary operators like <> and [] as well as the fixpoint operators bind like the negation:

1. 1¬
2. ∧ 
3. ⊕ 
4. 4∨ 
5. 5→ 
6. 6↔