Incorrect parsing of assignment in option block

[siraben]

init {
  if
  :: x = 3;
  :: b -> x = 3;
  fi
}

with the query ((assignment) @asgn) has the following highlighting

and has the parse tree

program:
  init:
    body:
      sequence:
        step:
          Special:
            if:
              options:
                option:
                  sequence:
                    step:
                      Stmnt:
                        assignment:
                          varref:
                            cmpnd:
                              pfld:
                          full_expr:
                            expr:
                              const:
                                number:
                option:
                  sequence:
                    step:
                      Stmnt:
                        full_expr:
                          expr:
                            ltl_expr:
                              expr:
                                varref:
                                  cmpnd:
                                    pfld:
                              ERROR:
                              expr:
                                const:
                                  number:

[siraben]

@nimble-code what is the expected parse for the option :: b -> x = 3; in Spin? Is this an ltl_expr?

[nimble-code]

just talking about spin itself: it's two statements: a side-effect free expression (b) followed by an assignment

[siraben]

Ah, this is because -> is interpreted as a statement separate in place of ;?

[siraben]

So these two programs should be equivalent

init {
  if
    :: 3; 4
  fi;
}

init {
  if
    :: 3 -> 4
  fi;
}

[nimble-code]

yes!

[nimble-code]

there is a notation for conditional expressions as well: (i -> t : e) is the Promela equivalent of C's (i ? t : e) sometimes very handy, eg to define conditional rv operations:

chan q[3] = [0] of { mtype } sender: q[(P->1:2)]!msg receiver: q[(Q->1:0]?msg

rendezvous is now only possible when P is true at the sender and Q is true at the receiver